Graded simple modules of a nonnegatively graded algebra with split degree-zero part

Let A be a k-algebra graded by 𝒜 : ℤ → Submodule k A and let e ∈ 𝒜 0. The quotient construction does not require idempotence. Write A₊e for the left ideal generated by the products x e with x homogeneous of positive degree. The graded module TauCeti.gradedPositiveMulQuotient is the quotient Ae / A₊e, the cokernel of the inclusion of graded modules A₊e ⟶ Ae.

Suppose that A is nonnegatively graded, and that a complete family of orthogonal nonzero idempotents eᵢ of degree zero spans the degree-zero piece 𝒜 0. This is the situation of the path-length grading of a path algebra of a finite quiver, or of its quotient by a homogeneous ideal contained in the arrow ideal. Then A₊eᵢ is the graded radical of A eᵢ, the intersection of its maximal graded submodules, so Sᵢ = A eᵢ / A₊eᵢ is the graded head of the graded projective A eᵢ, and:

• the graded head Sᵢ of A eᵢ is one-dimensional, spanned by the class of eᵢ in degree zero, so eⱼ acts on it by δᵢⱼ and the graded dimension of eⱼ • Sᵢ is δᵢⱼ;
• Sᵢ is a simple graded module;
• every simple finite graded module M is isomorphic to an internal shift Sᵢ{p}: take p to be the top degree of M and m ∈ Mₚ with eᵢ m ≠ 0; positive-degree elements kill eᵢ m, so x eᵢ ↦ x eᵢ m descends to a nonzero map Sᵢ{p} ⟶ M, which is injective because Sᵢ is simple, and surjective because M is simple.

The last argument uses only simplicity of the quotients Aeᵢ / A₊eᵢ, not the splitting of the degree-zero piece; TauCeti.Algebra.Category.GradedModuleCat.Idempotent.PrimitiveHead applies it to primitive idempotents over a semisimple degree-zero piece.

Main definitions

• TauCeti.gradedPositiveMulIdeal: the left ideal A₊e.
• TauCeti.gradedPositiveMulQuotient: the quotient Ae / A₊e for any degree-zero element e.
• TauCeti.gradedPositiveMulQuotientMk: the quotient map Ae ⟶ Ae / A₊e.
• TauCeti.gradedPositiveMulQuotientLift: the map Ae / A₊e ⟶ M, [x] ↦ x m, for m killed by A₊e.

Main results

• TauCeti.gradedPositiveMulQuotientMk_eq_zero_iff: the kernel of Ae ⟶ Ae / A₊e is A₊e.
• TauCeti.gradedPositiveMulQuotientπ: the quotient map bundled as a graded morphism.
• TauCeti.bijective_smulPieceMap_gradedPositiveMulQuotientπ_zero: this quotient map is an isomorphism on degree-zero coordinates, over any commutative coefficient ring.
• TauCeti.mem_gradedPositiveMulQuotient_piece_iff: the degree-p piece of Ae / A₊e consists of the classes of the degree-p elements of Ae.
• TauCeti.gradedPositiveMulQuotient_piece_eq_bot, TauCeti.gradedPositiveMulQuotient_piece_zero_eq_top: over a nonnegatively graded algebra, Ae / A₊e is concentrated in degree zero when e is idempotent.
• TauCeti.nontrivial_gradedPositiveMulQuotient: over a nonnegatively graded algebra, Ae / A₊e is nonzero when e is.
• TauCeti.decompose_eq_zero_of_mem_gradedPositiveMulIdeal: over a nonnegatively graded algebra, the elements of A₊e have no component in degrees ≤ 0.
• TauCeti.gradedPositiveMulQuotientLift_gradedPositiveMulQuotientMk, TauCeti.gradedPositiveMulQuotientLift_unique: the universal property of Ae / A₊e.
• TauCeti.smulGradedDimension_gradedIdempotentHead: the graded dimension of eⱼ • Sᵢ is δᵢⱼ.
• TauCeti.finrank_gradedIdempotentHead, TauCeti.isSimpleModule_gradedIdempotentHead, and TauCeti.isEmpty_linearEquiv_gradedIdempotentHead: the underlying heads are one-dimensional, simple, and pairwise nonisomorphic.
• TauCeti.simple_gradedIdempotentHead: each graded head Sᵢ is a simple graded module.
• TauCeti.isExhaustiveGradedSimpleFamily_gradedPositiveMulQuotient: for any complete family of orthogonal idempotents of degree zero whose nonzero members have simple quotients Aeᵢ / A₊eᵢ, every simple finite graded module is isomorphic to a shift of one of these quotients.
• TauCeti.isExhaustiveGradedSimpleFamily_gradedIdempotentHead: every simple finite graded module is isomorphic to a shift of some Sᵢ.

