Homogeneous left ideals as graded modules

Let A be a k-algebra graded by 𝒜 : ℤ → Submodule k A. A homogeneous left ideal I of A is a graded A-module whose degree-p piece is I ∩ 𝒜 p. This file records it as an object TauCeti.GradedModuleCat.ofIdeal 𝒜 I hI of the category of graded modules.

The main example is the left ideal Af generated by an idempotent f, which is homogeneous as soon as f is (Ideal.homogeneous_span; a nonzero homogeneous idempotent has degree zero). For idempotent f the module Af is projective, being a direct summand of A, and so it is a projective object of the graded category. Examples are the vertex projectives of a path algebra or of a zigzag algebra graded by path length, generated by the vertex idempotents.

For an idempotent e of degree zero, the subspaces e • (Af)ₚ read off by the idempotent graded dimension TauCeti.GradedModuleCat.smulGradedDimension are the graded pieces eAf ∩ 𝒜 p of the corner eAf. Hence the graded dimension of e • Af is ∑ₚ dim_k(eAf ∩ 𝒜 p) qᵖ: this is the formula for the graded Cartan matrix in idempotent coordinates.

Main definitions

• TauCeti.GradedModuleCat.ofIdeal 𝒜 I hI: a homogeneous left ideal as a graded module.

Main results

• TauCeti.GradedModuleCat.projective_ofIdeal_span_singleton: Af is a projective graded module for an idempotent f.
• TauCeti.GradedModuleCat.map_subtype_smul_ofIdeal_span_singleton_piece: e • (Af)ₚ, viewed inside A, is the graded piece eAf ∩ 𝒜 p of the corner.
• TauCeti.GradedModuleCat.coeff_smulGradedDimension_ofIdeal_span_singleton: the coefficient of qᵖ in the graded dimension of e • Af is dim_k(eAf ∩ 𝒜 p).

References

• C. Năstăsescu and F. Van Oystaeyen, Methods of Graded Rings, Section 2.3, for graded modules and projectivity in the graded category.
• I. Assem, D. Simson, A. Skowroński, Elements of the Representation Theory of Associative Algebras, Vol. 1, Sections I.4 and III.3, for the projectives Af and the corners eAf as Cartan-matrix entries.

Homogeneous left ideals

@[reducible, inline]

noncomputable abbrev TauCeti.GradedModuleCat.ofIdeal {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] (𝒜 : ℤ → Submodule k A) [GradedAlgebra 𝒜] (I : Ideal A) (hI : Ideal.IsHomogeneous 𝒜 I) : GradedModuleCat 𝒜

A homogeneous left ideal I of a graded algebra, as a graded module: its degree-p piece consists of the elements of I of degree p in A.

Equations

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

theorem TauCeti.GradedModuleCat.mem_ofIdeal_piece_iff {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} [GradedAlgebra 𝒜] {I : Ideal A} (hI : Ideal.IsHomogeneous 𝒜 I) {p : ℤ} {x : ↥I} : x ∈ (ofIdeal 𝒜 I hI).grading.piece p ↔ ↑x ∈ 𝒜 p

An element of a homogeneous left ideal has degree p exactly when it has degree p in the algebra.

The left ideal generated by an idempotent

theorem TauCeti.GradedModuleCat.projective_ofIdeal_span_singleton {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} [GradedAlgebra 𝒜] {f : A} (hf : IsIdempotentElem f) (hI : Ideal.IsHomogeneous 𝒜 (Ideal.span {f})) : CategoryTheory.Projective (ofIdeal 𝒜 (Ideal.span {f}) hI)

The left ideal generated by an idempotent is a projective graded module: its underlying module is a direct summand of A.

theorem TauCeti.GradedModuleCat.map_subtype_smul_ofIdeal_span_singleton_piece {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} [GradedAlgebra 𝒜] {e f : A} (he : IsIdempotentElem e) (he₀ : e ∈ 𝒜 0) (hf : IsIdempotentElem f) (hI : Ideal.IsHomogeneous 𝒜 (Ideal.span {f})) (p : ℤ) : Submodule.map (↑k (Submodule.subtype (Ideal.span {f}))) (e • (ofIdeal 𝒜 (Ideal.span {f}) hI).grading.piece p) = cornerSubmodule k e f ⊓ 𝒜 p

The idempotent pieces of Af are graded corners. For idempotents e of degree zero and f, the subspace e • (Af)ₚ, viewed inside A, is the degree-p part eAf ∩ 𝒜 p of the corner eAf.

theorem TauCeti.GradedModuleCat.coeff_smulGradedDimension_ofIdeal_span_singleton {k : Type uk} [Field k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} [GradedAlgebra 𝒜] {e f : A} (he : IsIdempotentElem e) (he₀ : e ∈ 𝒜 0) (hf : IsIdempotentElem f) (hI : Ideal.IsHomogeneous 𝒜 (Ideal.span {f})) [Module.Finite k (ofIdeal 𝒜 (Ideal.span {f}) hI).carrier] (p : ℤ) : (smulGradedDimension e (ofIdeal 𝒜 (Ideal.span {f}) hI)).coeff p = ↑(Module.finrank k ↥(cornerSubmodule k e f ⊓ 𝒜 p))

The graded dimension of e • Af is the graded dimension of the corner eAf: the coefficient of qᵖ is dim_k(eAf ∩ 𝒜 p).