The resolution theorem for a resolving subcategory

Let E be an exact structure on an additive category C and let P be a resolving property: it contains a zero object, is closed under binary direct sums and extensions, is closed under kernels of deflations between its objects, and every object of C admits a finite P-resolution. This file proves Weibel's resolution theorem in this generality: the inclusion of the full subcategory on P, with its induced exact structure, induces an isomorphism

K₀(P) ≃ K₀(C)

whose inverse sends the class of an object X to the alternating class [Q₀] - [Q₁] + ⋯ + (-1)ⁿ [Kₙ] of any finite P-resolution of X, computed in K₀(P).

Unlike the projective case of TauCeti/CategoryTheory/GrothendieckGroup/ProjectiveResolution.lean, conflations with a resolving quotient need not split, so neither Schanuel's lemma nor the horseshoe lemma is available. Both are replaced by pullbacks of deflations and the Noether conflation TauCeti.ExactStructure.exists_conflation_comp': two first steps K ↪ Q ↠ X and K' ↪ Q' ↠ X are compared through a single object Q'' of P covering their pullback, and the dimension shifting of TauCeti.ExactStructure.IsResolving.exists_finiteResolution_X₁_length_le_of_prop_X₂ keeps the inductions on lengths well founded.

Main results

• TauCeti.ExactStructure.IsResolving.eulerClassFullSubcategory_eq_eulerClassFullSubcategory: the alternating class of a finite P-resolution in K₀(P) depends only on the resolved object.
• TauCeti.ExactStructure.IsResolving.eulerClassOf_eq_add_of_conflation: the Euler class is additive on the conflations of C.
• TauCeti.ExactStructure.IsResolving.resolutionEquiv, TauCeti.ExactStructure.IsResolving.resolutionEquiv_of and TauCeti.ExactStructure.IsResolving.resolutionEquiv_symm_of: the resolution theorem.
• TauCeti.ExactStructure.IsResolving.map_comp_resolutionEquiv and TauCeti.ExactStructure.IsResolving.map_comp_resolutionEquiv_symm: naturality of the resolution theorem in a conflation-exact functor preserving the resolving properties.
• TauCeti.ExactStructure.IsResolving.mapEquiv_comp_resolutionEquiv: invariance of the resolution theorem under an exact equivalence identifying the resolving properties.

Implementation notes

The Euler class of an object is TauCeti.ExactStructure.eulerClassOf, with values in the exact K₀ of TauCeti.ExactStructure.fullSubcategory; the exact structure TauCeti.ExactStructure.resolvingSubcategory is by definition that induced structure, which is how the two are identified in the statement of the resolution theorem.

Well-definedness is proved by induction on the length of one of the two resolutions, and additivity by induction on the length of a resolution of the quotient term; both are stated as private auxiliaries over an explicit bound.

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 independence of the Euler class.
• Theo Bühler, Exact categories, Expositiones Mathematicae 28 (2010), 1--69, Proposition 2.12 and Lemma 3.5, for base change of conflations and the Noether conflation.

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

The Euler class in the K₀ of a resolving subcategory depends only on the resolved object. Any two finite P-resolutions of the same object have the same alternating class in the exact K₀ of the structure induced on P, whatever their lengths.

theorem TauCeti.ExactStructure.IsResolving.eulerClassOf_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} [E.IsResolving P] [CategoryTheory.LocallySmall.{w, v, u} C] [CategoryTheory.ObjectProperty.EssentiallySmall.{w, v, u} P] {X : C} (hX : E.admitsFiniteResolution P X) (r : E.FiniteResolution P X) : eulerClassOf ⋯ hX = FiniteResolution.eulerClassFullSubcategory ⋯ r

Every finite P-resolution of X computes TauCeti.ExactStructure.eulerClassOf.

@[simp]

theorem TauCeti.ExactStructure.IsResolving.eulerClassOf_of_prop {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] [CategoryTheory.LocallySmall.{w, v, u} C] [CategoryTheory.ObjectProperty.EssentiallySmall.{w, v, u} P] {X : C} (hX : P X) (h : E.admitsFiniteResolution P X) : eulerClassOf ⋯ h = ExactK0.of { obj := X, property := hX }

On an object satisfying P the Euler class is the class of that object.

theorem TauCeti.ExactStructure.IsResolving.eulerClassOf_eq_sub_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} [E.IsResolving P] [CategoryTheory.LocallySmall.{w, v, u} C] [CategoryTheory.ObjectProperty.EssentiallySmall.{w, v, u} 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 }) (hK : E.admitsFiniteResolution P K) (hX : E.admitsFiniteResolution P X) : eulerClassOf ⋯ hX = ExactK0.of { obj := Q, property := hQ } - eulerClassOf ⋯ hK

