The graded Cartan map

Let A be a k-algebra with homogeneous pieces 𝒜 : ℤ → Submodule k A. The finitely generated graded A-modules and the finitely generated graded modules whose underlying A-modules are projective are shift-stable full subcategories of TauCeti.GradedModuleCat 𝒜. This file equips them with their induced graded exact structures and constructs the Laurent-linear Cartan map

c_A^gr : K₀^gr(proj A) ⟶ G₀^gr(mod A).

Both subcategories are extension closed for any grading data: a short exact sequence with projective quotient splits on underlying modules. When 𝒜 is a decomposition of A, the exact structure on the graded projectives is moreover split: a conflation with projective quotient splits in the graded module category. The inclusion into the finite graded modules is compatible with the grading shift, so its map on Grothendieck groups is linear over ℤ[q,q⁻¹].

The map is constructed for arbitrary grading data, since its construction uses only extension closure and shift stability. Its source is K₀^gr(proj A) in the textbook sense when 𝒜 is a decomposition of A: then finite graded modules with projective underlying module are projective objects of the graded module category (TauCeti.GradedModuleCat.projective_of_module_projective), and their induced exact structure is the split one (TauCeti.gradedFiniteProjectiveModulesExactStructure_eq_split).

The smallness argument uses an explicit small model. A finite graded module is transported to a quotient of a finite-rank free A-module using Mathlib's FGModuleRepr; the grading and its compatibility with 𝒜 transport across the resulting linear equivalence. Thus both graded Grothendieck groups live in the same universe as the coefficient data.

Main definitions

• TauCeti.gradedFiniteModules and TauCeti.gradedFiniteProjectiveModules: the two object properties.
• TauCeti.gradedFiniteModulesExactStructure and TauCeti.gradedFiniteProjectiveModulesExactStructure: their induced graded exact structures.
• TauCeti.gradedCartanMap: the Laurent-linear graded Cartan map.

Main results

• TauCeti.isExtensionClosed_gradedFiniteModules and TauCeti.isExtensionClosed_gradedFiniteProjectiveModules: both properties are extension closed in the abelian category of graded modules.
• TauCeti.gradedFiniteModules_shift and TauCeti.gradedFiniteProjectiveModules_shift: both properties are stable under the grading shift.
• TauCeti.gradedFiniteModulesExactStructure_conflation_iff and TauCeti.gradedFiniteProjectiveModulesExactStructure_conflation_iff: the conflations of the two structures are the short exact sequences of graded modules with terms in the subcategory.
• TauCeti.gradedFiniteModulesExactStructureShiftFunctorCompιIso and TauCeti.gradedFiniteProjectiveModulesExactStructureShiftFunctorCompιIso: the restricted shifts agree with the ambient grading shift after inclusion.
• TauCeti.laurentK0_of_shiftObj: [M{d}] = qᵈ [M] in the graded Grothendieck group of finite graded modules.
• TauCeti.laurentK0_projective_of_shiftObj: [P{d}] = qᵈ [P] in the graded Grothendieck group of finite graded projectives.
• TauCeti.gradedFiniteProjectiveModulesExactStructure_eq_split: the underlying exact structure on finite graded projectives is split when 𝒜 is a decomposition of A.
• TauCeti.gradedCartanMap_of: the graded Cartan map sends the class of a projective to the class of the same graded module in the finite-module category.

References

• C. Năstăsescu and F. Van Oystaeyen, Methods of Graded Rings, Section 2.3, for graded projective modules and grading shifts.
• Z. Dancso and A. Licata, "Koszul algebras and flow lattices", Section 2.2, for the graded Cartan map over the Laurent coefficient ring.

The construction adapts the ungraded Cartan map of TauCeti.Algebra.Category.ModuleCat.CartanMap.Basic (TauCeti.cartanMap) to graded modules and the Laurent-linear Grothendieck group.

Finite graded modules

def TauCeti.gradedFiniteModules {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] (𝒜 : ℤ → Submodule k A) : CategoryTheory.ObjectProperty (GradedModuleCat 𝒜)

The object property of having a finitely generated underlying module.

Equations

• TauCeti.gradedFiniteModules 𝒜 M = Module.Finite A M.carrier

def TauCeti.gradedFiniteProjectiveModules {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] (𝒜 : ℤ → Submodule k A) : CategoryTheory.ObjectProperty (GradedModuleCat 𝒜)

The object property of having a finitely generated projective underlying module.

Equations

• TauCeti.gradedFiniteProjectiveModules 𝒜 M = (Module.Finite A M.carrier ∧ Module.Projective A M.carrier)

@[simp]

