-- Mathlib/CategoryTheory/Abelian/Exact.lean
/-- A functor preserving zero morphisms, monos, and cokernels preserves homology. -/
lemma preservesHomology_of_preservesMonos_and_cokernels [PreservesZeroMorphisms L]
    [PreservesMonomorphisms L] [∀ {X Y} (f : X ⟶ Y), PreservesColimit (parallelPair f 0) L] :
    PreservesHomology L

Proof state:
case hL
A : Type u₁
B : Type u₂
inst✝⁶ : Category.{v₁, u₁} A
inst✝⁵ : Category.{v₂, u₂} B
inst✝⁴ : Abelian A
inst✝³ : Abelian B
L : A ⥤ B
inst✝² : L.PreservesZeroMorphisms
inst✝¹ : L.PreservesMonomorphisms
inst✝ : ∀ {X Y : A} (f : X ⟶ Y), PreservesColimit (parallelPair f 0) L
⊢ ∀ (S : ShortComplex A), S.Exact → (S.map L).Exact

Tactic:
intro S hS

Result:
case hL
A : Type u₁
B : Type u₂
inst✝⁶ : Category.{v₁, u₁} A
inst✝⁵ : Category.{v₂, u₂} B
inst✝⁴ : Abelian A
inst✝³ : Abelian B
L : A ⥤ B
inst✝² : L.PreservesZeroMorphisms
inst✝¹ : L.PreservesMonomorphisms
inst✝ : ∀ {X Y : A} (f : X ⟶ Y), PreservesColimit (parallelPair f 0) L
S : ShortComplex A
hS : S.Exact
⊢ (S.map L).Exact

Proof state:
case hL
A : Type u₁
B : Type u₂
inst✝⁶ : Category.{v₁, u₁} A
inst✝⁵ : Category.{v₂, u₂} B
inst✝⁴ : Abelian A
inst✝³ : Abelian B
L : A ⥤ B
inst✝² : L.PreservesZeroMorphisms
inst✝¹ : L.PreservesMonomorphisms
inst✝ : ∀ {X Y : A} (f : X ⟶ Y), PreservesColimit (parallelPair f 0) L
S : ShortComplex A
hS : S.Exact
φ : (ShortComplex.mk S.f (coimage.π S.g) ⋯).map L ⟶ S.map L :=
  { τ₁ := 𝟙 ((ShortComplex.mk S.f (coimage.π S.g) ⋯).map L).X₁,
    τ₂ := 𝟙 ((ShortComplex.mk S.f (coimage.π S.g) ⋯).map L).X₂, τ₃ := L.map (Abelian.factorThruCoimage S.g),
    comm₁₂ := ⋯, comm₂₃ := ⋯ }
⊢ ((ShortComplex.mk S.f (coimage.π S.g) ⋯).map L).Exact

Tactic:
apply ShortComplex.exact_of_g_is_cokernel

Result:
case hL.hS
A : Type u₁
B : Type u₂
inst✝⁶ : Category.{v₁, u₁} A
inst✝⁵ : Category.{v₂, u₂} B
inst✝⁴ : Abelian A
inst✝³ : Abelian B
L : A ⥤ B
inst✝² : L.PreservesZeroMorphisms
inst✝¹ : L.PreservesMonomorphisms
inst✝ : ∀ {X Y : A} (f : X ⟶ Y), PreservesColimit (parallelPair f 0) L
S : ShortComplex A
hS : S.Exact
φ : (ShortComplex.mk S.f (coimage.π S.g) ⋯).map L ⟶ S.map L :=
  { τ₁ := 𝟙 ((ShortComplex.mk S.f (coimage.π S.g) ⋯).map L).X₁,
    τ₂ := 𝟙 ((ShortComplex.mk S.f (coimage.π S.g) ⋯).map L).X₂, τ₃ := L.map (Abelian.factorThruCoimage S.g),
    comm₁₂ := ⋯, comm₂₃ := ⋯ }
⊢ IsColimit (CokernelCofork.ofπ ((ShortComplex.mk S.f (coimage.π S.g) ⋯).map L).g ⋯)

