The simple-class basis from graded idempotent heads

For a nonnegatively graded finite-dimensional algebra with split degree-zero part, the heads of the projectives associated to its complete orthogonal idempotents form an exhaustive family of graded simples. Their classes form a basis of the graded Grothendieck group over ℤ[q,q⁻¹], and its coordinates are the graded idempotent coordinates.

Over a field that does not split the simple modules, take instead a degree-zero part A₀ that is a semisimple ring and a complete family of orthogonal primitive idempotents eᵢ of degree zero whose left ideals A eᵢ are pairwise nonisomorphic. The heads Sᵢ = A eᵢ / A₊eᵢ again give a basis of the graded Grothendieck group. Now the eᵢ-coordinate is dim_k End_A(Sᵢ) times the ith basis coordinate, as in the ungraded TauCeti.simpleClassBasis over a general field. The hypotheses on the eᵢ are those of the projective basis TauCeti.gradedIdempotentProjectiveBasisOfPrimitive.

Main definitions

• TauCeti.gradedIdempotentHeadBasis: the basis [Sᵢ] for a split degree-zero part.
• TauCeti.gradedIdempotentHeadBasisOfPrimitive: the basis [Sᵢ] for primitive idempotents over a semisimple degree-zero part.

Main results

• TauCeti.gradedIdempotentHeadBasis_repr_apply: in the split case the coordinates are the idempotent coordinates.
• TauCeti.gradedIdempotentCoordinate_eq_mul_gradedIdempotentHeadBasisOfPrimitive_repr: in general the eᵢ-coordinate is dim_k End_A(Sᵢ) times the ith coordinate.

The simple-class basis

noncomputable def TauCeti.gradedIdempotentHeadBasis {k : Type uk} [Field k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} [GradedAlgebra 𝒜] {I : Type uI} [Fintype I] {e : I → A} (hneg : ∀ p < 0, 𝒜 p = ⊥) (he : CompleteOrthogonalIdempotents e) (he₀ : ∀ (i : I), e i ∈ 𝒜 0) (hspan : 𝒜 0 ≤ Submodule.span k (Set.range e)) (hne : ∀ (i : I), e i ≠ 0) [Module.Finite k A] : Module.Basis I (LaurentPolynomial ℤ) (LaurentK0 (gradedFiniteModulesExactStructure 𝒜))

The graded heads of the A eᵢ form a basis of G₀^gr(mod A) over ℤ[q,q⁻¹], for a nonnegatively graded finite-dimensional algebra whose degree-zero piece is spanned by a complete family of orthogonal nonzero idempotents eᵢ. Its basis vector at i is the class [Sᵢ].

@[simp]

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

The basis vector of TauCeti.gradedIdempotentHeadBasis at i is the class [Sᵢ] of the graded head of A eᵢ.

@[simp]

theorem TauCeti.gradedIdempotentHeadBasis_repr_apply {k : Type uk} [Field k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} [GradedAlgebra 𝒜] {I : Type uI} [Fintype I] {e : I → A} (hneg : ∀ p < 0, 𝒜 p = ⊥) (he : CompleteOrthogonalIdempotents e) (he₀ : ∀ (i : I), e i ∈ 𝒜 0) (hspan : 𝒜 0 ≤ Submodule.span k (Set.range e)) (hne : ∀ (i : I), e i ≠ 0) [Module.Finite k A] (x : LaurentK0 (gradedFiniteModulesExactStructure 𝒜)) (i : I) : ((gradedIdempotentHeadBasis hneg he he₀ hspan hne).repr x) i = (gradedIdempotentCoordinate ⋯ ⋯) x

The coordinates in the basis [Sᵢ] are the idempotent coordinates: the ith coordinate of the class of M is the graded dimension ∑ₚ dim_k(eᵢ • Mₚ) qᵖ.

Primitive idempotents over a semisimple degree-zero part

noncomputable def TauCeti.gradedIdempotentHeadBasisOfPrimitive {k : Type uk} [Field k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} [GradedAlgebra 𝒜] {I : Type uI} [Fintype I] {e : I → A} (hneg : ∀ p < 0, 𝒜 p = ⊥) (he : CompleteOrthogonalIdempotents e) (he₀ : ∀ (i : I), e i ∈ 𝒜 0) [Module.Finite k A] [IsSemisimpleRing ↥(𝒜 0)] (hprim : ∀ (i : I), IsPrimitiveIdempotent (e i)) (hnoniso : Pairwise fun (i j : I) => IsEmpty (↥(Ideal.span {e i}) ≃ₗ[A] ↥(Ideal.span {e j}))) : Module.Basis I (LaurentPolynomial ℤ) (LaurentK0 (gradedFiniteModulesExactStructure 𝒜))

The graded heads of primitive idempotents form a basis of G₀^gr(mod A) over ℤ[q,q⁻¹], for a nonnegatively graded finite-dimensional algebra whose degree-zero part is a semisimple ring, and a complete family of orthogonal primitive idempotents eᵢ of degree zero whose left ideals A eᵢ are pairwise nonisomorphic. Its basis vector at i is the class [Sᵢ] of Sᵢ = A eᵢ / A₊eᵢ. The field need not split the simple modules.

@[simp]

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

The basis vector of TauCeti.gradedIdempotentHeadBasisOfPrimitive at i is the class [Sᵢ] of Sᵢ = A eᵢ / A₊eᵢ.

theorem TauCeti.gradedIdempotentCoordinate_eq_mul_gradedIdempotentHeadBasisOfPrimitive_repr {k : Type uk} [Field k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} [GradedAlgebra 𝒜] {I : Type uI} [Fintype I] {e : I → A} (hneg : ∀ p < 0, 𝒜 p = ⊥) (he : CompleteOrthogonalIdempotents e) (he₀ : ∀ (i : I), e i ∈ 𝒜 0) [Module.Finite k A] [IsSemisimpleRing ↥(𝒜 0)] (hprim : ∀ (i : I), IsPrimitiveIdempotent (e i)) (hnoniso : Pairwise fun (i j : I) => IsEmpty (↥(Ideal.span {e i}) ≃ₗ[A] ↥(Ideal.span {e j}))) (x : LaurentK0 (gradedFiniteModulesExactStructure 𝒜)) (i : I) : (gradedIdempotentCoordinate ⋯ ⋯) x = LaurentPolynomial.C ↑(Module.finrank k (Module.End A (gradedPositiveMulQuotient 𝒜 ⋯).carrier)) * ((gradedIdempotentHeadBasisOfPrimitive hneg he he₀ hprim hnoniso).repr x) i

The idempotent coordinates are the basis coordinates scaled by dim_k End_A(Sᵢ): the eᵢ-coordinate of x, the graded dimension ∑ₚ dim_k(eᵢ • Mₚ) qᵖ on the class of M, is dim_k End_A(Sᵢ) times the ith coordinate of x in the basis [Sᵢ].