From 51bba8efedb3f18b013fff88c6aca2ff1cbaf2df Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=ABl=20Riou?= Date: Mon, 12 Jan 2026 14:27:01 +0100 Subject: [PATCH 1/2] feat(Algebra/Homology/ShortComplex): cycles can be computed with a limit kernel fork --- .../Algebra/Homology/ShortComplex/Basic.lean | 8 ++++- .../Algebra/Homology/ShortComplex/Exact.lean | 30 +++++++++++++++++++ .../Homology/ShortComplex/Homology.lean | 6 ++++ .../Homology/ShortComplex/LeftHomology.lean | 19 ++++++++++++ .../Homology/ShortComplex/RightHomology.lean | 20 +++++++++++++ 5 files changed, 82 insertions(+), 1 deletion(-) diff --git a/Mathlib/Algebra/Homology/ShortComplex/Basic.lean b/Mathlib/Algebra/Homology/ShortComplex/Basic.lean index 20a2324b2ee0e1..98dc3003d70129 100644 --- a/Mathlib/Algebra/Homology/ShortComplex/Basic.lean +++ b/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 diff --git a/Mathlib/Algebra/Homology/ShortComplex/Exact.lean b/Mathlib/Algebra/Homology/ShortComplex/Exact.lean index beee9f0dc869a9..38285d78155ea9 100644 --- a/Mathlib/Algebra/Homology/ShortComplex/Exact.lean +++ b/Mathlib/Algebra/Homology/ShortComplex/Exact.lean @@ -829,6 +829,36 @@ section Abelian variable [Abelian C] +section + +variable {X Y : C} (f : X ⟶ Y) + +/-- The exact short complex `kernel f ⟶ X ⟶ Y` for any morphism `f : X ⟶ Y`. -/ +@[simps] +noncomputable def kernelSequence : ShortComplex C := + ShortComplex.mk _ _ (kernel.condition f) + +/-- The exact short complex `X ⟶ Y ⟶ cokernel f` for any morphism `f : X ⟶ Y`. -/ +@[simps] +noncomputable def cokernelSequence : ShortComplex C := + ShortComplex.mk _ _ (cokernel.condition f) + +instance : Mono (kernelSequence f).f := by + dsimp + infer_instance + +instance : Epi (cokernelSequence f).g := by + dsimp + infer_instance + +lemma kernelSequence_exact : (kernelSequence f).Exact := + exact_of_f_is_kernel _ (kernelIsKernel f) + +lemma cokernelSequence_exact : (cokernelSequence f).Exact := + exact_of_g_is_cokernel _ (cokernelIsCokernel f) + +end + /-- Given a morphism of short complexes `φ : S₁ ⟶ S₂` in an abelian category, if `S₁.f` and `S₁.g` are zero (e.g. when `S₁` is of the form `0 ⟶ S₁.X₂ ⟶ 0`) and `S₂.f = 0` (e.g when `S₂` is of the form `0 ⟶ S₂.X₂ ⟶ S₂.X₃`), then `φ` is a quasi-isomorphism iff diff --git a/Mathlib/Algebra/Homology/ShortComplex/Homology.lean b/Mathlib/Algebra/Homology/ShortComplex/Homology.lean index da80f1d73236af..d9ce2b088e7557 100644 --- a/Mathlib/Algebra/Homology/ShortComplex/Homology.lean +++ b/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₂)] : diff --git a/Mathlib/Algebra/Homology/ShortComplex/LeftHomology.lean b/Mathlib/Algebra/Homology/ShortComplex/LeftHomology.lean index ed538341e74c76..a7d3a07f797d52 100644 --- a/Mathlib/Algebra/Homology/ShortComplex/LeftHomology.lean +++ b/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] diff --git a/Mathlib/Algebra/Homology/ShortComplex/RightHomology.lean b/Mathlib/Algebra/Homology/ShortComplex/RightHomology.lean index 17d6e27efeb4f0..55cdca9ddc1f73 100644 --- a/Mathlib/Algebra/Homology/ShortComplex/RightHomology.lean +++ b/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] From 4aee9552148c8759e4493631c1c874c1e896da26 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=ABl=20Riou?= <37772949+joelriou@users.noreply.github.com> Date: Fri, 16 Jan 2026 23:54:41 +0100 Subject: [PATCH 2/2] Remove duplicate definitions --- .../Algebra/Homology/ShortComplex/Exact.lean | 30 ------------------- 1 file changed, 30 deletions(-) diff --git a/Mathlib/Algebra/Homology/ShortComplex/Exact.lean b/Mathlib/Algebra/Homology/ShortComplex/Exact.lean index 38285d78155ea9..beee9f0dc869a9 100644 --- a/Mathlib/Algebra/Homology/ShortComplex/Exact.lean +++ b/Mathlib/Algebra/Homology/ShortComplex/Exact.lean @@ -829,36 +829,6 @@ section Abelian variable [Abelian C] -section - -variable {X Y : C} (f : X ⟶ Y) - -/-- The exact short complex `kernel f ⟶ X ⟶ Y` for any morphism `f : X ⟶ Y`. -/ -@[simps] -noncomputable def kernelSequence : ShortComplex C := - ShortComplex.mk _ _ (kernel.condition f) - -/-- The exact short complex `X ⟶ Y ⟶ cokernel f` for any morphism `f : X ⟶ Y`. -/ -@[simps] -noncomputable def cokernelSequence : ShortComplex C := - ShortComplex.mk _ _ (cokernel.condition f) - -instance : Mono (kernelSequence f).f := by - dsimp - infer_instance - -instance : Epi (cokernelSequence f).g := by - dsimp - infer_instance - -lemma kernelSequence_exact : (kernelSequence f).Exact := - exact_of_f_is_kernel _ (kernelIsKernel f) - -lemma cokernelSequence_exact : (cokernelSequence f).Exact := - exact_of_g_is_cokernel _ (cokernelIsCokernel f) - -end - /-- Given a morphism of short complexes `φ : S₁ ⟶ S₂` in an abelian category, if `S₁.f` and `S₁.g` are zero (e.g. when `S₁` is of the form `0 ⟶ S₁.X₂ ⟶ 0`) and `S₂.f = 0` (e.g when `S₂` is of the form `0 ⟶ S₂.X₂ ⟶ S₂.X₃`), then `φ` is a quasi-isomorphism iff