theorem TauCeti.gradedFiniteModules_iff {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} {M : GradedModuleCat 𝒜} : gradedFiniteModules 𝒜 M ↔ Module.Finite A M.carrier

@[simp]

theorem TauCeti.gradedFiniteProjectiveModules_iff {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} {M : GradedModuleCat 𝒜} : gradedFiniteProjectiveModules 𝒜 M ↔ Module.Finite A M.carrier ∧ Module.Projective A M.carrier

theorem TauCeti.gradedFiniteProjectiveModules_le_finiteModules {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} : gradedFiniteProjectiveModules 𝒜 ≤ gradedFiniteModules 𝒜

A finite graded projective is, in particular, a finite graded module.

instance TauCeti.instFiniteCarrierObjGradedModuleCatGradedFiniteModules {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} (M : (gradedFiniteModules 𝒜).FullSubcategory) : Module.Finite A M.obj.carrier

instance TauCeti.instFiniteCarrierObjGradedModuleCatGradedFiniteModules_1 {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} [Module.Finite k A] (M : (gradedFiniteModules 𝒜).FullSubcategory) : Module.Finite k M.obj.carrier

Over an algebra finite as a module over its base ring, a finite graded module is finite over the base ring.

instance TauCeti.instFiniteCarrierObjGradedModuleCatGradedFiniteProjectiveModules {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} (M : (gradedFiniteProjectiveModules 𝒜).FullSubcategory) : Module.Finite A M.obj.carrier

instance TauCeti.instProjectiveCarrierObjGradedModuleCatGradedFiniteProjectiveModules {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} (M : (gradedFiniteProjectiveModules 𝒜).FullSubcategory) : Module.Projective A M.obj.carrier

instance TauCeti.instIsClosedUnderIsomorphismsGradedModuleCatGradedFiniteModules {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} : (gradedFiniteModules 𝒜).IsClosedUnderIsomorphisms

instance TauCeti.instIsClosedUnderIsomorphismsGradedModuleCatGradedFiniteProjectiveModules {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} : (gradedFiniteProjectiveModules 𝒜).IsClosedUnderIsomorphisms

A small model

instance TauCeti.instEssentiallySmallGradedModuleCatGradedFiniteModules {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} : CategoryTheory.ObjectProperty.EssentiallySmall.{uA, uA, max (uA + 1) uk} (gradedFiniteModules 𝒜)

Finite graded modules form an essentially small category.

instance TauCeti.instEssentiallySmallGradedModuleCatGradedFiniteProjectiveModules {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} : CategoryTheory.ObjectProperty.EssentiallySmall.{uA, uA, max (uA + 1) uk} (gradedFiniteProjectiveModules 𝒜)

Finite graded projective modules form an essentially small category.

Induced graded exact structures

instance TauCeti.instContainsZeroGradedModuleCatGradedFiniteModules {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} : (gradedFiniteModules 𝒜).ContainsZero

instance TauCeti.instContainsZeroGradedModuleCatGradedFiniteProjectiveModules {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} : (gradedFiniteProjectiveModules 𝒜).ContainsZero

theorem TauCeti.isExtensionClosed_gradedFiniteModules {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} : (ExactStructure.abelian (GradedModuleCat 𝒜)).IsExtensionClosed (gradedFiniteModules 𝒜)

Finite graded modules are extension closed in the abelian category of graded modules.

theorem TauCeti.isExtensionClosed_gradedFiniteProjectiveModules {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} : (ExactStructure.abelian (GradedModuleCat 𝒜)).IsExtensionClosed (gradedFiniteProjectiveModules 𝒜)

Finite graded modules with projective underlying module are extension closed in the abelian category of graded modules: a short exact sequence with projective quotient splits on the underlying modules.

instance TauCeti.instIsClosedUnderBinaryProductsGradedModuleCatGradedFiniteModules {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} : (gradedFiniteModules 𝒜).IsClosedUnderBinaryProducts

instance TauCeti.instIsClosedUnderBinaryProductsGradedModuleCatGradedFiniteProjectiveModules {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} : (gradedFiniteProjectiveModules 𝒜).IsClosedUnderBinaryProducts

theorem TauCeti.gradedFiniteModules_shift {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} : (gradedFiniteModules 𝒜).inverseImage (GradedModuleCat.shift 𝒜).functor = gradedFiniteModules 𝒜

Finite graded modules are stable under the grading shift.

theorem TauCeti.gradedFiniteProjectiveModules_shift {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} : (gradedFiniteProjectiveModules 𝒜).inverseImage (GradedModuleCat.shift 𝒜).functor = gradedFiniteProjectiveModules 𝒜

