TotalFunctorial.lean`

19 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.LittleFinitistic.RectificationTotal.biprodMap_comp line 9
def OAI.LittleFinitistic.RectificationTotal.coneMap line 17
Source documentation
A strictly commuting square induces the ordinary diagonal map of cones.
```
def coneMap (q : A ⟶ B) (q' : A' ⟶ B') (u : A ⟶ A') (v : B ⟶ B')
    (w : u ≫ q' = q ≫ v) : mappingCone q ⟶ mappingCone q' :=
…
```
theorem OAI.LittleFinitistic.RectificationTotal.coneMap_inl line 23
theorem OAI.LittleFinitistic.RectificationTotal.coneMap_inr line 34
theorem OAI.LittleFinitistic.RectificationTotal.cone_inl_termIso line 42
theorem OAI.LittleFinitistic.RectificationTotal.cone_inr_termIso line 48

theorem OAI.LittleFinitistic.RectificationTotal.coneMap_term line 54

Source documentation

On terms the cone map is exactly the sum of the two supplied maps.

theorem coneMap_term (q : A ⟶ B) (q' : A' ⟶ B') (u : A ⟶ A') (v : B ⟶ B')
    (w : u ≫ q' = q ≫ v) (i j : ℤ) (hij : i+1=j) :
    (coneMap q q' u v w).f i ≫ (homotopyCofiber.XIsoBiprod q' i j hij).hom =
      (homotopyCofiber.XIsoBiprod q i j hij).hom ≫ biprod.map (u.f j) (v.f i) := by
…

Mentions: OAI.LittleFinitistic.RectificationTotal.coneMap

theorem OAI.LittleFinitistic.RectificationTotal.coneMap_id line 65
theorem OAI.LittleFinitistic.RectificationTotal.coneMap_comp line 69
structure OAI.LittleFinitistic.RectificationTotal.MapData line 82
Source documentation
Morphisms preserve both degree-zero maps and the specified relation homotopy, which is part of the three-column input data.
```
structure MapData (p : L₁ ⟶ L₀) (q : L₂ ⟶ L₁) (h : Homotopy (q ≫ p) 0)
    (p' : M₁ ⟶ M₀) (q' : M₂ ⟶ M₁) (h' : Homotopy (q' ≫ p') 0) where
…
```
def OAI.LittleFinitistic.RectificationTotal.MapData.inner line 94
theorem OAI.LittleFinitistic.RectificationTotal.MapData.rectifyingMap_naturality line 96
def OAI.LittleFinitistic.RectificationTotal.MapData.totalMap line 108
Source documentation
The induced chain map of the native primary's actual iterated-cone total.
```
def totalMap : total p q h ⟶ total p' q' h' :=
…
```
Mentions: OAI.LittleFinitistic.RectificationTotal.total
theorem OAI.LittleFinitistic.RectificationTotal.MapData.inclusion_totalMap line 114
Source documentation
The zero-column inclusion is preserved by the actual induced total map.
```
theorem inclusion_totalMap : inclusion p q h ≫ a.totalMap =
    a.f₀ ≫ inclusion p' q' h' := by
…
```
Mentions: OAI.LittleFinitistic.RectificationTotal.inclusion
theorem OAI.LittleFinitistic.RectificationTotal.MapData.totalMap_term line 121
Source documentation
The induced total map is the actual diagonal triple under the native term decomposition, including both cohomological shifts.
```
theorem totalMap_term (n : ℤ) :
    a.totalMap.f n ≫ (termIso p' q' h' n).hom =
      (termIso p q h n).hom ≫
        biprod.map (biprod.map (a.f₂.f (n+2)) (a.f₁.f (n+1))) (a.f₀.f n) := by
…
```
Mentions: OAI.LittleFinitistic.RectificationTotal.termIso
def OAI.LittleFinitistic.RectificationTotal.MapData.id line 133
def OAI.LittleFinitistic.RectificationTotal.MapData.comp line 143
theorem OAI.LittleFinitistic.RectificationTotal.MapData.totalMap_id line 153
theorem OAI.LittleFinitistic.RectificationTotal.MapData.totalMap_comp line 156