Documentation

TauCeti.Algebra.Category.GradedModuleCat.CartanMap.ExtEuler.Matrix

The graded Cartan matrix and the q-Euler matrix #

Let A be a finite-dimensional algebra over a field k, graded by π’œ : β„€ β†’ Submodule k A. The q-Euler form Ο‡_q pairs Kβ‚€^gr(proj A) with Gβ‚€^gr(mod A), and, when every pair of finite graded modules is graded Euler-admissible, it also pairs Gβ‚€^gr(mod A) with itself. The two forms are related by the graded Cartan map c: Ο‡_q(c x, y) = Ο‡_q(x, y) (TauCeti.gradedExtEulerSesquilinear_gradedCartanMap).

In matrices this reads as follows. Write C for the graded Cartan matrix, whose (l, i) entry is the lth coordinate of c [Pα΅’], and E for the matrix of Ο‡_q on Gβ‚€^gr(mod A). Since Ο‡_q is q-antilinear in its first argument, Cα΄΄ * E is the matrix of the projective/module pairing, where Cα΄΄ is the transpose of C with q ↦ q⁻¹ applied to every entry.

If the projective basis consists of the classes [A eα΅’] of degree-zero idempotents eα΅’, and the module basis consists of classes [Sβ±Ό] with gdim(eα΅’ β€’ Sβ±Ό) = 0 for i β‰  j, then the projective/module pairing matrix is diagonal with entries gdim(eα΅’ β€’ Sα΅’), so Cα΄΄ * E = diagonal (fun i ↦ gdim(eα΅’ β€’ Sα΅’)). Over a general field, for Sα΅’ the simple head of A eα΅’ (for instance, eα΅’ a primitive idempotent of a finite-dimensional algebra) concentrated in degree zero, this entry is the constant dim_k End_A(Sα΅’), the dimension of a division algebra by Schur, as in the ungraded identity TauCeti.cartanMatrix_transpose_mul_extEulerMatrix_eq_diagonal. If every finite graded module has a finite graded-projective resolution, the graded Cartan matrix is invertible (TauCeti.isUnit_det_gradedCartanMatrix_of_le_admitsFiniteResolution), and therefore E = (Cα΄΄)⁻¹ * diagonal (fun i ↦ gdim(eα΅’ β€’ Sα΅’)).

When gdim(eα΅’ β€’ Sβ±Ό) = Ξ΄α΅’β±Ό, the projective/module pairing matrix is the identity. Such a projective basis is, for instance, TauCeti.gradedIndecomposableProjectiveClassBasis for an exhaustive family of indecomposable A eα΅’. Hence Cα΄΄ * E = 1: the q-Euler matrix of the graded simples is the inverse of the conjugate transpose of the graded Cartan matrix, and the determinant of the graded Cartan matrix is a unit of β„€[q,q⁻¹]. These are the graded analogues of TauCeti.cartanMatrix_transpose_mul_extEulerMatrix_eq_one and TauCeti.extEulerMatrix_eq_inverseCartanMatrix_transpose.

Euler-admissibility of all pairs of finite graded modules is a genuine hypothesis. For the dual numbers k[Ρ]/(Ρ²) with Ρ in degree two, the graded Cartan matrix is [1 + q²] (TauCeti.gradedCartanMatrix_dualNumber), whose determinant is not a unit, so the residue field is not graded Euler-admissible against itself (TauCeti.not_isGradedEulerAdmissible_dualNumberGradedResidue).

Main results #

References #

Matrices #

source
@[simp]
theorem TauCeti.gradedExtEulerMatrix_apply_eq_gradedProjectiveExtEuler {k : Type uk} [Field k] {A : Type uA} [Ring A] [Algebra k A] {π’œ : β„€ β†’ Submodule k A} [GradedAlgebra π’œ] [Module.Finite k A] [CategoryTheory.HasExt (GradedModuleCat π’œ)] {I : Type uI} {J' : Type uJ'} (bP : Module.Basis I (LaurentPolynomial β„€) (LaurentK0 (gradedFiniteProjectiveModulesExactStructure π’œ))) (bM : Module.Basis J' (LaurentPolynomial β„€) (LaurentK0 (gradedFiniteModulesExactStructure π’œ))) (i : I) (j : J') :
gradedExtEulerMatrix (GradedModuleCat.shift π’œ) (gradedFiniteProjectiveModules π’œ) (gradedFiniteModules π’œ) β‹― β‹― β‹― β‹― β‹― bP bM i j = ((gradedProjectiveExtEuler π’œ) (bP i)) (bM j)

