[Merged by Bors] - feat(Algebra/Homology/ShortComplex): cycles can be computed with a limit kernel fork

Mathlib/Algebra/Homology/ShortComplex/Basic.lean

@@ -43,7 +43,7 @@ structure ShortComplex where
   /-- the second morphism of a `ShortComplex` -/
   g : X₂ ⟶ X₃
   /-- the composition of the two given morphisms is zero -/
-  zero : f ≫ g = 0
+  zero : f ≫ g = 0 := by cat_disch
 
 namespace ShortComplex
 
@@ -221,6 +221,12 @@ def isoMk (e₁ : S₁.X₁ ≅ S₂.X₁) (e₂ : S₁.X₂ ≅ S₂.X₂) (e
 lemma isIso_of_isIso (f : S₁ ⟶ S₂) [IsIso f.τ₁] [IsIso f.τ₂] [IsIso f.τ₃] : IsIso f :=
   (isoMk (asIso f.τ₁) (asIso f.τ₂) (asIso f.τ₃)).isIso_hom
 
+lemma isIso_iff (f : S₁ ⟶ S₂) :
+    IsIso f ↔ IsIso f.τ₁ ∧ IsIso f.τ₂ ∧ IsIso f.τ₃ := by
+  refine ⟨fun _ ↦ ⟨inferInstance, inferInstance, inferInstance⟩, ?_⟩
+  rintro ⟨_, _, _⟩
+  apply isIso_of_isIso
+
 /-- The first map of a short complex, as a functor. -/
 @[simps] def fFunctor : ShortComplex C ⥤ Arrow C where
   obj S := .mk S.f

Mathlib/Algebra/Homology/ShortComplex/Homology.lean

@@ -694,6 +694,12 @@ lemma HomologyData.right_homologyIso_eq_left_homologyIso_trans_iso
   dsimp
   rw [← leftRightHomologyComparison'_fac, leftRightHomologyComparison'_eq]
 
+lemma HomologyData.left_homologyIso_eq_right_homologyIso_trans_iso_symm
+    (h : S.HomologyData) [S.HasHomology] :
+    h.left.homologyIso = h.right.homologyIso ≪≫ h.iso.symm := by
+  rw [right_homologyIso_eq_left_homologyIso_trans_iso]
+  cat_disch
+
 lemma hasHomology_of_isIso_leftRightHomologyComparison'
     (h₁ : S.LeftHomologyData) (h₂ : S.RightHomologyData)
     [IsIso (leftRightHomologyComparison' h₁ h₂)] :

Mathlib/Algebra/Homology/ShortComplex/LeftHomology.lean

@@ -971,6 +971,25 @@ noncomputable def cyclesIsoKernel [HasKernel S.g] : S.cycles ≅ kernel S.g wher
   hom := kernel.lift S.g S.iCycles (by simp)
   inv := S.liftCycles (kernel.ι S.g) (by simp)
 
+section
+
+variable {kf : KernelFork S.g} (hkf : IsLimit kf)
+
+/-- The isomorphism from the point of a limit kernel fork of `S.g` to `S.cycles`. -/
+noncomputable def isoCyclesOfIsLimit :
+    kf.pt ≅ S.cycles :=
+  IsLimit.conePointUniqueUpToIso hkf S.cyclesIsKernel
+
+@[reassoc (attr := simp)]
+lemma isoCyclesOfIsLimit_inv_ι : (S.isoCyclesOfIsLimit hkf).inv ≫ kf.ι = S.iCycles :=
+  IsLimit.conePointUniqueUpToIso_inv_comp _ _ WalkingParallelPair.zero
+
+@[reassoc (attr := simp)]
+lemma isoCyclesOfIsLimit_hom_iCycles : (S.isoCyclesOfIsLimit hkf).hom ≫ S.iCycles = kf.ι :=
+  IsLimit.conePointUniqueUpToIso_hom_comp _ _ WalkingParallelPair.zero
+
+end
+
 /-- The morphism `A ⟶ S.leftHomology` obtained from a morphism `k : A ⟶ S.X₂`
 such that `k ≫ S.g = 0.` -/
 @[simp]

Mathlib/Algebra/Homology/ShortComplex/RightHomology.lean

@@ -1253,6 +1253,26 @@ noncomputable def opcyclesIsoCokernel [HasCokernel S.f] : S.opcycles ≅ cokerne
   hom := S.descOpcycles (cokernel.π S.f) (by simp)
   inv := cokernel.desc S.f S.pOpcycles (by simp)
 
+section
+
+variable {cc : CokernelCofork S.f} (hcc : IsColimit cc)
+
+/-- The isomorphism from the point of a colimit cokernel cofork of `S.f` to `S.opcycles`. -/
+noncomputable def isoOpcyclesOfIsColimit :
+    cc.pt ≅ S.opcycles :=
+  IsColimit.coconePointUniqueUpToIso hcc S.opcyclesIsCokernel
+
+@[reassoc (attr := simp)]
+lemma π_isoOpcyclesOfIsColimit_hom : cc.π ≫ (S.isoOpcyclesOfIsColimit hcc).hom = S.pOpcycles :=
+  IsColimit.comp_coconePointUniqueUpToIso_hom _ _ WalkingParallelPair.one
+
+@[reassoc (attr := simp)]
+lemma pOpcycles_π_isoOpcyclesOfIsColimit_inv :
+    S.pOpcycles ≫ (S.isoOpcyclesOfIsColimit hcc).inv = cc.π :=
+  IsColimit.comp_coconePointUniqueUpToIso_inv _ S.opcyclesIsCokernel WalkingParallelPair.one
+
+end
+
 /-- The morphism `S.rightHomology ⟶ A` obtained from a morphism `k : S.X₂ ⟶ A`
 such that `S.f ≫ k = 0.` -/
 @[simp]