Graded exact structures on full subcategories

An extension-closed full additive subcategory of an exact category — explicitly, one containing a zero object and closed under binary products — inherits an exact structure. If the ambient category is graded and the object property is moreover stable under the grading shift, that shift restricts to an autoequivalence of the full subcategory and makes its induced exact structure graded.

Shift stability is the equality P.inverseImage E.shift.functor = P, that is, an object lies in P if and only if its shift does; one-way closure under the forward shift is not assumed. That equality, together with repleteness of the object property and the unit and counit isomorphisms, determines the matching invariance under the inverse shift. The restricted equivalence is Mathlib's CategoryTheory.Equivalence.congrFullSubcategory; its functor and inverse preserve conflations because the ambient shift and inverse shift do.

This construction is the bridge between objectwise graded invariants on extension-closed classes and the Laurent-module Grothendieck groups of those classes. In particular, it lets a graded Ext-Euler characteristic descend to the graded Grothendieck groups of selected subcategories.

Main definitions

• TauCeti.GradedExactStructure.fullSubcategoryShift: the grading-shift autoequivalence restricted to a shift-stable full subcategory.
• TauCeti.GradedExactStructure.fullSubcategory: the induced graded exact structure.
• TauCeti.GradedConflationExact.ι: the graded conflation-exact inclusion into the ambient category.
• TauCeti.GradedConflationExact.ιOfLE: the graded conflation-exact inclusion between two nested shift-stable full subcategories.
• TauCeti.GradedExactStructure.liftCommShift: the restriction to full subcategories of a shift-commutation isomorphism {1} ⋙ F ≅ F.

Main results

• TauCeti.GradedExactStructure.isConflationExact_lift: a conflation-exact functor carrying a shift-stable extension-closed property into an extension-closed one restricts to a conflation-exact functor of the induced structures.

References

• Zsuzsanna Dancso and Anthony Licata, "Koszul algebras and flow lattices", Journal of Combinatorial Theory, Series A 185 (2022), Section 2.2, for grading shifts on exact categories and their graded Grothendieck groups.
• TauCetiProject/TauCeti#5721, whose retired, unmerged formalization this construction adapts.

noncomputable def TauCeti.GradedExactStructure.fullSubcategoryShift {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] (E : GradedExactStructure C) (P : CategoryTheory.ObjectProperty C) [P.IsClosedUnderIsomorphisms] (hshift : P.inverseImage E.shift.functor = P) : P.FullSubcategory ≌ P.FullSubcategory

The grading shift restricted to a full subcategory stable under that shift.

The equation P.inverseImage E.shift.functor = P states exactly that an object belongs to P if and only if its shift does. Mathlib's full-subcategory restriction of an equivalence then uses the ambient inverse shift as its inverse.

Equations

• E.fullSubcategoryShift P hshift = E.shift.congrFullSubcategory hshift

def TauCeti.GradedExactStructure.fullSubcategoryShiftFunctorCompιIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] (E : GradedExactStructure C) (P : CategoryTheory.ObjectProperty C) [P.IsClosedUnderIsomorphisms] (hshift : P.inverseImage E.shift.functor = P) : (E.fullSubcategoryShift P hshift).functor.comp P.ι ≅ P.ι.comp E.shift.functor

The inclusion of the full subcategory intertwines its restricted shift with the ambient shift.

Equations

• E.fullSubcategoryShiftFunctorCompιIso P hshift = ⋯.mpr (P.liftCompιIso (P.ι.comp E.shift.functor) ⋯)

def TauCeti.GradedExactStructure.fullSubcategoryShiftInverseCompιIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] (E : GradedExactStructure C) (P : CategoryTheory.ObjectProperty C) [P.IsClosedUnderIsomorphisms] (hshift : P.inverseImage E.shift.functor = P) : (E.fullSubcategoryShift P hshift).inverse.comp P.ι ≅ P.ι.comp E.shift.inverse