An entry of the projective/module q-Euler matrix is the projective/module q-Euler form of the corresponding basis vectors.

source
theorem TauCeti.gradedCartanMatrix_map_invert_transpose_mul_gradedExtEulerMatrix {k : Type uk} [Field k] {A : Type uA} [Ring A] [Algebra k A] {π’œ : β„€ β†’ Submodule k A} [GradedAlgebra π’œ] [Module.Finite k A] [CategoryTheory.HasExt (GradedModuleCat π’œ)] {I : Type uI} {J : Type uJ} {J' : Type uJ'} [Fintype I] [Fintype J] (h : IsGradedEulerAdmissibleOn (gradedFiniteModules π’œ) (gradedFiniteModules π’œ)) (bP : Module.Basis I (LaurentPolynomial β„€) (LaurentK0 (gradedFiniteProjectiveModulesExactStructure π’œ))) (bM : Module.Basis J (LaurentPolynomial β„€) (LaurentK0 (gradedFiniteModulesExactStructure π’œ))) (bM' : Module.Basis J' (LaurentPolynomial β„€) (LaurentK0 (gradedFiniteModulesExactStructure π’œ))) :
((gradedCartanMatrix π’œ bP bM).map ⇑LaurentPolynomial.invert).transpose * gradedExtEulerMatrix (GradedModuleCat.shift π’œ) (gradedFiniteModules π’œ) (gradedFiniteModules π’œ) β‹― β‹― β‹― β‹― h bM bM' = gradedExtEulerMatrix (GradedModuleCat.shift π’œ) (gradedFiniteProjectiveModules π’œ) (gradedFiniteModules π’œ) β‹― β‹― β‹― β‹― β‹― bP bM'

The conjugate-transposed graded Cartan matrix times the q-Euler matrix is the projective/module q-Euler matrix. For bases bP of Kβ‚€^gr(proj A) and bM, bM' of Gβ‚€^gr(mod A), write C for the graded Cartan matrix in bP and bM, and E for the q-Euler matrix of Gβ‚€^gr(mod A) in bM and bM'. Then (C.map invert)α΅€ * E is the matrix of the projective/module q-Euler form in bP and bM'.

source
theorem TauCeti.gradedExtEulerMatrix_eq_diagonal_smulGradedDimension {k : Type uk} [Field k] {A : Type uA} [Ring A] [Algebra k A] {π’œ : β„€ β†’ Submodule k A} [GradedAlgebra π’œ] [Module.Finite k A] [CategoryTheory.HasExt (GradedModuleCat π’œ)] {I : Type uI} [DecidableEq I] (S : I β†’ (gradedFiniteModules π’œ).FullSubcategory) {e : I β†’ A} (he : βˆ€ (i : I), IsIdempotentElem (e i)) (heβ‚€ : βˆ€ (i : I), e i ∈ π’œ 0) (hI : βˆ€ (i : I), Ideal.IsHomogeneous π’œ (Ideal.span {e i})) (hne : Pairwise fun (i j : I) => GradedModuleCat.smulGradedDimension (e i) (S j).obj = 0) (bP : Module.Basis I (LaurentPolynomial β„€) (LaurentK0 (gradedFiniteProjectiveModulesExactStructure π’œ))) (hbP : βˆ€ (i : I), bP i = LaurentK0.of (gradedFiniteProjectiveModulesExactStructure π’œ) { obj := GradedModuleCat.ofIdeal π’œ (Ideal.span {e i}) β‹―, property := β‹― }) (bM : Module.Basis I (LaurentPolynomial β„€) (LaurentK0 (gradedFiniteModulesExactStructure π’œ))) (hbM : βˆ€ (i : I), bM i = LaurentK0.of (gradedFiniteModulesExactStructure π’œ) (S i)) :
gradedExtEulerMatrix (GradedModuleCat.shift π’œ) (gradedFiniteProjectiveModules π’œ) (gradedFiniteModules π’œ) β‹― β‹― β‹― β‹― β‹― bP bM = Matrix.diagonal fun (i : I) => GradedModuleCat.smulGradedDimension (e i) (S i).obj

