OAI/Algebra/Finitistic/Bimodule/BimoduleTotalUnderlying.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.LittleFinitistic.BimoduleTotal.forget line 12
2. def OAI.LittleFinitistic.BimoduleTotal.underlyingTerm line 16
3. def OAI.LittleFinitistic.BimoduleTotal.underlyingIso line 30

   Source documentation

   Forgetting the full left action recovers the frozen signed tensor total with its actual differential.

   def underlyingIso : (forget k B).obj (total k B P p hp Z) ≅ vectorTotal k B P p hp Z :=
   …

   Mentions: OAI.LittleFinitistic.BimoduleTotal.forget, OAI.LittleFinitistic.BimoduleTotal.total, OAI.LittleFinitistic.BimoduleTotal.vectorTotal

4. def OAI.LittleFinitistic.BimoduleTotal.underlyingComparison line 35

   Source documentation

   The comparison preserves the original maps in the arbitrary input complex.

   def underlyingComparison :
       functor k B P p hp ⋙ forget k B ≅ ComplexTensor.finiteTotalFunctor k B (right k B P) p hp :=
   …

   Mentions: OAI.LittleFinitistic.BimoduleTotal.functor, OAI.LittleFinitistic.BimoduleTotal.forget, OAI.LittleFinitistic.ComplexTensor.finiteTotalFunctor, OAI.LittleFinitistic.BimoduleTotal.right

5. instance OAI.LittleFinitistic.BimoduleTotal.restrictPreservesHomology line 46
6. theorem OAI.LittleFinitistic.BimoduleTotal.totalMap_quasiIso line 53

   Source documentation

   The frozen K-flatness proof applies to the total with its complete B action.

   theorem totalMap_quasiIso
       [∀ i, Module.Projective Bᵐᵒᵖ (ComplexTensor.rightTerm k B (right k B P) (p i))]
       {Z Z' : CochainComplex (ModuleCat.{u} B) ℤ} (f : Z ⟶ Z') [QuasiIso f] :
       QuasiIso (totalMap k B P p hp f) := by
   …

   Mentions: OAI.LittleFinitistic.ComplexTensor.rightTerm, OAI.LittleFinitistic.BimoduleTotal.right, OAI.LittleFinitistic.BimoduleTotal.totalMap