The inclusion of the full subcategory also intertwines the inverse restricted shift with the ambient inverse shift.

Equations

• E.fullSubcategoryShiftInverseCompιIso P hshift = ⋯.mpr (P.liftCompιIso (P.ι.comp E.shift.inverse) ⋯)

theorem TauCeti.GradedExactStructure.instIsClosedUnderIsomorphisms {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) [P.ContainsZero] [P.IsClosedUnderBinaryProducts] : P.IsClosedUnderIsomorphisms

noncomputable def TauCeti.GradedExactStructure.fullSubcategory {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] (E : GradedExactStructure C) (P : CategoryTheory.ObjectProperty C) [P.ContainsZero] [P.IsClosedUnderBinaryProducts] (hP : E.IsExtensionClosed P) (hshift : P.inverseImage E.shift.functor = P) : GradedExactStructure P.FullSubcategory

The graded exact structure induced on a shift-stable, extension-closed full additive subcategory, the additivity being required in the explicit form of containing a zero object and being closed under binary products.

Its exact structure is the one induced from the ambient exact category, and its grading shift is the restriction of the ambient shift.

Equations

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

@[simp]

theorem TauCeti.GradedExactStructure.fullSubcategory_toExactStructure {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] (E : GradedExactStructure C) (P : CategoryTheory.ObjectProperty C) [P.ContainsZero] [P.IsClosedUnderBinaryProducts] (hP : E.IsExtensionClosed P) (hshift : P.inverseImage E.shift.functor = P) : (E.fullSubcategory P hP hshift).toExactStructure = ExactStructure.fullSubcategory P hP

The underlying exact structure on the induced graded exact structure is the full-subcategory exact structure.

@[simp]

theorem TauCeti.GradedExactStructure.fullSubcategory_shift {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] (E : GradedExactStructure C) (P : CategoryTheory.ObjectProperty C) [P.ContainsZero] [P.IsClosedUnderBinaryProducts] (hP : E.IsExtensionClosed P) (hshift : P.inverseImage E.shift.functor = P) : (E.fullSubcategory P hP hshift).shift = E.fullSubcategoryShift P hshift

The shift on the induced graded exact structure is the restricted ambient shift.

theorem TauCeti.GradedExactStructure.fullSubcategory_conflation_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] (E : GradedExactStructure C) (P : CategoryTheory.ObjectProperty C) [P.ContainsZero] [P.IsClosedUnderBinaryProducts] (hP : E.IsExtensionClosed P) (hshift : P.inverseImage E.shift.functor = P) (S : CategoryTheory.ShortComplex P.FullSubcategory) : (E.fullSubcategory P hP hshift).Conflation S ↔ E.Conflation (S.map P.ι)

A short complex of the subcategory is a conflation of the induced graded exact structure exactly when its image in the ambient category is a conflation.