References

• C. Năstăsescu and F. Van Oystaeyen, Methods of Graded Rings, Section 2.3, for graded modules and their simple objects.
• I. Assem, D. Simson, A. Skowroński, Elements of the Representation Theory of Associative Algebras, Vol. 1, Sections III.2 and III.3, for the simple tops of the indecomposable projectives of a basic algebra.

The head of Ae

def TauCeti.gradedPositiveMulIdeal {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] (𝒜 : ℤ → Submodule k A) (e : A) : Ideal A

The left ideal A₊e generated by the products x e with x homogeneous of positive degree. It is the kernel of the quotient map Ae ⟶ Ae / A₊e (TauCeti.gradedPositiveMulQuotientMk_eq_zero_iff).

theorem TauCeti.mul_mem_gradedPositiveMulIdeal {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] (𝒜 : ℤ → Submodule k A) {e : A} {p : ℤ} (hp : 0 < p) {x : A} (hx : x ∈ 𝒜 p) : x * e ∈ gradedPositiveMulIdeal 𝒜 e

A product x e with x homogeneous of positive degree lies in A₊e.

theorem TauCeti.gradedPositiveMulIdeal_le_iff {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] (𝒜 : ℤ → Submodule k A) {e : A} {J : Ideal A} : gradedPositiveMulIdeal 𝒜 e ≤ J ↔ ∀ (p : ℤ), 0 < p → ∀ x ∈ 𝒜 p, x * e ∈ J

A left ideal contains A₊e exactly when it contains every positive homogeneous product x e.

noncomputable def TauCeti.gradedPositiveMulQuotient {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] (𝒜 : ℤ → Submodule k A) {e : A} [GradedAlgebra 𝒜] (he₀ : e ∈ 𝒜 0) : GradedModuleCat 𝒜

The quotient Ae / A₊e by the left ideal generated by the products x e with x homogeneous of positive degree, for any degree-zero element e; no idempotence is required. When A is nonnegatively graded and its degree-zero piece is spanned by a complete family of nonzero orthogonal idempotents containing e, it is the graded head of Ae, a simple graded module (TauCeti.simple_gradedIdempotentHead).

instance TauCeti.instFiniteCarrierGradedPositiveMulQuotient {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] (𝒜 : ℤ → Submodule k A) {e : A} [GradedAlgebra 𝒜] (he₀ : e ∈ 𝒜 0) : Module.Finite A (gradedPositiveMulQuotient 𝒜 he₀).carrier

The quotient Ae / A₊e is finitely generated, as a quotient of the cyclic module Ae.

instance TauCeti.instFiniteCarrierGradedPositiveMulQuotient_1 {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] (𝒜 : ℤ → Submodule k A) {e : A} [GradedAlgebra 𝒜] [Module.Finite k A] (he₀ : e ∈ 𝒜 0) : Module.Finite k (gradedPositiveMulQuotient 𝒜 he₀).carrier

The quotient Ae / A₊e is finite-dimensional when A is.

theorem TauCeti.gradedFiniteModules_gradedPositiveMulQuotient {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] (𝒜 : ℤ → Submodule k A) {e : A} [GradedAlgebra 𝒜] (he₀ : e ∈ 𝒜 0) : gradedFiniteModules 𝒜 (gradedPositiveMulQuotient 𝒜 he₀)

