Idempotent coordinates of simple heads over a general field #
If the idempotent projective Ae covers a simple graded module S concentrated in degree zero,
then the idempotent graded dimension of S is the constant dim_k End_A(S). Thus the diagonal
in the graded projective/simple pairing need not be one over a nonsplitting field.
The calculation combines evaluation at e with the projective-cover Hom dimension formula
TauCeti.IsProjectiveCover.finrank_linearMap_eq_finrank_end.
References #
- Peter Webb, A Course in Finite Group Representation Theory, Section 7.4, for the division-endomorphism correction to the projective/simple pairing.
theorem
TauCeti.GradedModuleCat.smulGradedDimension_eq_C_finrank_end_of_isProjectiveCover
{k : Type uk}
[Field k]
{A : Type uA}
[Ring A]
[Algebra k A]
{𝒜 : ℤ → Submodule k A}
{e : A}
(S : GradedModuleCat 𝒜)
[Module.Finite k S.carrier]
[IsSimpleModule A S.carrier]
(he : IsIdempotentElem e)
(hconc : ∀ (p : ℤ), p ≠ 0 → S.grading.piece ℤ p = ⊥)
{f : ↥(Ideal.span {e}) →ₗ[A] S.carrier}
(hf : IsProjectiveCover f)
:
If Ae covers the degree-zero simple S, its idempotent graded dimension is the constant
dimension of the division algebra End_A(S). The cover concerns the actual underlying modules;
no scalar action of this division algebra on other Hom spaces is asserted.