The Euler class of a finite resolution

For a finite P-resolution of an object X of an exact category, the Euler class is the alternating sum

[Q₀] - [Q₁] + ⋯ + (-1)ⁿ⁻¹ [Qₙ₋₁] + (-1)ⁿ [Kₙ]

of the classes of its resolving terms and its last syzygy in exact K₀. The conflation relation telescopes the alternating sum, so the Euler class of a resolution of X is [X]. This is the computation that makes the Euler class independent of the chosen resolution -- of its length, of zero padding, and of every other choice -- and it is the first half of Weibel's resolution theorem: it exhibits [X] as an integral combination of classes of objects satisfying P, so those classes generate exact K₀ as soon as every object admits a finite P-resolution.

For a property consisting of projectives, the second half — injectivity of the comparison map from the exact K₀ of the full subcategory on P — is proved by Schanuel's and the horseshoe lemmas in TauCeti/CategoryTheory/GrothendieckGroup/ProjectiveResolution.lean; see TauCeti.ExactStructure.resolutionEquiv. For a resolving subcategory it is proved with pullbacks of deflations and dimension shifting in TauCeti/CategoryTheory/GrothendieckGroup/Resolving.lean; see TauCeti.ExactStructure.IsResolving.resolutionEquiv.

The class of an object itself, as opposed to that of a resolution, is defined here by choosing one of its finite P-resolutions; each of those two files removes the choice from its own independence theorem.

Main definitions

• TauCeti.ExactStructure.FiniteResolution.eulerClass: the alternating class of a finite resolution in ambient exact K₀.
• TauCeti.ExactStructure.FiniteResolution.eulerClassFullSubcategory: the alternating class in the exact K₀ of an extension-closed full subcategory containing the resolution terms.
• TauCeti.ExactStructure.eulerClassOf: the alternating class, in that same K₀, of a chosen finite P-resolution of an object admitting one.

Main results

• TauCeti.ExactStructure.FiniteResolution.eulerClass_eq_of: the Euler class of a resolution of X is the class of X; TauCeti.ExactStructure.FiniteResolution.eulerClass_eq_eulerClass is the resulting independence of the resolution.
• TauCeti.ExactStructure.eulerClassOf_eq_of_forall_eulerClassFullSubcategory_eq: a resolution whose alternating class is shared by every finite P-resolution of the same object computes TauCeti.ExactStructure.eulerClassOf.
• TauCeti.ExactStructure.FiniteResolution.eulerClassFullSubcategory_map: the Euler class of the image of a finite resolution under a conflation-exact functor is the alternating sum of the classes of the images of its terms.
• TauCeti.ExactK0.mem_propClasses_iff: membership in the generator set propClasses E P is being the class of an object satisfying P.
• TauCeti.ExactK0.closure_propClasses_eq_top: if every object admits a finite P-resolution, the classes of the objects satisfying P generate exact K₀.

References

• Charles A. Weibel, The K-book: An Introduction to Algebraic K-theory, Chapter II, Theorem 7.6 and Lemma 7.6.1, the resolution theorem and the telescoping computation of the Euler class used here.

noncomputable def TauCeti.ExactStructure.FiniteResolution.eulerClass {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} [CategoryTheory.EssentiallySmall.{w, v, u} C] {X : C} : E.FiniteResolution P X → ExactK0 E

The Euler class of a finite P-resolution: the alternating sum of the classes of its resolving terms, ending with the class of its last syzygy.

Equations

• (TauCeti.ExactStructure.FiniteResolution.base hX).eulerClass = TauCeti.ExactK0.of x✝
• (TauCeti.ExactStructure.FiniteResolution.step hQ i p zero hp r).eulerClass = TauCeti.ExactK0.of Q - r.eulerClass

@[simp]

theorem TauCeti.ExactStructure.FiniteResolution.eulerClass_base {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} [CategoryTheory.EssentiallySmall.{w, v, u} C] {X : C} (hX : P X) : (base hX).eulerClass = ExactK0.of X

@[simp]

theorem TauCeti.ExactStructure.FiniteResolution.eulerClass_step {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} [CategoryTheory.EssentiallySmall.{w, v, u} C] {K Q X : C} (hQ : P Q) (i : K ⟶ Q) (p : Q ⟶ X) (zero : CategoryTheory.CategoryStruct.comp i p = 0) (hp : E.Conflation { X₁ := K, X₂ := Q, X₃ := X, f := i, g := p, zero := zero }) (r : E.FiniteResolution P K) : (step hQ i p zero hp r).eulerClass = ExactK0.of Q - r.eulerClass