The quotient Ae / A₊e is a finite graded module.

noncomputable def TauCeti.gradedPositiveMulQuotientMk {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} {e : A} [GradedAlgebra 𝒜] (he₀ : e ∈ 𝒜 0) : ↥(Ideal.span {e}) →ₗ[A] (gradedPositiveMulQuotient 𝒜 he₀).carrier

The quotient map Ae ⟶ Ae / A₊e, sending an element of Ae to its class.

theorem TauCeti.gradedPositiveMulQuotientMk_surjective {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} {e : A} [GradedAlgebra 𝒜] (he₀ : e ∈ 𝒜 0) : Function.Surjective ⇑(gradedPositiveMulQuotientMk he₀)

Every element of Ae / A₊e is the class of an element of Ae.

@[simp]

theorem TauCeti.gradedPositiveMulQuotientMk_eq_zero_iff {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} {e : A} [GradedAlgebra 𝒜] (he₀ : e ∈ 𝒜 0) (x : ↥(Ideal.span {e})) : (gradedPositiveMulQuotientMk he₀) x = 0 ↔ ↑x ∈ gradedPositiveMulIdeal 𝒜 e

The kernel of Ae ⟶ Ae / A₊e is A₊e.

@[simp]

theorem TauCeti.mem_gradedPositiveMulQuotient_piece_iff {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} {e : A} [GradedAlgebra 𝒜] (he₀ : e ∈ 𝒜 0) {p : ℤ} {y : (gradedPositiveMulQuotient 𝒜 he₀).carrier} : y ∈ (gradedPositiveMulQuotient 𝒜 he₀).grading.piece ℤ p ↔ ∃ (x : ↥(Ideal.span {e})), ↑x ∈ 𝒜 p ∧ (gradedPositiveMulQuotientMk he₀) x = y

The homogeneous pieces of Ae / A₊e: the degree-p piece consists of the classes of the elements of Ae of degree p.

noncomputable def TauCeti.gradedPositiveMulQuotientπ {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} {e : A} [GradedAlgebra 𝒜] (he₀ : e ∈ 𝒜 0) : GradedModuleCat.ofIdeal 𝒜 (Ideal.span {e}) ⋯ ⟶ gradedPositiveMulQuotient 𝒜 he₀

The quotient map Ae ⟶ Ae / A₊e, bundled as a morphism of graded modules.

@[simp]

theorem TauCeti.gradedPositiveMulQuotientπ_hom {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} {e : A} [GradedAlgebra 𝒜] (he₀ : e ∈ 𝒜 0) : (gradedPositiveMulQuotientπ he₀).hom = gradedPositiveMulQuotientMk he₀

noncomputable def TauCeti.gradedPositiveMulQuotientLift {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} {e : A} [GradedAlgebra 𝒜] (he₀ : e ∈ 𝒜 0) {M : Type u_1} [AddCommGroup M] [Module A M] (m : M) (hm : ∀ y ∈ gradedPositiveMulIdeal 𝒜 e, y • m = 0) : (gradedPositiveMulQuotient 𝒜 he₀).carrier →ₗ[A] M

The map Ae / A₊e ⟶ M sending the class of x to x m, for an element m of an A-module M killed by A₊e.

@[simp]

theorem TauCeti.gradedPositiveMulQuotientLift_gradedPositiveMulQuotientMk {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} {e : A} [GradedAlgebra 𝒜] (he₀ : e ∈ 𝒜 0) {M : Type u_1} [AddCommGroup M] [Module A M] (m : M) (hm : ∀ y ∈ gradedPositiveMulIdeal 𝒜 e, y • m = 0) (x : ↥(Ideal.span {e})) : (gradedPositiveMulQuotientLift he₀ m hm) ((gradedPositiveMulQuotientMk he₀) x) = ↑x • m

