Graded heads of primitive idempotents over a semisimple degree-zero part

Let A be a nonnegatively graded algebra over a field k whose degree-zero part A₀ = 𝒜 0 is a semisimple ring, and let f be a primitive idempotent of A of degree zero. The graded module Sf = A f / A₊f (TauCeti.gradedPositiveMulQuotient) is concentrated in degree zero, where it is a nonzero quotient of the A₀-module A₀ f, and positive-degree elements act on it by zero. Since f stays primitive in A₀ and A₀ is semisimple, this quotient is a simple A₀-module, so Sf is a simple A-module. When A is finite-dimensional, the quotient map A f ⟶ Sf is a projective cover.

Unlike the split situation of TauCeti.Algebra.Category.GradedModuleCat.Idempotent.Head, the degree-zero corner f A₀ f need not be the line k f: it is isomorphic to the opposite of the division algebra End_A(Sf), so its dimension is dim_k End_A(Sf), the constant graded dimension of f • Sf. A second primitive idempotent f' whose ungraded left ideal A f' is not isomorphic to A f kills Sf: otherwise A f' would cover Sf as well, and projective covers are unique. In particular the heads of such f and f' are not isomorphic, even as ungraded modules.

For a complete family of orthogonal primitive idempotents eᵢ of degree zero with pairwise nonisomorphic left ideals A eᵢ, the heads Sᵢ therefore satisfy the hypotheses of the general simple-class basis of graded G₀: gdim(eⱼ • Sᵢ) = 0 for i ≠ j, gdim(eᵢ • Sᵢ) is the nonzero constant dim_k End_A(Sᵢ), and every simple finite graded module is a shift of some Sᵢ. These are the hypotheses of TauCeti.gradedIdempotentProjectiveBasisOfPrimitive together with semisimplicity of A₀ and nonnegativity of the grading, so the field need not split the simples.

Main results

• TauCeti.isSimpleModule_gradedPositiveMulQuotient: A f / A₊f is a simple module.
• TauCeti.isProjectiveCover_gradedPositiveMulQuotientMk: A f ⟶ A f / A₊f is a projective cover.
• TauCeti.smul_gradedPositiveMulQuotient_eq_zero: a primitive idempotent with nonisomorphic left ideal kills A f / A₊f.
• TauCeti.isEmpty_linearEquiv_gradedPositiveMulQuotient: primitive idempotents with nonisomorphic left ideals have nonisomorphic heads.
• TauCeti.smulGradedDimension_gradedPositiveMulQuotient_self: gdim(f • Sf) = dim_k End_A(Sf).
• TauCeti.isUnit_smulGradedDimension_gradedPositiveMulQuotient_self_iff: gdim(f • Sf) is a unit of ℤ[q,q⁻¹] exactly when dim_k End_A(Sf) = 1.
• TauCeti.pairwise_smulGradedDimension_gradedPositiveMulQuotient_eq_zero: gdim(eⱼ • Sᵢ) = 0 for i ≠ j when the left ideals A eᵢ are pairwise nonisomorphic.
• TauCeti.isExhaustiveGradedSimpleFamily_gradedPositiveMulQuotient_of_isPrimitiveIdempotent: the heads of a complete family of primitive idempotents exhaust the simple finite graded modules up to shift.

References

• C. Năstăsescu and F. Van Oystaeyen, Methods of Graded Rings, Section 2.3, for graded simple modules.
• A. Beilinson, V. Ginzburg and W. Soergel, Koszul duality patterns in representation theory, Section 1.2, for positively graded rings with semisimple degree-zero part.
• Peter Webb, A Course in Finite Group Representation Theory, Section 7.4, for the division-endomorphism factor over a general field.

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

The quotient map A f ⟶ A f / A₊f is a projective cover for a primitive idempotent f of degree zero of a finite-dimensional nonnegatively graded algebra: A f / A₊f is a nonzero quotient of A f.

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

The graded dimension of f • (A f / A₊f) is nonzero for a nonzero idempotent f of degree zero: f • (A f / A₊f) contains the nonzero class of f.

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

The head A f / A₊f of a primitive idempotent is a simple module over a nonnegatively graded algebra whose degree-zero part is semisimple. As an A₀-module it is a nonzero quotient of the indecomposable left ideal A₀ f of the semisimple ring A₀, and positive-degree elements act on it by zero.

theorem TauCeti.smul_gradedPositiveMulQuotient_eq_zero {k : Type uk} [Field k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} [GradedAlgebra 𝒜] (hneg : ∀ p < 0, 𝒜 p = ⊥) [IsSemisimpleRing ↥(𝒜 0)] [Module.Finite k A] {f f' : A} (hf : IsPrimitiveIdempotent f) (hf₀ : f ∈ 𝒜 0) (hf' : IsPrimitiveIdempotent f') (hnoniso : IsEmpty (↥(Ideal.span {f}) ≃ₗ[A] ↥(Ideal.span {f'}))) (z : (gradedPositiveMulQuotient 𝒜 hf₀).carrier) : f' • z = 0

