-- Mathlib/CategoryTheory/Abelian/Exact.lean
/-- A functor preserving zero morphisms, epis, and kernels preserves homology. -/
lemma preservesHomology_of_preservesEpis_and_kernels [PreservesZeroMorphisms L]
    [PreservesEpimorphisms L] [∀ {X Y} (f : X ⟶ Y), PreservesLimit (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.PreservesEpimorphisms
inst✝ : ∀ {X Y : A} (f : X ⟶ Y), PreservesLimit (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.PreservesEpimorphisms
inst✝ : ∀ {X Y : A} (f : X ⟶ Y), PreservesLimit (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.PreservesEpimorphisms
inst✝ : ∀ {X Y : A} (f : X ⟶ Y), PreservesLimit (parallelPair f 0) L
S : ShortComplex A
hS : S.Exact
φ : S.map L ⟶ (ShortComplex.mk (Abelian.image.ι S.f) S.g ⋯).map L :=
  { τ₁ := L.map (Abelian.factorThruImage S.f), τ₂ := 𝟙 (S.map L).X₂, τ₃ := 𝟙 (S.map L).X₃, comm₁₂ := ⋯, comm₂₃ := ⋯ }
⊢ ((ShortComplex.mk (Abelian.image.ι S.f) S.g ⋯).map L).Exact

Tactic:
apply ShortComplex.exact_of_f_is_kernel

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.PreservesEpimorphisms
inst✝ : ∀ {X Y : A} (f : X ⟶ Y), PreservesLimit (parallelPair f 0) L
S : ShortComplex A
hS : S.Exact
φ : S.map L ⟶ (ShortComplex.mk (Abelian.image.ι S.f) S.g ⋯).map L :=
  { τ₁ := L.map (Abelian.factorThruImage S.f), τ₂ := 𝟙 (S.map L).X₂, τ₃ := 𝟙 (S.map L).X₃, comm₁₂ := ⋯, comm₂₃ := ⋯ }
⊢ IsLimit (KernelFork.ofι ((ShortComplex.mk (Abelian.image.ι S.f) S.g ⋯).map L).f ⋯)

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.PreservesEpimorphisms
inst✝ : ∀ {X Y : A} (f : X ⟶ Y), PreservesLimit (parallelPair f 0) L
S : ShortComplex A
hS : S.Exact
φ : S.map L ⟶ (ShortComplex.mk (Abelian.image.ι S.f) S.g ⋯).map L :=
  { τ₁ := L.map (Abelian.factorThruImage S.f), τ₂ := 𝟙 (S.map L).X₂, τ₃ := 𝟙 (S.map L).X₃, comm₁₂ := ⋯, comm₂₃ := ⋯ }
⊢ (S.map L).Exact

Tactic:
apply (ShortComplex.exact_iff_of_epi_of_isIso_of_mono φ).2

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.PreservesEpimorphisms
inst✝ : ∀ {X Y : A} (f : X ⟶ Y), PreservesLimit (parallelPair f 0) L
S : ShortComplex A
hS : S.Exact
φ : S.map L ⟶ (ShortComplex.mk (Abelian.image.ι S.f) S.g ⋯).map L :=
  { τ₁ := L.map (Abelian.factorThruImage S.f), τ₂ := 𝟙 (S.map L).X₂, τ₃ := 𝟙 (S.map L).X₃, comm₁₂ := ⋯, comm₂₃ := ⋯ }
⊢ ((ShortComplex.mk (Abelian.image.ι S.f) S.g ⋯).map L).Exact

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.PreservesEpimorphisms
inst✝ : ∀ {X Y : A} (f : X ⟶ Y), PreservesLimit (parallelPair f 0) L
S : ShortComplex A
hS : S.Exact
φ : S.map L ⟶ (ShortComplex.mk (Abelian.image.ι S.f) S.g ⋯).map L :=
  { τ₁ := L.map (Abelian.factorThruImage S.f), τ₂ := 𝟙 (S.map L).X₂, τ₃ := 𝟙 (S.map L).X₃, comm₁₂ := ⋯, comm₂₃ := ⋯ }
⊢ IsLimit (KernelFork.ofι ((ShortComplex.mk (Abelian.image.ι S.f) S.g ⋯).map L).f ⋯)

Tactic:
exact KernelFork.mapIsLimit _ ((S.exact_iff_exact_image_ι).1 hS).fIsKernel L

Result:
no goals

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.PreservesEpimorphisms
inst✝ : ∀ {X Y : A} (f : X ⟶ Y), PreservesLimit (parallelPair f 0) L
S : ShortComplex A
hS : S.Exact
⊢ (S.map L).Exact

Tactic:
let φ : S.map L ⟶ (ShortComplex.mk _ _ (Abelian.image_ι_comp_eq_zero S.zero)).map L :=
  { τ₁ := L.map (Abelian.factorThruImage S.f)
    τ₂ := 𝟙 _
    τ₃ := 𝟙 _
    comm₁₂ := by
      dsimp
      rw [Category.comp_id, ← L.map_comp, kernel.lift_ι] }

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.PreservesEpimorphisms
inst✝ : ∀ {X Y : A} (f : X ⟶ Y), PreservesLimit (parallelPair f 0) L
S : ShortComplex A
hS : S.Exact
φ : S.map L ⟶ (ShortComplex.mk (Abelian.image.ι S.f) S.g ⋯).map L :=
  { τ₁ := L.map (Abelian.factorThruImage S.f), τ₂ := 𝟙 (S.map L).X₂, τ₃ := 𝟙 (S.map L).X₃, comm₁₂ := ⋯, comm₂₃ := ⋯ }
⊢ (S.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.PreservesEpimorphisms
inst✝ : ∀ {X Y : A} (f : X ⟶ Y), PreservesLimit (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.PreservesEpimorphisms
inst✝ : ∀ {X Y : A} (f : X ⟶ Y), PreservesLimit (parallelPair f 0) L
⊢ ∀ (S : ShortComplex A), S.Exact → (S.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.PreservesEpimorphisms
inst✝ : ∀ {X Y : A} (f : X ⟶ Y), PreservesLimit (parallelPair f 0) L
S : ShortComplex A
hS : S.Exact
⊢ L.map (Abelian.factorThruImage S.f) ≫ L.map (kernel.ι (cokernel.π S.f)) = L.map S.f ≫ 𝟙 (L.obj S.X₂)

Tactic:
rw [Category.comp_id, ← L.map_comp, kernel.lift_ι]

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.PreservesEpimorphisms
inst✝ : ∀ {X Y : A} (f : X ⟶ Y), PreservesLimit (parallelPair f 0) L
S : ShortComplex A
hS : S.Exact
⊢ L.map (Abelian.factorThruImage S.f) ≫ ((ShortComplex.mk (Abelian.image.ι S.f) S.g ⋯).map L).f =
    (S.map L).f ≫ 𝟙 (S.map L).X₂

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.PreservesEpimorphisms
inst✝ : ∀ {X Y : A} (f : X ⟶ Y), PreservesLimit (parallelPair f 0) L
S : ShortComplex A
hS : S.Exact
⊢ L.map (Abelian.factorThruImage S.f) ≫ L.map (kernel.ι (cokernel.π S.f)) = L.map S.f ≫ 𝟙 (L.obj S.X₂)