Exact structures

An exact structure on an additive category is an isomorphism-closed class of kernel--cokernel pairs satisfying Quillen's axioms. This file packages those axioms in their self-dual E0/E1/E2 form. In particular, the E2 axioms return actual pushout and pullback squares; they do not assume that the ambient category has arbitrary pushouts or pullbacks.

The distinguished short complexes are called conflations. Their first maps are inflations, and their second maps are deflations. The structures here contain only this intrinsic data and the six Quillen axioms. The split and canonical abelian exact structures are constructed separately.

Main definitions

• TauCeti.ConflationClass is an isomorphism-closed class of kernel--cokernel pairs.
• TauCeti.ConflationClass.inflations and TauCeti.ConflationClass.deflations are the CategoryTheory.MorphismProperty of morphisms occurring as the first, resp. second, map of a conflation. TauCeti.ConflationClass.IsInflation and TauCeti.ConflationClass.IsDeflation are the corresponding predicates on a single morphism.
• TauCeti.ExactStructure equips a conflation class with E0/E0op, E1/E1op, and E2/E2op.

Implementation notes

The conflations are a CategoryTheory.ObjectProperty (CategoryTheory.ShortComplex C) closed under isomorphisms in Mathlib's sense, and the inflations and the deflations are each a CategoryTheory.MorphismProperty, so that the generic API applies: isomorphism-closure of the conflations makes the inflations and the deflations CategoryTheory.MorphismProperty.RespectsIso, and E0/E0op and E1/E1op are recorded as CategoryTheory.MorphismProperty.ContainsIdentities and CategoryTheory.MorphismProperty.IsStableUnderComposition instances. E2/E2op are recorded by the corresponding property-specific HasPushouts/HasPullbacks and IsStableUnderCobaseChange/IsStableUnderBaseChange classes. These assert existence only for pushouts of inflations and pullbacks of deflations, without requiring arbitrary pushouts or pullbacks in the ambient category.

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 give the axioms used here.
• TauCetiRoadmap/GrothendieckEulerForms/Suggested.lean, the human-authored roadmap formalization, fixes the design followed here: the ConflationClass/ExactStructure split, the E0/E0op, E1/E1op, E2/E2op fields, and the derived inflation and deflation predicates are its. This file replaces its bespoke PushoutWitness and PullbackWitness by Mathlib's property-specific pushout and pullback classes, and its pair of composable morphisms by a CategoryTheory.ShortComplex.

structure TauCeti.ConflationClass (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] : Type (max u v)

An isomorphism-closed class of kernel--cokernel pairs in a preadditive category.

This is the relation underlying an exact structure, before imposing the Quillen axioms.

• Conflation : CategoryTheory.ObjectProperty (CategoryTheory.ShortComplex C)

  The distinguished short complexes.

• isKernelCokernelPair (S : CategoryTheory.ShortComplex C) : self.Conflation S → IsKernelCokernelPair S

  Every conflation is a kernel--cokernel pair.

• isClosedUnderIsomorphisms : self.Conflation.IsClosedUnderIsomorphisms

  The class of conflations is closed under isomorphisms of short complexes.

