Documentation

TauCeti.Algebra.Category.GradedModuleCat.CartanMap.Idempotent.Matrix

The graded Cartan matrix in idempotent bases #

Let A be a nonnegatively graded finite-dimensional algebra whose degree-zero piece is spanned by a complete family of orthogonal nonzero idempotents eᵢ, as for the path-length grading of the path algebra of a finite acyclic quiver or of its quotient by a homogeneous ideal inside the arrow ideal. Such an algebra carries two canonical Laurent bases: the projective classes [A eᵢ] of K₀^gr(proj A) (TauCeti.gradedIdempotentProjectiveBasis) and the head classes [Sᵢ] of G₀^gr(mod A) (TauCeti.gradedIdempotentHeadBasis).

In these bases the graded Cartan matrix has no hypotheses left: the coefficient of qᵖ in its (i, j) entry is dim_k(eᵢ A eⱼ ∩ 𝒜 p), the graded multiplicity of Sᵢ{p} in A eⱼ. The entries have no negative powers of q and constant term δᵢⱼ, so the matrix is congruent to the identity modulo q.

Over a field that does not split the simple modules, let the degree-zero piece instead be a semisimple ring and let the eᵢ be primitive with pairwise nonisomorphic left ideals A eᵢ. In the bases TauCeti.gradedIdempotentProjectiveBasisOfPrimitive and TauCeti.gradedIdempotentHeadBasisOfPrimitive, the corner dimension dim_k(eᵢ A eⱼ ∩ 𝒜 p) is then dim_k End_A(Sᵢ) times the coefficient of qᵖ. Also in this generality, the negative-degree coefficients vanish and the constant coefficient matrix is the identity: the quotient A eᵢ ⟶ Sᵢ is an isomorphism in degree zero, so the division-endomorphism dimensions cancel.

The two bases are also the input of the projective/simple duality and of the relation between the graded Cartan matrix and the q-Euler matrix: TauCeti.gradedIdempotentProjectiveBasis_apply supplies the hypothesis, that the projective basis vectors are the classes [A eᵢ], of TauCeti.gradedCartanMatrix_map_invert_transpose_mul_gradedExtEulerMatrix_eq_one and TauCeti.gradedProjectiveExtEuler_basis_eq_dualBasis.

Main results #

References #

theorem TauCeti.coeff_gradedCartanMatrix_gradedIdempotentProjectiveBasis {k : Type uk} [Field k] {A : Type uA} [Ring A] [Algebra k A] [Module.Finite k A] {𝒜 : ℤ → Submodule k A} [GradedAlgebra 𝒜] {I : Type uI} [Fintype I] {e : I → A} (he : CompleteOrthogonalIdempotents e) (he₀ : ∀ (i : I), e i ∈ 𝒜 0) (hI : ∀ (i : I), Ideal.IsHomogeneous 𝒜 (Ideal.span {e i})) (hneg : ∀ p < 0, 𝒜 p = ⊥) (hspan : 𝒜 0 ≤ Submodule.span k (Set.range e)) (hne : ∀ (i : I), e i ≠ 0) (i j : I) (p : ℤ) :
(gradedCartanMatrix 𝒜 (gradedIdempotentProjectiveBasis he hI hneg hspan hne) (gradedIdempotentHeadBasis hneg he he₀ hspan hne) i j).coeff p = ↑(Module.finrank k ↥(cornerSubmodule k (e i) (e j) ⊓ 𝒜 p))

The graded Cartan matrix in the canonical bases counts graded corner dimensions. In the projective basis [A eⱼ] and the head basis [Sᵢ], the coefficient of qᵖ in the (i, j) entry of the graded Cartan matrix is dim_k(eᵢ A eⱼ ∩ 𝒜 p).