Proof state:
case hL.hS
A : Type u₁
B : Type u₂
inst✝⁶ : Category.{v₁, u₁} A
inst✝⁵ : Category.{v₂, u₂} B
inst✝⁴ : Abelian A
inst✝³ : Abelian B
L : A ⥤ B
inst✝² : L.PreservesZeroMorphisms
inst✝¹ : L.PreservesMonomorphisms
inst✝ : ∀ {X Y : A} (f : X ⟶ Y), PreservesColimit (parallelPair f 0) L
S : ShortComplex A
hS : S.Exact
φ : (ShortComplex.mk S.f (coimage.π S.g) ⋯).map L ⟶ S.map L :=
  { τ₁ := 𝟙 ((ShortComplex.mk S.f (coimage.π S.g) ⋯).map L).X₁,
    τ₂ := 𝟙 ((ShortComplex.mk S.f (coimage.π S.g) ⋯).map L).X₂, τ₃ := L.map (Abelian.factorThruCoimage S.g),
    comm₁₂ := ⋯, comm₂₃ := ⋯ }
⊢ IsColimit (CokernelCofork.ofπ ((ShortComplex.mk S.f (coimage.π S.g) ⋯).map L).g ⋯)

Tactic:
exact CokernelCofork.mapIsColimit _ ((S.exact_iff_exact_coimage_π).1 hS).gIsCokernel L

Result:
no goals

Proof state:
A : Type u₁
B : Type u₂
inst✝⁶ : Category.{v₁, u₁} A
inst✝⁵ : Category.{v₂, u₂} B
inst✝⁴ : Abelian A
inst✝³ : Abelian B
L : A ⥤ B
inst✝² : L.PreservesZeroMorphisms
inst✝¹ : L.PreservesMonomorphisms
inst✝ : ∀ {X Y : A} (f : X ⟶ Y), PreservesColimit (parallelPair f 0) L
S : ShortComplex A
hS : S.Exact
⊢ 𝟙 (L.obj S.X₂) ≫ L.map S.g = L.map (cokernel.π (kernel.ι S.g)) ≫ L.map (Abelian.factorThruCoimage S.g)

Tactic:
rw [Category.id_comp, ← L.map_comp, cokernel.π_desc]

Result:
no goals

Proof state:
A : Type u₁
B : Type u₂
inst✝⁶ : Category.{v₁, u₁} A
inst✝⁵ : Category.{v₂, u₂} B
inst✝⁴ : Abelian A
inst✝³ : Abelian B
L : A ⥤ B
inst✝² : L.PreservesZeroMorphisms
inst✝¹ : L.PreservesMonomorphisms
inst✝ : ∀ {X Y : A} (f : X ⟶ Y), PreservesColimit (parallelPair f 0) L
⊢ L.PreservesHomology

Tactic:
apply preservesHomology_of_map_exact

Result:
case hL
A : Type u₁
B : Type u₂
inst✝⁶ : Category.{v₁, u₁} A
inst✝⁵ : Category.{v₂, u₂} B
inst✝⁴ : Abelian A
inst✝³ : Abelian B
L : A ⥤ B
inst✝² : L.PreservesZeroMorphisms
inst✝¹ : L.PreservesMonomorphisms
inst✝ : ∀ {X Y : A} (f : X ⟶ Y), PreservesColimit (parallelPair f 0) L
⊢ ∀ (S : ShortComplex A), S.Exact → (S.map L).Exact

Proof state:
case hL
A : Type u₁
B : Type u₂
inst✝⁶ : Category.{v₁, u₁} A
inst✝⁵ : Category.{v₂, u₂} B
inst✝⁴ : Abelian A
inst✝³ : Abelian B
L : A ⥤ B
inst✝² : L.PreservesZeroMorphisms
inst✝¹ : L.PreservesMonomorphisms
inst✝ : ∀ {X Y : A} (f : X ⟶ Y), PreservesColimit (parallelPair f 0) L
S : ShortComplex A
hS : S.Exact
⊢ (S.map L).Exact

Tactic:
let φ : (ShortComplex.mk _ _ (Abelian.comp_coimage_π_eq_zero S.zero)).map L ⟶ S.map L :=
  { τ₁ := 𝟙 _
    τ₂ := 𝟙 _
    τ₃ := L.map (Abelian.factorThruCoimage S.g)
    comm₂₃ := by
      dsimp
      rw [Category.id_comp, ← L.map_comp, cokernel.π_desc] }

