Conflations along admissible base change, and the Noether conflation

Quillen's axiom E2 produces a pushout of an inflation along an arbitrary morphism and asserts only that the resulting morphism is again an inflation. This file identifies the cokernel of that inflation: cobase change of a conflation X ⟶ Y ⟶ Z along u : X ⟶ X' produces a conflation X' ⟶ Q ⟶ Z with the same third term. Dually, base change of a conflation along u : Z' ⟶ Z produces a conflation X ⟶ Q ⟶ Z' with the same first term.

The second half of the file uses this to describe the conflations attached to a composite of two inflations. If X ⟶ Y ⟶ Z and Y ⟶ W ⟶ V are conflations, then the pushout Q of the inflation Y ⟶ W along the deflation Y ⟶ Z is at once the third term of a conflation X ⟶ W ⟶ Q and the second term of a conflation Z ⟶ Q ⟶ V. This is the exact-category form of Noether's second isomorphism theorem, Q ≅ W/X with (W/X)/(Y/X) ≅ W/Y, and it is what makes extension-closed subcategories inherit axiom E1.

Main definitions

• TauCeti.cobaseChange: the conflation X' ⟶ Q ⟶ Z obtained from S : X ⟶ Y ⟶ Z and a pushout square along u : X ⟶ X'.
• TauCeti.baseChange: the conflation X ⟶ Q ⟶ Z' obtained from S : X ⟶ Y ⟶ Z and a pullback square along u : Z' ⟶ Z.

Main results

• TauCeti.ExactStructure.conflation_cobaseChange and TauCeti.ExactStructure.conflation_baseChange: base and cobase change of a conflation along an arbitrary morphism is a conflation; the inflation or deflation in the original conflation is the admissible morphism being pushed out or pulled back.
• TauCeti.ExactStructure.conflation_comp_of_isPushout and TauCeti.ExactStructure.conflation_comp_of_isPullback: the cokernel of a composite of inflations, and the kernel of a composite of deflations, computed as a pushout resp. pullback.
• TauCeti.ExactStructure.exists_conflation_comp: the Noether package for a composite of two inflations.

References

• Theo Bühler, Exact categories, Expositiones Mathematicae 28 (2010), 1--69, https://arxiv.org/abs/0811.1480. Proposition 2.12 identifies the cokernel along a cobase change and Lemma 3.5 is the Noether isomorphism proved here.

