Graded Cartan coefficients over nonsplitting fields

Let Sᵢ be an exhaustive family of graded simples concentrated in degree zero, and let eᵢ be degree-zero idempotents with diagonal, nonzero action on this family. Put dᵢ = dim_k(eᵢ • (Sᵢ)₀). For every finite graded module M, its simple-basis coefficient mᵢₚ satisfies

dᵢ mᵢₚ = dim_k(eᵢ • Mₚ).

In particular mᵢₚ is nonnegative and the dimension on the right is divisible by dᵢ. Applied to a projective A fⱼ, this computes the coefficient of qᵖ in the graded Cartan matrix as the exact quotient dim_k(eᵢ A fⱼ ∩ 𝒜 p) / dᵢ. The divisor is not assumed to be one. When Sᵢ is the simple head of A eᵢ, it is the division-endomorphism dimension; the statements here require only the diagonal idempotent data and do not construct an action of that division algebra on arbitrary Hom spaces.

These are coefficient computations in the existing simple-class basis, rather than a new definition of a graded Jordan–Hölder multiplicity.

References

• Peter Webb, A Course in Finite Group Representation Theory, Sections 7.3--7.4, for the division-endomorphism correction to projective/simple multiplicity formulas.
• Zsuzsanna Dancso and Anthony Licata, Koszul algebras and flow lattices, Section 2.2, for graded Cartan matrices and the convention [M{p}] = qᵖ[M].

theorem TauCeti.finrank_smul_simple_piece_zero_mul_coeff_repr {k : Type uk} [Field k] {A : Type uA} [Ring A] [Algebra k A] [Module.Finite k A] {𝒜 : ℤ → Submodule k A} {I : Type uI} (S : I → (gradedFiniteModules 𝒜).FullSubcategory) {e : I → A} (he : ∀ (i : I), IsIdempotentElem (e i)) (he₀ : ∀ (i : I), e i ∈ 𝒜 0) (hne : Pairwise fun (i j : I) => GradedModuleCat.smulGradedDimension (e i) (S j).obj = 0) (hself : ∀ (i : I), GradedModuleCat.smulGradedDimension (e i) (S i).obj ≠ 0) (hS : IsExhaustiveGradedSimpleFamily S) (M : (gradedFiniteModules 𝒜).FullSubcategory) (i : I) (hconc : ∀ (p : ℤ), p ≠ 0 → (S i).obj.grading.piece ℤ p = ⊥) (p : ℤ) : ↑(Module.finrank k ↥(e i • (S i).obj.grading.piece ℤ 0)) * (((gradedSimpleClassBasisOfNeZero S he he₀ hne hself hS).repr (LaurentK0.of (gradedFiniteModulesExactStructure 𝒜) M)) i).coeff p = ↑(Module.finrank k ↥(e i • M.obj.grading.piece ℤ p))

The simple-basis coefficient of a finite graded module, multiplied by the diagonal idempotent dimension, is the dimension of the corresponding homogeneous idempotent summand.

theorem TauCeti.coeff_gradedSimpleClassBasisOfNeZero_repr_nonneg {k : Type uk} [Field k] {A : Type uA} [Ring A] [Algebra k A] [Module.Finite k A] {𝒜 : ℤ → Submodule k A} {I : Type uI} (S : I → (gradedFiniteModules 𝒜).FullSubcategory) {e : I → A} (he : ∀ (i : I), IsIdempotentElem (e i)) (he₀ : ∀ (i : I), e i ∈ 𝒜 0) (hne : Pairwise fun (i j : I) => GradedModuleCat.smulGradedDimension (e i) (S j).obj = 0) (hself : ∀ (i : I), GradedModuleCat.smulGradedDimension (e i) (S i).obj ≠ 0) (hS : IsExhaustiveGradedSimpleFamily S) (M : (gradedFiniteModules 𝒜).FullSubcategory) (i : I) (hconc : ∀ (p : ℤ), p ≠ 0 → (S i).obj.grading.piece ℤ p = ⊥) (p : ℤ) : 0 ≤ (((gradedSimpleClassBasisOfNeZero S he he₀ hne hself hS).repr (LaurentK0.of (gradedFiniteModulesExactStructure 𝒜) M)) i).coeff p

All coefficients of an actual finite graded module in the simple-class basis are nonnegative. The field need not split the simple modules.