The map Ae / A₊e ⟶ M induced by m sends the class of x to x m.

theorem TauCeti.gradedPositiveMulQuotient_linearMap_ext {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} {e : A} [GradedAlgebra 𝒜] (he₀ : e ∈ 𝒜 0) {M : Type u_1} [AddCommGroup M] [Module A M] {f g : (gradedPositiveMulQuotient 𝒜 he₀).carrier →ₗ[A] M} (h : f ∘ₗ gradedPositiveMulQuotientMk he₀ = g ∘ₗ gradedPositiveMulQuotientMk he₀) : f = g

Two linear maps out of Ae / A₊e agreeing on the classes of all elements of Ae are equal.

theorem TauCeti.gradedPositiveMulQuotient_linearMap_ext_iff {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} {e : A} [GradedAlgebra 𝒜] {he₀ : e ∈ 𝒜 0} {M : Type u_1} [AddCommGroup M] [Module A M] {f g : (gradedPositiveMulQuotient 𝒜 he₀).carrier →ₗ[A] M} : f = g ↔ f ∘ₗ gradedPositiveMulQuotientMk he₀ = g ∘ₗ gradedPositiveMulQuotientMk he₀

theorem TauCeti.gradedPositiveMulQuotientLift_unique {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} {e : A} [GradedAlgebra 𝒜] (he₀ : e ∈ 𝒜 0) {M : Type u_1} [AddCommGroup M] [Module A M] (m : M) (hm : ∀ y ∈ gradedPositiveMulIdeal 𝒜 e, y • m = 0) (f : (gradedPositiveMulQuotient 𝒜 he₀).carrier →ₗ[A] M) (hf : ∀ (x : ↥(Ideal.span {e})), f ((gradedPositiveMulQuotientMk he₀) x) = ↑x • m) : f = gradedPositiveMulQuotientLift he₀ m hm

The map Ae / A₊e ⟶ M induced by m is unique: it is the only linear map sending the class of each x to x m.

theorem TauCeti.gradedPositiveMulQuotient_piece_eq_bot {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} {e : A} [GradedAlgebra 𝒜] (hneg : ∀ p < 0, 𝒜 p = ⊥) (he : IsIdempotentElem e) (he₀ : e ∈ 𝒜 0) {p : ℤ} (hp : p ≠ 0) : (gradedPositiveMulQuotient 𝒜 he₀).grading.piece ℤ p = ⊥

Ae / A₊e is concentrated in degree zero for an idempotent e of degree zero of a nonnegatively graded algebra: its pieces in all nonzero degrees vanish.

theorem TauCeti.gradedPositiveMulQuotient_piece_zero_eq_top {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} {e : A} [GradedAlgebra 𝒜] (hneg : ∀ p < 0, 𝒜 p = ⊥) (he : IsIdempotentElem e) (he₀ : e ∈ 𝒜 0) : (gradedPositiveMulQuotient 𝒜 he₀).grading.piece ℤ 0 = ⊤

Ae / A₊e is its own degree-zero piece for an idempotent e of degree zero of a nonnegatively graded algebra.

theorem TauCeti.decompose_eq_zero_of_mem_gradedPositiveMulIdeal {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} [GradedAlgebra 𝒜] (hneg : ∀ p < 0, 𝒜 p = ⊥) {f : A} (hf₀ : f ∈ 𝒜 0) {y : A} (hy : y ∈ gradedPositiveMulIdeal 𝒜 f) {q : ℤ} (hq : q ≤ 0) : ↑(((DirectSum.decompose 𝒜) y) q) = 0

In a nonnegatively graded algebra, every element of A₊e has vanishing components in all degrees q ≤ 0.

theorem TauCeti.bijective_smulPieceMap_gradedPositiveMulQuotientπ_zero {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} [GradedAlgebra 𝒜] (hneg : ∀ p < 0, 𝒜 p = ⊥) {f : A} (hf₀ : f ∈ 𝒜 0) (e : A) (he₀ : e ∈ 𝒜 0) : Function.Bijective ⇑(GradedModuleCat.smulPieceMap e (gradedPositiveMulQuotientπ hf₀) 0)

