ZeroColumnTotal.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

def OAI.LittleFinitistic.ZeroColumnTotal.biprodInrIso line 10
theorem OAI.LittleFinitistic.ZeroColumnTotal.complex_zero line 20
theorem OAI.LittleFinitistic.ZeroColumnTotal.cone_inr_isIso line 27
Source documentation
If the cone source is zero, its original inclusion is an isomorphism.
```
theorem cone_inr_isIso {X Y : CochainComplex D ℤ} (f : X ⟶ Y) (hX : IsZero X) :
    IsIso (mappingCone.inr f) := by
…
```

theorem OAI.LittleFinitistic.ZeroColumnTotal.mappedCone_zero line 42

Source documentation

A mapped cone whose two columns vanish is actually zero.

theorem mappedCone_zero {X Y : CochainComplex C ℤ} (f : X ⟶ Y)
    (F : C ⥤ D) [F.Additive]
    (hX : ∀ i, IsZero (F.obj (X.X i))) (hY : ∀ i, IsZero (F.obj (Y.X i))) :
    IsZero ((F.mapHomologicalComplex (.up ℤ)).obj (mappingCone f)) := by
…

theorem OAI.LittleFinitistic.ZeroColumnTotal.mapped_inclusion_isIso line 53

Source documentation

Vanishing higher columns make the original zero-column inclusion an isomorphism.

theorem mapped_inclusion_isIso {L₀ L₁ L₂ : CochainComplex C ℤ}
    (p : L₁ ⟶ L₀) (q : L₂ ⟶ L₁) (h : Homotopy (q ≫ p) 0)
    (F : C ⥤ D) [F.Additive]
    (h₁ : ∀ i, IsZero (F.obj (L₁.X i))) (h₂ : ∀ i, IsZero (F.obj (L₂.X i))) :
    IsIso ((F.mapHomologicalComplex (.up ℤ)).map (RectificationTotal.inclusion p q h)) := by
…

Mentions: OAI.LittleFinitistic.RectificationTotal.inclusion