Kernel–cokernel pairs

A kernel–cokernel pair in a category with zero morphisms is a pair of composable morphisms X ⟶ Y ⟶ Z with zero composite in which the first morphism is a kernel of the second and the second is a cokernel of the first. Following Bühler, the first morphism of such a pair is called its inflation and the second its deflation. Quillen exact structures are, by definition, isomorphism-closed classes of such pairs, so this file supplies the objects an ExactStructure will range over, together with the calculus those axioms are stated in.

The point of the notion is that it makes sense in an arbitrary additive category: neither kernels nor cokernels are assumed to exist, so the two universal properties are asserted explicitly rather than read off from ambient (co)completeness. In a balanced preadditive category with homology the notion coincides with Mathlib's CategoryTheory.ShortComplex.ShortExact; that comparison is TauCeti.isKernelCokernelPair_iff_shortExact.

Main definitions

• TauCeti.IsKernelCokernelPair: the predicate on a CategoryTheory.ShortComplex saying that its two morphisms form a kernel–cokernel pair. Its noncomputable accessors TauCeti.IsKernelCokernelPair.fIsKernel and TauCeti.IsKernelCokernelPair.gIsCokernel produce the two universal properties.
• TauCeti.IsKernelCokernelPair.lift and TauCeti.IsKernelCokernelPair.desc: the two factorizations, with their defining equations and their uniqueness.
• TauCeti.IsKernelCokernelPair.splittingOfSection: the splitting of a kernel–cokernel pair determined by a section of its deflation.

Main results

• TauCeti.IsKernelCokernelPair.of_iso and TauCeti.isKernelCokernelPair_iff_of_iso: the class of kernel–cokernel pairs is closed under isomorphism of short complexes, as an exact structure requires.
• TauCeti.IsKernelCokernelPair.map: a functor preserving the two relevant (co)limits carries kernel–cokernel pairs to kernel–cokernel pairs, and TauCeti.IsKernelCokernelPair.of_map: a fully faithful functor reflects them.
• TauCeti.IsKernelCokernelPair.op, TauCeti.isKernelCokernelPair_op_iff and TauCeti.isKernelCokernelPair_unop_iff: the notion is self-dual, which is what makes the Bühler axioms transport to the opposite category.
• TauCeti.IsKernelCokernelPair.of_isIso_f_of_isZero and TauCeti.IsKernelCokernelPair.of_isIso_g_of_isZero: an isomorphism is both an inflation and a deflation.
• TauCeti.IsKernelCokernelPair.of_splitting and TauCeti.IsKernelCokernelPair.of_hasBinaryBiproduct: split short complexes, in particular X₁ ⟶ X₁ ⊞ X₂ ⟶ X₂, are kernel–cokernel pairs. These are the conflations of the split exact structure.
• TauCeti.IsKernelCokernelPair.biprod: a direct sum of kernel–cokernel pairs is a kernel–cokernel pair.
• TauCeti.isKernelCokernelPair_iff_shortExact: in a balanced preadditive category the kernel–cokernel pairs among the short complexes with homology are exactly the short exact ones. These are the conflations of the canonical exact structure on an abelian category.

Implementation notes

IsKernelCokernelPair is a Prop whose fields are Nonempty universal properties, following CategoryTheory.IsPushout. A class of conflations must be a class in the set-theoretic sense, so membership has to be a proposition; the universal properties are recovered by choice, which is harmless because CategoryTheory.Limits.IsLimit is a subsingleton.

of_isIso_f_of_isZero and of_isIso_g_of_isZero are proved directly rather than deduced from CategoryTheory.ShortComplex.Splitting.ofIsIsoOfIsZero and its sibling together with of_splitting, which would need a preadditive category with a zero object. The direct proofs are no longer, and they keep these two statements — Bühler's axiom E0, that an isomorphism is both an inflation and a deflation — in the same bare CategoryTheory.Limits.HasZeroMorphisms generality as the rest of the core API. For the same reason of_hasBinaryBiproduct and biprod are stated for a bare CategoryTheory.Limits.HasZeroMorphisms category with the biproducts they mention: Mathlib's CategoryTheory.Limits.biprod.isKernelSndKernelFork and its siblings already provide the witnesses there, so routing through of_splitting would gratuitously assume a preadditive category with a zero object.

References

• Theo Bühler, Exact categories, Expositiones Mathematicae 28 (2010), 1–69, https://arxiv.org/abs/0811.1480. Definition 2.1 and Remarks 2.2–2.8 fix the notion of a kernel–cokernel pair and the axioms an exact structure imposes on a class of them.

structure TauCeti.IsKernelCokernelPair {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) : Prop