theorem TauCeti.finrank_smul_simple_piece_zero_dvd_finrank_smul_piece {k : Type uk} [Field k] {A : Type uA} [Ring A] [Algebra k A] [Module.Finite k A] {𝒜 : ℤ → Submodule k A} {I : Type uI} (S : I → (gradedFiniteModules 𝒜).FullSubcategory) {e : I → A} (he : ∀ (i : I), IsIdempotentElem (e i)) (he₀ : ∀ (i : I), e i ∈ 𝒜 0) (hne : Pairwise fun (i j : I) => GradedModuleCat.smulGradedDimension (e i) (S j).obj = 0) (hself : ∀ (i : I), GradedModuleCat.smulGradedDimension (e i) (S i).obj ≠ 0) (hS : IsExhaustiveGradedSimpleFamily S) (M : (gradedFiniteModules 𝒜).FullSubcategory) (i : I) (hconc : ∀ (p : ℤ), p ≠ 0 → (S i).obj.grading.piece ℤ p = ⊥) (p : ℤ) : Module.finrank k ↥(e i • (S i).obj.grading.piece ℤ 0) ∣ Module.finrank k ↥(e i • M.obj.grading.piece ℤ p)

The diagonal simple dimension divides each homogeneous idempotent-summand dimension of a finite graded module.

theorem TauCeti.finrank_smul_simple_piece_zero_mul_coeff_gradedCartanMatrix {k : Type uk} [Field k] {A : Type uA} [Ring A] [Algebra k A] [Module.Finite k A] {𝒜 : ℤ → Submodule k A} {I : Type uI} (S : I → (gradedFiniteModules 𝒜).FullSubcategory) {e : I → A} (he : ∀ (i : I), IsIdempotentElem (e i)) (he₀ : ∀ (i : I), e i ∈ 𝒜 0) (hne : Pairwise fun (i j : I) => GradedModuleCat.smulGradedDimension (e i) (S j).obj = 0) (hself : ∀ (i : I), GradedModuleCat.smulGradedDimension (e i) (S i).obj ≠ 0) (hS : IsExhaustiveGradedSimpleFamily S) [GradedAlgebra 𝒜] {J : Type uJ} [Fintype J] [Finite I] (bP : Module.Basis J (LaurentPolynomial ℤ) (LaurentK0 (gradedFiniteProjectiveModulesExactStructure 𝒜))) {f : A} (hf : IsIdempotentElem f) (hF : Ideal.IsHomogeneous 𝒜 (Ideal.span {f})) (j : J) (hj : bP j = LaurentK0.of (gradedFiniteProjectiveModulesExactStructure 𝒜) { obj := GradedModuleCat.ofIdeal 𝒜 (Ideal.span {f}) hF, property := ⋯ }) (i : I) (hconc : ∀ (p : ℤ), p ≠ 0 → (S i).obj.grading.piece ℤ p = ⊥) (p : ℤ) : ↑(Module.finrank k ↥(e i • (S i).obj.grading.piece ℤ 0)) * (gradedCartanMatrix 𝒜 bP (gradedSimpleClassBasisOfNeZero S he he₀ hne hself hS) i j).coeff p = ↑(Module.finrank k ↥(cornerSubmodule k (e i) f ⊓ 𝒜 p))

The weighted graded Cartan coefficient formula. A coefficient in a column [A f], multiplied by dim_k(eᵢ • (Sᵢ)₀), is the corresponding graded corner dimension.

theorem TauCeti.coeff_gradedCartanMatrix_eq_div {k : Type uk} [Field k] {A : Type uA} [Ring A] [Algebra k A] [Module.Finite k A] {𝒜 : ℤ → Submodule k A} {I : Type uI} (S : I → (gradedFiniteModules 𝒜).FullSubcategory) {e : I → A} (he : ∀ (i : I), IsIdempotentElem (e i)) (he₀ : ∀ (i : I), e i ∈ 𝒜 0) (hne : Pairwise fun (i j : I) => GradedModuleCat.smulGradedDimension (e i) (S j).obj = 0) (hself : ∀ (i : I), GradedModuleCat.smulGradedDimension (e i) (S i).obj ≠ 0) (hS : IsExhaustiveGradedSimpleFamily S) [GradedAlgebra 𝒜] {J : Type uJ} [Fintype J] [Finite I] (bP : Module.Basis J (LaurentPolynomial ℤ) (LaurentK0 (gradedFiniteProjectiveModulesExactStructure 𝒜))) {f : A} (hf : IsIdempotentElem f) (hF : Ideal.IsHomogeneous 𝒜 (Ideal.span {f})) (j : J) (hj : bP j = LaurentK0.of (gradedFiniteProjectiveModulesExactStructure 𝒜) { obj := GradedModuleCat.ofIdeal 𝒜 (Ideal.span {f}) hF, property := ⋯ }) (i : I) (hconc : ∀ (p : ℤ), p ≠ 0 → (S i).obj.grading.piece ℤ p = ⊥) (p : ℤ) : (gradedCartanMatrix 𝒜 bP (gradedSimpleClassBasisOfNeZero S he he₀ hne hself hS) i j).coeff p = ↑(Module.finrank k ↥(cornerSubmodule k (e i) f ⊓ 𝒜 p)) / ↑(Module.finrank k ↥(e i • (S i).obj.grading.piece ℤ 0))

An exact integer quotient computes graded Cartan coefficients over a nonsplitting field. The divisor is positive and the division has no remainder.