Result:
case hL
A : Type u₁
B : Type u₂
inst✝⁶ : Category.{v₁, u₁} A
inst✝⁵ : Category.{v₂, u₂} B
inst✝⁴ : Abelian A
inst✝³ : Abelian B
L : A ⥤ B
inst✝² : L.PreservesZeroMorphisms
inst✝¹ : L.PreservesMonomorphisms
inst✝ : ∀ {X Y : A} (f : X ⟶ Y), PreservesColimit (parallelPair f 0) L
S : ShortComplex A
hS : S.Exact
φ : (ShortComplex.mk S.f (coimage.π S.g) ⋯).map L ⟶ S.map L :=
  { τ₁ := 𝟙 ((ShortComplex.mk S.f (coimage.π S.g) ⋯).map L).X₁,
    τ₂ := 𝟙 ((ShortComplex.mk S.f (coimage.π S.g) ⋯).map L).X₂, τ₃ := L.map (Abelian.factorThruCoimage S.g),
    comm₁₂ := ⋯, comm₂₃ := ⋯ }
⊢ (S.map L).Exact

Proof state:
case hL
A : Type u₁
B : Type u₂
inst✝⁶ : Category.{v₁, u₁} A
inst✝⁵ : Category.{v₂, u₂} B
inst✝⁴ : Abelian A
inst✝³ : Abelian B
L : A ⥤ B
inst✝² : L.PreservesZeroMorphisms
inst✝¹ : L.PreservesMonomorphisms
inst✝ : ∀ {X Y : A} (f : X ⟶ Y), PreservesColimit (parallelPair f 0) L
S : ShortComplex A
hS : S.Exact
φ : (ShortComplex.mk S.f (coimage.π S.g) ⋯).map L ⟶ S.map L :=
  { τ₁ := 𝟙 ((ShortComplex.mk S.f (coimage.π S.g) ⋯).map L).X₁,
    τ₂ := 𝟙 ((ShortComplex.mk S.f (coimage.π S.g) ⋯).map L).X₂, τ₃ := L.map (Abelian.factorThruCoimage S.g),
    comm₁₂ := ⋯, comm₂₃ := ⋯ }
⊢ (S.map L).Exact

Tactic:
apply (ShortComplex.exact_iff_of_epi_of_isIso_of_mono φ).1

Result:
case hL
A : Type u₁
B : Type u₂
inst✝⁶ : Category.{v₁, u₁} A
inst✝⁵ : Category.{v₂, u₂} B
inst✝⁴ : Abelian A
inst✝³ : Abelian B
L : A ⥤ B
inst✝² : L.PreservesZeroMorphisms
inst✝¹ : L.PreservesMonomorphisms
inst✝ : ∀ {X Y : A} (f : X ⟶ Y), PreservesColimit (parallelPair f 0) L
S : ShortComplex A
hS : S.Exact
φ : (ShortComplex.mk S.f (coimage.π S.g) ⋯).map L ⟶ S.map L :=
  { τ₁ := 𝟙 ((ShortComplex.mk S.f (coimage.π S.g) ⋯).map L).X₁,
    τ₂ := 𝟙 ((ShortComplex.mk S.f (coimage.π S.g) ⋯).map L).X₂, τ₃ := L.map (Abelian.factorThruCoimage S.g),
    comm₁₂ := ⋯, comm₂₃ := ⋯ }
⊢ ((ShortComplex.mk S.f (coimage.π S.g) ⋯).map L).Exact

Proof state:
A : Type u₁
B : Type u₂
inst✝⁶ : Category.{v₁, u₁} A
inst✝⁵ : Category.{v₂, u₂} B
inst✝⁴ : Abelian A
inst✝³ : Abelian B
L : A ⥤ B
inst✝² : L.PreservesZeroMorphisms
inst✝¹ : L.PreservesMonomorphisms
inst✝ : ∀ {X Y : A} (f : X ⟶ Y), PreservesColimit (parallelPair f 0) L
S : ShortComplex A
hS : S.Exact
⊢ 𝟙 ((ShortComplex.mk S.f (coimage.π S.g) ⋯).map L).X₂ ≫ (S.map L).g =
    ((ShortComplex.mk S.f (coimage.π S.g) ⋯).map L).g ≫ L.map (Abelian.factorThruCoimage S.g)

Tactic:
dsimp

Result:
A : Type u₁
B : Type u₂
inst✝⁶ : Category.{v₁, u₁} A
inst✝⁵ : Category.{v₂, u₂} B
inst✝⁴ : Abelian A
inst✝³ : Abelian B
L : A ⥤ B
inst✝² : L.PreservesZeroMorphisms
inst✝¹ : L.PreservesMonomorphisms
inst✝ : ∀ {X Y : A} (f : X ⟶ Y), PreservesColimit (parallelPair f 0) L
S : ShortComplex A
hS : S.Exact
⊢ 𝟙 (L.obj S.X₂) ≫ L.map S.g = L.map (cokernel.π (kernel.ι S.g)) ≫ L.map (Abelian.factorThruCoimage S.g)