theorem TauCeti.ExactStructure.FiniteResolution.eulerClass_eq_of {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} [CategoryTheory.EssentiallySmall.{w, v, u} C] {X : C} (r : E.FiniteResolution P X) : r.eulerClass = ExactK0.of X

The Euler class of a resolution of X is the class of X. The conflation relation telescopes the alternating sum.

theorem TauCeti.ExactStructure.FiniteResolution.eulerClass_eq_eulerClass {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} [CategoryTheory.EssentiallySmall.{w, v, u} C] {X : C} (r s : E.FiniteResolution P X) : r.eulerClass = s.eulerClass

The Euler class does not depend on the resolution: any two finite P-resolutions of the same object have the same Euler class, whatever their lengths.

@[simp]

theorem TauCeti.ExactStructure.FiniteResolution.eulerClass_ofIso {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} [CategoryTheory.EssentiallySmall.{w, v, u} C] [P.IsClosedUnderIsomorphisms] {X Y : C} (e : X ≅ Y) (r : E.FiniteResolution P X) : (ofIso e r).eulerClass = r.eulerClass

@[simp]

theorem TauCeti.ExactStructure.FiniteResolution.eulerClass_zeroPad {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} [CategoryTheory.EssentiallySmall.{w, v, u} C] [P.IsClosedUnderIsomorphisms] [P.ContainsZero] {X : C} (r : E.FiniteResolution P X) : r.zeroPad.eulerClass = r.eulerClass

@[simp]

theorem TauCeti.ExactStructure.FiniteResolution.eulerClass_pad {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} [CategoryTheory.EssentiallySmall.{w, v, u} C] [P.IsClosedUnderIsomorphisms] [P.ContainsZero] {X : C} (r : E.FiniteResolution P X) (n : ℕ) : (r.pad n).eulerClass = r.eulerClass

@[simp]

theorem TauCeti.ExactStructure.FiniteResolution.eulerClass_biprod {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} [CategoryTheory.EssentiallySmall.{w, v, u} C] [P.IsClosedUnderIsomorphisms] [P.IsClosedUnderBinaryProducts] {X Y : C} (r : E.FiniteResolution P X) (s : E.FiniteResolution P Y) : (r.biprod s).eulerClass = r.eulerClass + s.eulerClass

