From 8bf233051fa95b0562c0794f9735f62b1056050f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=ABl=20Riou?= Date: Wed, 31 Dec 2025 16:37:59 +0100 Subject: [PATCH 1/4] wip --- Mathlib.lean | 1 + .../Algebra/Homology/ExactSequenceFour.lean | 84 +++++++++++++++++++ 2 files changed, 85 insertions(+) create mode 100644 Mathlib/Algebra/Homology/ExactSequenceFour.lean diff --git a/Mathlib.lean b/Mathlib.lean index 73f4357ce74b0b..5d67467c5d9196 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -578,6 +578,7 @@ public import Mathlib.Algebra.Homology.Embedding.TruncGEHomology public import Mathlib.Algebra.Homology.Embedding.TruncLE public import Mathlib.Algebra.Homology.Embedding.TruncLEHomology public import Mathlib.Algebra.Homology.ExactSequence +public import Mathlib.Algebra.Homology.ExactSequenceFour public import Mathlib.Algebra.Homology.Factorizations.Basic public import Mathlib.Algebra.Homology.Factorizations.CM5b public import Mathlib.Algebra.Homology.Functor diff --git a/Mathlib/Algebra/Homology/ExactSequenceFour.lean b/Mathlib/Algebra/Homology/ExactSequenceFour.lean new file mode 100644 index 00000000000000..2db8ca5d22a94d --- /dev/null +++ b/Mathlib/Algebra/Homology/ExactSequenceFour.lean @@ -0,0 +1,84 @@ +/- +Copyright (c) 2025 Joël Riou. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Joël Riou +-/ +module + +public import Mathlib.Algebra.Homology.ExactSequence + +/-! +# Exact sequences with four terms + +-/ + +@[expose] public section + +namespace CategoryTheory + +open Category Limits + +namespace ComposableArrows + +section HasZeroMorphisms + +namespace IsComplex + +variable {C : Type*} [Category* C] [HasZeroMorphisms C] {n : ℕ} {S : ComposableArrows C (n + 3)} + (hS : S.IsComplex) (k : ℕ) + +section + +variable (hk : k ≤ n) (cc : CokernelCofork (S.map' k (k + 1))) + (kf : KernelFork (S.map' (k + 2) (k + 3))) (hcc : IsColimit cc) (hkf : IsLimit kf) + +/-- If `S : ComposableArrows C (n + 3)` and `k : ℕ` satisfies `k ≤ n`, this is the induced +map from a cokernel of `S.map' k (k + 1)` to a kernel of `S.map' (k + 2) (k + 3)`. -/ +def cokerToKer' : cc.pt ⟶ kf.pt := + IsColimit.desc hcc + (CokernelCofork.ofπ (π := IsLimit.lift hkf (KernelFork.ofι _ (hS.zero (k + 1)))) + (Fork.IsLimit.hom_ext hkf (by simpa using hS.zero k))) + +-- `reassoc` no longer works if we make this file a module +--@[reassoc (attr := simp)] +lemma cokerToKer'_fac : + cc.π ≫ hS.cokerToKer' k hk cc kf hcc hkf ≫ kf.ι = + S.map' (k + 1) (k + 2) := by + simp [cokerToKer'] + +end + +section + +variable (hk : k ≤ n := by lia) + [HasCokernel (S.map' k (k + 1))] [HasKernel (S.map' (k + 2) (k + 3))] + +/- +The following definition produces the following error when making this file a module: + +Unknown constant `_private.Mathlib.Algebra.Homology.ExactSequenceFour.0._proof_15` + +Note: A private declaration `_proof_15` (from the current module) exists but would need +to be public to access here.-/ + +/-- If `S : ComposableArrows C (n + 3)` and `k : ℕ` satisfies `k ≤ n`, this is the induced +map from the cokernel of `S.map' k (k + 1)` to the kernel of `S.map' (k + 2) (k + 3)`. -/ +noncomputable def cokerToKer : + cokernel (S.map' k (k + 1) _ _) ⟶ kernel (S.map' (k + 2) (k + 3) _ _) := + hS.cokerToKer' k hk (CokernelCofork.ofπ _ (cokernel.condition _)) + (KernelFork.ofι _ (kernel.condition _)) (cokernelIsCokernel _) (kernelIsKernel _) + +@[reassoc (attr := simp)] +lemma cokerToKer_fac : + cokernel.π _ ≫ hS.cokerToKer k ≫ kernel.ι _ = S.map' (k + 1) (k + 2) := + hS.cokerToKer'_fac k hk _ _ (cokernelIsCokernel _) (kernelIsKernel _) + +end + +end IsComplex + +end HasZeroMorphisms + +end ComposableArrows + +end CategoryTheory From cda3027ca6307f1ea998637b3d406c93de8c33b7 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=ABl=20Riou?= Date: Wed, 31 Dec 2025 17:15:45 +0100 Subject: [PATCH 2/4] fix --- .../Algebra/Homology/ExactSequenceFour.lean | 42 ++++++------------- 1 file changed, 13 insertions(+), 29 deletions(-) diff --git a/Mathlib/Algebra/Homology/ExactSequenceFour.lean b/Mathlib/Algebra/Homology/ExactSequenceFour.lean index 2db8ca5d22a94d..be21eb765f777b 100644 --- a/Mathlib/Algebra/Homology/ExactSequenceFour.lean +++ b/Mathlib/Algebra/Homology/ExactSequenceFour.lean @@ -27,54 +27,38 @@ namespace IsComplex variable {C : Type*} [Category* C] [HasZeroMorphisms C] {n : ℕ} {S : ComposableArrows C (n + 3)} (hS : S.IsComplex) (k : ℕ) -section - -variable (hk : k ≤ n) (cc : CokernelCofork (S.map' k (k + 1))) - (kf : KernelFork (S.map' (k + 2) (k + 3))) (hcc : IsColimit cc) (hkf : IsLimit kf) - /-- If `S : ComposableArrows C (n + 3)` and `k : ℕ` satisfies `k ≤ n`, this is the induced map from a cokernel of `S.map' k (k + 1)` to a kernel of `S.map' (k + 2) (k + 3)`. -/ -def cokerToKer' : cc.pt ⟶ kf.pt := +def cokerToKer' (hk : k ≤ n) (cc : CokernelCofork (S.map' k (k + 1))) + (kf : KernelFork (S.map' (k + 2) (k + 3))) + (hcc : IsColimit cc) (hkf : IsLimit kf) : + cc.pt ⟶ kf.pt := IsColimit.desc hcc (CokernelCofork.ofπ (π := IsLimit.lift hkf (KernelFork.ofι _ (hS.zero (k + 1)))) (Fork.IsLimit.hom_ext hkf (by simpa using hS.zero k))) --- `reassoc` no longer works if we make this file a module ---@[reassoc (attr := simp)] -lemma cokerToKer'_fac : +@[reassoc (attr := simp)] +lemma cokerToKer'_fac (hk : k ≤ n) (cc : CokernelCofork (S.map' k (k + 1))) + (kf : KernelFork (S.map' (k + 2) (k + 3))) + (hcc : IsColimit cc) (hkf : IsLimit kf) : cc.π ≫ hS.cokerToKer' k hk cc kf hcc hkf ≫ kf.ι = S.map' (k + 1) (k + 2) := by simp [cokerToKer'] -end - -section - -variable (hk : k ≤ n := by lia) - [HasCokernel (S.map' k (k + 1))] [HasKernel (S.map' (k + 2) (k + 3))] - -/- -The following definition produces the following error when making this file a module: - -Unknown constant `_private.Mathlib.Algebra.Homology.ExactSequenceFour.0._proof_15` - -Note: A private declaration `_proof_15` (from the current module) exists but would need -to be public to access here.-/ - /-- If `S : ComposableArrows C (n + 3)` and `k : ℕ` satisfies `k ≤ n`, this is the induced map from the cokernel of `S.map' k (k + 1)` to the kernel of `S.map' (k + 2) (k + 3)`. -/ -noncomputable def cokerToKer : +noncomputable def cokerToKer (hk : k ≤ n) + [HasCokernel (S.map' k (k + 1))] [HasKernel (S.map' (k + 2) (k + 3))] : cokernel (S.map' k (k + 1) _ _) ⟶ kernel (S.map' (k + 2) (k + 3) _ _) := hS.cokerToKer' k hk (CokernelCofork.ofπ _ (cokernel.condition _)) (KernelFork.ofι _ (kernel.condition _)) (cokernelIsCokernel _) (kernelIsKernel _) @[reassoc (attr := simp)] -lemma cokerToKer_fac : - cokernel.π _ ≫ hS.cokerToKer k ≫ kernel.ι _ = S.map' (k + 1) (k + 2) := +lemma cokerToKer_fac (hk : k ≤ n) + [HasCokernel (S.map' k (k + 1))] [HasKernel (S.map' (k + 2) (k + 3))] : + cokernel.π _ ≫ hS.cokerToKer k hk ≫ kernel.ι _ = S.map' (k + 1) (k + 2) := hS.cokerToKer'_fac k hk _ _ (cokernelIsCokernel _) (kernelIsKernel _) -end - end IsComplex end HasZeroMorphisms From a1138dd9a0444866930640ea4e201e561e5037b3 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=ABl=20Riou?= Date: Mon, 12 Jan 2026 15:15:21 +0100 Subject: [PATCH 3/4] feat(Algebra/Homology): exact sequences with four terms --- Mathlib/Algebra/Homology/ExactSequence.lean | 13 ++ .../Algebra/Homology/ExactSequenceFour.lean | 191 ++++++++++++++++-- 2 files changed, 185 insertions(+), 19 deletions(-) diff --git a/Mathlib/Algebra/Homology/ExactSequence.lean b/Mathlib/Algebra/Homology/ExactSequence.lean index b0081ee5fef5c5..f23298d04ad5d6 100644 --- a/Mathlib/Algebra/Homology/ExactSequence.lean +++ b/Mathlib/Algebra/Homology/ExactSequence.lean @@ -136,6 +136,19 @@ lemma Exact.exact' (hS : S.Exact) (i j k : ℕ) (hij : i + 1 = j := by omega) subst hij hjk exact hS.exact i hk +/-- The (exact) short complex consisting of maps `S.map' i j` and `S.map' j k` when we know +that `S : ComposableArrows C n` is exact. -/ +abbrev Exact.sc' (hS : S.Exact) (i j k : ℕ) (hij : i + 1 = j := by lia) + (hjk : j + 1 = k := by lia) (hk : k ≤ n := by lia) : + ShortComplex C := + S.sc' hS.toIsComplex i j k + +/-- The short complex consisting of maps `S.map' i (i + 1)` and `S.map' (i + 1) (i + 2)` +when we know that `S : ComposableArrows C n` is exact. -/ +abbrev Exact.sc (hS : S.Exact) (i : ℕ) (hi : i + 2 ≤ n := by lia) : + ShortComplex C := + S.sc' hS.toIsComplex i (i + 1) (i + 2) + /-- Functoriality maps for `ComposableArrows.sc'`. -/ @[simps] def sc'Map {S₁ S₂ : ComposableArrows C n} (φ : S₁ ⟶ S₂) (h₁ : S₁.IsComplex) (h₂ : S₂.IsComplex) diff --git a/Mathlib/Algebra/Homology/ExactSequenceFour.lean b/Mathlib/Algebra/Homology/ExactSequenceFour.lean index be21eb765f777b..442ebdf4d549f6 100644 --- a/Mathlib/Algebra/Homology/ExactSequenceFour.lean +++ b/Mathlib/Algebra/Homology/ExactSequenceFour.lean @@ -10,6 +10,11 @@ public import Mathlib.Algebra.Homology.ExactSequence /-! # Exact sequences with four terms +The main definition in this file is `ComposableArrows.Exact.cokerIsoKer`: +given an exact sequence `S` (involving at least four objects), +this is the isomorphism from the cokernel of `S.map' k (k + 1)` +to the kernel of `S.map' (k + 2) (k + 3)`. + -/ @[expose] public section @@ -24,45 +29,193 @@ section HasZeroMorphisms namespace IsComplex -variable {C : Type*} [Category* C] [HasZeroMorphisms C] {n : ℕ} {S : ComposableArrows C (n + 3)} +variable {C : Type*} [Category C] [HasZeroMorphisms C] {n : ℕ} {S : ComposableArrows C (n + 3)} (hS : S.IsComplex) (k : ℕ) -/-- If `S : ComposableArrows C (n + 3)` and `k : ℕ` satisfies `k ≤ n`, this is the induced -map from a cokernel of `S.map' k (k + 1)` to a kernel of `S.map' (k + 2) (k + 3)`. -/ +section + +/-- If `S` is a complex, this is the morphism from a cokernel of `S.map' k (k + 1)` +to a kernel of `S.map' (k + 2) (k + 3)`. -/ def cokerToKer' (hk : k ≤ n) (cc : CokernelCofork (S.map' k (k + 1))) - (kf : KernelFork (S.map' (k + 2) (k + 3))) - (hcc : IsColimit cc) (hkf : IsLimit kf) : - cc.pt ⟶ kf.pt := - IsColimit.desc hcc - (CokernelCofork.ofπ (π := IsLimit.lift hkf (KernelFork.ofι _ (hS.zero (k + 1)))) - (Fork.IsLimit.hom_ext hkf (by simpa using hS.zero k))) + (kf : KernelFork (S.map' (k + 2) (k + 3))) (hcc : IsColimit cc) (hkf : IsLimit kf) : + cc.pt ⟶ kf.pt := + IsColimit.desc hcc (CokernelCofork.ofπ _ + (show S.map' k (k + 1) ≫ IsLimit.lift hkf (KernelFork.ofι _ (hS.zero (k + 1))) = _ from + Fork.IsLimit.hom_ext hkf (by simpa using hS.zero k))) @[reassoc (attr := simp)] lemma cokerToKer'_fac (hk : k ≤ n) (cc : CokernelCofork (S.map' k (k + 1))) - (kf : KernelFork (S.map' (k + 2) (k + 3))) - (hcc : IsColimit cc) (hkf : IsLimit kf) : + (kf : KernelFork (S.map' (k + 2) (k + 3))) (hcc : IsColimit cc) (hkf : IsLimit kf) : cc.π ≫ hS.cokerToKer' k hk cc kf hcc hkf ≫ kf.ι = S.map' (k + 1) (k + 2) := by simp [cokerToKer'] -/-- If `S : ComposableArrows C (n + 3)` and `k : ℕ` satisfies `k ≤ n`, this is the induced -map from the cokernel of `S.map' k (k + 1)` to the kernel of `S.map' (k + 2) (k + 3)`. -/ -noncomputable def cokerToKer (hk : k ≤ n) - [HasCokernel (S.map' k (k + 1))] [HasKernel (S.map' (k + 2) (k + 3))] : - cokernel (S.map' k (k + 1) _ _) ⟶ kernel (S.map' (k + 2) (k + 3) _ _) := +end + +section + +/-- If `S` is a complex, this is the morphism from the cokernel of `S.map' k (k + 1)` +to the kernel of `S.map' (k + 2) (k + 3)`. -/ +noncomputable def cokerToKer (hk : k ≤ n := by lia) + [HasCokernel (S.map' k (k + 1))] [HasKernel (S.map' (k + 2) (k + 3))] : + cokernel (S.map' k (k + 1)) ⟶ kernel (S.map' (k + 2) (k + 3)) := hS.cokerToKer' k hk (CokernelCofork.ofπ _ (cokernel.condition _)) (KernelFork.ofι _ (kernel.condition _)) (cokernelIsCokernel _) (kernelIsKernel _) @[reassoc (attr := simp)] -lemma cokerToKer_fac (hk : k ≤ n) - [HasCokernel (S.map' k (k + 1))] [HasKernel (S.map' (k + 2) (k + 3))] : - cokernel.π _ ≫ hS.cokerToKer k hk ≫ kernel.ι _ = S.map' (k + 1) (k + 2) := +lemma cokerToKer_fac (hk : k ≤ n := by lia) + [HasCokernel (S.map' k (k + 1))] [HasKernel (S.map' (k + 2) (k + 3))] : + cokernel.π _ ≫ hS.cokerToKer k hk ≫ kernel.ι _ = S.map' (k + 1) (k + 2) := hS.cokerToKer'_fac k hk _ _ (cokernelIsCokernel _) (kernelIsKernel _) +end + +section + +/-- If `S` is a complex, this is the morphism from the opcycles of `S` in +degree `k + 1` to the cycles of `S` in degree `k + 2`. -/ +noncomputable def opcyclesToCycles (hk : k ≤ n := by lia) + [(S.sc hS k).HasRightHomology] [(S.sc hS (k + 1)).HasLeftHomology] : + (S.sc hS k _).opcycles ⟶ (S.sc hS (k + 1) _).cycles := + hS.cokerToKer' k hk _ _ (S.sc hS k _).opcyclesIsCokernel + (S.sc hS (k + 1) _).cyclesIsKernel + +@[reassoc (attr := simp)] +lemma opcyclesToCycles_fac (hk : k ≤ n := by lia) + [(S.sc hS k).HasRightHomology] [(S.sc hS (k + 1)).HasLeftHomology] : + (S.sc hS k _).pOpcycles ≫ hS.opcyclesToCycles k ≫ (S.sc hS (k + 1) _).iCycles = + S.map' (k + 1) (k + 2) := + hS.cokerToKer'_fac k hk _ _ (S.sc hS k _).opcyclesIsCokernel + (S.sc hS (k + 1) _).cyclesIsKernel + +end + end IsComplex end HasZeroMorphisms +section Preadditive + +variable {C : Type*} [Category C] [Preadditive C] {n : ℕ} {S : ComposableArrows C (n + 3)} + +namespace IsComplex + +variable (hS : S.IsComplex) (k : ℕ) (hk : k ≤ n) + (cc : CokernelCofork (S.map' k (k + 1))) (kf : KernelFork (S.map' (k + 2) (k + 3))) + (hcc : IsColimit cc) (hkf : IsLimit kf) + +lemma epi_cokerToKer' (hS' : (S.sc hS (k + 1)).Exact) : + Epi (hS.cokerToKer' k hk cc kf hcc hkf) := by + have := hS'.hasZeroObject + have := hS'.hasHomology + have : Epi cc.π := ⟨fun _ _ => Cofork.IsColimit.hom_ext hcc⟩ + let h := hS'.leftHomologyDataOfIsLimitKernelFork kf hkf + have := h.exact_iff_epi_f'.1 hS' + have fac : cc.π ≫ hS.cokerToKer' k hk cc kf hcc hkf = h.f' := by + rw [← cancel_mono h.i, h.f'_i, ShortComplex.Exact.leftHomologyDataOfIsLimitKernelFork_i, + assoc, IsComplex.cokerToKer'_fac] + exact epi_of_epi_fac fac + +lemma mono_cokerToKer' (hS' : (S.sc hS k).Exact) : + Mono (hS.cokerToKer' k hk cc kf hcc hkf) := by + have := hS'.hasZeroObject + have := hS'.hasHomology + have : Mono kf.ι := ⟨fun _ _ => Fork.IsLimit.hom_ext hkf⟩ + let h := hS'.rightHomologyDataOfIsColimitCokernelCofork cc hcc + have := h.exact_iff_mono_g'.1 hS' + have fac : hS.cokerToKer' k hk cc kf hcc hkf ≫ kf.ι = h.g' := by + rw [← cancel_epi h.p, h.p_g', ShortComplex.Exact.rightHomologyDataOfIsColimitCokernelCofork_p, + cokerToKer'_fac] + exact mono_of_mono_fac fac + +end IsComplex + +end Preadditive + +section Balanced + +variable {C : Type*} [Category C] [Preadditive C] [Balanced C] {n : ℕ} + {S : ComposableArrows C (n + 3)} (hS : S.Exact) + +namespace Exact + +section + +variable (k : ℕ) (hk : k ≤ n) + (cc : CokernelCofork (S.map' k (k + 1))) (kf : KernelFork (S.map' (k + 2) (k + 3))) + (hcc : IsColimit cc) (hkf : IsLimit kf) + +/-- If `S` is an exact sequence, this is the morphism from a cokernel +of `S.map' k (k + 1)` to a kernel of `S.map' (k + 2) (k + 3)`. -/ +abbrev cokerToKer' : cc.pt ⟶ kf.pt := + hS.toIsComplex.cokerToKer' k hk cc kf hcc hkf + +instance isIso_cokerToKer' : IsIso (hS.cokerToKer' k hk cc kf hcc hkf) := by + have : Mono (hS.cokerToKer' k hk cc kf hcc hkf) := + hS.toIsComplex.mono_cokerToKer' k hk cc kf hcc hkf + (hS.exact k) + have : Epi (hS.cokerToKer' k hk cc kf hcc hkf) := + hS.epi_cokerToKer' k hk cc kf hcc hkf (hS.exact (k + 1)) + apply isIso_of_mono_of_epi + +/-- If `S` is an exact sequence, this is the isomorphism from a cokernel +of `S.map' k (k + 1)` to a kernel of `S.map' (k + 2) (k + 3)`. -/ +@[simps! hom] +noncomputable def cokerIsoKer' : cc.pt ≅ kf.pt := + asIso (hS.cokerToKer' k hk cc kf hcc hkf) + +@[reassoc (attr := simp)] +lemma cokerIsoKer'_hom_inv_id : + hS.cokerToKer' k hk cc kf hcc hkf ≫ (hS.cokerIsoKer' k hk cc kf hcc hkf).inv = 𝟙 _ := + (hS.cokerIsoKer' k hk cc kf hcc hkf).hom_inv_id + +@[reassoc (attr := simp)] +lemma cokerIsoKer'_inv_hom_id : + (hS.cokerIsoKer' k hk cc kf hcc hkf).inv ≫ hS.cokerToKer' k hk cc kf hcc hkf = 𝟙 _ := + (hS.cokerIsoKer' k hk cc kf hcc hkf).inv_hom_id + +end + +section + +/-- If `S` is an exact sequence, this is the isomorphism from the cokernel +of `S.map' k (k + 1)` to the kernel of `S.map' (k + 2) (k + 3)`. -/ +noncomputable def cokerIsoKer (k : ℕ) (hk : k ≤ n := by lia) + [HasCokernel (S.map' k (k + 1))] [HasKernel (S.map' (k + 2) (k + 3))] : + cokernel (S.map' k (k + 1) _ _) ≅ kernel (S.map' (k + 2) (k + 3) _ _) := + hS.cokerIsoKer' k hk (CokernelCofork.ofπ _ (cokernel.condition _)) + (KernelFork.ofι _ (kernel.condition _)) (cokernelIsCokernel _) (kernelIsKernel _) + +@[reassoc (attr := simp)] +lemma cokerIsoKer_hom_fac (k : ℕ) (hk : k ≤ n := by lia) + [HasCokernel (S.map' k (k + 1))] [HasKernel (S.map' (k + 2) (k + 3))] : + cokernel.π _ ≫ (hS.cokerIsoKer k).hom ≫ kernel.ι _ = S.map' (k + 1) (k + 2) := + hS.toIsComplex.cokerToKer_fac k + +end + +section + +/-- If `S` is an exact sequence, this is the isomorphism from the opcycles of `S` in +degree `k + 1` to the cycles of `S` in degree `k + 2`. -/ +noncomputable def opcyclesIsoCycles (k : ℕ) (hk : k ≤ n := by lia) + [h₁ : (hS.sc k).HasRightHomology] [h₂ : (hS.sc (k + 1)).HasLeftHomology] : + (hS.sc k _).opcycles ≅ (hS.sc (k + 1) _).cycles := + hS.cokerIsoKer' k hk _ _ (hS.sc k _).opcyclesIsCokernel (hS.sc (k + 1) _).cyclesIsKernel + +@[reassoc (attr := simp)] +lemma opcyclesIsoCycles_hom_fac (k : ℕ) (hk : k ≤ n := by lia) + [h₁ : (hS.sc k).HasRightHomology] [h₂ : (hS.sc (k + 1)).HasLeftHomology] : + (hS.sc k _).pOpcycles ≫ (hS.opcyclesIsoCycles k).hom ≫ (hS.sc (k + 1) _).iCycles = + S.map' (k + 1) (k + 2) := + hS.toIsComplex.opcyclesToCycles_fac k hk + +end + +end Exact + +end Balanced + end ComposableArrows end CategoryTheory From fcbef20f459024e6711edb6e5f5fb4031a17911a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=ABl=20Riou?= Date: Thu, 22 Jan 2026 19:18:19 +0100 Subject: [PATCH 4/4] added condition on the category --- Mathlib/Algebra/Homology/ExactSequenceFour.lean | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/Mathlib/Algebra/Homology/ExactSequenceFour.lean b/Mathlib/Algebra/Homology/ExactSequenceFour.lean index 442ebdf4d549f6..85b4eabe864d70 100644 --- a/Mathlib/Algebra/Homology/ExactSequenceFour.lean +++ b/Mathlib/Algebra/Homology/ExactSequenceFour.lean @@ -13,7 +13,9 @@ public import Mathlib.Algebra.Homology.ExactSequence The main definition in this file is `ComposableArrows.Exact.cokerIsoKer`: given an exact sequence `S` (involving at least four objects), this is the isomorphism from the cokernel of `S.map' k (k + 1)` -to the kernel of `S.map' (k + 2) (k + 3)`. +to the kernel of `S.map' (k + 2) (k + 3)`. This is intended +to be used for exact sequences in abelian categories, but the +construction works for preadditive balanced categories. -/