theorem TauCeti.coeff_gradedCartanMatrix_gradedIdempotentProjectiveBasis_of_neg {k : Type uk} [Field k] {A : Type uA} [Ring A] [Algebra k A] [Module.Finite k A] {𝒜 : ℤ → Submodule k A} [GradedAlgebra 𝒜] {I : Type uI} [Fintype I] {e : I → A} (he : CompleteOrthogonalIdempotents e) (he₀ : ∀ (i : I), e i ∈ 𝒜 0) (hI : ∀ (i : I), Ideal.IsHomogeneous 𝒜 (Ideal.span {e i})) (hneg : ∀ p < 0, 𝒜 p = ⊥) (hspan : 𝒜 0 ≤ Submodule.span k (Set.range e)) (hne : ∀ (i : I), e i ≠ 0) (i j : I) {p : ℤ} (hp : p < 0) :
(gradedCartanMatrix 𝒜 (gradedIdempotentProjectiveBasis he hI hneg hspan hne) (gradedIdempotentHeadBasis hneg he he₀ hspan hne) i j).coeff p = 0

The entries of the graded Cartan matrix in the canonical bases have no negative powers of q.

theorem TauCeti.coeff_zero_gradedCartanMatrix_gradedIdempotentProjectiveBasis {k : Type uk} [Field k] {A : Type uA} [Ring A] [Algebra k A] [Module.Finite k A] {𝒜 : ℤ → Submodule k A} [GradedAlgebra 𝒜] {I : Type uI} [Fintype I] {e : I → A} (he : CompleteOrthogonalIdempotents e) (he₀ : ∀ (i : I), e i ∈ 𝒜 0) (hI : ∀ (i : I), Ideal.IsHomogeneous 𝒜 (Ideal.span {e i})) (hneg : ∀ p < 0, 𝒜 p = ⊥) (hspan : 𝒜 0 ≤ Submodule.span k (Set.range e)) (hne : ∀ (i : I), e i ≠ 0) [DecidableEq I] (i j : I) :
(gradedCartanMatrix 𝒜 (gradedIdempotentProjectiveBasis he hI hneg hspan hne) (gradedIdempotentHeadBasis hneg he he₀ hspan hne) i j).coeff 0 = if i = j then 1 else 0

The graded Cartan matrix in the canonical bases is the identity modulo q: the constant term of its (i, j) entry is 1 if i = j and 0 otherwise.

Primitive idempotents over a semisimple degree-zero part #

theorem TauCeti.finrank_end_mul_coeff_gradedCartanMatrix_gradedIdempotentProjectiveBasisOfPrimitive {k : Type uk} [Field k] {A : Type uA} [Ring A] [Algebra k A] [Module.Finite k A] {𝒜 : ℤ → Submodule k A} [GradedAlgebra 𝒜] {I : Type uI} [Fintype I] {e : I → A} (he : CompleteOrthogonalIdempotents e) (he₀ : ∀ (i : I), e i ∈ 𝒜 0) (hI : ∀ (i : I), Ideal.IsHomogeneous 𝒜 (Ideal.span {e i})) (hneg : ∀ p < 0, 𝒜 p = ⊥) [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 j : I) (p : ℤ) :
↑(Module.finrank k (Module.End A (gradedPositiveMulQuotient 𝒜 ⋯).carrier)) * (gradedCartanMatrix 𝒜 (gradedIdempotentProjectiveBasisOfPrimitive he hI hprim hnoniso) (gradedIdempotentHeadBasisOfPrimitive hneg he he₀ hprim hnoniso) i j).coeff p = ↑(Module.finrank k ↥(cornerSubmodule k (e i) (e j) ⊓ 𝒜 p))

The graded Cartan matrix in the canonical bases over a nonsplitting field. For a complete family of orthogonal primitive idempotents eᵢ of degree zero with pairwise nonisomorphic left ideals, over a nonnegatively graded algebra with semisimple degree-zero part, take the projective basis [A eⱼ] and the head basis [Sᵢ]. The coefficient of qᵖ in the (i, j) entry of the graded Cartan matrix, multiplied by dim_k End_A(Sᵢ), is dim_k(eᵢ A eⱼ ∩ 𝒜 p).

theorem TauCeti.coeff_gradedCartanMatrix_gradedIdempotentProjectiveBasisOfPrimitive_of_neg {k : Type uk} [Field k] {A : Type uA} [Ring A] [Algebra k A] [Module.Finite k A] {𝒜 : ℤ → Submodule k A} [GradedAlgebra 𝒜] {I : Type uI} [Fintype I] {e : I → A} (he : CompleteOrthogonalIdempotents e) (he₀ : ∀ (i : I), e i ∈ 𝒜 0) (hI : ∀ (i : I), Ideal.IsHomogeneous 𝒜 (Ideal.span {e i})) (hneg : ∀ p < 0, 𝒜 p = ⊥) [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 j : I) {p : ℤ} (hp : p < 0) :
(gradedCartanMatrix 𝒜 (gradedIdempotentProjectiveBasisOfPrimitive he hI hprim hnoniso) (gradedIdempotentHeadBasisOfPrimitive hneg he he₀ hprim hnoniso) i j).coeff p = 0