The classes [A eα΅’] and [Sβ±Ό] pair diagonally under the q-Euler form: if gdim(eα΅’ β€’ Sβ±Ό) = 0 for i β‰  j, then in a projective basis of classes [A eα΅’] and a module basis of classes [Sβ±Ό], the matrix of the projective/module q-Euler form is diagonal with entries gdim(eα΅’ β€’ Sα΅’). Over a general field this entry is the constant dim_k End_A(Sα΅’) when Sα΅’ is the simple head of A eα΅’ (for instance, eα΅’ a primitive idempotent of a finite-dimensional algebra) concentrated in degree zero, so it need not be 1.

source
theorem TauCeti.gradedCartanMatrix_map_invert_transpose_mul_gradedExtEulerMatrix_eq_diagonal {k : Type uk} [Field k] {A : Type uA} [Ring A] [Algebra k A] {π’œ : β„€ β†’ Submodule k A} [GradedAlgebra π’œ] [Module.Finite k A] [CategoryTheory.HasExt (GradedModuleCat π’œ)] {I : Type uI} [Fintype I] [DecidableEq I] (S : I β†’ (gradedFiniteModules π’œ).FullSubcategory) {e : I β†’ A} (he : βˆ€ (i : I), IsIdempotentElem (e i)) (heβ‚€ : βˆ€ (i : I), e i ∈ π’œ 0) (hI : βˆ€ (i : I), Ideal.IsHomogeneous π’œ (Ideal.span {e i})) (hne : Pairwise fun (i j : I) => GradedModuleCat.smulGradedDimension (e i) (S j).obj = 0) (bP : Module.Basis I (LaurentPolynomial β„€) (LaurentK0 (gradedFiniteProjectiveModulesExactStructure π’œ))) (hbP : βˆ€ (i : I), bP i = LaurentK0.of (gradedFiniteProjectiveModulesExactStructure π’œ) { obj := GradedModuleCat.ofIdeal π’œ (Ideal.span {e i}) β‹―, property := β‹― }) (bM : Module.Basis I (LaurentPolynomial β„€) (LaurentK0 (gradedFiniteModulesExactStructure π’œ))) (hbM : βˆ€ (i : I), bM i = LaurentK0.of (gradedFiniteModulesExactStructure π’œ) (S i)) (h : IsGradedEulerAdmissibleOn (gradedFiniteModules π’œ) (gradedFiniteModules π’œ)) :
((gradedCartanMatrix π’œ bP bM).map ⇑LaurentPolynomial.invert).transpose * gradedExtEulerMatrix (GradedModuleCat.shift π’œ) (gradedFiniteModules π’œ) (gradedFiniteModules π’œ) β‹― β‹― β‹― β‹― h bM bM = Matrix.diagonal fun (i : I) => GradedModuleCat.smulGradedDimension (e i) (S i).obj

The general-field graded Cartan/q-Euler identity. Let C be the graded Cartan matrix in a projective basis of classes [A eα΅’] and a module basis of classes [Sβ±Ό], with gdim(eα΅’ β€’ Sβ±Ό) = 0 for i β‰  j, and let E be the q-Euler matrix of the Sα΅’. If every pair of finite graded modules is graded Euler-admissible, then (C.map invert)α΅€ * E is the diagonal matrix of the graded dimensions gdim(eα΅’ β€’ Sα΅’).