The head quotient is an isomorphism on each degree-zero coordinate e • M₀. No semisimplicity or splitting hypothesis is needed: the kernel A₊e has no degree-zero part.

Nonnegative gradings with split degree-zero part

theorem TauCeti.exists_eq_smul_of_mem_zero {k : Type uk} [Field k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} {I : Type uI} {e : I → A} (he : OrthogonalIdempotents e) (hspan : 𝒜 0 ≤ Submodule.span k (Set.range e)) {i : I} {x : A} (hx : x ∈ 𝒜 0) (hxi : x ∈ Ideal.span {e i}) : ∃ (c : k), x = c • e i

A degree-zero element of A eᵢ is a scalar multiple of eᵢ.

theorem TauCeti.isExhaustiveGradedSimpleFamily_gradedPositiveMulQuotient {k : Type uk} [Field k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} {I : Type uI} {e : I → A} [GradedAlgebra 𝒜] [Fintype I] [Module.Finite k A] (hcomplete : CompleteOrthogonalIdempotents e) (he₀ : ∀ (i : I), e i ∈ 𝒜 0) (hsimple : ∀ (i : I), e i ≠ 0 → IsSimpleModule A (gradedPositiveMulQuotient 𝒜 ⋯).carrier) : IsExhaustiveGradedSimpleFamily fun (i : I) => { obj := gradedPositiveMulQuotient 𝒜 ⋯, property := ⋯ }

Every simple finite graded module is a shift of some A eᵢ / A₊eᵢ, for a complete family of orthogonal idempotents eᵢ of degree zero such that A eᵢ / A₊eᵢ is a simple module whenever eᵢ ≠ 0. If p is the top degree of M and m ∈ Mₚ satisfies eᵢ m ≠ 0, then x eᵢ ↦ x eᵢ m is an isomorphism (A eᵢ / A₊eᵢ){p} ≅ M. No positivity of the grading and no splitting of the degree-zero part is needed.

theorem TauCeti.gradedPositiveMulQuotientMk_spanSingletonGenerator_ne_zero {k : Type uk} [Field k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} [GradedAlgebra 𝒜] (hneg : ∀ p < 0, 𝒜 p = ⊥) {f : A} (hf₀ : f ∈ 𝒜 0) (hne : f ≠ 0) : (gradedPositiveMulQuotientMk hf₀) (spanSingletonGenerator f) ≠ 0

The class of f in A f / A₊f is nonzero for a nonzero element f of degree zero of a nonnegatively graded algebra: A₊f has no degree-zero component.

theorem TauCeti.nontrivial_gradedPositiveMulQuotient {k : Type uk} [Field k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} [GradedAlgebra 𝒜] (hneg : ∀ p < 0, 𝒜 p = ⊥) {f : A} (hf₀ : f ∈ 𝒜 0) (hne : f ≠ 0) : Nontrivial (gradedPositiveMulQuotient 𝒜 hf₀).carrier

A f / A₊f is a nonzero module for a nonzero element f of degree zero of a nonnegatively graded algebra.

theorem TauCeti.smulGradedDimension_gradedIdempotentHead {k : Type uk} [Field k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} {I : Type uI} {e : I → A} [GradedAlgebra 𝒜] (hneg : ∀ p < 0, 𝒜 p = ⊥) (he : OrthogonalIdempotents e) (he₀ : ∀ (i : I), e i ∈ 𝒜 0) (hspan : 𝒜 0 ≤ Submodule.span k (Set.range e)) [Module.Finite k A] [DecidableEq I] (j i : I) (hne : e i ≠ 0) : GradedModuleCat.smulGradedDimension (e j) (gradedPositiveMulQuotient 𝒜 ⋯) = if j = i then 1 else 0