Negative coefficients of the Cartan matrix in primitive-idempotent bases vanish over any field, not only a splitting field.

theorem TauCeti.coeff_zero_gradedCartanMatrix_gradedIdempotentProjectiveBasisOfPrimitive {k : Type uk} [Field k] {A : Type uA} [Ring A] [Algebra k A] [Module.Finite k A] {𝒜 : ℤ → Submodule k A} [GradedAlgebra 𝒜] {I : Type uI} [Fintype I] {e : I → A} (he : CompleteOrthogonalIdempotents e) (he₀ : ∀ (i : I), e i ∈ 𝒜 0) (hI : ∀ (i : I), Ideal.IsHomogeneous 𝒜 (Ideal.span {e i})) (hneg : ∀ p < 0, 𝒜 p = ⊥) [IsSemisimpleRing ↥(𝒜 0)] (hprim : ∀ (i : I), IsPrimitiveIdempotent (e i)) (hnoniso : Pairwise fun (i j : I) => IsEmpty (↥(Ideal.span {e i}) ≃ₗ[A] ↥(Ideal.span {e j}))) [DecidableEq I] (i j : I) :
(gradedCartanMatrix 𝒜 (gradedIdempotentProjectiveBasisOfPrimitive he hI hprim hnoniso) (gradedIdempotentHeadBasisOfPrimitive hneg he he₀ hprim hnoniso) i j).coeff 0 = if i = j then 1 else 0

The graded Cartan matrix in primitive-idempotent bases is the identity in degree zero, even over a nonsplitting field. The division-endomorphism dimensions cancel on both sides.

Unimodularity #

theorem TauCeti.isUnit_det_gradedCartanMatrix_gradedIdempotentProjectiveBasis {k : Type uk} [Field k] {A : Type uA} [Ring A] [Algebra k A] [Module.Finite k A] {𝒜 : ℤ → Submodule k A} [GradedAlgebra 𝒜] {I : Type uI} [Fintype I] {e : I → A} (he : CompleteOrthogonalIdempotents e) (he₀ : ∀ (i : I), e i ∈ 𝒜 0) (hI : ∀ (i : I), Ideal.IsHomogeneous 𝒜 (Ideal.span {e i})) (hneg : ∀ p < 0, 𝒜 p = ⊥) (hspan : 𝒜 0 ≤ Submodule.span k (Set.range e)) (hne : ∀ (i : I), e i ≠ 0) [DecidableEq I] [CategoryTheory.HasExt (GradedModuleCat 𝒜)] (h : ∀ (i j : I), IsGradedEulerAdmissible k (GradedModuleCat.shift 𝒜) (gradedPositiveMulQuotient 𝒜 ⋯) (gradedPositiveMulQuotient 𝒜 ⋯)) :
IsUnit (gradedCartanMatrix 𝒜 (gradedIdempotentProjectiveBasis he hI hneg hspan hne) (gradedIdempotentHeadBasis hneg he he₀ hspan hne)).det

Graded Cartan unimodularity follows from admissibility of the graded heads. If every pair (Sᵢ, Sⱼ) of graded heads of the A eᵢ is graded Euler-admissible, then the graded Cartan matrix in the canonical bases has unit determinant in ℤ[q,q⁻¹].

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

Graded Cartan unimodularity over a nonsplitting field. For a complete family of orthogonal primitive idempotents eᵢ of degree zero with pairwise nonisomorphic left ideals, over a nonnegatively graded algebra with semisimple degree-zero part, if every pair (Sᵢ, Sⱼ) of graded heads of the A eᵢ is graded Euler-admissible, then the graded Cartan matrix in the bases [A eⱼ] and [Sᵢ] has unit determinant in ℤ[q,q⁻¹].