Relative projectives in an exact category, and the horseshoe lemma

Let E be a Quillen exact structure on an additive category C. An object Q is E-projective when every morphism out of Q lifts along every deflation of E. This is the relative notion Bühler uses: it depends on the exact structure, not just on the category. For the split exact structure every object is projective, and for the canonical exact structure of an abelian category it is Mathlib's CategoryTheory.Projective.

Two theorems make relative projectives usable for resolutions, and both are proved by the same method — pull a conflation back along a deflation, then split the resulting conflation because its third term is projective — although each builds its own pullback square. Schanuel's lemma says that two conflations K ↪ Q ↠ X and K' ↪ Q' ↠ X with projective middle terms have stably isomorphic kernels, K ⊞ Q' ≅ K' ⊞ Q.

The main theorem is the horseshoe lemma. Given a conflation X ↪ Y ↠ Z and first steps K_X ↪ Q_X ↠ X and K_Z ↪ Q_Z ↠ Z of resolutions of the two outer terms, with Q_Z projective, there is a conflation

K ↪ Q_X ⊞ Q_Z ↠ Y

whose middle term is the direct sum of the two resolving terms and whose kernel K is itself an extension K_X ↪ K ↠ K_Z of the two syzygies, compatibly with the two given conflations. Iterating it resolves the middle term of a conflation from resolutions of the outer terms, and that is the form in which the last result of this file states it: for an object property P consisting of projectives, containing a zero object and closed under binary biproducts, admitting a finite P-resolution is closed under extensions, with no increase in length.

That closure property is what makes the objects of finite projective dimension an extension-closed subcategory, so that TauCeti.ExactStructure.fullSubcategory equips them with an induced exact structure — the setting in which the resolution theorem compares their Grothendieck group with the one generated by the projectives themselves.

Main definitions

• TauCeti.ExactStructure.isProjective: the object property of being projective relative to an exact structure, together with the lift TauCeti.ExactStructure.isProjective.factorThru of a morphism along a deflation.
• TauCeti.ExactStructure.splittingOfProjective: the splitting of a conflation whose third term is projective.
• TauCeti.ExactStructure.ProjectivePresentation and TauCeti.ExactStructure.EnoughProjectives: relative projective presentations and the condition that every object admits one.

Main results

• TauCeti.ExactStructure.split_isProjective and TauCeti.ExactStructure.abelian_isProjective_iff: the two calibrating computations. Every object is projective for the split exact structure, and for the canonical exact structure of an abelian category the notion is Mathlib's CategoryTheory.Projective.
• TauCeti.ExactStructure.split_enoughProjectives and TauCeti.ExactStructure.abelian_enoughProjectives: the corresponding enough-projective calibrations.
• TauCeti.ExactStructure.isProjective_map_adjoint: a left adjoint preserves relative projectives when its right adjoint is conflation-exact.
• TauCeti.ExactStructure.isProjective_map_equivalence_iff: conflation-exact equivalences preserve and reflect projectivity.
• TauCeti.ExactStructure.nonempty_iso_biprod_of_projective: Schanuel's lemma, that two conflations over the same object with projective middle terms have stably isomorphic kernels.
• TauCeti.ExactStructure.exists_conflation_biprod_of_conflation_of_projective: the horseshoe lemma.
• TauCeti.ExactStructure.exists_finiteResolution_length_le_of_conflation: the middle term of a conflation admits a finite P-resolution of length at most the common bound on the lengths of resolutions of the two outer terms, when P consists of projectives, contains a zero object and is closed under binary biproducts.
• TauCeti.ExactStructure.isExtensionClosed_admitsFiniteResolution: under those same hypotheses on P, admitting a finite P-resolution is closed under extensions.
• TauCeti.ExactStructure.isExtensionClosed_of_le_isProjective and TauCeti.ExactStructure.fullSubcategory_eq_split: a property consisting of projectives is itself extension closed, and the exact structure it inherits is the split one.

Implementation notes

