The split exact structure on an additive category

Every additive category C carries a Quillen exact structure ExactStructure.split C whose conflations are the short complexes admitting a splitting, that is, the short complexes isomorphic to X ⟶ X ⊞ Z ⟶ Z.

In this exact structure a morphism i : X ⟶ Y is an inflation exactly when it is the inclusion of a biproduct summand: there are an object Z and an isomorphism e : Y ≅ X ⊞ Z with i ≫ e.hom = biprod.inl. Being a split monomorphism is not enough, because the complementary summand need not exist; the two notions agree as soon as the relevant idempotent splits.

The split structure is the smallest exact structure on C: the last section proves that a short complex with a splitting is a conflation for every exact structure E on C. This is Bühler's Lemma 2.7, and it is what makes the comparison out of split K₀ available for an arbitrary exact structure.

Main definitions

• TauCeti.biprodShortComplex X Z: the short complex X ⟶ X ⊞ Z ⟶ Z.
• TauCeti.ConflationClass.split: the class of short complexes admitting a splitting.
• TauCeti.ExactStructure.split: the split exact structure on an additive category.

Main results

• TauCeti.ConflationClass.split_isInflation_iff and TauCeti.ConflationClass.split_isDeflation_iff: the split inflations are the biproduct inclusions and the split deflations are the biproduct projections.
• TauCeti.ConflationClass.exists_isPushout_of_split_isInflation and TauCeti.ConflationClass.exists_isPullback_of_split_isDeflation: the E2/E2op squares, computed explicitly in the biproduct decomposition.
• TauCeti.ExactStructure.conflation_of_splitting: a split short complex is a conflation of every exact structure, so ExactStructure.split C is the smallest one.
• TauCeti.ExactStructure.conflation_zero_id and TauCeti.ExactStructure.conflation_id_zero: the two trivial conflations, split by the identity, are conflations of every exact structure.
• TauCeti.ExactStructure.split_isInflation_iff and TauCeti.ExactStructure.split_isDeflation_iff: the characteristic API of TauCeti.ExactStructure.split.
• TauCeti.ExactStructure.split_isInflation_iff_isDeflation_unop: split inflations of Cᵒᵖ are the opposites of split deflations of C.
• TauCeti.ExactStructure.split_isInflation_biprod_lift_id_left and TauCeti.ExactStructure.split_isDeflation_biprod_desc_id_left, with their _right variants: the graph biprod.lift (𝟙 X) g of a morphism is a split inflation, and dually biprod.desc (𝟙 X) g is a split deflation.

References

• Theo Bühler, Exact categories, Expositiones Mathematicae 28 (2010), 1–69, https://arxiv.org/abs/0811.1480. Section 13.1 constructs the split exact structure, and Lemma 2.7 shows that split short complexes are conflations of any exact structure.
• Charles A. Weibel, The K-book: An Introduction to Algebraic K-theory, Chapter II, Section 5, where split K₀ is presented through the split exact structure.

@[reducible, inline]