source
theorem TauCeti.gradedExtEulerMatrix_eq_inv_gradedCartanMatrix_map_invert_transpose_mul_diagonal {k : Type uk} [Field k] {A : Type uA} [Ring A] [Algebra k A] {π’œ : β„€ β†’ Submodule k A} [GradedAlgebra π’œ] [Module.Finite k A] [CategoryTheory.HasExt (GradedModuleCat π’œ)] {I : Type uI} [Fintype I] [DecidableEq I] (S : I β†’ (gradedFiniteModules π’œ).FullSubcategory) {e : I β†’ A} (he : βˆ€ (i : I), IsIdempotentElem (e i)) (heβ‚€ : βˆ€ (i : I), e i ∈ π’œ 0) (hI : βˆ€ (i : I), Ideal.IsHomogeneous π’œ (Ideal.span {e i})) (hne : Pairwise fun (i j : I) => GradedModuleCat.smulGradedDimension (e i) (S j).obj = 0) (bP : Module.Basis I (LaurentPolynomial β„€) (LaurentK0 (gradedFiniteProjectiveModulesExactStructure π’œ))) (hbP : βˆ€ (i : I), bP i = LaurentK0.of (gradedFiniteProjectiveModulesExactStructure π’œ) { obj := GradedModuleCat.ofIdeal π’œ (Ideal.span {e i}) β‹―, property := β‹― }) (bM : Module.Basis I (LaurentPolynomial β„€) (LaurentK0 (gradedFiniteModulesExactStructure π’œ))) (hbM : βˆ€ (i : I), bM i = LaurentK0.of (gradedFiniteModulesExactStructure π’œ) (S i)) (hres : gradedFiniteModules π’œ ≀ (gradedModuleCanonicalExactStructure π’œ).admitsFiniteResolution (gradedFiniteProjectiveModules π’œ)) :
gradedExtEulerMatrix (GradedModuleCat.shift π’œ) (gradedFiniteModules π’œ) (gradedFiniteModules π’œ) β‹― β‹― β‹― β‹― β‹― bM bM = ((gradedCartanMatrix π’œ bP bM).map ⇑LaurentPolynomial.invert).transpose⁻¹ * Matrix.diagonal fun (i : I) => GradedModuleCat.smulGradedDimension (e i) (S i).obj

The q-Euler matrix in terms of the inverse graded Cartan matrix, over a general field. If every finite graded module has a finite graded-projective resolution, then in the bases of TauCeti.gradedCartanMatrix_map_invert_transpose_mul_gradedExtEulerMatrix_eq_diagonal, E = ((C.map invert)α΅€)⁻¹ * diagonal (fun i ↦ gdim(eα΅’ β€’ Sα΅’)).

source
theorem TauCeti.gradedExtEuler_eq_inv_gradedCartanMatrix_map_invert_transpose_mul_smulGradedDimension {k : Type uk} [Field k] {A : Type uA} [Ring A] [Algebra k A] {π’œ : β„€ β†’ Submodule k A} [GradedAlgebra π’œ] [Module.Finite k A] [CategoryTheory.HasExt (GradedModuleCat π’œ)] {I : Type uI} [Fintype I] [DecidableEq I] (S : I β†’ (gradedFiniteModules π’œ).FullSubcategory) {e : I β†’ A} (he : βˆ€ (i : I), IsIdempotentElem (e i)) (heβ‚€ : βˆ€ (i : I), e i ∈ π’œ 0) (hI : βˆ€ (i : I), Ideal.IsHomogeneous π’œ (Ideal.span {e i})) (hne : Pairwise fun (i j : I) => GradedModuleCat.smulGradedDimension (e i) (S j).obj = 0) (bP : Module.Basis I (LaurentPolynomial β„€) (LaurentK0 (gradedFiniteProjectiveModulesExactStructure π’œ))) (hbP : βˆ€ (i : I), bP i = LaurentK0.of (gradedFiniteProjectiveModulesExactStructure π’œ) { obj := GradedModuleCat.ofIdeal π’œ (Ideal.span {e i}) β‹―, property := β‹― }) (bM : Module.Basis I (LaurentPolynomial β„€) (LaurentK0 (gradedFiniteModulesExactStructure π’œ))) (hbM : βˆ€ (i : I), bM i = LaurentK0.of (gradedFiniteModulesExactStructure π’œ) (S i)) (hres : gradedFiniteModules π’œ ≀ (gradedModuleCanonicalExactStructure π’œ).admitsFiniteResolution (gradedFiniteProjectiveModules π’œ)) (i j : I) :
gradedExtEuler k (GradedModuleCat.shift π’œ) β‹― = ((gradedCartanMatrix π’œ bP bM).map ⇑LaurentPolynomial.invert).transpose⁻¹ i j * GradedModuleCat.smulGradedDimension (e j) (S j).obj

