Idempotent graded dimensions of graded modules

Let A be a k-algebra with homogeneous pieces 𝒜 : ℤ → Submodule k A, and let e ∈ 𝒜 0 be an idempotent of degree zero. For a graded A-module M, a morphism restricts degreewise to the subspaces e • Mₚ. These restrictions preserve exactness, and hence the Laurent-polynomial-valued graded dimension

gdim_e(M) = ∑ₚ dim_k(e • Mₚ) qᵖ

is additive on short exact sequences of finite-dimensional graded modules. Shifting the grading by n multiplies this dimension by qⁿ.

Main definitions

• TauCeti.GradedModuleCat.smulPieceMap e f p: the restriction e • Mₚ ⟶ e • Nₚ of a morphism of graded modules.
• TauCeti.GradedModuleCat.smulGradedDimension e M: the graded dimension ∑ₚ dim_k(e • Mₚ) qᵖ.

Main results

• TauCeti.GradedModuleCat.exact_smulPieceMap: restriction to e • Mₚ preserves exactness when e is an idempotent of degree zero.
• TauCeti.GradedModuleCat.smulGradedDimension_shortExact: gdim_e is additive on short exact sequences.
• TauCeti.GradedModuleCat.smulGradedDimension_shiftObj: gdim_e(M{n}) = qⁿ gdim_e(M).

References

• C. Năstăsescu and F. Van Oystaeyen, Methods of Graded Rings, Section 2.3, for graded modules and their degree shifts.
• Z. Dancso and A. Licata, "Koszul algebras and flow lattices", Section 2.2, for graded dimensions.

The subspaces e • Mₚ

def TauCeti.GradedModuleCat.smulPieceMap {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} (e : A) {M N : GradedModuleCat 𝒜} (f : M ⟶ N) (p : ℤ) : ↥(e • M.grading.piece p) →ₗ[k] ↥(e • N.grading.piece p)

A morphism of graded modules restricts to the subspaces e • Mₚ ⟶ e • Nₚ.

Equations

• TauCeti.GradedModuleCat.smulPieceMap e f p = (↑k f.hom).restrict ⋯

@[simp]

theorem TauCeti.GradedModuleCat.coe_smulPieceMap_apply {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} (e : A) {M N : GradedModuleCat 𝒜} (f : M ⟶ N) (p : ℤ) (x : ↥(e • M.grading.piece p)) : ↑((smulPieceMap e f p) x) = f.hom ↑x

@[simp]

theorem TauCeti.GradedModuleCat.smulPieceMap_id {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} (e : A) (M : GradedModuleCat 𝒜) (p : ℤ) : smulPieceMap e (CategoryTheory.CategoryStruct.id M) p = LinearMap.id

@[simp]

theorem TauCeti.GradedModuleCat.smulPieceMap_comp {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} (e : A) {M N P : GradedModuleCat 𝒜} (f : M ⟶ N) (g : N ⟶ P) (p : ℤ) : smulPieceMap e (CategoryTheory.CategoryStruct.comp f g) p = smulPieceMap e g p ∘ₗ smulPieceMap e f p

theorem TauCeti.GradedModuleCat.smulPieceMap_injective {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} {e : A} {M N : GradedModuleCat 𝒜} {f : M ⟶ N} (hf : Function.Injective ⇑f.hom) (p : ℤ) : Function.Injective ⇑(smulPieceMap e f p)

Restriction to e • Mₚ preserves injectivity.

theorem TauCeti.GradedModuleCat.smulPieceMap_surjective {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} {e : A} {N P : GradedModuleCat 𝒜} {g : N ⟶ P} (hg : Function.Surjective ⇑g.hom) (p : ℤ) : Function.Surjective ⇑(smulPieceMap e g p)

Restriction to e • Mₚ preserves surjectivity: a preimage can be chosen of degree p.

theorem TauCeti.GradedModuleCat.smul_grading_piece_le {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} {e : A} (he₀ : e ∈ 𝒜 0) (M : GradedModuleCat 𝒜) (p : ℤ) : e • M.grading.piece p ≤ M.grading.piece p

An element of degree zero carries Mₚ into itself.

theorem TauCeti.GradedModuleCat.exact_smulPieceMap {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} {e : A} {M N P : GradedModuleCat 𝒜} (he : IsIdempotentElem e) (he₀ : e ∈ 𝒜 0) {f : M ⟶ N} {g : N ⟶ P} (hfg : Function.Exact ⇑f.hom ⇑g.hom) (p : ℤ) : Function.Exact ⇑(smulPieceMap e f p) ⇑(smulPieceMap e g p)

Restriction to e • Mₚ preserves exactness when e is an idempotent of degree zero.

The graded dimension of e • M

theorem TauCeti.GradedModuleCat.hasFiniteLaurentSupport_smul_grading_piece {k : Type uk} [Field k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} (e : A) (M : GradedModuleCat 𝒜) [Module.Finite k M.carrier] : HasFiniteLaurentSupport k fun (p : ℤ) => ↥(e • M.grading.piece p)

A graded module that is finite-dimensional over k has finitely many nonzero subspaces e • Mₚ, all finite-dimensional.

noncomputable def TauCeti.GradedModuleCat.smulGradedDimension {k : Type uk} [Field k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} (e : A) (M : GradedModuleCat 𝒜) [Module.Finite k M.carrier] : LaurentPolynomial ℤ

The graded dimension of e • M, ∑ₚ dim_k(e • Mₚ) qᵖ, for a graded module that is finite-dimensional over k.

Equations

• TauCeti.GradedModuleCat.smulGradedDimension e M = TauCeti.gradedDimension k (fun (p : ℤ) => ↥(e • M.grading.piece p)) ⋯

@[simp]

theorem TauCeti.GradedModuleCat.coeff_smulGradedDimension {k : Type uk} [Field k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} (e : A) (M : GradedModuleCat 𝒜) [Module.Finite k M.carrier] (p : ℤ) : (smulGradedDimension e M).coeff p = ↑(Module.finrank k ↥(e • M.grading.piece p))

theorem TauCeti.GradedModuleCat.smulGradedDimension_congr {k : Type uk} [Field k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} (e : A) {M N : GradedModuleCat 𝒜} [Module.Finite k M.carrier] [Module.Finite k N.carrier] (i : M ≅ N) : smulGradedDimension e M = smulGradedDimension e N

Isomorphic graded modules have the same graded dimension of e • M.

@[simp]

theorem TauCeti.GradedModuleCat.smulGradedDimension_shiftObj {k : Type uk} [Field k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} (e : A) (M : GradedModuleCat 𝒜) [Module.Finite k M.carrier] (n : ℤ) : smulGradedDimension e (M.shiftObj n) = LaurentPolynomial.T n * smulGradedDimension e M

Shifting the grading multiplies the graded dimension of e • M by a power of q: gdim_e(M{n}) = qⁿ gdim_e(M).

theorem TauCeti.GradedModuleCat.smulGradedDimension_shortExact {k : Type uk} [Field k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} {e : A} (he : IsIdempotentElem e) (he₀ : e ∈ 𝒜 0) {S : CategoryTheory.ShortComplex (GradedModuleCat 𝒜)} (hS : S.ShortExact) [Module.Finite k S.X₁.carrier] [Module.Finite k S.X₂.carrier] [Module.Finite k S.X₃.carrier] : smulGradedDimension e S.X₂ = smulGradedDimension e S.X₁ + smulGradedDimension e S.X₃

The graded dimension of e • M is additive on short exact sequences of graded modules when e is an idempotent of degree zero.