The horseshoe is proved without ever choosing a lift of Q_Z into Y by hand. Pulling the conflation X ↪ Y ↠ Z back along the deflation Q_Z ↠ Z gives a conflation X ↪ W ↠ Q_Z, which splits because Q_Z is projective, while pulling the conflation K_Z ↪ Q_Z ↠ Z back along Y ↠ Z exhibits the same object W as an extension of Y by K_Z. Composing the resulting deflation W ↠ Y with the direct sum Q_X ⊞ Q_Z ↠ X ⊞ Q_Z ≅ W and applying the dual Noether package TauCeti.ExactStructure.exists_conflation_comp' produces the conflation and identifies its kernel in one step.

References

• Theo Bühler, Exact categories, Expositiones Mathematicae 28 (2010), 1–69, https://arxiv.org/abs/0811.1480. Sections 11–12 develop projective objects and resolutions in a Quillen exact category, of which Schanuel's lemma and the horseshoe lemma proved here are the two basic constructions.
• Charles A. Weibel, The K-book: An Introduction to Algebraic K-theory, Chapter II, Section 7, where finite resolutions and the resolution theorem consume this closure property.
• Mathlib/CategoryTheory/Preadditive/Projective/Basic.lean, whose factorThru, factorThru_comp, Adjunction.map_projective, and isomorphism, zero-object and biproduct closure API for absolute projectivity is the layout adapted here to the relative setting, and Mathlib/Algebra/Homology/ShortComplex/ShortExact.lean, whose CategoryTheory.ShortComplex.ShortExact.splittingOfProjective is the balanced-category ancestor of TauCeti.ExactStructure.splittingOfProjective.
• The Tau Ceti Grothendieck groups, Cartan maps, and Euler forms roadmap, Layer 3, whose projective-resolution calculus requires the horseshoe lemma and whose subsequent finite-resolution applications require the resulting extension-closed object property.

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

The objects that are projective relative to the exact structure E: those Q for which every morphism out of Q factors through every deflation of E.

This depends on E and not only on C. For the split exact structure every object is projective, by TauCeti.ExactStructure.split_isProjective; for the canonical exact structure of an abelian category the notion is Mathlib's CategoryTheory.Projective, by TauCeti.ExactStructure.abelian_isProjective_iff.

Equations

• E.isProjective Q = ∀ ⦃X Y : C⦄ {p : X ⟶ Y}, E.IsDeflation p → ∀ (f : Q ⟶ Y), ∃ (g : Q ⟶ X), CategoryTheory.CategoryStruct.comp g p = f

theorem TauCeti.ExactStructure.isProjective_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} {Q : C} : E.isProjective Q ↔ ∀ ⦃X Y : C⦄ {p : X ⟶ Y}, E.IsDeflation p → ∀ (f : Q ⟶ Y), ∃ (g : Q ⟶ X), CategoryTheory.CategoryStruct.comp g p = f

The defining lifting property, as the characterisation of TauCeti.ExactStructure.isProjective available to code that cannot unfold its body.

noncomputable def TauCeti.ExactStructure.isProjective.factorThru {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} {Q : C} (hQ : E.isProjective Q) {X Y : C} {p : X ⟶ Y} (hp : E.IsDeflation p) (f : Q ⟶ Y) : Q ⟶ X

The chosen lift of f : Q ⟶ Y along a deflation p : X ⟶ Y, for Q projective.

Equations

• hQ.factorThru hp f = ⋯.choose

@[simp]

theorem TauCeti.ExactStructure.isProjective.factorThru_comp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} {Q : C} (hQ : E.isProjective Q) {X Y : C} {p : X ⟶ Y} (hp : E.IsDeflation p) (f : Q ⟶ Y) : CategoryTheory.CategoryStruct.comp (hQ.factorThru hp f) p = f

@[simp]

theorem TauCeti.ExactStructure.isProjective.factorThru_comp_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} {Q : C} (hQ : E.isProjective Q) {X Y : C} {p : X ⟶ Y} (hp : E.IsDeflation p) (f : Q ⟶ Y) {Z : C} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (hQ.factorThru hp f) (CategoryTheory.CategoryStruct.comp p h) = CategoryTheory.CategoryStruct.comp f h