The q-Euler characteristic of two simples over a general field: if every finite graded module has a finite graded-projective resolution, then Ο‡_q(Sα΅’, Sβ±Ό) is the (i, j) entry of ((C.map invert)α΅€)⁻¹ times gdim(eβ±Ό β€’ Sβ±Ό), in the bases of TauCeti.gradedCartanMatrix_map_invert_transpose_mul_gradedExtEulerMatrix_eq_diagonal.

source
theorem TauCeti.gradedExtEulerMatrix_gradedSimpleClassBasis_eq_one {k : Type uk} [Field k] {A : Type uA} [Ring A] [Algebra k A] {π’œ : β„€ β†’ Submodule k A} [GradedAlgebra π’œ] [Module.Finite k A] [CategoryTheory.HasExt (GradedModuleCat π’œ)] {I : Type uI} [DecidableEq I] (S : I β†’ (gradedFiniteModules π’œ).FullSubcategory) {e : I β†’ A} (he : βˆ€ (i : I), IsIdempotentElem (e i)) (heβ‚€ : βˆ€ (i : I), e i ∈ π’œ 0) (hI : βˆ€ (i : I), Ideal.IsHomogeneous π’œ (Ideal.span {e i})) (hne : Pairwise fun (i j : I) => GradedModuleCat.smulGradedDimension (e i) (S j).obj = 0) (hself : βˆ€ (i : I), GradedModuleCat.smulGradedDimension (e i) (S i).obj = 1) (hS : IsExhaustiveGradedSimpleFamily S) (bP : Module.Basis I (LaurentPolynomial β„€) (LaurentK0 (gradedFiniteProjectiveModulesExactStructure π’œ))) (hbP : βˆ€ (i : I), bP i = LaurentK0.of (gradedFiniteProjectiveModulesExactStructure π’œ) { obj := GradedModuleCat.ofIdeal π’œ (Ideal.span {e i}) β‹―, property := β‹― }) :
gradedExtEulerMatrix (GradedModuleCat.shift π’œ) (gradedFiniteProjectiveModules π’œ) (gradedFiniteModules π’œ) β‹― β‹― β‹― β‹― β‹― bP (gradedSimpleClassBasis S he heβ‚€ hne hself hS) = 1

The classes [A eα΅’] are dual to the graded simples under the q-Euler form: in a projective basis consisting of the classes [A eα΅’] and the graded simple-class basis [Sβ±Ό], the matrix of the projective/module q-Euler form is the identity.

source
theorem TauCeti.gradedCartanMatrix_map_invert_transpose_mul_gradedExtEulerMatrix_eq_one {k : Type uk} [Field k] {A : Type uA} [Ring A] [Algebra k A] {π’œ : β„€ β†’ Submodule k A} [GradedAlgebra π’œ] [Module.Finite k A] [CategoryTheory.HasExt (GradedModuleCat π’œ)] {I : Type uI} [Fintype I] [DecidableEq I] (S : I β†’ (gradedFiniteModules π’œ).FullSubcategory) {e : I β†’ A} (he : βˆ€ (i : I), IsIdempotentElem (e i)) (heβ‚€ : βˆ€ (i : I), e i ∈ π’œ 0) (hI : βˆ€ (i : I), Ideal.IsHomogeneous π’œ (Ideal.span {e i})) (hne : Pairwise fun (i j : I) => GradedModuleCat.smulGradedDimension (e i) (S j).obj = 0) (hself : βˆ€ (i : I), GradedModuleCat.smulGradedDimension (e i) (S i).obj = 1) (hS : IsExhaustiveGradedSimpleFamily S) (bP : Module.Basis I (LaurentPolynomial β„€) (LaurentK0 (gradedFiniteProjectiveModulesExactStructure π’œ))) (hbP : βˆ€ (i : I), bP i = LaurentK0.of (gradedFiniteProjectiveModulesExactStructure π’œ) { obj := GradedModuleCat.ofIdeal π’œ (Ideal.span {e i}) β‹―, property := β‹― }) (h : IsGradedEulerAdmissibleOn (gradedFiniteModules π’œ) (gradedFiniteModules π’œ)) :
((gradedCartanMatrix π’œ bP (gradedSimpleClassBasis S he heβ‚€ hne hself hS)).map ⇑LaurentPolynomial.invert).transpose * gradedExtEulerMatrix (GradedModuleCat.shift π’œ) (gradedFiniteModules π’œ) (gradedFiniteModules π’œ) β‹― β‹― β‹― β‹― h (gradedSimpleClassBasis S he heβ‚€ hne hself hS) (gradedSimpleClassBasis S he heβ‚€ hne hself hS) = 1

