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/3] 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 b2a79ba5e969a98698cde8738f628e1f7848a2c7 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=ABl=20Riou?= Date: Mon, 12 Jan 2026 14:36:30 +0100 Subject: [PATCH 2/3] feat(Algebra/Homology): an homology data from an epi-mono factorization --- .../Homology/ShortComplex/Abelian.lean | 170 +++++++++++++++++- .../Limits/Shapes/Equalizers.lean | 7 +- 2 files changed, 173 insertions(+), 4 deletions(-) diff --git a/Mathlib/Algebra/Homology/ShortComplex/Abelian.lean b/Mathlib/Algebra/Homology/ShortComplex/Abelian.lean index 56759f82a449c4..7baff2279806bd 100644 --- a/Mathlib/Algebra/Homology/ShortComplex/Abelian.lean +++ b/Mathlib/Algebra/Homology/ShortComplex/Abelian.lean @@ -6,7 +6,10 @@ Authors: Joël Riou module public import Mathlib.Algebra.Homology.ShortComplex.Homology +public import Mathlib.Algebra.Homology.ShortComplex.Limits +public import Mathlib.Algebra.Homology.ShortComplex.Preadditive public import Mathlib.CategoryTheory.Abelian.Basic +public import Batteries.Tactic.Lint /-! # Abelian categories have homology @@ -24,17 +27,23 @@ these left and right homology data are compatible (i.e. provide a `HomologyData`) is obtained by using the coimage-image isomorphism in abelian categories. +We also provide a constructor `HomologyData.ofEpiMonoFactorisation` +which takes as an input an epi-mono factorization `kf.pt ⟶ H ⟶ cc.pt` +of `kf.ι ≫ cc.π` where `kf` is a limit kernel fork of `S.g` and +`cc` is a limit cokernel cofork of `S.f`. + -/ @[expose] public section -universe v u +universe v v' u u' namespace CategoryTheory open Category Limits variable {C : Type u} [Category.{v} C] [Abelian C] (S : ShortComplex C) + {D : Type u'} [Category.{v'} D] [HasZeroMorphisms D] namespace ShortComplex @@ -185,6 +194,165 @@ instance _root_.CategoryTheory.categoryWithHomology_of_abelian : CategoryWithHomology C where hasHomology S := HasHomology.mk' (HomologyData.ofAbelian S) +noncomputable instance : IsNormalMonoCategory (ShortComplex C) := ⟨fun i _ => ⟨by + refine NormalMono.mk _ (cokernel.π i) (cokernel.condition _) + (isLimitOfIsLimitπ _ ?_ ?_ ?_) + all_goals apply Abelian.isLimitMapConeOfKernelForkOfι⟩⟩ + +noncomputable instance : IsNormalEpiCategory (ShortComplex C) := ⟨fun p _ => ⟨by + refine NormalEpi.mk _ (kernel.ι p) (kernel.condition _) + (isColimitOfIsColimitπ _ ?_ ?_ ?_) + all_goals apply Abelian.isColimitMapCoconeOfCokernelCoforkOfπ⟩⟩ + +noncomputable instance : Abelian (ShortComplex C) where + +attribute [local instance] strongEpi_of_epi + +/-- The homology of a short complex `S` in an abelian category identifies to +the image of `S.iCycles ≫ S.pOpcycles : S.cycles ⟶ S.opcycles`. -/ +noncomputable def homologyIsoImageICyclesCompPOpcycles : + S.homology ≅ image (S.iCycles ≫ S.pOpcycles) := + image.isoStrongEpiMono _ _ S.homology_π_ι + +@[reassoc (attr := simp)] +lemma homologyIsoImageICyclesCompPOpcycles_ι : + S.homologyIsoImageICyclesCompPOpcycles.hom ≫ image.ι (S.iCycles ≫ S.pOpcycles) = + S.homologyι := + image.isoStrongEpiMono_hom_comp_ι _ _ _ + +namespace HomologyData + +namespace ofEpiMonoFactorisation + +variable {kf : KernelFork S.g} {cc : CokernelCofork S.f} + (hkf : IsLimit kf) (hcc : IsColimit cc) + {H : C} {π : kf.pt ⟶ H} {ι : H ⟶ cc.pt} + (fac : kf.ι ≫ cc.π = π ≫ ι) + [Epi π] [Mono ι] + +/-- Let `S` be a short complex in an abelian category. Let `kf` be a +limit kernel fork of `S.g` and `cc` a limit cokernel cofork of `S.f`. +Let `kf.pt ⟶ H ⟶ cc.pt` be an epi-mono factorization of `kf.ι ≫ cc.π : kf.pt ⟶ cc.pt`, +then `H` identifies to the image of `S.iCycles ≫ S.pOpcycles : S.cycles ⟶ S.opcycles`. -/ +noncomputable def isoImage : H ≅ image (S.iCycles ≫ S.pOpcycles) := by + have : ((S.isoCyclesOfIsLimit hkf).inv ≫ π) ≫ ι ≫ + (S.isoOpcyclesOfIsColimit hcc).hom = S.iCycles ≫ S.pOpcycles := by + simp [← reassoc_of% fac] + exact image.isoStrongEpiMono _ _ this + +@[reassoc (attr := simp)] +lemma isoImage_ι : + (isoImage S hkf hcc fac).hom ≫ image.ι (S.iCycles ≫ S.pOpcycles) = + ι ≫ (S.isoOpcyclesOfIsColimit hcc).hom := by + apply image.isoStrongEpiMono_hom_comp_ι + simp [← reassoc_of% fac] + +/-- Let `S` be a short complex in an abelian category. Let `kf` be a +limit kernel fork of `S.g` and `cc` a limit cokernel cofork of `S.f`. +Let `kf.pt ⟶ H ⟶ cc.pt` be an epi-mono factorization of `kf.ι ≫ cc.π : kf.pt ⟶ cc.pt`, +then `H` identifies to the homology of `S`. -/ +noncomputable def isoHomology : H ≅ S.homology := + isoImage S hkf hcc fac ≪≫ S.homologyIsoImageICyclesCompPOpcycles.symm + +@[reassoc (attr := simp)] +lemma π_comp_isoHomology_hom : + π ≫ (isoHomology S hkf hcc fac).hom = (S.isoCyclesOfIsLimit hkf).hom ≫ S.homologyπ := by + dsimp [isoHomology] + simp [← cancel_mono (S.homologyIsoImageICyclesCompPOpcycles.hom), + ← cancel_mono (image.ι (S.iCycles ≫ S.pOpcycles)), + ← reassoc_of% fac] + +@[reassoc (attr := simp)] +lemma isoHomology_hom_comp_ι : + (isoHomology S hkf hcc fac).inv ≫ ι = S.homologyι ≫ (S.isoOpcyclesOfIsColimit hcc).inv := by + simp [← cancel_epi S.homologyπ, ← cancel_epi (S.isoCyclesOfIsLimit hkf).hom, + ← π_comp_isoHomology_hom_assoc S hkf hcc fac, ← fac] + +lemma f'_eq : + hkf.lift (KernelFork.ofι S.f S.zero) = + S.toCycles ≫ (S.isoCyclesOfIsLimit hkf).inv := by + have := Fork.IsLimit.mono hkf + simp [← cancel_mono kf.ι] + +lemma g'_eq : hcc.desc (CokernelCofork.ofπ S.g S.zero) = + (S.isoOpcyclesOfIsColimit hcc).hom ≫ S.fromOpcycles := by + have := Cofork.IsColimit.epi hcc + simp [← cancel_epi cc.π] + +@[reassoc (attr := simp)] +lemma homologyπ_isoHomology_inv : + S.homologyπ ≫ (isoHomology S hkf hcc fac).inv = (S.isoCyclesOfIsLimit hkf).inv ≫ π := by + simp only [← cancel_mono (isoHomology S hkf hcc fac).hom, assoc, Iso.inv_hom_id, comp_id, + π_comp_isoHomology_hom, Iso.inv_hom_id_assoc] + +@[reassoc (attr := simp)] +lemma isoHomology_inv_homologyι : + (isoHomology S hkf hcc fac).hom ≫ S.homologyι = + ι ≫ (S.isoOpcyclesOfIsColimit hcc).hom := by + rw [← cancel_mono (S.isoOpcyclesOfIsColimit hcc).inv, assoc, assoc, Iso.hom_inv_id, + comp_id, ← isoHomology_hom_comp_ι S hkf hcc fac, Iso.hom_inv_id_assoc] + +/-- Let `S` be a short complex in an abelian category. Let `kf` be a +limit kernel fork of `S.g` and `cc` a limit cokernel cofork of `S.f`. +Let `kf.pt ⟶ H ⟶ cc.pt` be an epi-mono factorization of `kf.ι ≫ cc.π : kf.pt ⟶ cc.pt`. +This is the left homology data expressing `H` as the homology of `S`. -/ +@[simps] +noncomputable def leftHomologyData : S.LeftHomologyData where + K := kf.pt + H := H + i := kf.ι + π := π + wi := KernelFork.condition kf + hi := IsLimit.ofIsoLimit hkf (Fork.ext (Iso.refl _) (by simp)) + wπ := by + dsimp + rw [← cancel_mono (isoHomology S hkf hcc fac).hom, assoc, assoc, id_comp, + π_comp_isoHomology_hom, zero_comp, f'_eq, + assoc, Iso.inv_hom_id_assoc, toCycles_comp_homologyπ] + hπ := by + refine (IsColimit.equivOfNatIsoOfIso ?_ _ _ ?_).2 S.homologyIsCokernel + · exact parallelPair.ext (Iso.refl _) (S.isoCyclesOfIsLimit hkf) + · exact Cofork.ext (isoHomology S hkf hcc fac) (by simp [Cofork.π]) + +attribute [local simp] g'_eq in +/-- Let `S` be a short complex in an abelian category. Let `kf` be a +limit kernel fork of `S.g` and `cc` a limit cokernel cofork of `S.f`. +Let `kf.pt ⟶ H ⟶ cc.pt` be an epi-mono factorization of `kf.ι ≫ cc.π : kf.pt ⟶ cc.pt`. +This is the right homology data expressing `H` as the homology of `S`. -/ +@[simps] +noncomputable def rightHomologyData : S.RightHomologyData where + Q := cc.pt + H := H + p := cc.π + ι := ι + wp := CokernelCofork.condition cc + hp := IsColimit.ofIsoColimit hcc (Cofork.ext (Iso.refl _) (by simp)) + wι := by + dsimp + rw [id_comp, g'_eq, ← cancel_epi (isoHomology S hkf hcc fac).inv, comp_zero, + isoHomology_hom_comp_ι_assoc, Iso.inv_hom_id_assoc, homologyι_comp_fromOpcycles] + hι := by + refine (IsLimit.equivOfNatIsoOfIso ?_ _ _ ?_).2 S.homologyIsKernel + · exact parallelPair.ext (S.isoOpcyclesOfIsColimit hcc) (Iso.refl _) + · exact Fork.ext (isoHomology S hkf hcc fac) (by simp [Fork.ι]) + +end ofEpiMonoFactorisation + +/-- Let `S` be a short complex in an abelian category. Let `kf` be a +limit kernel fork of `S.g` and `cc` a limit cokernel cofork of `S.f`. +Let `kf.pt ⟶ H ⟶ cc.pt` be an epi-mono factorization of `kf.ι ≫ cc.π : kf.pt ⟶ cc.pt`. +This is the homology data expressing `H` as the homology of `S`. -/ +@[simps] +noncomputable def ofEpiMonoFactorisation {kf : KernelFork S.g} {cc : CokernelCofork S.f} + (hkf : IsLimit kf) (hcc : IsColimit cc) {H : C} {π : kf.pt ⟶ H} {ι : H ⟶ cc.pt} + (fac : kf.ι ≫ cc.π = π ≫ ι) [Epi π] [Mono ι] : + S.HomologyData where + left := ofEpiMonoFactorisation.leftHomologyData S hkf hcc fac + right := ofEpiMonoFactorisation.rightHomologyData S hkf hcc fac + iso := Iso.refl _ + +end HomologyData + end ShortComplex end CategoryTheory diff --git a/Mathlib/CategoryTheory/Limits/Shapes/Equalizers.lean b/Mathlib/CategoryTheory/Limits/Shapes/Equalizers.lean index 185610d7147608..e4709b2fb7425b 100644 --- a/Mathlib/CategoryTheory/Limits/Shapes/Equalizers.lean +++ b/Mathlib/CategoryTheory/Limits/Shapes/Equalizers.lean @@ -297,9 +297,10 @@ theorem parallelPairHom_app_one {X' Y' : C} (f g : X ⟶ Y) (f' g' : X' ⟶ Y') /-- Construct a natural isomorphism between functors out of the walking parallel pair from its components. -/ @[simps!] -def parallelPair.ext {F G : WalkingParallelPair ⥤ C} (zero : F.obj zero ≅ G.obj zero) - (one : F.obj one ≅ G.obj one) (left : F.map left ≫ one.hom = zero.hom ≫ G.map left) - (right : F.map right ≫ one.hom = zero.hom ≫ G.map right) : F ≅ G := +def parallelPair.ext {F G : WalkingParallelPair ⥤ C} + (zero : F.obj zero ≅ G.obj zero) (one : F.obj one ≅ G.obj one) + (left : F.map left ≫ one.hom = zero.hom ≫ G.map left := by cat_disch) + (right : F.map right ≫ one.hom = zero.hom ≫ G.map right := by cat_disch) : F ≅ G := NatIso.ofComponents (by rintro ⟨j⟩ From 9d4b9c808bc2bc2afe041167784865ebc2d69443 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=ABl=20Riou?= Date: Fri, 23 Jan 2026 19:42:11 +0100 Subject: [PATCH 3/3] removed unnecessary import --- Mathlib/Algebra/Homology/ShortComplex/Abelian.lean | 1 - 1 file changed, 1 deletion(-) diff --git a/Mathlib/Algebra/Homology/ShortComplex/Abelian.lean b/Mathlib/Algebra/Homology/ShortComplex/Abelian.lean index 7baff2279806bd..b0cee5debaaea2 100644 --- a/Mathlib/Algebra/Homology/ShortComplex/Abelian.lean +++ b/Mathlib/Algebra/Homology/ShortComplex/Abelian.lean @@ -9,7 +9,6 @@ public import Mathlib.Algebra.Homology.ShortComplex.Homology public import Mathlib.Algebra.Homology.ShortComplex.Limits public import Mathlib.Algebra.Homology.ShortComplex.Preadditive public import Mathlib.CategoryTheory.Abelian.Basic -public import Batteries.Tactic.Lint /-! # Abelian categories have homology