instance TauCeti.ExactStructure.instIsStableUnderRetractsIsProjective {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} : E.isProjective.IsStableUnderRetracts

Relative projectives are closed under retracts.

instance TauCeti.ExactStructure.instContainsZeroIsProjective {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} : E.isProjective.ContainsZero

A zero object is projective: every morphism out of it is zero.

theorem TauCeti.ExactStructure.isProjective_biprod {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} {Q₁ Q₂ : C} (h₁ : E.isProjective Q₁) (h₂ : E.isProjective Q₂) : E.isProjective (Q₁ ⊞ Q₂)

A binary direct sum of projectives is projective: lift the two components separately.

instance TauCeti.ExactStructure.instIsClosedUnderBinaryProductsIsProjective {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} : E.isProjective.IsClosedUnderBinaryProducts

The projectives are closed under binary products: in a preadditive category those are biproducts.

noncomputable def TauCeti.ExactStructure.splittingOfProjective {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) (h₃ : E.isProjective S.X₃) : S.Splitting

A conflation with projective third term splits. The section of its deflation is the lift of the identity of that term.

This is the exact-structure analogue of Mathlib's CategoryTheory.ShortComplex.ShortExact.splittingOfProjective, with the balancedness hypothesis on the ambient category replaced by the kernel–cokernel pair carried by a conflation.

Equations

• E.splittingOfProjective hS h₃ = ⋯.splittingOfSection (h₃.factorThru ⋯ (CategoryTheory.CategoryStruct.id S.X₃)) ⋯

@[simp]

theorem TauCeti.ExactStructure.splittingOfProjective_s {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) (h₃ : E.isProjective S.X₃) : (E.splittingOfProjective hS h₃).s = h₃.factorThru ⋯ (CategoryTheory.CategoryStruct.id S.X₃)

@[simp]

theorem TauCeti.ExactStructure.splittingOfProjective_r {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) (h₃ : E.isProjective S.X₃) : (E.splittingOfProjective hS h₃).r = ⋯.lift (CategoryTheory.CategoryStruct.id S.X₂ - CategoryTheory.CategoryStruct.comp S.g (h₃.factorThru ⋯ (CategoryTheory.CategoryStruct.id S.X₃))) ⋯

@[simp]

theorem TauCeti.ExactStructure.split_isProjective {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] (X : C) : (split C).isProjective X

Every object is projective for the split exact structure. Its deflations are split epimorphisms, along which every morphism visibly lifts.

@[simp]

theorem TauCeti.ExactStructure.abelian_isProjective_iff {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] (X : A) : (abelian A).isProjective X ↔ CategoryTheory.Projective X

For the canonical exact structure of an abelian category, relative projectivity is Mathlib's CategoryTheory.Projective. The deflations there are exactly the epimorphisms.