noncomputable def TauCeti.GradedExactStructure.liftCommShift {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] (E : GradedExactStructure C) (P : CategoryTheory.ObjectProperty C) [P.ContainsZero] [P.IsClosedUnderBinaryProducts] {D : Type u'} [CategoryTheory.Category.{v', u'} D] {Q : CategoryTheory.ObjectProperty D} {F : CategoryTheory.Functor C D} (hP : E.IsExtensionClosed P) (hshift : P.inverseImage E.shift.functor = P) (hPQ : ∀ (X : P.FullSubcategory), Q (F.obj X.obj)) (comm : E.shift.functor.comp F ≅ F) : (E.fullSubcategory P hP hshift).shift.functor.comp (Q.lift (P.ι.comp F) hPQ) ≅ Q.lift (P.ι.comp F) hPQ

The restriction of a shift-commutation isomorphism to full subcategories. A functor F out of a graded exact category with {1} ⋙ F ≅ F restricts, on a shift-stable full subcategory of its source and a full subcategory of its target containing the image, to a functor with the same commutation isomorphism: the restricted shift is the ambient one.

This is the datum which, together with conflation-exactness, forgets the grading on the subcategory in TauCeti.LaurentK0.forgetGrading.

Equations

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

theorem TauCeti.GradedExactStructure.isConflationExact_lift {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] (E : GradedExactStructure C) (P : CategoryTheory.ObjectProperty C) [P.ContainsZero] [P.IsClosedUnderBinaryProducts] {D : Type u'} [CategoryTheory.Category.{v', u'} D] {Q : CategoryTheory.ObjectProperty D} {F : CategoryTheory.Functor C D} (hP : E.IsExtensionClosed P) (hshift : P.inverseImage E.shift.functor = P) (hPQ : ∀ (X : P.FullSubcategory), Q (F.obj X.obj)) [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] [Q.ContainsZero] [Q.IsClosedUnderBinaryProducts] [F.Additive] {E' : ExactStructure D} (hQ : E'.IsExtensionClosed Q) (hF : E.IsConflationExact E' F) : (E.fullSubcategory P hP hshift).IsConflationExact (ExactStructure.fullSubcategory Q hQ) (Q.lift (P.ι.comp F) hPQ)

A conflation-exact functor carrying a shift-stable extension-closed property P into an extension-closed property Q restricts to a conflation-exact functor from the graded exact structure induced on P to the exact structure induced on Q.

theorem TauCeti.GradedConflationExact.instIsClosedUnderIsomorphisms {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) [P.ContainsZero] [P.IsClosedUnderBinaryProducts] : P.IsClosedUnderIsomorphisms

def TauCeti.GradedConflationExact.ι {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] (E : GradedExactStructure C) (P : CategoryTheory.ObjectProperty C) [P.ContainsZero] [P.IsClosedUnderBinaryProducts] (hP : E.IsExtensionClosed P) (hshift : P.inverseImage E.shift.functor = P) : GradedConflationExact (E.fullSubcategory P hP hshift) E P.ι

The inclusion of a shift-stable, extension-closed full additive subcategory — one containing a zero object and closed under binary products — is graded conflation-exact. Its commutation isomorphism is the canonical comparison between the restricted shift followed by inclusion and the ambient shift.

Equations

• TauCeti.GradedConflationExact.ι E P hP hshift = { isConflationExact := ⋯, commShift := id (E.fullSubcategoryShiftFunctorCompιIso P hshift) }

@[simp]

theorem TauCeti.GradedConflationExact.ι_commShift {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] (E : GradedExactStructure C) (P : CategoryTheory.ObjectProperty C) [P.ContainsZero] [P.IsClosedUnderBinaryProducts] (hP : E.IsExtensionClosed P) (hshift : P.inverseImage E.shift.functor = P) : (ι E P hP hshift).commShift ≍ E.fullSubcategoryShiftFunctorCompιIso P hshift

The shift-commutation isomorphism of the graded conflation-exact full-subcategory inclusion.

noncomputable def TauCeti.GradedConflationExact.ιOfLE {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] (E : GradedExactStructure C) (P : CategoryTheory.ObjectProperty C) [P.ContainsZero] [P.IsClosedUnderBinaryProducts] {Q : CategoryTheory.ObjectProperty C} [Q.ContainsZero] [Q.IsClosedUnderBinaryProducts] (hP : E.IsExtensionClosed P) (hQ : E.IsExtensionClosed Q) (hPshift : P.inverseImage E.shift.functor = P) (hQshift : Q.inverseImage E.shift.functor = Q) (h : P ≤ Q) : GradedConflationExact (E.fullSubcategory P hP hPshift) (E.fullSubcategory Q hQ hQshift) (CategoryTheory.ObjectProperty.ιOfLE h)

The inclusion associated to an implication P ≤ Q between two shift-stable, extension-closed full additive subcategories is graded conflation-exact for their induced graded exact structures. Its commutation isomorphism is the one whose image under the inclusion of Q is the composite of the two restricted-shift comparisons with the ambient shift.

Equations

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