noncomputable abbrev TauCeti.biprodShortComplex {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (X Z : C) [CategoryTheory.Limits.HasBinaryBiproduct X Z] : CategoryTheory.ShortComplex C

The biproduct short complex X ⟶ X ⊞ Z ⟶ Z. Up to isomorphism these are exactly the conflations of the split exact structure.

Equations

• TauCeti.biprodShortComplex X Z = { X₁ := X, X₂ := X ⊞ Z, X₃ := Z, f := CategoryTheory.Limits.biprod.inl, g := CategoryTheory.Limits.biprod.snd, zero := ⋯ }

noncomputable def TauCeti.isoBiprodShortComplex {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {S : CategoryTheory.ShortComplex C} (s : S.Splitting) [CategoryTheory.Limits.HasBinaryBiproduct S.X₁ S.X₃] : S ≅ biprodShortComplex S.X₁ S.X₃

A splitting of S identifies S with the biproduct short complex on its outer terms.

Equations

• TauCeti.isoBiprodShortComplex s = CategoryTheory.ShortComplex.isoMk (CategoryTheory.Iso.refl S.X₁) s.isoBinaryBiproduct (CategoryTheory.Iso.refl S.X₃) ⋯ ⋯

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

The class of short complexes admitting a splitting. These are the conflations of the split exact structure.

Equations

• TauCeti.ConflationClass.split C = { Conflation := fun (S : CategoryTheory.ShortComplex C) => Nonempty S.Splitting, isKernelCokernelPair := ⋯, isClosedUnderIsomorphisms := ⋯ }

@[simp]

theorem TauCeti.ConflationClass.split_conflation_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (S : CategoryTheory.ShortComplex C) : (split C).Conflation S ↔ Nonempty S.Splitting

The split conflations are exactly the short complexes admitting a splitting.

theorem TauCeti.ConflationClass.split_conflation_biprodShortComplex {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (X Z : C) [CategoryTheory.Limits.HasBinaryBiproduct X Z] : (split C).Conflation (biprodShortComplex X Z)

The biproduct short complex X ⟶ X ⊞ Z ⟶ Z is a split conflation.

theorem TauCeti.ConflationClass.split_conflation_biprod_inr_fst {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (X Z : C) [CategoryTheory.Limits.HasBinaryBiproduct X Z] : (split C).Conflation { X₁ := Z, X₂ := X ⊞ Z, X₃ := X, f := CategoryTheory.Limits.biprod.inr, g := CategoryTheory.Limits.biprod.fst, zero := ⋯ }

The short complex Z ⟶ X ⊞ Z ⟶ X on the other biproduct summand is a split conflation.

@[simp]

theorem TauCeti.ConflationClass.split_isInflation_biprod_inl {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (X Z : C) [CategoryTheory.Limits.HasBinaryBiproduct X Z] : (split C).IsInflation CategoryTheory.Limits.biprod.inl

A biproduct inclusion is a split inflation.

@[simp]

theorem TauCeti.ConflationClass.split_isInflation_biprod_inr {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (X Z : C) [CategoryTheory.Limits.HasBinaryBiproduct X Z] : (split C).IsInflation CategoryTheory.Limits.biprod.inr

The other biproduct inclusion is a split inflation as well.

@[simp]

theorem TauCeti.ConflationClass.split_isDeflation_biprod_snd {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (X Z : C) [CategoryTheory.Limits.HasBinaryBiproduct X Z] : (split C).IsDeflation CategoryTheory.Limits.biprod.snd

A biproduct projection is a split deflation.

@[simp]

theorem TauCeti.ConflationClass.split_isDeflation_biprod_fst {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (X Z : C) [CategoryTheory.Limits.HasBinaryBiproduct X Z] : (split C).IsDeflation CategoryTheory.Limits.biprod.fst

The other biproduct projection is a split deflation as well.

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

Every split inflation is a split monomorphism. The converse fails in general: a split monomorphism is an inflation only once its complementary idempotent splits.

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

Every split deflation is a split epimorphism.

theorem TauCeti.ConflationClass.split_isInflation_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {X Y : C} (i : X ⟶ Y) : (split C).IsInflation i ↔ ∃ (Z : C) (e : Y ≅ X ⊞ Z), CategoryTheory.CategoryStruct.comp i e.hom = CategoryTheory.Limits.biprod.inl

The split inflations are the biproduct inclusions. A split monomorphism whose complementary idempotent does not split is not an inflation of the split exact structure.

theorem TauCeti.ConflationClass.split_isDeflation_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {Y Z : C} (p : Y ⟶ Z) : (split C).IsDeflation p ↔ ∃ (X : C) (e : Y ≅ X ⊞ Z), CategoryTheory.CategoryStruct.comp e.inv p = CategoryTheory.Limits.biprod.snd

The split deflations are the biproduct projections.

theorem TauCeti.ConflationClass.split_isInflation_comp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {X Y W : C} {i : X ⟶ Y} {j : Y ⟶ W} (hi : (split C).IsInflation i) (hj : (split C).IsInflation j) : (split C).IsInflation (CategoryTheory.CategoryStruct.comp i j)

E1 for the split exact structure: a composite of split inflations is a split inflation. The cokernel of i ≫ j is the biproduct of the two cokernels.

theorem TauCeti.ConflationClass.split_isDeflation_comp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {X Y Z : C} {p : X ⟶ Y} {q : Y ⟶ Z} (hp : (split C).IsDeflation p) (hq : (split C).IsDeflation q) : (split C).IsDeflation (CategoryTheory.CategoryStruct.comp p q)

E1op for the split exact structure: a composite of split deflations is a split deflation. The kernel of p ≫ q is the biproduct of the two kernels.

theorem TauCeti.ConflationClass.exists_isPushout_of_split_isInflation {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {A B A' : C} {i : A ⟶ B} (hi : (split C).IsInflation i) (g : A ⟶ A') : ∃ (T : C) (inl : B ⟶ T) (inr : A' ⟶ T), CategoryTheory.IsPushout i g inl inr ∧ (split C).IsInflation inr

E2 for the split exact structure: the pushout of a split inflation i : A ⟶ B along an arbitrary g : A ⟶ A' exists and its cobase change is again a split inflation. Concretely, if B ≅ A ⊞ Z identifies i with biprod.inl, then the pushout is A' ⊞ Z.

theorem TauCeti.ConflationClass.exists_isPullback_of_split_isDeflation {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {Y Z A : C} {p : Y ⟶ Z} (hp : (split C).IsDeflation p) (f : A ⟶ Z) : ∃ (T : C) (fst : T ⟶ A) (snd : T ⟶ Y), CategoryTheory.IsPullback fst snd f p ∧ (split C).IsDeflation fst

E2op for the split exact structure: the pullback of a split deflation p : Y ⟶ Z along an arbitrary f : A ⟶ Z exists and its base change is again a split deflation. Concretely, if Y ≅ X ⊞ Z identifies p with biprod.snd, then the pullback is X ⊞ A.

noncomputable def TauCeti.ExactStructure.split (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] : ExactStructure C

The split exact structure on an additive category: its conflations are the short complexes admitting a splitting.

Its conflations are only the split short complexes, whereas those of the canonical exact structure of an abelian category are all the short exact ones; see TauCeti.ExactStructure.conflation_of_splitting for the general comparison.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.ExactStructure.split_conflation {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] (S : CategoryTheory.ShortComplex C) : (split C).Conflation S ↔ Nonempty S.Splitting

The conflations of the split exact structure are exactly the short complexes admitting a splitting.

@[simp]

theorem TauCeti.ExactStructure.split_isInflation_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {X Y : C} (i : X ⟶ Y) : (split C).IsInflation i ↔ ∃ (Z : C) (e : Y ≅ X ⊞ Z), CategoryTheory.CategoryStruct.comp i e.hom = CategoryTheory.Limits.biprod.inl

The inflations of the split exact structure are the biproduct inclusions.

@[simp]

theorem TauCeti.ExactStructure.split_isDeflation_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {Y Z : C} (p : Y ⟶ Z) : (split C).IsDeflation p ↔ ∃ (X : C) (e : Y ≅ X ⊞ Z), CategoryTheory.CategoryStruct.comp e.inv p = CategoryTheory.Limits.biprod.snd

The deflations of the split exact structure are the biproduct projections.

theorem TauCeti.ExactStructure.isSplitMono_of_split_isInflation {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {X Y : C} {i : X ⟶ Y} (hi : (split C).IsInflation i) : CategoryTheory.IsSplitMono i

Every inflation of the split exact structure is a split monomorphism.

theorem TauCeti.ExactStructure.isSplitEpi_of_split_isDeflation {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {Y Z : C} {p : Y ⟶ Z} (hp : (split C).IsDeflation p) : CategoryTheory.IsSplitEpi p

Every deflation of the split exact structure is a split epimorphism.

theorem TauCeti.ExactStructure.split_isInflation_biprod_lift_id_left {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {X Z : C} (g : X ⟶ Z) : (split C).IsInflation (CategoryTheory.Limits.biprod.lift (CategoryTheory.CategoryStruct.id X) g)

The graph biprod.lift (𝟙 X) g : X ⟶ X ⊞ Z of a morphism g : X ⟶ Z is a split inflation: the shear (x, z) ↦ (x, z - g x) carries it to biprod.inl.

theorem TauCeti.ExactStructure.split_isInflation_biprod_lift_id_right {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {X Z : C} (g : X ⟶ Z) : (split C).IsInflation (CategoryTheory.Limits.biprod.lift g (CategoryTheory.CategoryStruct.id X))

The graph biprod.lift g (𝟙 X) : X ⟶ Z ⊞ X of a morphism g : X ⟶ Z is a split inflation.

theorem TauCeti.ExactStructure.split_isDeflation_biprod_desc_id_left {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {X Z : C} (g : Z ⟶ X) : (split C).IsDeflation (CategoryTheory.Limits.biprod.desc (CategoryTheory.CategoryStruct.id X) g)

The map biprod.desc (𝟙 X) g : X ⊞ Z ⟶ X is a split deflation: the shear (x, z) ↦ (x + g z, z) carries it to the projection onto X.

theorem TauCeti.ExactStructure.split_isDeflation_biprod_desc_id_right {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {X Z : C} (g : Z ⟶ X) : (split C).IsDeflation (CategoryTheory.Limits.biprod.desc g (CategoryTheory.CategoryStruct.id X))

The map biprod.desc g (𝟙 X) : Z ⊞ X ⟶ X is a split deflation.

theorem TauCeti.ExactStructure.split_conflation_biprod_lift_id_right {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {X Z : C} (g : X ⟶ Z) : (split C).Conflation { X₁ := X, X₂ := Z ⊞ X, X₃ := Z, f := CategoryTheory.Limits.biprod.lift g (CategoryTheory.CategoryStruct.id X), g := CategoryTheory.Limits.biprod.desc (CategoryTheory.CategoryStruct.id Z) (-g), zero := ⋯ }

The graph biprod.lift g (𝟙 X) : X ⟶ Z ⊞ X of a morphism g : X ⟶ Z and the map biprod.desc (𝟙 Z) (-g) : Z ⊞ X ⟶ Z form a split conflation X ⟶ Z ⊞ X ⟶ Z.

theorem TauCeti.ExactStructure.split_conflation_biprod_lift_id_left {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {X Z : C} (g : X ⟶ Z) : (split C).Conflation { X₁ := X, X₂ := X ⊞ Z, X₃ := Z, f := CategoryTheory.Limits.biprod.lift (CategoryTheory.CategoryStruct.id X) g, g := CategoryTheory.Limits.biprod.desc g (-CategoryTheory.CategoryStruct.id Z), zero := ⋯ }

The graph biprod.lift (𝟙 X) g : X ⟶ X ⊞ Z of a morphism g : X ⟶ Z and the map biprod.desc g (-𝟙 Z) : X ⊞ Z ⟶ Z form a split conflation X ⟶ X ⊞ Z ⟶ Z.

theorem TauCeti.ExactStructure.split_isInflation_iff_isDeflation_unop {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {X Y : Cᵒᵖ} (f : X ⟶ Y) : (split Cᵒᵖ).IsInflation f ↔ (split C).IsDeflation f.unop

A morphism of Cᵒᵖ is a split inflation exactly when its unopposite is a split deflation of C: splittings of short complexes correspond under ShortComplex.Splitting.op and ShortComplex.Splitting.unop.

@[simp]

theorem TauCeti.ExactStructure.conflation_biprodShortComplex {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] (E : ExactStructure C) (X Z : C) : E.Conflation (biprodShortComplex X Z)

In every exact structure the biproduct short complex X ⟶ X ⊞ Z ⟶ Z is a conflation.

No exact structure can therefore omit a biproduct decomposition. This is the key step of Bühler's Lemma 2.7, from which TauCeti.ExactStructure.conflation_of_splitting — the minimality of the split exact structure — follows by closure under isomorphisms.

theorem TauCeti.ExactStructure.conflation_of_splitting {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] (E : ExactStructure C) {S : CategoryTheory.ShortComplex C} (s : S.Splitting) : E.Conflation S

A short complex with a splitting is a conflation of every exact structure. Equivalently, the split exact structure is the smallest exact structure on C.

theorem TauCeti.ExactStructure.conflation_zero_id {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] (E : ExactStructure C) (X : C) : E.Conflation { X₁ := 0, X₂ := X, X₃ := X, f := 0, g := CategoryTheory.CategoryStruct.id X, zero := ⋯ }

The trivial conflation 0 ↪ X ↠ X, split by the identity.

theorem TauCeti.ExactStructure.conflation_id_zero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] (E : ExactStructure C) (X : C) : E.Conflation { X₁ := X, X₂ := X, X₃ := 0, f := CategoryTheory.CategoryStruct.id X, g := 0, zero := ⋯ }

The trivial conflation X → X → 0, dual to conflation_zero_id.

theorem TauCeti.ExactStructure.conflation_of_split_conflation {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] (E : ExactStructure C) {S : CategoryTheory.ShortComplex C} (hS : (split C).Conflation S) : E.Conflation S

A conflation of the split exact structure is a conflation of every exact structure.

theorem TauCeti.ExactStructure.isInflation_of_split_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} (hi : (split C).IsInflation i) : E.IsInflation i

Every split inflation is an inflation of any exact structure.

theorem TauCeti.ExactStructure.isDeflation_of_split_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} (hp : (split C).IsDeflation p) : E.IsDeflation p

Every split deflation is a deflation of any exact structure.