The graded dimension of eⱼ • Sᵢ is δᵢⱼ: the graded head Sᵢ of A eᵢ is one-dimensional, concentrated in degree zero, and eⱼ acts on it by δᵢⱼ.

Simplicity and exhaustiveness

theorem TauCeti.finrank_gradedIdempotentHead {k : Type uk} [Field k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} {I : Type uI} {e : I → A} [GradedAlgebra 𝒜] (hneg : ∀ p < 0, 𝒜 p = ⊥) (he : OrthogonalIdempotents e) (he₀ : ∀ (i : I), e i ∈ 𝒜 0) (hspan : 𝒜 0 ≤ Submodule.span k (Set.range e)) (i : I) (hne : e i ≠ 0) : Module.finrank k (gradedPositiveMulQuotient 𝒜 ⋯).carrier = 1

The underlying vector space of the head of A eᵢ is one-dimensional.

theorem TauCeti.isSimpleModule_gradedIdempotentHead {k : Type uk} [Field k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} {I : Type uI} {e : I → A} [GradedAlgebra 𝒜] (hneg : ∀ p < 0, 𝒜 p = ⊥) (he : OrthogonalIdempotents e) (he₀ : ∀ (i : I), e i ∈ 𝒜 0) (hspan : 𝒜 0 ≤ Submodule.span k (Set.range e)) (i : I) (hne : e i ≠ 0) : IsSimpleModule A (gradedPositiveMulQuotient 𝒜 ⋯).carrier

Forgetting the grading of an idempotent head still gives a simple module.

theorem TauCeti.isEmpty_linearEquiv_gradedIdempotentHead {k : Type uk} [Field k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} {I : Type uI} {e : I → A} [GradedAlgebra 𝒜] (hneg : ∀ p < 0, 𝒜 p = ⊥) (he : OrthogonalIdempotents e) (he₀ : ∀ (i : I), e i ∈ 𝒜 0) (hspan : 𝒜 0 ≤ Submodule.span k (Set.range e)) {i j : I} (hij : i ≠ j) (hi : e i ≠ 0) : IsEmpty ((gradedPositiveMulQuotient 𝒜 ⋯).carrier ≃ₗ[A] (gradedPositiveMulQuotient 𝒜 ⋯).carrier)

Distinct nonzero orthogonal idempotents give nonisomorphic underlying heads.

theorem TauCeti.simple_gradedIdempotentHead {k : Type uk} [Field k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} {I : Type uI} {e : I → A} [GradedAlgebra 𝒜] (hneg : ∀ p < 0, 𝒜 p = ⊥) (he : OrthogonalIdempotents e) (he₀ : ∀ (i : I), e i ∈ 𝒜 0) (hspan : 𝒜 0 ≤ Submodule.span k (Set.range e)) (i : I) (hne : e i ≠ 0) : CategoryTheory.Simple (gradedPositiveMulQuotient 𝒜 ⋯)

The graded head Sᵢ of A eᵢ is a simple graded module. It is one-dimensional, spanned by the class of eᵢ, so a nonzero graded submodule is everything.

theorem TauCeti.isExhaustiveGradedSimpleFamily_gradedIdempotentHead {k : Type uk} [Field k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} {I : Type uI} {e : I → A} [GradedAlgebra 𝒜] (hneg : ∀ p < 0, 𝒜 p = ⊥) [Fintype I] [Module.Finite k A] (he₀ : ∀ (i : I), e i ∈ 𝒜 0) (hspan : 𝒜 0 ≤ Submodule.span k (Set.range e)) (hcomplete : CompleteOrthogonalIdempotents e) : IsExhaustiveGradedSimpleFamily fun (i : I) => { obj := gradedPositiveMulQuotient 𝒜 ⋯, property := ⋯ }

Every simple finite graded module is a shift of a graded head Sᵢ, for a nonnegatively graded algebra whose degree-zero piece is spanned by a complete family of orthogonal idempotents eᵢ: each nonzero eᵢ has a simple head (TauCeti.isSimpleModule_gradedIdempotentHead).