theorem TauCeti.ExactStructure.FiniteResolution.instIsClosedUnderIsomorphisms {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.

noncomputable def TauCeti.ExactStructure.FiniteResolution.eulerClassFullSubcategory {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} [CategoryTheory.LocallySmall.{w, v, u} C] [CategoryTheory.ObjectProperty.EssentiallySmall.{w, v, u} P] [P.ContainsZero] [P.IsClosedUnderBinaryProducts] (hP : E.IsExtensionClosed P) {X : C} : E.FiniteResolution P X → ExactK0 (fullSubcategory P hP)

The Euler class of a finite P-resolution in the K₀ of the full subcategory on P: the alternating sum [Q₀] - [Q₁] + ⋯ + (-1)ⁿ [Kₙ] of the classes of its resolving terms and its last syzygy, all of which satisfy P, formed in the exact K₀ of the exact structure induced on the full subcategory on P.

Unlike TauCeti.ExactStructure.FiniteResolution.eulerClass, which lives in the K₀ of the ambient category and telescopes to [X], this class carries genuine information: nothing in the subcategory relates it to X. When P consists of projectives, its independence of the chosen resolution is TauCeti.ExactStructure.FiniteResolution.eulerClassFullSubcategory_eq_eulerClassFullSubcategory.

Equations

• One or more equations did not get rendered due to their size.
• TauCeti.ExactStructure.FiniteResolution.eulerClassFullSubcategory hP (TauCeti.ExactStructure.FiniteResolution.base hX) = TauCeti.ExactK0.of { obj := x✝, property := hX }

@[simp]

theorem TauCeti.ExactStructure.FiniteResolution.eulerClassFullSubcategory_base {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} [CategoryTheory.LocallySmall.{w, v, u} C] [CategoryTheory.ObjectProperty.EssentiallySmall.{w, v, u} P] [P.ContainsZero] [P.IsClosedUnderBinaryProducts] (hP : E.IsExtensionClosed P) {X : C} (hX : P X) : eulerClassFullSubcategory hP (base hX) = ExactK0.of { obj := X, property := hX }

@[simp]

theorem TauCeti.ExactStructure.FiniteResolution.eulerClassFullSubcategory_step {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} [CategoryTheory.LocallySmall.{w, v, u} C] [CategoryTheory.ObjectProperty.EssentiallySmall.{w, v, u} P] [P.ContainsZero] [P.IsClosedUnderBinaryProducts] (hP : E.IsExtensionClosed P) {K Q X : C} (hQ : P Q) (i : K ⟶ Q) (p : Q ⟶ X) (zero : CategoryTheory.CategoryStruct.comp i p = 0) (hp : E.Conflation { X₁ := K, X₂ := Q, X₃ := X, f := i, g := p, zero := zero }) (r : E.FiniteResolution P K) : eulerClassFullSubcategory hP (step hQ i p zero hp r) = ExactK0.of { obj := Q, property := hQ } - eulerClassFullSubcategory hP r

@[simp]

theorem TauCeti.ExactStructure.FiniteResolution.eulerClassFullSubcategory_ofIso {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} [CategoryTheory.LocallySmall.{w, v, u} C] [CategoryTheory.ObjectProperty.EssentiallySmall.{w, v, u} P] [P.ContainsZero] [P.IsClosedUnderBinaryProducts] (hP : E.IsExtensionClosed P) {X Y : C} (e : X ≅ Y) (r : E.FiniteResolution P X) : eulerClassFullSubcategory hP (ofIso e r) = eulerClassFullSubcategory hP r

@[simp]

theorem TauCeti.ExactStructure.FiniteResolution.eulerClassFullSubcategory_zeroPad {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} [CategoryTheory.LocallySmall.{w, v, u} C] [CategoryTheory.ObjectProperty.EssentiallySmall.{w, v, u} P] [P.ContainsZero] [P.IsClosedUnderBinaryProducts] (hP : E.IsExtensionClosed P) {X : C} (r : E.FiniteResolution P X) : eulerClassFullSubcategory hP r.zeroPad = eulerClassFullSubcategory hP r

Padding a finite resolution by one trivial conflation does not change its Euler class.

@[simp]

theorem TauCeti.ExactStructure.FiniteResolution.eulerClassFullSubcategory_pad {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} [CategoryTheory.LocallySmall.{w, v, u} C] [CategoryTheory.ObjectProperty.EssentiallySmall.{w, v, u} P] [P.ContainsZero] [P.IsClosedUnderBinaryProducts] (hP : E.IsExtensionClosed P) {X : C} (r : E.FiniteResolution P X) (n : ℕ) : eulerClassFullSubcategory hP (r.pad n) = eulerClassFullSubcategory hP r

Padding a finite resolution by any number of trivial conflations does not change its Euler class.

@[simp]

theorem TauCeti.ExactStructure.FiniteResolution.eulerClassFullSubcategory_biprod {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} [CategoryTheory.LocallySmall.{w, v, u} C] [CategoryTheory.ObjectProperty.EssentiallySmall.{w, v, u} P] [P.ContainsZero] [P.IsClosedUnderBinaryProducts] (hP : E.IsExtensionClosed P) {X Y : C} (r : E.FiniteResolution P X) (s : E.FiniteResolution P Y) : eulerClassFullSubcategory hP (r.biprod s) = eulerClassFullSubcategory hP r + eulerClassFullSubcategory hP s

@[simp]

theorem TauCeti.ExactStructure.FiniteResolution.map_eulerClassFullSubcategory {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} [CategoryTheory.LocallySmall.{w, v, u} C] [CategoryTheory.ObjectProperty.EssentiallySmall.{w, v, u} P] [P.ContainsZero] [P.IsClosedUnderBinaryProducts] (hP : E.IsExtensionClosed P) [CategoryTheory.EssentiallySmall.{w, v, u} C] {X : C} (r : E.FiniteResolution P X) : (ExactK0.map P.ι ⋯) (eulerClassFullSubcategory hP r) = r.eulerClass

Mapping the Euler class of a finite resolution along the full-subcategory inclusion gives its Euler class in the ambient exact Grothendieck group.

theorem TauCeti.ExactStructure.FiniteResolution.eulerClassFullSubcategory_map {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} {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] [CategoryTheory.LocallySmall.{w', v', u'} D] {E' : ExactStructure D} {P' : CategoryTheory.ObjectProperty D} [CategoryTheory.ObjectProperty.EssentiallySmall.{w', v', u'} P'] [P'.ContainsZero] [P'.IsClosedUnderBinaryProducts] {F : CategoryTheory.Functor C D} [F.Additive] {X : C} (hP' : E'.IsExtensionClosed P') (hF : E.IsConflationExact E' F) (hPP' : P ≤ P'.inverseImage F) (r : E.FiniteResolution P X) : eulerClassFullSubcategory hP' (map hF hPP' r) = foldAlternating (fun (Z : C) (hZ : P Z) => ExactK0.of { obj := F.obj Z, property := ⋯ }) r

The Euler class of an image resolution. Applying a conflation-exact functor carrying P into P' to a finite P-resolution gives a finite P'-resolution whose Euler class is the alternating sum of the classes of the images of the terms.

theorem TauCeti.ExactStructure.instIsClosedUnderIsomorphisms {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.

noncomputable def TauCeti.ExactStructure.eulerClassOf {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} [CategoryTheory.LocallySmall.{w, v, u} C] [CategoryTheory.ObjectProperty.EssentiallySmall.{w, v, u} P] [P.ContainsZero] [P.IsClosedUnderBinaryProducts] (hP : E.IsExtensionClosed P) {X : C} (hX : E.admitsFiniteResolution P X) : ExactK0 (fullSubcategory P hP)

The Euler class of an object of finite P-dimension, in the exact K₀ of the structure induced on the full subcategory on P: the alternating class of some, hence when P consists of E-projectives, by TauCeti.ExactStructure.eulerClassOf_eq, or when P is resolving, by TauCeti.ExactStructure.IsResolving.eulerClassOf_eq, of any, finite P-resolution of it.

Equations

• TauCeti.ExactStructure.eulerClassOf hP hX = TauCeti.ExactStructure.FiniteResolution.eulerClassFullSubcategory hP ⋯.some

theorem TauCeti.ExactStructure.eulerClassOf_eq_of_forall_eulerClassFullSubcategory_eq {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} [CategoryTheory.LocallySmall.{w, v, u} C] [CategoryTheory.ObjectProperty.EssentiallySmall.{w, v, u} P] [P.ContainsZero] [P.IsClosedUnderBinaryProducts] (hP : E.IsExtensionClosed P) {X : C} (hX : E.admitsFiniteResolution P X) (r : E.FiniteResolution P X) (h : ∀ (s : E.FiniteResolution P X), FiniteResolution.eulerClassFullSubcategory hP s = FiniteResolution.eulerClassFullSubcategory hP r) : eulerClassOf hP hX = FiniteResolution.eulerClassFullSubcategory hP r

If every finite P-resolution of X has the same alternating class as the resolution r, then r computes TauCeti.ExactStructure.eulerClassOf.

def TauCeti.ExactK0.propClasses {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) [CategoryTheory.EssentiallySmall.{w, v, u} C] : Set (ExactK0 E)

The classes of the objects satisfying P, as a subset of exact K₀.

Equations

• TauCeti.ExactK0.propClasses E P = TauCeti.ExactK0.of '' {X : C | P X}

@[simp]

theorem TauCeti.ExactK0.mem_propClasses_iff {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} [CategoryTheory.EssentiallySmall.{w, v, u} C] {x : ExactK0 E} : x ∈ propClasses E P ↔ ∃ (Q : C), P Q ∧ of Q = x

Membership in the generator set propClasses E P: an element of exact K₀ lies in it exactly when it is the class of an object satisfying P.

theorem TauCeti.ExactK0.of_mem_propClasses {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} [CategoryTheory.EssentiallySmall.{w, v, u} C] {Q : C} (hQ : P Q) : of Q ∈ propClasses E P

The class of an object satisfying P is one of the generators propClasses E P.

theorem TauCeti.ExactK0.of_mem_closure_propClasses {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} [CategoryTheory.EssentiallySmall.{w, v, u} C] {X : C} (hX : E.admitsFiniteResolution P X) : of X ∈ AddSubgroup.closure (propClasses E P)

The class of an object admitting a finite P-resolution is an integral combination of classes of objects satisfying P.

theorem TauCeti.ExactK0.closure_propClasses_eq_top {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) [CategoryTheory.EssentiallySmall.{w, v, u} C] (h : ∀ (X : C), E.admitsFiniteResolution P X) : AddSubgroup.closure (propClasses E P) = ⊤

The generating half of the resolution theorem. If every object of C admits a finite P-resolution, then the classes of the objects satisfying P generate exact K₀.