Finite graded modules with projective underlying module are stable under the grading shift.

noncomputable def TauCeti.gradedFiniteModulesExactStructure {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] (𝒜 : ℤ → Submodule k A) : GradedExactStructure (gradedFiniteModules 𝒜).FullSubcategory

The induced graded exact structure on finite graded modules.

Equations

• TauCeti.gradedFiniteModulesExactStructure 𝒜 = (TauCeti.gradedModuleExactStructure✝ 𝒜).fullSubcategory (TauCeti.gradedFiniteModules 𝒜) ⋯ ⋯

noncomputable def TauCeti.gradedFiniteProjectiveModulesExactStructure {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] (𝒜 : ℤ → Submodule k A) : GradedExactStructure (gradedFiniteProjectiveModules 𝒜).FullSubcategory

The induced graded exact structure on finite graded modules with projective underlying module. When 𝒜 is a decomposition of A, it is the split exact structure, by TauCeti.gradedFiniteProjectiveModulesExactStructure_eq_split.

Equations

• TauCeti.gradedFiniteProjectiveModulesExactStructure 𝒜 = (TauCeti.gradedModuleExactStructure✝ 𝒜).fullSubcategory (TauCeti.gradedFiniteProjectiveModules 𝒜) ⋯ ⋯

theorem TauCeti.gradedFiniteModulesExactStructure_eq_fullSubcategory {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} (hP : (GradedExactStructure.abelian (GradedModuleCat 𝒜) (GradedModuleCat.shift 𝒜)).IsExtensionClosed (gradedFiniteModules 𝒜)) (hshift : (gradedFiniteModules 𝒜).inverseImage (GradedExactStructure.abelian (GradedModuleCat 𝒜) (GradedModuleCat.shift 𝒜)).shift.functor = gradedFiniteModules 𝒜) : gradedFiniteModulesExactStructure 𝒜 = (GradedExactStructure.abelian (GradedModuleCat 𝒜) (GradedModuleCat.shift 𝒜)).fullSubcategory (gradedFiniteModules 𝒜) hP hshift

The graded exact structure on finite graded modules is the one induced from the canonical graded exact structure on all graded modules, for any proofs of the side conditions.

theorem TauCeti.gradedFiniteProjectiveModulesExactStructure_eq_fullSubcategory {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} (hP : (GradedExactStructure.abelian (GradedModuleCat 𝒜) (GradedModuleCat.shift 𝒜)).IsExtensionClosed (gradedFiniteProjectiveModules 𝒜)) (hshift : (gradedFiniteProjectiveModules 𝒜).inverseImage (GradedExactStructure.abelian (GradedModuleCat 𝒜) (GradedModuleCat.shift 𝒜)).shift.functor = gradedFiniteProjectiveModules 𝒜) : gradedFiniteProjectiveModulesExactStructure 𝒜 = (GradedExactStructure.abelian (GradedModuleCat 𝒜) (GradedModuleCat.shift 𝒜)).fullSubcategory (gradedFiniteProjectiveModules 𝒜) hP hshift

The graded exact structure on finite graded modules with projective underlying module is the one induced from the canonical graded exact structure on all graded modules, for any proofs of the side conditions.

noncomputable def TauCeti.gradedFiniteModulesExactStructureShiftFunctorCompιIso {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} : (gradedFiniteModulesExactStructure 𝒜).shift.functor.comp (gradedFiniteModules 𝒜).ι ≅ (gradedFiniteModules 𝒜).ι.comp (GradedModuleCat.shift 𝒜).functor

The shift on finite graded modules agrees with the ambient grading shift after applying the full-subcategory inclusion.

Equations

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

noncomputable def TauCeti.gradedFiniteProjectiveModulesExactStructureShiftFunctorCompιIso {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} : (gradedFiniteProjectiveModulesExactStructure 𝒜).shift.functor.comp (gradedFiniteProjectiveModules 𝒜).ι ≅ (gradedFiniteProjectiveModules 𝒜).ι.comp (GradedModuleCat.shift 𝒜).functor

The shift on finite graded projective modules agrees with the ambient grading shift after applying the full-subcategory inclusion.

Equations

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

@[simp]

theorem TauCeti.gradedFiniteModulesExactStructure_conflation_iff {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} (S : CategoryTheory.ShortComplex (gradedFiniteModules 𝒜).FullSubcategory) : (gradedFiniteModulesExactStructure 𝒜).Conflation S ↔ (S.map (gradedFiniteModules 𝒜).ι).ShortExact

The conflations of finite graded modules are the short exact sequences of graded modules whose three terms are finitely generated.

