TotalExact.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.LittleFinitistic.RectificationTotal.prodIso_naturality line 13

Source documentation

The canonical binary sum/product identification respects the supplied maps.

theorem prodIso_naturality {X Y X' Y' : ModuleCat.{u} S} (f : X ⟶ X') (g : Y ⟶ Y') :
    biprod.map f g ≫ (ModuleCat.biprodIsoProd X' Y').hom =
      (ModuleCat.biprodIsoProd X Y).hom ≫ ModuleCat.ofHom (f.hom.prodMap g.hom) := by
…

def OAI.LittleFinitistic.RectificationTotal.totalTermIso line 33
Source documentation
The native total's term as the actual product of the three input modules.
```
def totalTermIso (p : L₁ ⟶ L₀) (q : L₂ ⟶ L₁) (h : Homotopy (q ≫ p) 0) (n : ℤ) :
    (total p q h).X n ≅ ModuleCat.of S ((L₂.X (n+2) × L₁.X (n+1)) × L₀.X n) :=
…
```
Mentions: OAI.LittleFinitistic.RectificationTotal.total

theorem OAI.LittleFinitistic.RectificationTotal.MapData.totalMap_product line 43

Source documentation

The explicit total map acts componentwise in the concrete term product.

theorem totalMap_product (n : ℤ) :
    a.totalMap.f n ≫ (totalTermIso p' q' h' n).hom =
      (totalTermIso p q h n).hom ≫ ModuleCat.ofHom
        (((a.f₂.f (n+2)).hom.prodMap (a.f₁.f (n+1)).hom).prodMap (a.f₀.f n).hom) := by
…

Mentions: OAI.LittleFinitistic.RectificationTotal.totalTermIso

theorem OAI.LittleFinitistic.RectificationTotal.MapData.totalMap_shortExact line 63

Source documentation

A short exact triple of column maps induces short exactness of the actual supplied total maps, retaining the inclusion and quotient maps themselves.

theorem totalMap_shortExact (b : MapData p' q' h' p'' q'' h'')
    (ex₀ : ∀ n, Function.Exact (a.f₀.f n) (b.f₀.f n))
    (ex₁ : ∀ n, Function.Exact (a.f₁.f n) (b.f₁.f n))
    (ex₂ : ∀ n, Function.Exact (a.f₂.f n) (b.f₂.f n))
    (inj₀ : ∀ n, Function.Injective (a.f₀.f n))
    (inj₁ : ∀ n, Function.Injective (a.f₁.f n))
    (inj₂ : ∀ n, Function.Injective (a.f₂.f n))
    (surj₀ : ∀ n, Function.Surjective (b.f₀.f n))
    (surj₁ : ∀ n, Function.Surjective (b.f₁.f n))
    (surj₂ : ∀ n, Function.Surjective (b.f₂.f n)) (n : ℤ) :
    Function.Injective (a.totalMap.f n) ∧
      Function.Exact (a.totalMap.f n) (b.totalMap.f n) ∧
…

Mentions: OAI.LittleFinitistic.RectificationTotal.MapData