theorem TauCeti.ExactStructure.isProjective_map_adjoint_of_map_isDeflation {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (E : ExactStructure C) (E' : ExactStructure D) (adj : F ⊣ G) (hG : ∀ ⦃X Y : D⦄ (p : X ⟶ Y), E'.IsDeflation p → E.IsDeflation (G.map p)) {Q : C} (hQ : E.isProjective Q) : E'.isProjective (F.obj Q)

A left adjoint carries relative projectives to relative projectives when its right adjoint carries deflations to deflations.

theorem TauCeti.ExactStructure.isProjective_map_adjoint {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} [G.Additive] (E : ExactStructure C) (E' : ExactStructure D) (adj : F ⊣ G) (hG : E'.IsConflationExact E G) {Q : C} (hQ : E.isProjective Q) : E'.isProjective (F.obj Q)

A left adjoint carries relative projectives to relative projectives when its right adjoint is conflation-exact.

theorem TauCeti.ExactStructure.isProjective_map_equivalence_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] (E : ExactStructure C) (E' : ExactStructure D) (e : C ≌ D) [e.functor.Additive] (hF : E.IsConflationExact E' e.functor) (hG : E'.IsConflationExact E e.inverse) (Q : C) : E'.isProjective (e.functor.obj Q) ↔ E.isProjective Q

A conflation-exact equivalence preserves and reflects relative projectivity.

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

A projective presentation of X relative to E is a conflation K → P → X whose middle term is E-projective.

• K : C

  The kernel term of the presentation.

• P : C

  The relatively projective middle term.

• i : self.K ⟶ self.P

  The inflation into the projective term.

• p : self.P ⟶ X

  The deflation onto the presented object.

• zero : CategoryTheory.CategoryStruct.comp self.i self.p = 0

  The two presentation maps form a short complex.

• conflation : E.Conflation { X₁ := self.K, X₂ := self.P, X₃ := X, f := self.i, g := self.p, zero := ⋯ }

  The presentation is a conflation of E.

• isProjective : E.isProjective self.P

  The middle term is projective relative to E.

structure TauCeti.ExactStructure.EnoughProjectives {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] (E : ExactStructure C) : Prop

An exact structure has enough projectives if every object admits a relative projective presentation.

• presentation (X : C) : Nonempty (E.ProjectivePresentation X)

def TauCeti.ExactStructure.ProjectivePresentation.map {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] {E' : ExactStructure D} {X : C} {F : CategoryTheory.Functor C D} [F.Additive] (P : E.ProjectivePresentation X) (hF : E.IsConflationExact E' F) (hPP' : E.isProjective ≤ E'.isProjective.inverseImage F) : E'.ProjectivePresentation (F.obj X)

The image of a relative projective presentation under a conflation-exact functor that carries relative projectives to relative projectives.

Equations

• P.map hF hPP' = { K := F.obj P.K, P := F.obj P.P, i := F.map P.i, p := F.map P.p, zero := ⋯, conflation := ⋯, isProjective := ⋯ }

@[simp]

theorem TauCeti.ExactStructure.ProjectivePresentation.map_K {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] {E' : ExactStructure D} {X : C} {F : CategoryTheory.Functor C D} [F.Additive] (P : E.ProjectivePresentation X) (hF : E.IsConflationExact E' F) (hPP' : E.isProjective ≤ E'.isProjective.inverseImage F) : (P.map hF hPP').K = F.obj P.K

@[simp]

theorem TauCeti.ExactStructure.ProjectivePresentation.map_P {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] {E' : ExactStructure D} {X : C} {F : CategoryTheory.Functor C D} [F.Additive] (P : E.ProjectivePresentation X) (hF : E.IsConflationExact E' F) (hPP' : E.isProjective ≤ E'.isProjective.inverseImage F) : (P.map hF hPP').P = F.obj P.P

@[simp]

theorem TauCeti.ExactStructure.ProjectivePresentation.map_i {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] {E' : ExactStructure D} {X : C} {F : CategoryTheory.Functor C D} [F.Additive] (P : E.ProjectivePresentation X) (hF : E.IsConflationExact E' F) (hPP' : E.isProjective ≤ E'.isProjective.inverseImage F) : (P.map hF hPP').i ≍ F.map P.i

@[simp]

theorem TauCeti.ExactStructure.ProjectivePresentation.map_p {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] {E' : ExactStructure D} {X : C} {F : CategoryTheory.Functor C D} [F.Additive] (P : E.ProjectivePresentation X) (hF : E.IsConflationExact E' F) (hPP' : E.isProjective ≤ E'.isProjective.inverseImage F) : (P.map hF hPP').p ≍ F.map P.p

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

The tautological projective presentation in the split exact structure.

Equations

• TauCeti.ExactStructure.ProjectivePresentation.split X = { K := 0, P := X, i := 0, p := CategoryTheory.CategoryStruct.id X, zero := ⋯, conflation := ⋯, isProjective := ⋯ }

@[simp]

theorem TauCeti.ExactStructure.ProjectivePresentation.split_K {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] (X : C) : (split X).K = 0

@[simp]

theorem TauCeti.ExactStructure.ProjectivePresentation.split_P {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] (X : C) : (split X).P = X

@[simp]

theorem TauCeti.ExactStructure.ProjectivePresentation.split_i {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] (X : C) : (split X).i ≍ 0

@[simp]

theorem TauCeti.ExactStructure.ProjectivePresentation.split_p {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] (X : C) : (split X).p ≍ CategoryTheory.CategoryStruct.id X

noncomputable def TauCeti.ExactStructure.ProjectivePresentation.abelian {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] [CategoryTheory.EnoughProjectives A] (X : A) : (ExactStructure.abelian A).ProjectivePresentation X

Mathlib's projective presentation gives a relative projective presentation for the canonical exact structure of an abelian category.

Equations

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

@[simp]

theorem TauCeti.ExactStructure.ProjectivePresentation.abelian_K {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] [CategoryTheory.EnoughProjectives A] (X : A) : (abelian X).K = CategoryTheory.Limits.kernel (CategoryTheory.Projective.π X)

@[simp]

theorem TauCeti.ExactStructure.ProjectivePresentation.abelian_P {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] [CategoryTheory.EnoughProjectives A] (X : A) : (abelian X).P = CategoryTheory.Projective.over X

@[simp]

theorem TauCeti.ExactStructure.ProjectivePresentation.abelian_i {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] [CategoryTheory.EnoughProjectives A] (X : A) : (abelian X).i ≍ CategoryTheory.Limits.kernel.ι (CategoryTheory.Projective.π X)

@[simp]

theorem TauCeti.ExactStructure.ProjectivePresentation.abelian_p {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] [CategoryTheory.EnoughProjectives A] (X : A) : (abelian X).p ≍ CategoryTheory.Projective.π X

noncomputable def TauCeti.ExactStructure.ProjectivePresentation.middleMap {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} (P : E.ProjectivePresentation X) (Q : E.ProjectivePresentation Y) (f : X ⟶ Y) : P.P ⟶ Q.P

The lift of f : X ⟶ Y to the projective middle terms of relative projective presentations P of X and Q of Y, chosen by relative projectivity of P.P.

Equations

• P.middleMap Q f = ⋯.factorThru ⋯ (CategoryTheory.CategoryStruct.comp P.p f)

@[simp]

theorem TauCeti.ExactStructure.ProjectivePresentation.middleMap_comp_p {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} (P : E.ProjectivePresentation X) (Q : E.ProjectivePresentation Y) (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp (P.middleMap Q f) Q.p = CategoryTheory.CategoryStruct.comp P.p f

The chosen middle-term map lifts f across the two deflations.

@[simp]

theorem TauCeti.ExactStructure.ProjectivePresentation.middleMap_comp_p_assoc {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} (P : E.ProjectivePresentation X) (Q : E.ProjectivePresentation Y) (f : X ⟶ Y) {Z : C} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (P.middleMap Q f) (CategoryTheory.CategoryStruct.comp Q.p h) = CategoryTheory.CategoryStruct.comp P.p (CategoryTheory.CategoryStruct.comp f h)

The chosen middle-term map lifts f across the two deflations.

noncomputable def TauCeti.ExactStructure.ProjectivePresentation.kernelMap {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} (P : E.ProjectivePresentation X) (Q : E.ProjectivePresentation Y) (f : X ⟶ Y) : P.K ⟶ Q.K

The morphism induced by f : X ⟶ Y on the kernel terms of relative projective presentations, through the chosen lift TauCeti.ExactStructure.ProjectivePresentation.middleMap of the projective middle terms.

Equations

• P.kernelMap Q f = ⋯.lift (CategoryTheory.CategoryStruct.comp P.i (P.middleMap Q f)) ⋯

@[simp]

theorem TauCeti.ExactStructure.ProjectivePresentation.kernelMap_comp_i {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} (P : E.ProjectivePresentation X) (Q : E.ProjectivePresentation Y) (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp (P.kernelMap Q f) Q.i = CategoryTheory.CategoryStruct.comp P.i (P.middleMap Q f)

The induced morphism on kernel terms makes the square on the two inflations commute.

@[simp]

theorem TauCeti.ExactStructure.ProjectivePresentation.kernelMap_comp_i_assoc {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} (P : E.ProjectivePresentation X) (Q : E.ProjectivePresentation Y) (f : X ⟶ Y) {Z : C} (h : Q.P ⟶ Z) : CategoryTheory.CategoryStruct.comp (P.kernelMap Q f) (CategoryTheory.CategoryStruct.comp Q.i h) = CategoryTheory.CategoryStruct.comp P.i (CategoryTheory.CategoryStruct.comp (P.middleMap Q f) h)

The induced morphism on kernel terms makes the square on the two inflations commute.

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

The split exact structure has enough relative projectives.

theorem TauCeti.ExactStructure.abelian_enoughProjectives {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] [CategoryTheory.EnoughProjectives A] : (abelian A).EnoughProjectives

Enough ordinary projectives give enough relative projectives for the canonical exact structure on an abelian category.

noncomputable def TauCeti.ExactStructure.EnoughProjectives.projectivePresentation {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} (h : E.EnoughProjectives) (X : C) : E.ProjectivePresentation X

Choose a relative projective presentation from enough relative projectives.

Equations

• h.projectivePresentation X = ⋯.some

theorem TauCeti.ExactStructure.nonempty_iso_biprod_of_projective {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} {X K Q : C} {m : K ⟶ Q} {a : Q ⟶ X} {hm : CategoryTheory.CategoryStruct.comp m a = 0} (hc : E.Conflation { X₁ := K, X₂ := Q, X₃ := X, f := m, g := a, zero := hm }) (hQ : E.isProjective Q) {K' Q' : C} {m' : K' ⟶ Q'} {a' : Q' ⟶ X} {hm' : CategoryTheory.CategoryStruct.comp m' a' = 0} (hc' : E.Conflation { X₁ := K', X₂ := Q', X₃ := X, f := m', g := a', zero := hm' }) (hQ' : E.isProjective Q') : Nonempty (K ⊞ Q' ≅ K' ⊞ Q)

Schanuel's lemma. Two conflations K ↪ Q ↠ X and K' ↪ Q' ↠ X with projective middle terms have stably isomorphic kernels: K ⊞ Q' ≅ K' ⊞ Q.

Both isomorphisms come from the pullback Q ×_X Q', which base change exhibits at once as an extension of Q' by K and as an extension of Q by K'; projectivity splits both.

theorem TauCeti.ExactStructure.exists_conflation_biprod_of_conflation_of_projective {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) {KX QX : C} {mX : KX ⟶ QX} {aX : QX ⟶ S.X₁} {hmX : CategoryTheory.CategoryStruct.comp mX aX = 0} (hcX : E.Conflation { X₁ := KX, X₂ := QX, X₃ := S.X₁, f := mX, g := aX, zero := hmX }) {KZ QZ : C} {mZ : KZ ⟶ QZ} {aZ : QZ ⟶ S.X₃} {hmZ : CategoryTheory.CategoryStruct.comp mZ aZ = 0} (hcZ : E.Conflation { X₁ := KZ, X₂ := QZ, X₃ := S.X₃, f := mZ, g := aZ, zero := hmZ }) (hQZ : E.isProjective QZ) : ∃ (K : C) (u : K ⟶ QX ⊞ QZ) (a : QX ⊞ QZ ⟶ S.X₂) (hu : CategoryTheory.CategoryStruct.comp u a = 0) (v : KX ⟶ K) (w : K ⟶ KZ) (hv : CategoryTheory.CategoryStruct.comp v w = 0), E.Conflation { X₁ := K, X₂ := QX ⊞ QZ, X₃ := S.X₂, f := u, g := a, zero := hu } ∧ E.Conflation { X₁ := KX, X₂ := K, X₃ := KZ, f := v, g := w, zero := hv } ∧ CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl a = CategoryTheory.CategoryStruct.comp aX S.f ∧ CategoryTheory.CategoryStruct.comp a S.g = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.snd aZ ∧ CategoryTheory.CategoryStruct.comp v u = CategoryTheory.CategoryStruct.comp mX CategoryTheory.Limits.biprod.inl ∧ CategoryTheory.CategoryStruct.comp u CategoryTheory.Limits.biprod.snd = CategoryTheory.CategoryStruct.comp w mZ

The horseshoe lemma. Let S : X ↪ Y ↠ Z be a conflation and let K_X ↪ Q_X ↠ X and K_Z ↪ Q_Z ↠ Z be conflations resolving its two outer terms, with Q_Z projective. Then Y is the third term of a conflation whose middle term is Q_X ⊞ Q_Z and whose first term is an extension of K_Z by K_X.

The two conflations form a horseshoe over the given one: the new deflation a restricts on the first summand to Q_X ↠ X ↪ Y and covers Q_Z ↠ Z on the second, while the new inflation u restricts on K_X to K_X ↪ Q_X ↪ Q_X ⊞ Q_Z and covers K_Z ↪ Q_Z on the second summand.

Iterating this is what lifts resolutions of X and of Z to a resolution of Y; see TauCeti.ExactStructure.exists_finiteResolution_length_le_of_conflation.

theorem TauCeti.ExactStructure.isExtensionClosed_of_le_isProjective {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} {P : CategoryTheory.ObjectProperty C} [P.IsClosedUnderIsomorphisms] [P.IsClosedUnderBinaryProducts] (hP : P ≤ E.isProjective) : E.IsExtensionClosed P

A property consisting of projectives is extension closed, as soon as it is replete and closed under binary biproducts: a conflation whose third term is projective splits, so its middle term is the biproduct of the two outer ones.

Together with TauCeti.ExactStructure.fullSubcategory this equips the objects satisfying P with an induced exact structure — necessarily the split one, by TauCeti.ExactStructure.fullSubcategory_eq_split.

theorem TauCeti.ExactStructure.instIsClosedUnderIsomorphismsOfContainsZeroOfIsClosedUnderBinaryProducts {C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.ObjectProperty C} [P.ContainsZero] [P.IsClosedUnderBinaryProducts] : P.IsClosedUnderIsomorphisms

A property containing a zero object and closed under binary products is automatically replete, by CategoryTheory.ObjectProperty.isClosedUnderIsomorphisms_of_containsZero; so the results below need no separate repleteness hypothesis, even though the resolution API they call does.

theorem TauCeti.ExactStructure.fullSubcategory_eq_split {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} {P : CategoryTheory.ObjectProperty C} [P.ContainsZero] [P.IsClosedUnderBinaryProducts] (hP : P ≤ E.isProjective) : fullSubcategory P ⋯ = split P.FullSubcategory

The exact structure induced on a subcategory of projectives is the split one.

theorem TauCeti.ExactStructure.exists_finiteResolution_length_le_of_conflation {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} {P : CategoryTheory.ObjectProperty C} [P.ContainsZero] [P.IsClosedUnderBinaryProducts] (hP : P ≤ E.isProjective) (n : ℕ) {S : CategoryTheory.ShortComplex C} (hS : E.Conflation S) (h₁ : ∃ (r : E.FiniteResolution P S.X₁), r.length ≤ n) (h₃ : ∃ (t : E.FiniteResolution P S.X₃), t.length ≤ n) : ∃ (u : E.FiniteResolution P S.X₂), u.length ≤ n

Finite resolutions by projectives lift along a conflation. If P consists of E-projectives, contains a zero object and is closed under binary biproducts, and both outer terms of a conflation admit a finite P-resolution of length at most n, then so does its middle term.

This is the horseshoe lemma, iterated: at each stage the two resolving terms are added, and the new syzygy is an extension of the two old ones.

theorem TauCeti.ExactStructure.isExtensionClosed_admitsFiniteResolution {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} {P : CategoryTheory.ObjectProperty C} [P.ContainsZero] [P.IsClosedUnderBinaryProducts] (hP : P ≤ E.isProjective) : E.IsExtensionClosed (E.admitsFiniteResolution P)

The objects of finite P-dimension are extension closed, for an object property P consisting of E-projectives which contains a zero object and is closed under binary biproducts. The middle term of a conflation is covered by TauCeti.ExactStructure.IsExtensionClosed.prop_X₂.

Together with TauCeti.ExactStructure.fullSubcategory this equips them with an induced exact structure, in which the resolution theorem compares their Grothendieck group with the one generated by the objects satisfying P.