OAI/Algebra/Finitistic/Rectification/TotalInterchange.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.LittleFinitistic.RectificationTotal.mapComplex line 12
2. def OAI.LittleFinitistic.RectificationTotal.coneInterchange line 17

   Source documentation

   The canonical additive comparison for one cone.

   def coneInterchange (q : A ⟶ B) :
       (mapComplex F).obj (mappingCone q) ≅ mappingCone ((mapComplex F).map q) :=
   …

   Mentions: OAI.LittleFinitistic.RectificationTotal.mapComplex

3. theorem OAI.LittleFinitistic.RectificationTotal.coneInterchange_inv_inl line 22
4. theorem OAI.LittleFinitistic.RectificationTotal.coneInterchange_inv_inr line 28
5. theorem OAI.LittleFinitistic.RectificationTotal.coneInterchange_hom_inl line 34
6. theorem OAI.LittleFinitistic.RectificationTotal.coneInterchange_hom_inr line 41
7. def OAI.LittleFinitistic.RectificationTotal.mapNullHomotopy line 52

   Source documentation

   Apply the functor to the supplied null-homotopy, transporting only functorial composition and zero equalities.

   def mapNullHomotopy : Homotopy ((mapComplex F).map q ≫ (mapComplex F).map p) 0 :=
   …

   Mentions: OAI.LittleFinitistic.RectificationTotal.mapComplex

8. theorem OAI.LittleFinitistic.RectificationTotal.mapNullHomotopy_hom line 56
9. theorem OAI.LittleFinitistic.RectificationTotal.rectifyingMap_interchange_inv line 61

   Source documentation

   Mapping the rectifying map agrees with rectifying the mapped data.

   theorem rectifyingMap_interchange_inv :
       (coneInterchange F q).inv ≫ (mapComplex F).map (rectifyingMap p q h) =
         rectifyingMap ((mapComplex F).map p) ((mapComplex F).map q)
           (mapNullHomotopy F p q h) := by
   …

   Mentions: OAI.LittleFinitistic.RectificationTotal.coneInterchange, OAI.LittleFinitistic.RectificationTotal.mapComplex, OAI.LittleFinitistic.RectificationTotal.rectifyingMap, OAI.LittleFinitistic.RectificationTotal.mapNullHomotopy

10. theorem OAI.LittleFinitistic.RectificationTotal.rectifyingMap_interchange line 76
11. def OAI.LittleFinitistic.RectificationTotal.totalInterchange line 84

    Source documentation

    Arbitrary additive functors commute with the actual iterated-cone total.

    def totalInterchange : (mapComplex F).obj (total p q h) ≅
        total ((mapComplex F).map p) ((mapComplex F).map q) (mapNullHomotopy F p q h) :=
    …

    Mentions: OAI.LittleFinitistic.RectificationTotal.mapComplex, OAI.LittleFinitistic.RectificationTotal.total, OAI.LittleFinitistic.RectificationTotal.mapNullHomotopy

12. theorem OAI.LittleFinitistic.RectificationTotal.inclusion_totalInterchange line 93

    Source documentation

    The original zero-column inclusion is carried to the original inclusion.

    theorem inclusion_totalInterchange :
        (mapComplex F).map (inclusion p q h) ≫ (totalInterchange F p q h).hom =
          inclusion ((mapComplex F).map p) ((mapComplex F).map q) (mapNullHomotopy F p q h) := by
    …

    Mentions: OAI.LittleFinitistic.RectificationTotal.mapComplex, OAI.LittleFinitistic.RectificationTotal.inclusion, OAI.LittleFinitistic.RectificationTotal.totalInterchange, OAI.LittleFinitistic.RectificationTotal.mapNullHomotopy