theorem TauCeti.ConflationClass.ext {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (E F : ConflationClass C) (h : ∀ (S : CategoryTheory.ShortComplex C), E.Conflation S ↔ F.Conflation S) : E = F

Two conflation classes are equal when they distinguish the same short complexes.

theorem TauCeti.ConflationClass.ext_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {E F : ConflationClass C} : E = F ↔ ∀ (S : CategoryTheory.ShortComplex C), E.Conflation S ↔ F.Conflation S

def TauCeti.ConflationClass.inflations {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (E : ConflationClass C) : CategoryTheory.MorphismProperty C

The inflations: the morphisms occurring as the first map of a conflation.

Equations

• E.inflations i = ∃ (Z : C) (p : Y ⟶ Z) (zero : CategoryTheory.CategoryStruct.comp i p = 0), E.Conflation { X₁ := x✝, X₂ := Y, X₃ := Z, f := i, g := p, zero := zero }

def TauCeti.ConflationClass.deflations {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (E : ConflationClass C) : CategoryTheory.MorphismProperty C

The deflations: the morphisms occurring as the second map of a conflation.

Equations

• E.deflations p = ∃ (X : C) (i : X ⟶ Y) (zero : CategoryTheory.CategoryStruct.comp i p = 0), E.Conflation { X₁ := X, X₂ := Y, X₃ := x✝, f := i, g := p, zero := zero }

@[reducible, inline]

abbrev TauCeti.ConflationClass.IsInflation {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (E : ConflationClass C) {X Y : C} (i : X ⟶ Y) : Prop

A morphism is an inflation when it is the first map of a conflation.

Equations

• E.IsInflation i = E.inflations i

@[reducible, inline]

abbrev TauCeti.ConflationClass.IsDeflation {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (E : ConflationClass C) {Y Z : C} (p : Y ⟶ Z) : Prop

A morphism is a deflation when it is the second map of a conflation.

Equations

• E.IsDeflation p = E.deflations p

theorem TauCeti.ConflationClass.isInflation_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (E : ConflationClass C) {X Y : C} (i : X ⟶ Y) : E.IsInflation i ↔ ∃ (Z : C) (p : Y ⟶ Z) (zero : CategoryTheory.CategoryStruct.comp i p = 0), E.Conflation { X₁ := X, X₂ := Y, X₃ := Z, f := i, g := p, zero := zero }

A morphism is an inflation exactly when it is the first map of a conflation.

theorem TauCeti.ConflationClass.isDeflation_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (E : ConflationClass C) {Y Z : C} (p : Y ⟶ Z) : E.IsDeflation p ↔ ∃ (X : C) (i : X ⟶ Y) (zero : CategoryTheory.CategoryStruct.comp i p = 0), E.Conflation { X₁ := X, X₂ := Y, X₃ := Z, f := i, g := p, zero := zero }

A morphism is a deflation exactly when it is the second map of a conflation.

theorem TauCeti.ConflationClass.isInflation_f {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (E : ConflationClass C) {S : CategoryTheory.ShortComplex C} (hS : E.Conflation S) : E.IsInflation S.f

A conflation's first map is an inflation.

theorem TauCeti.ConflationClass.isDeflation_g {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (E : ConflationClass C) {S : CategoryTheory.ShortComplex C} (hS : E.Conflation S) : E.IsDeflation S.g

A conflation's second map is a deflation.

theorem TauCeti.ConflationClass.IsInflation.mono {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {E : ConflationClass C} {X Y : C} {i : X ⟶ Y} (hi : E.IsInflation i) : CategoryTheory.Mono i

Every inflation is a monomorphism.

theorem TauCeti.ConflationClass.IsDeflation.epi {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {E : ConflationClass C} {Y Z : C} {p : Y ⟶ Z} (hp : E.IsDeflation p) : CategoryTheory.Epi p

Every deflation is an epimorphism.

theorem TauCeti.ConflationClass.conflation_of_iso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (E : ConflationClass C) {S T : CategoryTheory.ShortComplex C} (e : S ≅ T) (hS : E.Conflation S) : E.Conflation T

An isomorphism of short complexes transports the property of being a conflation.

theorem TauCeti.ConflationClass.conflation_iff_of_iso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (E : ConflationClass C) {S T : CategoryTheory.ShortComplex C} (e : S ≅ T) : E.Conflation S ↔ E.Conflation T

Isomorphic short complexes are conflations together.

theorem TauCeti.ConflationClass.conflation_of_isColimit_of_isInflation {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (E : ConflationClass C) {S : CategoryTheory.ShortComplex C} (hS : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ S.g ⋯)) (hf : E.IsInflation S.f) : E.Conflation S

A short complex whose first map is an inflation and whose second map is a cokernel of the first is a conflation: the conflation witnessing the inflation has the same cokernel, so the two short complexes are isomorphic.

Only the cokernel half of TauCeti.IsKernelCokernelPair is needed, because the kernel half is then inherited from the witnessing conflation.

theorem TauCeti.ConflationClass.conflation_of_isLimit_of_isDeflation {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (E : ConflationClass C) {S : CategoryTheory.ShortComplex C} (hS : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.KernelFork.ofι S.f ⋯)) (hg : E.IsDeflation S.g) : E.Conflation S

A short complex whose second map is a deflation and whose first map is a kernel of the second is a conflation: the conflation witnessing the deflation has the same kernel, so the two short complexes are isomorphic.

theorem TauCeti.ConflationClass.conflation_of_isKernelCokernelPair_of_isInflation {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (E : ConflationClass C) {S : CategoryTheory.ShortComplex C} (hS : IsKernelCokernelPair S) (hf : E.IsInflation S.f) : E.Conflation S

A kernel–cokernel pair whose first map is an inflation is a conflation.

theorem TauCeti.ConflationClass.conflation_of_isKernelCokernelPair_of_isDeflation {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (E : ConflationClass C) {S : CategoryTheory.ShortComplex C} (hS : IsKernelCokernelPair S) (hg : E.IsDeflation S.g) : E.Conflation S

A kernel–cokernel pair whose second map is a deflation is a conflation.

instance TauCeti.ConflationClass.instRespectsIsoInflations {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (E : ConflationClass C) : E.inflations.RespectsIso

Being an inflation is invariant under composing with isomorphisms on either side: the witnessing conflation transports along the isomorphism.

instance TauCeti.ConflationClass.instRespectsIsoDeflations {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (E : ConflationClass C) : E.deflations.RespectsIso

Being a deflation is invariant under composing with isomorphisms on either side: the witnessing conflation transports along the isomorphism.

structure TauCeti.ExactStructure (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] extends TauCeti.ConflationClass C : Type (max u v)

A Quillen exact structure on an additive category, in the self-dual E0/E1/E2 presentation.

The E2 fields provide genuine universal squares through Mathlib's pushout and pullback APIs. No ambient pushouts or pullbacks are assumed.

• Conflation : CategoryTheory.ObjectProperty (CategoryTheory.ShortComplex C)
• isKernelCokernelPair (S : CategoryTheory.ShortComplex C) : self.Conflation S → IsKernelCokernelPair S
• isClosedUnderIsomorphisms : self.Conflation.IsClosedUnderIsomorphisms
• isInflation_id (X : C) : self.IsInflation (CategoryTheory.CategoryStruct.id X)

  E0: identity morphisms are inflations.

• isDeflation_id (X : C) : self.IsDeflation (CategoryTheory.CategoryStruct.id X)

  E0op: identity morphisms are deflations.

• isInflation_comp {X Y Z : C} (i : X ⟶ Y) (j : Y ⟶ Z) : self.IsInflation i → self.IsInflation j → self.IsInflation (CategoryTheory.CategoryStruct.comp i j)

  E1: a composite of inflations is an inflation.

• isDeflation_comp {X Y Z : C} (p : X ⟶ Y) (q : Y ⟶ Z) : self.IsDeflation p → self.IsDeflation q → self.IsDeflation (CategoryTheory.CategoryStruct.comp p q)

  E1op: a composite of deflations is a deflation.

• hasPushouts_inflations : self.inflations.HasPushouts

  E2 existence: pushouts of inflations along arbitrary morphisms exist.

• isStableUnderCobaseChange_inflations : self.inflations.IsStableUnderCobaseChange

  E2 stability: every cobase change of an inflation is an inflation.

• hasPullbacks_deflations : self.deflations.HasPullbacks

  E2op existence: pullbacks of deflations along arbitrary morphisms exist.

• isStableUnderBaseChange_deflations : self.deflations.IsStableUnderBaseChange

  E2op stability: every base change of a deflation is a deflation.

theorem TauCeti.ExactStructure.ext {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] (E F : ExactStructure C) (h : ∀ (S : CategoryTheory.ShortComplex C), E.Conflation S ↔ F.Conflation S) : E = F

Two exact structures are equal when they have the same conflations.

theorem TauCeti.ExactStructure.ext_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E F : ExactStructure C} : E = F ↔ ∀ (S : CategoryTheory.ShortComplex C), E.Conflation S ↔ F.Conflation S

@[reducible, inline]

abbrev TauCeti.ExactStructure.IsInflation {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] (E : ExactStructure C) {X Y : C} (i : X ⟶ Y) : Prop

The predicate that a morphism is the first map of a distinguished conflation.

Equations

• E.IsInflation i = E.IsInflation i

@[reducible, inline]

abbrev TauCeti.ExactStructure.IsDeflation {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] (E : ExactStructure C) {Y Z : C} (p : Y ⟶ Z) : Prop

The predicate that a morphism is the second map of a distinguished conflation.

Equations

• E.IsDeflation p = E.IsDeflation p

instance TauCeti.ExactStructure.instContainsIdentitiesInflations {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] (E : ExactStructure C) : E.inflations.ContainsIdentities

E0, as the statement that the inflations contain the identities.

instance TauCeti.ExactStructure.instContainsIdentitiesDeflations {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] (E : ExactStructure C) : E.deflations.ContainsIdentities

E0op, as the statement that the deflations contain the identities.

instance TauCeti.ExactStructure.instIsStableUnderCompositionInflations {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] (E : ExactStructure C) : E.inflations.IsStableUnderComposition

E1, as the statement that the inflations are stable under composition.

instance TauCeti.ExactStructure.instIsStableUnderCompositionDeflations {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] (E : ExactStructure C) : E.deflations.IsStableUnderComposition

E1op, as the statement that the deflations are stable under composition.

instance TauCeti.ExactStructure.instHasPushoutsInflations {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] (E : ExactStructure C) : E.inflations.HasPushouts

E2 existence, as property-specific availability of pushouts.

instance TauCeti.ExactStructure.instIsStableUnderCobaseChangeInflations {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] (E : ExactStructure C) : E.inflations.IsStableUnderCobaseChange

E2 stability, as stability of inflations under cobase change.

instance TauCeti.ExactStructure.instHasPullbacksDeflations {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] (E : ExactStructure C) : E.deflations.HasPullbacks

E2op existence, as property-specific availability of pullbacks.

instance TauCeti.ExactStructure.instIsStableUnderBaseChangeDeflations {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] (E : ExactStructure C) : E.deflations.IsStableUnderBaseChange

E2op stability, as stability of deflations under base change.