The Euler class drops by one step along a conflation with resolving middle term: χ(X) = [Q] - χ(K) for a conflation K ↪ Q ↠ X with P Q.

theorem TauCeti.ExactStructure.IsResolving.eulerClassOf_congr {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] [CategoryTheory.LocallySmall.{w, v, u} C] [CategoryTheory.ObjectProperty.EssentiallySmall.{w, v, u} P] {X Y : C} (e : X ≅ Y) (hX : E.admitsFiniteResolution P X) (hY : E.admitsFiniteResolution P Y) : eulerClassOf ⋯ hX = eulerClassOf ⋯ hY

The Euler class is invariant under isomorphism of the resolved object.

theorem TauCeti.ExactStructure.IsResolving.eulerClassOf_eq_add_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} [E.IsResolving P] [CategoryTheory.LocallySmall.{w, v, u} C] [CategoryTheory.ObjectProperty.EssentiallySmall.{w, v, u} P] {S : CategoryTheory.ShortComplex C} (hS : E.Conflation S) (a₁ : E.admitsFiniteResolution P S.X₁) (a₂ : E.admitsFiniteResolution P S.X₂) (a₃ : E.admitsFiniteResolution P S.X₃) : eulerClassOf ⋯ a₂ = eulerClassOf ⋯ a₁ + eulerClassOf ⋯ a₃

The Euler class is additive on conflations. Together with TauCeti.ExactStructure.IsResolving.eulerClassOf_eq it makes the alternating class of a finite P-resolution a conflation-additive invariant of the objects of C.

theorem TauCeti.ExactStructure.IsResolving.instEssentiallySmall {C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.ObjectProperty C} [CategoryTheory.EssentiallySmall.{w, v, u} C] : CategoryTheory.ObjectProperty.EssentiallySmall.{w, v, u} P

A property of an essentially small category is essentially small.

noncomputable def TauCeti.ExactStructure.IsResolving.eulerHom {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] [CategoryTheory.EssentiallySmall.{w, v, u} C] : ExactK0 E →+ ExactK0 (E.resolvingSubcategory P)

The inverse of the comparison map of the resolution theorem: the homomorphism sending the class of an object to the alternating class of any of its finite P-resolutions.

Equations

• TauCeti.ExactStructure.IsResolving.eulerHom E P = TauCeti.ExactK0.lift (TauCeti.ExactStructure.IsResolving.eulerInvariant✝ E P)

@[simp]

theorem TauCeti.ExactStructure.IsResolving.eulerHom_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) [E.IsResolving P] [CategoryTheory.EssentiallySmall.{w, v, u} C] (X : C) : (eulerHom E P) (ExactK0.of X) = eulerClassOf ⋯ ⋯

noncomputable def TauCeti.ExactStructure.IsResolving.resolutionEquiv {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] [CategoryTheory.EssentiallySmall.{w, v, u} C] : ExactK0 (E.resolvingSubcategory P) ≃+ ExactK0 E

The resolution theorem. For a resolving property P of an exact category, the inclusion of the full subcategory on P induces an isomorphism of exact Grothendieck groups. Its inverse sends the class of an object to the alternating class of any finite P-resolution of it, by TauCeti.ExactStructure.IsResolving.resolutionEquiv_symm_of.

Equations

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

@[simp]

theorem TauCeti.ExactStructure.IsResolving.resolutionEquiv_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) [E.IsResolving P] [CategoryTheory.EssentiallySmall.{w, v, u} C] (X : P.FullSubcategory) : (resolutionEquiv E P) (ExactK0.of X) = ExactK0.of X.obj

The forward map of the resolution theorem sends a P-object to its class in K₀(C).

@[simp]

theorem TauCeti.ExactStructure.IsResolving.resolutionEquiv_symm_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) [E.IsResolving P] [CategoryTheory.EssentiallySmall.{w, v, u} C] (X : C) : (resolutionEquiv E P).symm (ExactK0.of X) = eulerClassOf ⋯ ⋯

The inverse map of the resolution theorem sends an object class to its Euler class.