A short complex S : X₁ ⟶ X₂ ⟶ X₃ is a kernel–cokernel pair when S.f is a kernel of S.g and S.g is a cokernel of S.f. This is Bühler's notion of a kernel–cokernel pair; the conflations of a Quillen exact structure are an isomorphism-closed class of these.

• nonempty_fIsKernel : Nonempty (CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.KernelFork.ofι S.f ⋯))

  S.f is a kernel of S.g.

• nonempty_gIsCokernel : Nonempty (CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ S.g ⋯))

  S.g is a cokernel of S.f.

noncomputable def TauCeti.IsKernelCokernelPair.fIsKernel {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S : CategoryTheory.ShortComplex C} (h : IsKernelCokernelPair S) : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.KernelFork.ofι S.f ⋯)

The universal property exhibiting S.f as a kernel of S.g.

Equations

• h.fIsKernel = ⋯.some

noncomputable def TauCeti.IsKernelCokernelPair.gIsCokernel {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S : CategoryTheory.ShortComplex C} (h : IsKernelCokernelPair S) : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ S.g ⋯)

The universal property exhibiting S.g as a cokernel of S.f.

Equations

• h.gIsCokernel = ⋯.some

theorem TauCeti.IsKernelCokernelPair.mono_f {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S : CategoryTheory.ShortComplex C} (h : IsKernelCokernelPair S) : CategoryTheory.Mono S.f

The inflation of a kernel–cokernel pair is a monomorphism.

theorem TauCeti.IsKernelCokernelPair.epi_g {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S : CategoryTheory.ShortComplex C} (h : IsKernelCokernelPair S) : CategoryTheory.Epi S.g

The deflation of a kernel–cokernel pair is an epimorphism.

noncomputable def TauCeti.IsKernelCokernelPair.lift {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S : CategoryTheory.ShortComplex C} {A : C} (h : IsKernelCokernelPair S) (k : A ⟶ S.X₂) (hk : CategoryTheory.CategoryStruct.comp k S.g = 0) : A ⟶ S.X₁

The factorization through the kernel S.f of a morphism into S.X₂ killed by S.g.

Equations

• h.lift k hk = ↑(CategoryTheory.Limits.KernelFork.IsLimit.lift' h.fIsKernel k hk)

@[simp]

theorem TauCeti.IsKernelCokernelPair.lift_f {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S : CategoryTheory.ShortComplex C} {A : C} (h : IsKernelCokernelPair S) (k : A ⟶ S.X₂) (hk : CategoryTheory.CategoryStruct.comp k S.g = 0) : CategoryTheory.CategoryStruct.comp (h.lift k hk) S.f = k

The kernel factorization lift satisfies lift ≫ S.f = k.

@[simp]

theorem TauCeti.IsKernelCokernelPair.lift_f_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S : CategoryTheory.ShortComplex C} {A : C} (h : IsKernelCokernelPair S) (k : A ⟶ S.X₂) (hk : CategoryTheory.CategoryStruct.comp k S.g = 0) {Z : C} (h✝ : S.X₂ ⟶ Z) : CategoryTheory.CategoryStruct.comp (h.lift k hk) (CategoryTheory.CategoryStruct.comp S.f h✝) = CategoryTheory.CategoryStruct.comp k h✝

The kernel factorization lift satisfies lift ≫ S.f = k.

theorem TauCeti.IsKernelCokernelPair.eq_lift {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S : CategoryTheory.ShortComplex C} {A : C} (h : IsKernelCokernelPair S) (k : A ⟶ S.X₂) (hk : CategoryTheory.CategoryStruct.comp k S.g = 0) (l : A ⟶ S.X₁) (hl : CategoryTheory.CategoryStruct.comp l S.f = k) : l = h.lift k hk

IsKernelCokernelPair.lift is the unique factorization through S.f.

noncomputable def TauCeti.IsKernelCokernelPair.desc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S : CategoryTheory.ShortComplex C} {A : C} (h : IsKernelCokernelPair S) (k : S.X₂ ⟶ A) (hk : CategoryTheory.CategoryStruct.comp S.f k = 0) : S.X₃ ⟶ A

The factorization through the cokernel S.g of a morphism out of S.X₂ killed by S.f.

Equations

• h.desc k hk = ↑(CategoryTheory.Limits.CokernelCofork.IsColimit.desc' h.gIsCokernel k hk)

@[simp]

theorem TauCeti.IsKernelCokernelPair.g_desc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S : CategoryTheory.ShortComplex C} {A : C} (h : IsKernelCokernelPair S) (k : S.X₂ ⟶ A) (hk : CategoryTheory.CategoryStruct.comp S.f k = 0) : CategoryTheory.CategoryStruct.comp S.g (h.desc k hk) = k

