OAI/Algebra/Finitistic/Iteration/IntegerIterateSupport.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.DerivedBar.IterateSupport.object line 18

   Source documentation

   The already constructed genuine derived iterate, viewed in integer degrees.

   abbrev object (r : ℕ) := (chainToIntegerDerived D).obj
   …

   Mentions: OAI.DerivedBar.chainToIntegerDerived

2. instance OAI.DerivedBar.IterateSupport.isLE_zero line 24

   Source documentation

   Every actual iterate is cohomologically nonpositive. This uses the proved integer comparison and its actual nonnegative chain representative.

   instance isLE_zero (r : ℕ) : (object k D X N r).IsLE 0 := by
   …

   Mentions: OAI.DerivedBar.IterateSupport.object

3. theorem OAI.DerivedBar.IterateSupport.positive_homology_zero line 32
4. theorem OAI.DerivedBar.IterateSupport.nonzero_homology line 37

   Source documentation

   Nonzero actual iterates have a nonzero cohomology group in nonpositive degree.

   theorem nonzero_homology (r : ℕ) (h : ¬ IsZero (object k D X N r)) :
       ∃ n : ℕ, ¬ IsZero ((DerivedCategory.homologyFunctor (ModuleCat D) (-(n : ℤ))).obj
         (object k D X N r)) := by
   …

   Mentions: OAI.DerivedBar.IterateSupport.object