theorem TauCeti.ExactStructure.IsResolving.map_comp_resolutionEquiv {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] [CategoryTheory.EssentiallySmall.{w, v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] [CategoryTheory.EssentiallySmall.{w', v', u'} D] {E' : ExactStructure D} {P' : CategoryTheory.ObjectProperty D} [E'.IsResolving P'] (F : CategoryTheory.Functor C D) [F.Additive] (hF : E.IsConflationExact E' F) (hPP' : ∀ (X : P.FullSubcategory), P' (F.obj X.obj)) : (ExactK0.map F hF).comp (resolutionEquiv E P).toAddMonoidHom = (resolutionEquiv E' P').toAddMonoidHom.comp (ExactK0.map (P'.lift (P.ι.comp F) hPP') ⋯)

Naturality of the resolution theorem. A conflation-exact functor carrying the resolving property P into P' commutes with the comparison from the exact K₀ of the resolving subcategory to the ambient exact K₀.

theorem TauCeti.ExactStructure.IsResolving.map_comp_resolutionEquiv_symm {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] [CategoryTheory.EssentiallySmall.{w, v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] [CategoryTheory.EssentiallySmall.{w', v', u'} D] {E' : ExactStructure D} {P' : CategoryTheory.ObjectProperty D} [E'.IsResolving P'] (F : CategoryTheory.Functor C D) [F.Additive] (hF : E.IsConflationExact E' F) (hPP' : ∀ (X : P.FullSubcategory), P' (F.obj X.obj)) : (ExactK0.map (P'.lift (P.ι.comp F) hPP') ⋯).comp (resolutionEquiv E P).symm.toAddMonoidHom = (resolutionEquiv E' P').symm.toAddMonoidHom.comp (ExactK0.map F hF)

The inverse maps in the resolution theorem are natural: applying a functor to the Euler class of a finite resolution gives the Euler class after applying the functor.

@[simp]

theorem TauCeti.ExactStructure.IsResolving.map_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} [E.IsResolving P] [CategoryTheory.EssentiallySmall.{w, v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] [CategoryTheory.EssentiallySmall.{w', v', u'} D] {E' : ExactStructure D} {P' : CategoryTheory.ObjectProperty D} [E'.IsResolving P'] (F : CategoryTheory.Functor C D) [F.Additive] (hF : E.IsConflationExact E' F) (hPP' : ∀ (X : P.FullSubcategory), P' (F.obj X.obj)) (X : C) : (ExactK0.map (P'.lift (P.ι.comp F) hPP') ⋯) (eulerClassOf ⋯ ⋯) = eulerClassOf ⋯ ⋯

Applying a conflation-exact functor preserving resolving objects carries the Euler class of an object to the Euler class of its image.

theorem TauCeti.ExactStructure.IsResolving.instIsClosedUnderIsomorphismsOfContainsZeroOfIsClosedUnderBinaryProducts {D : Type u'} [CategoryTheory.Category.{v', u'} D] (Q : CategoryTheory.ObjectProperty D) [Q.ContainsZero] [Q.IsClosedUnderBinaryProducts] : Q.IsClosedUnderIsomorphisms

theorem TauCeti.ExactStructure.IsResolving.mapEquiv_comp_resolutionEquiv {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] [CategoryTheory.EssentiallySmall.{w, v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] [CategoryTheory.EssentiallySmall.{w', v', u'} D] {E' : ExactStructure D} {P' : CategoryTheory.ObjectProperty D} [E'.IsResolving P'] (e : C ≌ D) [e.functor.Additive] [e.inverse.Additive] (hF : E.IsConflationExact E' e.functor) (hG : E'.IsConflationExact E e.inverse) (h : P'.inverseImage e.functor = P) : (ExactK0.mapEquiv e hF hG).toAddMonoidHom.comp (resolutionEquiv E P).toAddMonoidHom = (resolutionEquiv E' P').toAddMonoidHom.comp (ExactK0.mapEquiv (e.congrFullSubcategory h) ⋯ ⋯).toAddMonoidHom

Equivalence invariance of the resolution theorem. An exact equivalence identifying two resolving properties intertwines both the ambient exact K₀ equivalence and the equivalence of the resolving subcategories with their resolution-theorem comparisons.

theorem TauCeti.ExactStructure.IsResolving.mapEquiv_comp_resolutionEquiv_symm {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] [CategoryTheory.EssentiallySmall.{w, v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] [CategoryTheory.EssentiallySmall.{w', v', u'} D] {E' : ExactStructure D} {P' : CategoryTheory.ObjectProperty D} [E'.IsResolving P'] (e : C ≌ D) [e.functor.Additive] [e.inverse.Additive] (hF : E.IsConflationExact E' e.functor) (hG : E'.IsConflationExact E e.inverse) (h : P'.inverseImage e.functor = P) : (ExactK0.mapEquiv (e.congrFullSubcategory h) ⋯ ⋯).toAddMonoidHom.comp (resolutionEquiv E P).symm.toAddMonoidHom = (resolutionEquiv E' P').symm.toAddMonoidHom.comp (ExactK0.mapEquiv e hF hG).toAddMonoidHom

The inverse resolution maps are invariant under an exact equivalence identifying the resolving properties.