OAI/Algebra/Finitistic/Iteration/FiniteIntegerIterate.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. instance OAI.DerivedBar.IterateSupport.tensor_finite line 26
2. instance OAI.DerivedBar.IterateSupport.indexed_finite line 37
3. theorem OAI.DerivedBar.IterateSupport.homology_finite line 55

   Source documentation

   Homology is a quotient of a subspace of the term in that degree.

   theorem homology_finite {ι : Type*} (c : ComplexShape ι)
       (Z : HomologicalComplex (ModuleCat.{u} D) c) (i : ι)
       [FiniteDimensional k ((ModuleCat.restrictScalars (algebraMap k D)).obj (Z.X i))] :
       FiniteDimensional k ((ModuleCat.restrictScalars (algebraMap k D)).obj (Z.homology i)) := by
   …

4. theorem OAI.DerivedBar.IterateSupport.cohomology_finite line 69

   Source documentation

   Actual cohomology of every derived iterate is finite-dimensional in every degree.

   theorem cohomology_finite (r : ℕ) (i : ℤ) : FiniteDimensional k
       ((ModuleCat.restrictScalars (algebraMap k D)).obj
         ((DerivedCategory.homologyFunctor (ModuleCat D) i).obj (object k D X N r))) := by
   …

   Mentions: OAI.DerivedBar.IterateSupport.object