OAI/Algebra/Finitistic/Localization/TwoDegreeExtVanishing.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.LittleFinitistic.TwoDegreeFormality.pd_lt_three line 13
2. theorem OAI.LittleFinitistic.TwoDegreeFormality.ext_eq_zero line 20

   Source documentation

   Actual higher Ext vanishing from the proved global-dimension bound for B.

   theorem ext_eq_zero (X Y : ModuleCat.{max u v} (B P)) (n : ℕ) (hn : 3 ≤ n)
       (x : Ext X Y n) : x = 0 := by
   …

3. theorem OAI.LittleFinitistic.TwoDegreeFormality.shifted_hom_eq_zero line 26

   Source documentation

   In particular every possible degree-four connecting morphism is zero.

   theorem shifted_hom_eq_zero (X Y : ModuleCat.{max u v} (B P)) (n : ℕ) (hn : 3 ≤ n)
       (f : (DerivedCategory.singleFunctor _ 0).obj X ⟶
         ((DerivedCategory.singleFunctor _ 0).obj Y)⟦(n : ℤ)⟧) : f = 0 := by
   …