The cokernel factorization desc satisfies S.g ≫ desc = k.

@[simp]

theorem TauCeti.IsKernelCokernelPair.g_desc_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S : CategoryTheory.ShortComplex C} {A : C} (h : IsKernelCokernelPair S) (k : S.X₂ ⟶ A) (hk : CategoryTheory.CategoryStruct.comp S.f k = 0) {Z : C} (h✝ : A ⟶ Z) : CategoryTheory.CategoryStruct.comp S.g (CategoryTheory.CategoryStruct.comp (h.desc k hk) h✝) = CategoryTheory.CategoryStruct.comp k h✝

The cokernel factorization desc satisfies S.g ≫ desc = k.

theorem TauCeti.IsKernelCokernelPair.eq_desc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S : CategoryTheory.ShortComplex C} {A : C} (h : IsKernelCokernelPair S) (k : S.X₂ ⟶ A) (hk : CategoryTheory.CategoryStruct.comp S.f k = 0) (l : S.X₃ ⟶ A) (hl : CategoryTheory.CategoryStruct.comp S.g l = k) : l = h.desc k hk

IsKernelCokernelPair.desc is the unique factorization through S.g.

theorem TauCeti.IsKernelCokernelPair.of_iso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ S₂ : CategoryTheory.ShortComplex C} (h : IsKernelCokernelPair S₁) (e : S₁ ≅ S₂) : IsKernelCokernelPair S₂

Being a kernel–cokernel pair is invariant under isomorphism of short complexes; this is the closure property an exact structure demands of its class of conflations.

theorem TauCeti.IsKernelCokernelPair.map {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S : CategoryTheory.ShortComplex C} {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Limits.HasZeroMorphisms D] (h : IsKernelCokernelPair S) (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair S.g 0) F] [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair S.f 0) F] : IsKernelCokernelPair (S.map F)

A functor preserving zero morphisms and the two relevant (co)limits — for instance an equivalence, or an exact functor between abelian categories — carries kernel–cokernel pairs to kernel–cokernel pairs.

theorem TauCeti.IsKernelCokernelPair.of_map {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S : CategoryTheory.ShortComplex C} {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Limits.HasZeroMorphisms D] (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] [F.Full] [F.Faithful] (h : IsKernelCokernelPair (S.map F)) : IsKernelCokernelPair S

A fully faithful functor preserving zero morphisms reflects kernel–cokernel pairs. This is what makes a full subcategory inherit the kernel–cokernel pairs of its ambient category: the universal properties only have to be tested against objects of the subcategory.

theorem TauCeti.IsKernelCokernelPair.of_isIso_f_of_isZero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) [CategoryTheory.IsIso S.f] (h₃ : CategoryTheory.Limits.IsZero S.X₃) : IsKernelCokernelPair S

A short complex whose first morphism is an isomorphism and whose last object is zero is a kernel–cokernel pair: an isomorphism is an inflation.

theorem TauCeti.IsKernelCokernelPair.of_isIso_g_of_isZero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) [CategoryTheory.IsIso S.g] (h₁ : CategoryTheory.Limits.IsZero S.X₁) : IsKernelCokernelPair S

A short complex whose second morphism is an isomorphism and whose first object is zero is a kernel–cokernel pair: an isomorphism is a deflation.

theorem TauCeti.IsKernelCokernelPair.op {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S : CategoryTheory.ShortComplex C} (h : IsKernelCokernelPair S) : IsKernelCokernelPair S.op

The opposite of a kernel–cokernel pair is a kernel–cokernel pair.

theorem TauCeti.IsKernelCokernelPair.unop {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S : CategoryTheory.ShortComplex Cᵒᵖ} (h : IsKernelCokernelPair S) : IsKernelCokernelPair S.unop

The un-opposite of a kernel–cokernel pair is a kernel–cokernel pair.

theorem TauCeti.IsKernelCokernelPair.of_hasBinaryBiproduct {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (X₁ X₂ : C) [CategoryTheory.Limits.HasBinaryBiproduct X₁ X₂] : IsKernelCokernelPair { X₁ := X₁, X₂ := X₁ ⊞ X₂, X₃ := X₂, f := CategoryTheory.Limits.biprod.inl, g := CategoryTheory.Limits.biprod.snd, zero := ⋯ }

The biproduct short complex X₁ ⟶ X₁ ⊞ X₂ ⟶ X₂ is a kernel–cokernel pair.

theorem TauCeti.IsKernelCokernelPair.biprod {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ S₂ : CategoryTheory.ShortComplex C} [CategoryTheory.Limits.HasBinaryBiproduct S₁.X₁ S₂.X₁] [CategoryTheory.Limits.HasBinaryBiproduct S₁.X₂ S₂.X₂] [CategoryTheory.Limits.HasBinaryBiproduct S₁.X₃ S₂.X₃] (h₁ : IsKernelCokernelPair S₁) (h₂ : IsKernelCokernelPair S₂) : IsKernelCokernelPair (shortComplexBiprod S₁ S₂)

A direct sum of two kernel–cokernel pairs is a kernel–cokernel pair.

theorem TauCeti.isKernelCokernelPair_iff_of_iso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ S₂ : CategoryTheory.ShortComplex C} (e : S₁ ≅ S₂) : IsKernelCokernelPair S₁ ↔ IsKernelCokernelPair S₂