@[simp]

theorem TauCeti.gradedFiniteProjectiveModulesExactStructure_conflation_iff {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} (S : CategoryTheory.ShortComplex (gradedFiniteProjectiveModules 𝒜).FullSubcategory) : (gradedFiniteProjectiveModulesExactStructure 𝒜).Conflation S ↔ (S.map (gradedFiniteProjectiveModules 𝒜).ι).ShortExact

The conflations of finite graded modules with projective underlying module are the short exact sequences of graded modules whose three terms are of this kind.

Classes of shifted modules

theorem TauCeti.gradedFiniteModules_shiftObj {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} {M : GradedModuleCat 𝒜} (hM : gradedFiniteModules 𝒜 M) (d : ℤ) : gradedFiniteModules 𝒜 (M.shiftObj d)

An internal shift of a finite graded module is finite: it has the same underlying module.

theorem TauCeti.laurentK0_of_shiftObj {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} (M : (gradedFiniteModules 𝒜).FullSubcategory) (d : ℤ) : LaurentK0.of (gradedFiniteModulesExactStructure 𝒜) { obj := M.obj.shiftObj d, property := ⋯ } = LaurentPolynomial.T d • LaurentK0.of (gradedFiniteModulesExactStructure 𝒜) M

[M{d}] = qᵈ [M] in the graded Grothendieck group of finite graded modules, for the explicit internal shift M{d} with (M{d})ₚ = M_{p-d}.

theorem TauCeti.gradedFiniteProjectiveModules_shiftObj {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} {M : GradedModuleCat 𝒜} (hM : gradedFiniteProjectiveModules 𝒜 M) (d : ℤ) : gradedFiniteProjectiveModules 𝒜 (M.shiftObj d)

An internal shift of a finite graded projective has the same underlying finite projective module.

theorem TauCeti.laurentK0_projective_of_shiftObj {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} (P : (gradedFiniteProjectiveModules 𝒜).FullSubcategory) (d : ℤ) : LaurentK0.of (gradedFiniteProjectiveModulesExactStructure 𝒜) { obj := P.obj.shiftObj d, property := ⋯ } = LaurentPolynomial.T d • LaurentK0.of (gradedFiniteProjectiveModulesExactStructure 𝒜) P

[P{d}] = qᵈ [P] in the Laurent Grothendieck group of finite graded projectives, for the explicit internal shift with (P{d})ₚ = P_{p-d}.

The graded Cartan map

noncomputable def TauCeti.gradedCartanMap {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] (𝒜 : ℤ → Submodule k A) : LaurentK0 (gradedFiniteProjectiveModulesExactStructure 𝒜) →ₗ[LaurentPolynomial ℤ] LaurentK0 (gradedFiniteModulesExactStructure 𝒜)

The graded Cartan map c_A^gr : K₀^gr(proj A) ⟶ G₀^gr(mod A), induced by inclusion of finite graded modules with projective underlying module into all finite graded modules.

It is defined for arbitrary grading data. Its source is the Grothendieck group of the induced exact structure on finite graded modules with projective underlying module; when 𝒜 is a decomposition of A, these are the finite graded projectives and that structure is split (TauCeti.gradedFiniteProjectiveModulesExactStructure_eq_split), so the source is K₀^gr(proj A).

Equations

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

@[simp]

theorem TauCeti.gradedCartanMap_of {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} {M : GradedModuleCat 𝒜} (hM : gradedFiniteProjectiveModules 𝒜 M) : (gradedCartanMap 𝒜) (LaurentK0.of (gradedFiniteProjectiveModulesExactStructure 𝒜) { obj := M, property := hM }) = LaurentK0.of (gradedFiniteModulesExactStructure 𝒜) { obj := M, property := ⋯ }

The graded Cartan map sends the class of a finite graded projective to the class of the same graded module in the finite-module category.

Splitting over a decomposition

theorem TauCeti.gradedFiniteProjectiveModules_le_isProjective {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} [DirectSum.Decomposition 𝒜] : gradedFiniteProjectiveModules 𝒜 ≤ (ExactStructure.abelian (GradedModuleCat 𝒜)).isProjective

A finite graded module with projective underlying module is relatively projective for the canonical exact structure on graded modules.

theorem TauCeti.gradedFiniteProjectiveModulesExactStructure_eq_split {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} [DirectSum.Decomposition 𝒜] : (gradedFiniteProjectiveModulesExactStructure 𝒜).toExactStructure = ExactStructure.split (gradedFiniteProjectiveModules 𝒜).FullSubcategory

The underlying exact structure on finite graded projectives is the split exact structure.