The conjugate-transposed graded Cartan matrix inverts the q-Euler matrix of the graded simples. Let C be the graded Cartan matrix in a projective basis of classes [A eα΅’] and the graded simple-class basis [Sβ±Ό], with gdim(eα΅’ β€’ Sβ±Ό) = Ξ΄α΅’β±Ό, and let E be the q-Euler matrix of the graded simples. If every pair of finite graded modules is graded Euler-admissible, then (C.map invert)α΅€ * E = 1.

source
theorem TauCeti.gradedExtEulerMatrix_eq_inv_gradedCartanMatrix_map_invert_transpose {k : Type uk} [Field k] {A : Type uA} [Ring A] [Algebra k A] {π’œ : β„€ β†’ Submodule k A} [GradedAlgebra π’œ] [Module.Finite k A] [CategoryTheory.HasExt (GradedModuleCat π’œ)] {I : Type uI} [Fintype I] [DecidableEq I] (S : I β†’ (gradedFiniteModules π’œ).FullSubcategory) {e : I β†’ A} (he : βˆ€ (i : I), IsIdempotentElem (e i)) (heβ‚€ : βˆ€ (i : I), e i ∈ π’œ 0) (hI : βˆ€ (i : I), Ideal.IsHomogeneous π’œ (Ideal.span {e i})) (hne : Pairwise fun (i j : I) => GradedModuleCat.smulGradedDimension (e i) (S j).obj = 0) (hself : βˆ€ (i : I), GradedModuleCat.smulGradedDimension (e i) (S i).obj = 1) (hS : IsExhaustiveGradedSimpleFamily S) (bP : Module.Basis I (LaurentPolynomial β„€) (LaurentK0 (gradedFiniteProjectiveModulesExactStructure π’œ))) (hbP : βˆ€ (i : I), bP i = LaurentK0.of (gradedFiniteProjectiveModulesExactStructure π’œ) { obj := GradedModuleCat.ofIdeal π’œ (Ideal.span {e i}) β‹―, property := β‹― }) (h : IsGradedEulerAdmissibleOn (gradedFiniteModules π’œ) (gradedFiniteModules π’œ)) :
gradedExtEulerMatrix (GradedModuleCat.shift π’œ) (gradedFiniteModules π’œ) (gradedFiniteModules π’œ) β‹― β‹― β‹― β‹― h (gradedSimpleClassBasis S he heβ‚€ hne hself hS) (gradedSimpleClassBasis S he heβ‚€ hne hself hS) = ((gradedCartanMatrix π’œ bP (gradedSimpleClassBasis S he heβ‚€ hne hself hS)).map ⇑LaurentPolynomial.invert).transpose⁻¹

The q-Euler matrix of the graded simples is the inverse of the conjugate-transposed graded Cartan matrix: E = ((C.map invert)α΅€)⁻¹, in the bases of TauCeti.gradedCartanMatrix_map_invert_transpose_mul_gradedExtEulerMatrix_eq_one.