Being a kernel–cokernel pair only depends on the isomorphism class of a short complex.

@[simp]

theorem TauCeti.isKernelCokernelPair_op_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S : CategoryTheory.ShortComplex C} : IsKernelCokernelPair S.op ↔ IsKernelCokernelPair S

A short complex is a kernel–cokernel pair if and only if its opposite is; the notion is self-dual.

@[simp]

theorem TauCeti.isKernelCokernelPair_unop_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S : CategoryTheory.ShortComplex Cᵒᵖ} : IsKernelCokernelPair S.unop ↔ IsKernelCokernelPair S

A short complex in Cᵒᵖ is a kernel–cokernel pair if and only if its un-opposite is; the notion is self-dual.

theorem TauCeti.IsKernelCokernelPair.of_splitting {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {S : CategoryTheory.ShortComplex C} (s : S.Splitting) : IsKernelCokernelPair S

A split short complex is a kernel–cokernel pair. These are the conflations of the split exact structure on an additive category.

noncomputable def TauCeti.IsKernelCokernelPair.splittingOfSection {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {S : CategoryTheory.ShortComplex C} (h : IsKernelCokernelPair S) (s : S.X₃ ⟶ S.X₂) (hs : CategoryTheory.CategoryStruct.comp s S.g = CategoryTheory.CategoryStruct.id S.X₃) : S.Splitting

A kernel–cokernel pair whose deflation admits a section is split. The retraction is the factorization of 𝟙 - S.g ≫ s through the kernel S.f.

Mathlib's CategoryTheory.ShortComplex.Splitting.ofExactOfSection proves this for an exact short complex in a balanced category; here the kernel–cokernel hypothesis replaces balancedness, so the statement applies inside an arbitrary additive category carrying an exact structure.

Equations

• h.splittingOfSection s hs = { r := h.lift (CategoryTheory.CategoryStruct.id S.X₂ - CategoryTheory.CategoryStruct.comp S.g s) ⋯, s := s, f_r := ⋯, s_g := hs, id := ⋯ }

@[simp]

theorem TauCeti.IsKernelCokernelPair.splittingOfSection_s {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {S : CategoryTheory.ShortComplex C} (h : IsKernelCokernelPair S) (s : S.X₃ ⟶ S.X₂) (hs : CategoryTheory.CategoryStruct.comp s S.g = CategoryTheory.CategoryStruct.id S.X₃) : (h.splittingOfSection s hs).s = s

@[simp]

theorem TauCeti.IsKernelCokernelPair.splittingOfSection_r {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {S : CategoryTheory.ShortComplex C} (h : IsKernelCokernelPair S) (s : S.X₃ ⟶ S.X₂) (hs : CategoryTheory.CategoryStruct.comp s S.g = CategoryTheory.CategoryStruct.id S.X₃) : (h.splittingOfSection s hs).r = h.lift (CategoryTheory.CategoryStruct.id S.X₂ - CategoryTheory.CategoryStruct.comp S.g s) ⋯

theorem TauCeti.IsKernelCokernelPair.shortExact {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {S : CategoryTheory.ShortComplex C} [S.HasHomology] (h : IsKernelCokernelPair S) : S.ShortExact

A kernel–cokernel pair with homology is a short exact short complex.

theorem TauCeti.IsKernelCokernelPair.of_shortExact {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {S : CategoryTheory.ShortComplex C} [CategoryTheory.Balanced C] (h : S.ShortExact) : IsKernelCokernelPair S

In a balanced preadditive category, a short exact short complex is a kernel–cokernel pair.

theorem TauCeti.isKernelCokernelPair_iff_shortExact {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Balanced C] (S : CategoryTheory.ShortComplex C) [S.HasHomology] : IsKernelCokernelPair S ↔ S.ShortExact

In a balanced preadditive category the kernel–cokernel pairs among the short complexes with homology are exactly the short exact ones. This identifies the conflations of the canonical exact structure of an abelian category with Mathlib's CategoryTheory.ShortComplex.ShortExact.