OAI/Algebra/Finitistic/Bar/TotalMap.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. instance OAI.DerivedBar.finiteTotalDiagonal line 13

   Source documentation

   Each diagonal of a first-quadrant total complex is finite.

   instance finiteTotalDiagonal (n : ℕ) : Finite ((ComplexShape.π c c c) ⁻¹' {n}) := by
   …

2. instance OAI.DerivedBar.fintypeTotalDiagonal line 26
3. abbrev OAI.DerivedBar.mapBicomplex line 32
4. def OAI.DerivedBar.totalMapDesc line 36

   Source documentation

   Maps out of the image of a total term, using only a finite coproduct.

   def totalMapDesc {n : ℕ} {Y : ModuleCat.{u} D}
       (f : ∀ i q (_ : i+q=n), G.obj ((K.X i).X q) ⟶ Y) :
       G.obj ((K.total c).X n) ⟶ Y :=
   …

5. theorem OAI.DerivedBar.ι_totalMapDesc line 45
6. theorem OAI.DerivedBar.totalMap_hom_ext line 52
7. def OAI.DerivedBar.totalMapIsoX line 63

   Source documentation

   Additive functors commute with each finite diagonal sum.

   def totalMapIsoX (n : ℕ) :
       G.obj ((K.total c).X n) ≅ ((mapBicomplex G K).total c).X n where
   …

   Mentions: OAI.DerivedBar.mapBicomplex

8. theorem OAI.DerivedBar.ι_totalMapIsoX_inv line 71
9. theorem OAI.DerivedBar.ιTotalOrZero_totalMapIsoX_inv line 76
10. theorem OAI.DerivedBar.d₁_totalMapIsoX_inv line 85
11. theorem OAI.DerivedBar.d₂_totalMapIsoX_inv line 96
12. def OAI.DerivedBar.totalMapIso line 109

    Source documentation

    Additive functors commute with first-quadrant totalization as chain complexes, with the actual horizontal and signed vertical differential.

    def totalMapIso : (G.mapHomologicalComplex c).obj (K.total c) ≅
        (mapBicomplex G K).total c :=
    …

    Mentions: OAI.DerivedBar.mapBicomplex