source
theorem TauCeti.gradedExtEuler_eq_inv_gradedCartanMatrix_map_invert_transpose {k : Type uk} [Field k] {A : Type uA} [Ring A] [Algebra k A] {π’œ : β„€ β†’ Submodule k A} [GradedAlgebra π’œ] [Module.Finite k A] [CategoryTheory.HasExt (GradedModuleCat π’œ)] {I : Type uI} [Fintype I] [DecidableEq I] (S : I β†’ (gradedFiniteModules π’œ).FullSubcategory) {e : I β†’ A} (he : βˆ€ (i : I), IsIdempotentElem (e i)) (heβ‚€ : βˆ€ (i : I), e i ∈ π’œ 0) (hI : βˆ€ (i : I), Ideal.IsHomogeneous π’œ (Ideal.span {e i})) (hne : Pairwise fun (i j : I) => GradedModuleCat.smulGradedDimension (e i) (S j).obj = 0) (hself : βˆ€ (i : I), GradedModuleCat.smulGradedDimension (e i) (S i).obj = 1) (hS : IsExhaustiveGradedSimpleFamily S) (bP : Module.Basis I (LaurentPolynomial β„€) (LaurentK0 (gradedFiniteProjectiveModulesExactStructure π’œ))) (hbP : βˆ€ (i : I), bP i = LaurentK0.of (gradedFiniteProjectiveModulesExactStructure π’œ) { obj := GradedModuleCat.ofIdeal π’œ (Ideal.span {e i}) β‹―, property := β‹― }) (h : IsGradedEulerAdmissibleOn (gradedFiniteModules π’œ) (gradedFiniteModules π’œ)) (i j : I) :
gradedExtEuler k (GradedModuleCat.shift π’œ) β‹― = ((gradedCartanMatrix π’œ bP (gradedSimpleClassBasis S he heβ‚€ hne hself hS)).map ⇑LaurentPolynomial.invert).transpose⁻¹ i j

The q-Euler characteristic of two graded simples is an entry of the inverse conjugate-transposed graded Cartan matrix: Ο‡_q(Sα΅’, Sβ±Ό) is the (i, j) entry of ((C.map invert)α΅€)⁻¹, in the bases of TauCeti.gradedCartanMatrix_map_invert_transpose_mul_gradedExtEulerMatrix_eq_one.

source
theorem TauCeti.isUnit_det_gradedCartanMatrix {k : Type uk} [Field k] {A : Type uA} [Ring A] [Algebra k A] {π’œ : β„€ β†’ Submodule k A} [GradedAlgebra π’œ] [Module.Finite k A] [CategoryTheory.HasExt (GradedModuleCat π’œ)] {I : Type uI} [Fintype I] [DecidableEq I] (S : I β†’ (gradedFiniteModules π’œ).FullSubcategory) {e : I β†’ A} (he : βˆ€ (i : I), IsIdempotentElem (e i)) (heβ‚€ : βˆ€ (i : I), e i ∈ π’œ 0) (hI : βˆ€ (i : I), Ideal.IsHomogeneous π’œ (Ideal.span {e i})) (hne : Pairwise fun (i j : I) => GradedModuleCat.smulGradedDimension (e i) (S j).obj = 0) (hself : βˆ€ (i : I), GradedModuleCat.smulGradedDimension (e i) (S i).obj = 1) (hS : IsExhaustiveGradedSimpleFamily S) (bP : Module.Basis I (LaurentPolynomial β„€) (LaurentK0 (gradedFiniteProjectiveModulesExactStructure π’œ))) (hbP : βˆ€ (i : I), bP i = LaurentK0.of (gradedFiniteProjectiveModulesExactStructure π’œ) { obj := GradedModuleCat.ofIdeal π’œ (Ideal.span {e i}) β‹―, property := β‹― }) (h : IsGradedEulerAdmissibleOn (gradedFiniteModules π’œ) (gradedFiniteModules π’œ)) :
IsUnit (gradedCartanMatrix π’œ bP (gradedSimpleClassBasis S he heβ‚€ hne hself hS)).det

Graded Cartan unimodularity: in the bases of TauCeti.gradedCartanMatrix_map_invert_transpose_mul_gradedExtEulerMatrix_eq_one, if every pair of finite graded modules is graded Euler-admissible, then the determinant of the graded Cartan matrix is a unit of β„€[q,q⁻¹].