A primitive idempotent with a nonisomorphic left ideal kills the head of A f. If f' acted nontrivially on A f / A₊f, then x ↦ x • (f' • z) would make A f' a second projective cover of this simple module, and projective covers are unique up to isomorphism.

theorem TauCeti.smulGradedDimension_gradedPositiveMulQuotient_eq_zero {k : Type uk} [Field k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} [GradedAlgebra 𝒜] (hneg : ∀ p < 0, 𝒜 p = ⊥) [IsSemisimpleRing ↥(𝒜 0)] [Module.Finite k A] {f f' : A} (hf : IsPrimitiveIdempotent f) (hf₀ : f ∈ 𝒜 0) (hf' : IsPrimitiveIdempotent f') (hnoniso : IsEmpty (↥(Ideal.span {f}) ≃ₗ[A] ↥(Ideal.span {f'}))) : GradedModuleCat.smulGradedDimension f' (gradedPositiveMulQuotient 𝒜 hf₀) = 0

The graded dimension of f' • (A f / A₊f) vanishes for a primitive idempotent f' whose left ideal is not isomorphic to A f.

theorem TauCeti.isEmpty_linearEquiv_gradedPositiveMulQuotient {k : Type uk} [Field k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} [GradedAlgebra 𝒜] (hneg : ∀ p < 0, 𝒜 p = ⊥) [IsSemisimpleRing ↥(𝒜 0)] [Module.Finite k A] {f f' : A} (hf : IsPrimitiveIdempotent f) (hf₀ : f ∈ 𝒜 0) (hf' : IsPrimitiveIdempotent f') (hf'₀ : f' ∈ 𝒜 0) (hnoniso : IsEmpty (↥(Ideal.span {f}) ≃ₗ[A] ↥(Ideal.span {f'}))) : IsEmpty ((gradedPositiveMulQuotient 𝒜 hf₀).carrier ≃ₗ[A] (gradedPositiveMulQuotient 𝒜 hf'₀).carrier)

Heads of primitive idempotents with nonisomorphic left ideals are nonisomorphic, even as ungraded modules: f' fixes the nonzero class of f' in A f' / A₊f', but kills A f / A₊f.

theorem TauCeti.smulGradedDimension_gradedPositiveMulQuotient_self {k : Type uk} [Field k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} [GradedAlgebra 𝒜] (hneg : ∀ p < 0, 𝒜 p = ⊥) [IsSemisimpleRing ↥(𝒜 0)] [Module.Finite k A] {f : A} (hf : IsPrimitiveIdempotent f) (hf₀ : f ∈ 𝒜 0) : GradedModuleCat.smulGradedDimension f (gradedPositiveMulQuotient 𝒜 hf₀) = LaurentPolynomial.C ↑(Module.finrank k (Module.End A (gradedPositiveMulQuotient 𝒜 hf₀).carrier))

The graded dimension of f • (A f / A₊f) is the constant dim_k End_A(A f / A₊f), the dimension of a division algebra by Schur, which need not be one over a field that does not split the simple modules.

theorem TauCeti.isUnit_smulGradedDimension_gradedPositiveMulQuotient_self_iff {k : Type uk} [Field k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} [GradedAlgebra 𝒜] (hneg : ∀ p < 0, 𝒜 p = ⊥) [IsSemisimpleRing ↥(𝒜 0)] [Module.Finite k A] {f : A} (hf : IsPrimitiveIdempotent f) (hf₀ : f ∈ 𝒜 0) : IsUnit (GradedModuleCat.smulGradedDimension f (gradedPositiveMulQuotient 𝒜 hf₀)) ↔ Module.finrank k (Module.End A (gradedPositiveMulQuotient 𝒜 hf₀).carrier) = 1

The diagonal graded dimension gdim(f • A f / A₊f) = dim_k End_A(A f / A₊f) of a primitive idempotent f of degree zero is a unit of ℤ[q,q⁻¹] exactly when it is 1.

theorem TauCeti.pairwise_smulGradedDimension_gradedPositiveMulQuotient_eq_zero {k : Type uk} [Field k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} [GradedAlgebra 𝒜] (hneg : ∀ p < 0, 𝒜 p = ⊥) [IsSemisimpleRing ↥(𝒜 0)] [Module.Finite k A] {I : Type uI} {e : I → A} (he₀ : ∀ (i : I), e i ∈ 𝒜 0) (hprim : ∀ (i : I), IsPrimitiveIdempotent (e i)) (hnoniso : Pairwise fun (i j : I) => IsEmpty (↥(Ideal.span {e i}) ≃ₗ[A] ↥(Ideal.span {e j}))) : Pairwise fun (i j : I) => GradedModuleCat.smulGradedDimension (e i) (gradedPositiveMulQuotient 𝒜 ⋯) = 0

The heads of primitive idempotents of degree zero with pairwise nonisomorphic left ideals have vanishing off-diagonal graded dimensions: gdim(eᵢ • A eⱼ / A₊eⱼ) = 0 for i ≠ j.

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

The heads of a complete family of primitive idempotents exhaust the simple finite graded modules up to shift, over a finite-dimensional nonnegatively graded algebra with semisimple degree-zero part.