Resolving subcategories of exact categories

Let E be an exact structure on an additive category C. An object property P is resolving for E when it contains a zero object, is closed under binary direct sums and extensions, is closed under kernels of deflations between P-objects, and every object of C admits a finite P-resolution.

This file packages those hypotheses as TauCeti.ExactStructure.IsResolving. The full subcategory on a resolving property inherits the exact structure induced from E; its inclusion preserves and reflects conflations. These are the exact-category data used by the general resolution theorem. Repleteness is derived from zero and binary-product closure rather than stored as a redundant field.

The property of all objects is resolving. More substantially, the relatively projective objects are resolving whenever every object admits a finite projective resolution. For the latter example, kernel closure follows because a conflation with projective quotient splits, making its kernel a retract of the projective middle term.

Finally, the resolving hypotheses control P-dimension along conflations with a resolving term. The proofs use only pullbacks of deflations and the Noether conflation of a composite deflation, never a splitting, and are what make the Euler class of a finite resolution well defined in TauCeti/CategoryTheory/GrothendieckGroup/Resolving.lean.

Main definitions

• TauCeti.ExactStructure.IsResolving: the resolving hypotheses for an object property.
• TauCeti.ExactStructure.resolvingSubcategory: the induced exact structure on the full subcategory.

Main results

• TauCeti.ExactStructure.IsResolving.prop_X₁: closure under kernels of admissible deflations.
• TauCeti.ExactStructure.IsResolving.isConflationExact_ι and TauCeti.ExactStructure.IsResolving.reflectsConflations_ι: the inclusion preserves and reflects conflations.
• TauCeti.ExactStructure.isResolving_top: the full category is resolving.
• TauCeti.ExactStructure.isResolving_isProjective: finite projective resolutions make the relatively projective objects a resolving subcategory.
• TauCeti.ExactStructure.IsResolving.exists_finiteResolution_X₁_length_le_of_prop_X₂: dimension shifting. If K ↪ Q ↠ X is a conflation with Q resolving and X has P-dimension at most n + 1, then K has P-dimension at most n.
• TauCeti.ExactStructure.IsResolving.exists_finiteResolution_X₂_length_le_of_prop_X₃ and TauCeti.ExactStructure.IsResolving.exists_finiteResolution_X₁_length_le_of_prop_X₃: extensions of a resolving object, and kernels of deflations onto one, do not raise P-dimension.

References

• Charles A. Weibel, The K-book: An Introduction to Algebraic K-theory, Chapter II, Section 7, especially Theorem II.7.6.

class TauCeti.ExactStructure.IsResolving {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) extends P.ContainsZero, P.IsClosedUnderLimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) : Prop

An object property is resolving for an exact structure when it is additive and extension closed, is closed under kernels of deflations between its objects, and gives a finite resolution of every ambient object.

The first two fields imply that P is closed under isomorphisms, so repleteness is exposed as a derived theorem rather than duplicated in the structure.

• exists_zero : ∃ (Z : C), Limits.IsZero Z ∧ P Z
• limitsOfShape_le : P.limitsOfShape (Discrete Limits.WalkingPair) ≤ P
• isExtensionClosed : E.IsExtensionClosed P

  Extensions of two resolving objects are resolving.

• prop_X₁ {S : CategoryTheory.ShortComplex C} (hS : E.Conflation S) (h₂ : P S.X₂) (h₃ : P S.X₃) : P S.X₁

  The kernel term of a conflation is resolving when its middle and quotient terms are.

• finiteResolution (X : C) : E.admitsFiniteResolution P X

  Every object admits a finite resolution by resolving objects.

@[reducible, inline]

noncomputable abbrev TauCeti.ExactStructure.resolvingSubcategory {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) [E.IsResolving P] : ExactStructure P.FullSubcategory

The exact structure on the full subcategory of resolving objects induced from the ambient exact structure. Its conflations are precisely the ambient conflations whose three terms satisfy P. It is by definition TauCeti.ExactStructure.fullSubcategory, so the Grothendieck-group API of induced structures applies to it unchanged.

Equations

• E.resolvingSubcategory P = TauCeti.ExactStructure.fullSubcategory P ⋯

theorem TauCeti.ExactStructure.IsResolving.isConflationExact_ι {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) [E.IsResolving P] : (E.resolvingSubcategory P).IsConflationExact E P.ι

The inclusion of a resolving subcategory preserves conflations.

theorem TauCeti.ExactStructure.IsResolving.reflectsConflations_ι {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) [E.IsResolving P] : (E.resolvingSubcategory P).ReflectsConflations E P.ι

The inclusion of a resolving subcategory reflects conflations.

instance TauCeti.ExactStructure.isResolving_top {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] (E : ExactStructure C) : E.IsResolving ⊤

The property of all objects is resolving for every exact structure.

theorem TauCeti.ExactStructure.isResolving_isProjective {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] (E : ExactStructure C) (hfinite : ∀ (X : C), E.admitsFiniteResolution E.isProjective X) : E.IsResolving E.isProjective

If every object admits a finite resolution by relative projectives, then the relative projectives form a resolving subcategory.

Extension closure follows because an extension with projective quotient splits. For kernel closure, a conflation with projective quotient identifies its middle term with the biproduct of its kernel and quotient; hence the kernel is a retract of the projective middle term.

theorem TauCeti.ExactStructure.IsResolving.exists_finiteResolution_X₂_length_le_of_prop_X₃ {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} [E.IsResolving P] {n : ℕ} {S : CategoryTheory.ShortComplex C} (hS : E.Conflation S) (h₃ : P S.X₃) (h₁ : ∃ (r : E.FiniteResolution P S.X₁), r.length ≤ n) : ∃ (r : E.FiniteResolution P S.X₂), r.length ≤ n

An extension of an object of P by an object of P-dimension at most n has P-dimension at most n.

theorem TauCeti.ExactStructure.IsResolving.exists_finiteResolution_X₁_length_le_of_prop_X₂ {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} [E.IsResolving P] {n : ℕ} {S : CategoryTheory.ShortComplex C} (hS : E.Conflation S) (h₂ : P S.X₂) (h₃ : ∃ (r : E.FiniteResolution P S.X₃), r.length ≤ n + 1) : ∃ (r : E.FiniteResolution P S.X₁), r.length ≤ n

Dimension shifting. If K ↪ Q ↠ X is a conflation with Q in the resolving subcategory and X has P-dimension at most n + 1, then K has P-dimension at most n, whichever first step Q ↠ X is chosen.