noncomputable def TauCeti.cobaseChangeπ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (S : CategoryTheory.ShortComplex C) {X' Q : C} {u : S.X₁ ⟶ X'} {v : S.X₂ ⟶ Q} {w : X' ⟶ Q} (sq : CategoryTheory.IsPushout S.f u v w) : Q ⟶ S.X₃

The morphism Q ⟶ S.X₃ out of a cobase change of S.f along u, induced by S.g on the one summand and by 0 on the other.

Equations

• TauCeti.cobaseChangeπ S sq = sq.desc S.g 0 ⋯

@[simp]

theorem TauCeti.inl_cobaseChangeπ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (S : CategoryTheory.ShortComplex C) {X' Q : C} {u : S.X₁ ⟶ X'} {v : S.X₂ ⟶ Q} {w : X' ⟶ Q} (sq : CategoryTheory.IsPushout S.f u v w) : CategoryTheory.CategoryStruct.comp v (cobaseChangeπ S sq) = S.g

@[simp]

theorem TauCeti.inl_cobaseChangeπ_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (S : CategoryTheory.ShortComplex C) {X' Q : C} {u : S.X₁ ⟶ X'} {v : S.X₂ ⟶ Q} {w : X' ⟶ Q} (sq : CategoryTheory.IsPushout S.f u v w) {Z : C} (h : S.X₃ ⟶ Z) : CategoryTheory.CategoryStruct.comp v (CategoryTheory.CategoryStruct.comp (cobaseChangeπ S sq) h) = CategoryTheory.CategoryStruct.comp S.g h

@[simp]

theorem TauCeti.inr_cobaseChangeπ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (S : CategoryTheory.ShortComplex C) {X' Q : C} {u : S.X₁ ⟶ X'} {v : S.X₂ ⟶ Q} {w : X' ⟶ Q} (sq : CategoryTheory.IsPushout S.f u v w) : CategoryTheory.CategoryStruct.comp w (cobaseChangeπ S sq) = 0

@[simp]

theorem TauCeti.inr_cobaseChangeπ_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (S : CategoryTheory.ShortComplex C) {X' Q : C} {u : S.X₁ ⟶ X'} {v : S.X₂ ⟶ Q} {w : X' ⟶ Q} (sq : CategoryTheory.IsPushout S.f u v w) {Z : C} (h : S.X₃ ⟶ Z) : CategoryTheory.CategoryStruct.comp w (CategoryTheory.CategoryStruct.comp (cobaseChangeπ S sq) h) = CategoryTheory.CategoryStruct.comp 0 h

noncomputable def TauCeti.cobaseChange {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (S : CategoryTheory.ShortComplex C) {X' Q : C} {u : S.X₁ ⟶ X'} {v : S.X₂ ⟶ Q} {w : X' ⟶ Q} (sq : CategoryTheory.IsPushout S.f u v w) : CategoryTheory.ShortComplex C

The cobase change of a short complex S along u : S.X₁ ⟶ X': the short complex X' ⟶ Q ⟶ S.X₃ attached to a pushout square of S.f along u.

Equations

• TauCeti.cobaseChange S sq = { X₁ := X', X₂ := Q, X₃ := S.X₃, f := w, g := TauCeti.cobaseChangeπ S sq, zero := ⋯ }

theorem TauCeti.cobaseChange_def {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (S : CategoryTheory.ShortComplex C) {X' Q : C} {u : S.X₁ ⟶ X'} {v : S.X₂ ⟶ Q} {w : X' ⟶ Q} (sq : CategoryTheory.IsPushout S.f u v w) : cobaseChange S sq = { X₁ := X', X₂ := Q, X₃ := S.X₃, f := w, g := cobaseChangeπ S sq, zero := ⋯ }

The defining equation for cobaseChange.

@[simp]

theorem TauCeti.cobaseChange_X₁ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (S : CategoryTheory.ShortComplex C) {X' Q : C} {u : S.X₁ ⟶ X'} {v : S.X₂ ⟶ Q} {w : X' ⟶ Q} (sq : CategoryTheory.IsPushout S.f u v w) : (cobaseChange S sq).X₁ = X'

@[simp]

theorem TauCeti.cobaseChange_X₂ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (S : CategoryTheory.ShortComplex C) {X' Q : C} {u : S.X₁ ⟶ X'} {v : S.X₂ ⟶ Q} {w : X' ⟶ Q} (sq : CategoryTheory.IsPushout S.f u v w) : (cobaseChange S sq).X₂ = Q

@[simp]

theorem TauCeti.cobaseChange_X₃ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (S : CategoryTheory.ShortComplex C) {X' Q : C} {u : S.X₁ ⟶ X'} {v : S.X₂ ⟶ Q} {w : X' ⟶ Q} (sq : CategoryTheory.IsPushout S.f u v w) : (cobaseChange S sq).X₃ = S.X₃

@[simp]

theorem TauCeti.cobaseChange_f {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (S : CategoryTheory.ShortComplex C) {X' Q : C} {u : S.X₁ ⟶ X'} {v : S.X₂ ⟶ Q} {w : X' ⟶ Q} (sq : CategoryTheory.IsPushout S.f u v w) : (cobaseChange S sq).f ≍ w

@[simp]

theorem TauCeti.cobaseChange_g {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (S : CategoryTheory.ShortComplex C) {X' Q : C} {u : S.X₁ ⟶ X'} {v : S.X₂ ⟶ Q} {w : X' ⟶ Q} (sq : CategoryTheory.IsPushout S.f u v w) : (cobaseChange S sq).g ≍ cobaseChangeπ S sq

noncomputable def TauCeti.baseChangeι {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (S : CategoryTheory.ShortComplex C) {Z' Q : C} {u : Z' ⟶ S.X₃} {v : Q ⟶ S.X₂} {w : Q ⟶ Z'} (sq : CategoryTheory.IsPullback v w S.g u) : S.X₁ ⟶ Q

The morphism S.X₁ ⟶ Q into a base change of S.g along u, induced by S.f on the one factor and by 0 on the other.

Equations

• TauCeti.baseChangeι S sq = sq.lift S.f 0 ⋯

@[simp]

theorem TauCeti.baseChangeι_fst {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (S : CategoryTheory.ShortComplex C) {Z' Q : C} {u : Z' ⟶ S.X₃} {v : Q ⟶ S.X₂} {w : Q ⟶ Z'} (sq : CategoryTheory.IsPullback v w S.g u) : CategoryTheory.CategoryStruct.comp (baseChangeι S sq) v = S.f

@[simp]

theorem TauCeti.baseChangeι_fst_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (S : CategoryTheory.ShortComplex C) {Z' Q : C} {u : Z' ⟶ S.X₃} {v : Q ⟶ S.X₂} {w : Q ⟶ Z'} (sq : CategoryTheory.IsPullback v w S.g u) {Z : C} (h : S.X₂ ⟶ Z) : CategoryTheory.CategoryStruct.comp (baseChangeι S sq) (CategoryTheory.CategoryStruct.comp v h) = CategoryTheory.CategoryStruct.comp S.f h

@[simp]

theorem TauCeti.baseChangeι_snd {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (S : CategoryTheory.ShortComplex C) {Z' Q : C} {u : Z' ⟶ S.X₃} {v : Q ⟶ S.X₂} {w : Q ⟶ Z'} (sq : CategoryTheory.IsPullback v w S.g u) : CategoryTheory.CategoryStruct.comp (baseChangeι S sq) w = 0

@[simp]

theorem TauCeti.baseChangeι_snd_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (S : CategoryTheory.ShortComplex C) {Z' Q : C} {u : Z' ⟶ S.X₃} {v : Q ⟶ S.X₂} {w : Q ⟶ Z'} (sq : CategoryTheory.IsPullback v w S.g u) {Z : C} (h : Z' ⟶ Z) : CategoryTheory.CategoryStruct.comp (baseChangeι S sq) (CategoryTheory.CategoryStruct.comp w h) = CategoryTheory.CategoryStruct.comp 0 h

noncomputable def TauCeti.baseChange {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (S : CategoryTheory.ShortComplex C) {Z' Q : C} {u : Z' ⟶ S.X₃} {v : Q ⟶ S.X₂} {w : Q ⟶ Z'} (sq : CategoryTheory.IsPullback v w S.g u) : CategoryTheory.ShortComplex C

The base change of a short complex S along u : Z' ⟶ S.X₃: the short complex S.X₁ ⟶ Q ⟶ Z' attached to a pullback square of S.g along u.

Equations

• TauCeti.baseChange S sq = { X₁ := S.X₁, X₂ := Q, X₃ := Z', f := TauCeti.baseChangeι S sq, g := w, zero := ⋯ }

theorem TauCeti.baseChange_def {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (S : CategoryTheory.ShortComplex C) {Z' Q : C} {u : Z' ⟶ S.X₃} {v : Q ⟶ S.X₂} {w : Q ⟶ Z'} (sq : CategoryTheory.IsPullback v w S.g u) : baseChange S sq = { X₁ := S.X₁, X₂ := Q, X₃ := Z', f := baseChangeι S sq, g := w, zero := ⋯ }

The defining equation for baseChange.

@[simp]

theorem TauCeti.baseChange_X₁ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (S : CategoryTheory.ShortComplex C) {Z' Q : C} {u : Z' ⟶ S.X₃} {v : Q ⟶ S.X₂} {w : Q ⟶ Z'} (sq : CategoryTheory.IsPullback v w S.g u) : (baseChange S sq).X₁ = S.X₁

@[simp]

theorem TauCeti.baseChange_X₂ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (S : CategoryTheory.ShortComplex C) {Z' Q : C} {u : Z' ⟶ S.X₃} {v : Q ⟶ S.X₂} {w : Q ⟶ Z'} (sq : CategoryTheory.IsPullback v w S.g u) : (baseChange S sq).X₂ = Q

@[simp]

theorem TauCeti.baseChange_X₃ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (S : CategoryTheory.ShortComplex C) {Z' Q : C} {u : Z' ⟶ S.X₃} {v : Q ⟶ S.X₂} {w : Q ⟶ Z'} (sq : CategoryTheory.IsPullback v w S.g u) : (baseChange S sq).X₃ = Z'

@[simp]

theorem TauCeti.baseChange_g {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (S : CategoryTheory.ShortComplex C) {Z' Q : C} {u : Z' ⟶ S.X₃} {v : Q ⟶ S.X₂} {w : Q ⟶ Z'} (sq : CategoryTheory.IsPullback v w S.g u) : (baseChange S sq).g ≍ w

@[simp]

theorem TauCeti.baseChange_f {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (S : CategoryTheory.ShortComplex C) {Z' Q : C} {u : Z' ⟶ S.X₃} {v : Q ⟶ S.X₂} {w : Q ⟶ Z'} (sq : CategoryTheory.IsPullback v w S.g u) : (baseChange S sq).f ≍ baseChangeι S sq

theorem TauCeti.ExactStructure.conflation_cobaseChange {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 : E.Conflation S) {X' Q : C} {u : S.X₁ ⟶ X'} {v : S.X₂ ⟶ Q} {w : X' ⟶ Q} (sq : CategoryTheory.IsPushout S.f u v w) : E.Conflation (cobaseChange S sq)

Cobase change of a conflation is a conflation with the same cokernel. The pushout of a conflation X ⟶ Y ⟶ Z along a morphism u : X ⟶ X' is a conflation X' ⟶ Q ⟶ Z.

Axiom E2 alone gives only that X' ⟶ Q is an inflation; the content here is that its cokernel may be taken to be the original Z.

theorem TauCeti.ExactStructure.conflation_baseChange {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 : E.Conflation S) {Z' Q : C} {u : Z' ⟶ S.X₃} {v : Q ⟶ S.X₂} {w : Q ⟶ Z'} (sq : CategoryTheory.IsPullback v w S.g u) : E.Conflation (baseChange S sq)

Base change of a conflation is a conflation with the same kernel. The pullback of a conflation X ⟶ Y ⟶ Z along a morphism u : Z' ⟶ Z is a conflation X ⟶ Q ⟶ Z'.

theorem TauCeti.ExactStructure.conflation_comp_of_isPushout {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] (E : ExactStructure C) {X Y Z W V Q : C} {i : X ⟶ Y} {p : Y ⟶ Z} {hip : CategoryTheory.CategoryStruct.comp i p = 0} (h₁ : E.Conflation { X₁ := X, X₂ := Y, X₃ := Z, f := i, g := p, zero := hip }) {j : Y ⟶ W} {v : W ⟶ V} {hjv : CategoryTheory.CategoryStruct.comp j v = 0} (h₂ : E.Conflation { X₁ := Y, X₂ := W, X₃ := V, f := j, g := v, zero := hjv }) {c : W ⟶ Q} {α : Z ⟶ Q} (sq : CategoryTheory.IsPushout j p c α) : E.Conflation { X₁ := X, X₂ := W, X₃ := Q, f := CategoryTheory.CategoryStruct.comp i j, g := c, zero := ⋯ }

The cokernel of a composite of inflations. If X ⟶ Y ⟶ Z and Y ⟶ W ⟶ V are conflations, then the pushout Q of the inflation Y ⟶ W along the deflation Y ⟶ Z is a cokernel of the composite inflation X ⟶ W.

theorem TauCeti.ExactStructure.conflation_comp_of_isPullback {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] (E : ExactStructure C) {X Y Z W V Q : C} {i : X ⟶ Y} {p : Y ⟶ Z} {hip : CategoryTheory.CategoryStruct.comp i p = 0} (h₁ : E.Conflation { X₁ := X, X₂ := Y, X₃ := Z, f := i, g := p, zero := hip }) {v : V ⟶ W} {q : W ⟶ Y} {hvq : CategoryTheory.CategoryStruct.comp v q = 0} (h₂ : E.Conflation { X₁ := V, X₂ := W, X₃ := Y, f := v, g := q, zero := hvq }) {c : Q ⟶ W} {α : Q ⟶ X} (sq : CategoryTheory.IsPullback c α q i) : E.Conflation { X₁ := Q, X₂ := W, X₃ := Z, f := c, g := CategoryTheory.CategoryStruct.comp q p, zero := ⋯ }

The kernel of a composite of deflations. If X ⟶ Y ⟶ Z and V ⟶ W ⟶ Y are conflations, then the pullback Q of the deflation W ⟶ Y along the inflation X ⟶ Y is a kernel of the composite deflation W ⟶ Z.

theorem TauCeti.ExactStructure.exists_conflation_comp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] (E : ExactStructure C) {X Y Z W V : C} {i : X ⟶ Y} {p : Y ⟶ Z} {hip : CategoryTheory.CategoryStruct.comp i p = 0} (h₁ : E.Conflation { X₁ := X, X₂ := Y, X₃ := Z, f := i, g := p, zero := hip }) {j : Y ⟶ W} {v : W ⟶ V} {hjv : CategoryTheory.CategoryStruct.comp j v = 0} (h₂ : E.Conflation { X₁ := Y, X₂ := W, X₃ := V, f := j, g := v, zero := hjv }) : ∃ (Q : C) (c : W ⟶ Q) (α : Z ⟶ Q) (β : Q ⟶ V) (hc : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp i j) c = 0) (hβ : CategoryTheory.CategoryStruct.comp α β = 0), E.Conflation { X₁ := X, X₂ := W, X₃ := Q, f := CategoryTheory.CategoryStruct.comp i j, g := c, zero := hc } ∧ E.Conflation { X₁ := Z, X₂ := Q, X₃ := V, f := α, g := β, zero := hβ } ∧ CategoryTheory.CategoryStruct.comp j c = CategoryTheory.CategoryStruct.comp p α ∧ CategoryTheory.CategoryStruct.comp c β = v

The Noether isomorphism for exact categories. Given conflations X ⟶ Y ⟶ Z and Y ⟶ W ⟶ V, there is an object Q — the pushout of Y ⟶ W along Y ⟶ Z — which is at once the cokernel of the composite inflation X ⟶ W and an extension of V by Z.

In the classical notation Q ≅ W/X, and the second conflation is Y/X ⟶ W/X ⟶ W/Y. This is Bühler's Lemma 3.5, and it is exactly what an extension-closed subcategory needs in order to inherit axiom E1.

theorem TauCeti.ExactStructure.exists_conflation_comp' {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] (E : ExactStructure C) {X Y Z W V : C} {i : X ⟶ Y} {p : Y ⟶ Z} {hip : CategoryTheory.CategoryStruct.comp i p = 0} (h₁ : E.Conflation { X₁ := X, X₂ := Y, X₃ := Z, f := i, g := p, zero := hip }) {v : V ⟶ W} {q : W ⟶ Y} {hvq : CategoryTheory.CategoryStruct.comp v q = 0} (h₂ : E.Conflation { X₁ := V, X₂ := W, X₃ := Y, f := v, g := q, zero := hvq }) : ∃ (Q : C) (c : Q ⟶ W) (α : Q ⟶ X) (β : V ⟶ Q) (hc : CategoryTheory.CategoryStruct.comp c (CategoryTheory.CategoryStruct.comp q p) = 0) (hβ : CategoryTheory.CategoryStruct.comp β α = 0), E.Conflation { X₁ := Q, X₂ := W, X₃ := Z, f := c, g := CategoryTheory.CategoryStruct.comp q p, zero := hc } ∧ E.Conflation { X₁ := V, X₂ := Q, X₃ := X, f := β, g := α, zero := hβ } ∧ CategoryTheory.CategoryStruct.comp c q = CategoryTheory.CategoryStruct.comp α i ∧ CategoryTheory.CategoryStruct.comp β c = v

The dual Noether isomorphism. Given conflations X ⟶ Y ⟶ Z and V ⟶ W ⟶ Y, the pullback Q of W ⟶ Y along X ⟶ Y is at once the kernel of the composite deflation W ⟶ Z and an extension of X by V.