Documentation

TauCeti.Algebra.Category.GradedModuleCat.CartanMap.ExtEuler.Poincare

The graded Cartan matrix and the diagonal Ext Poincaré matrix #

Let A be a finite-dimensional graded algebra over a field k, let the Sᵢ be concentrated in internal degree zero, and let C be the graded Cartan matrix in a projective basis of classes [A eᵢ] and a module basis [Sⱼ]. The diagonal Ext Poincaré matrix P(t) has (i, j) entry ∑ n, dim_k Extⁿ(Sᵢ, Sⱼ{n}) tⁿ (TauCeti.diagonalExtPoincareMatrix, truncated below a cohomological vanishing bound).

If every pair of finite graded modules is graded Euler-admissible, every Sᵢ has a linear graded projective resolution, and gdim(eᵢ • Sⱼ) = 0 for i ≠ j, then Cᵀ · P(-q) = diagonal (fun i ↦ gdim(eᵢ • Sᵢ)). When Aeᵢ covers the simple Sᵢ, the corresponding diagonal entry is the constant dim_k End_A(Sᵢ). This retains the division-algebra factor over a general field. If all these dimensions are one, the identity says that P(-q) is the inverse of Cᵀ.

The identity follows from the conjugate-transpose relation between the graded Cartan and q-Euler matrices. For a linearly resolved source and a degree-zero target, invert χ_q(Sᵢ, Sⱼ) = Pᵢⱼ(-q) (TauCeti.GradedProjectiveResolution.IsLinear.invert_gradedExtEuler_eq_eval₂). The constant diagonal is fixed by the Laurent involution.

Main results #

A common truncation degree for finitely many simples exists by TauCeti.exists_forall_isGradedExtBoundedBy, and the truncated matrix does not depend on its choice (TauCeti.diagonalExtPoincareMatrix_eq_of_le).

References #

theorem TauCeti.gradedCartanMatrix_transpose_mul_gradedExtEulerMatrix_map_invert_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 𝒜)) (hconc : ∀ (i : I) (p : ℤ), p ≠ 0 → (S i).obj.grading.piece ℤ p = ⊥) :

The graded Cartan matrix against the inverted q-Euler matrix. If every Sᵢ is concentrated in internal degree zero, then Cᵀ · Ē = diagonal (fun i ↦ gdim(eᵢ • Sᵢ)), where Ē is the q-Euler matrix of the Sᵢ with q ↦ q⁻¹ applied to every entry. Concentration makes the diagonal entries constant, hence fixed by the involution.

theorem TauCeti.gradedCartanMatrix_transpose_mul_diagonalExtPoincareMatrix_map_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 𝒜)) (hlin : ∀ (i : I), ∃ (r : GradedProjectiveResolution 𝒜 (S i).obj.grading), r.IsLinear) (hconc : ∀ (i : I) (p : ℤ), p ≠ 0 → (S i).obj.grading.piece ℤ p = ⊥) {b : ℕ} (hb : ∀ (i j : I), IsGradedExtBoundedBy (GradedModuleCat.shift 𝒜) (S i).obj (S j).obj b) :

The general-field Cartan--Poincaré identity. Let C be the graded Cartan matrix in a projective basis of classes [A eᵢ] and the module basis [Sⱼ], with gdim(eᵢ • Sⱼ) = 0 for i ≠ j. Suppose every pair of finite graded modules is graded Euler-admissible, that every Sᵢ is concentrated in internal degree zero and has a linear graded projective resolution, and that b bounds the cohomological support of Ext between any two Sᵢ. Then Cᵀ · P(-q) = diagonal (fun i ↦ gdim(eᵢ • Sᵢ)), where P is the diagonal Ext Poincaré matrix truncated below b. Concentration makes these diagonal entries constant.

theorem TauCeti.gradedCartanMatrix_transpose_mul_diagonalExtPoincareMatrix_map_eq_diagonal_finrank_end {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)) [∀ (i : I), IsSimpleModule A (S i).obj.carrier] {f : (i : I) → ↥(Ideal.span {e i}) →ₗ[A] (S i).obj.carrier} (hf : ∀ (i : I), IsProjectiveCover (f i)) (h : IsGradedEulerAdmissibleOn (gradedFiniteModules 𝒜) (gradedFiniteModules 𝒜)) (hlin : ∀ (i : I), ∃ (r : GradedProjectiveResolution 𝒜 (S i).obj.grading), r.IsLinear) (hconc : ∀ (i : I) (p : ℤ), p ≠ 0 → (S i).obj.grading.piece ℤ p = ⊥) {b : ℕ} (hb : ∀ (i j : I), IsGradedExtBoundedBy (GradedModuleCat.shift 𝒜) (S i).obj (S j).obj b) :

The division-endomorphism correction to the Cartan--Poincaré identity. If the Aeᵢ cover the degree-zero simples Sᵢ, the diagonal is dim_k End_A(Sᵢ), without a splitting-field hypothesis.

theorem TauCeti.diagonalExtPoincareMatrix_map_eq_inv_gradedCartanMatrix_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) (bP : Module.Basis I (LaurentPolynomial ℤ) (LaurentK0 (gradedFiniteProjectiveModulesExactStructure 𝒜))) (hbP : ∀ (i : I), bP i = LaurentK0.of (gradedFiniteProjectiveModulesExactStructure 𝒜) { obj := GradedModuleCat.ofIdeal 𝒜 (Ideal.span {e i}) ⋯, property := ⋯ }) (hself : ∀ (i : I), GradedModuleCat.smulGradedDimension (e i) (S i).obj = 1) (hS : IsExhaustiveGradedSimpleFamily S) (h : IsGradedEulerAdmissibleOn (gradedFiniteModules 𝒜) (gradedFiniteModules 𝒜)) (hlin : ∀ (i : I), ∃ (r : GradedProjectiveResolution 𝒜 (S i).obj.grading), r.IsLinear) (hconc : ∀ (i : I) (p : ℤ), p ≠ 0 → (S i).obj.grading.piece ℤ p = ⊥) {b : ℕ} (hb : ∀ (i j : I), IsGradedExtBoundedBy (GradedModuleCat.shift 𝒜) (S i).obj (S j).obj b) :

The diagonal Ext Poincaré matrix at -q is the inverse of the transposed graded Cartan matrix: P(-q) = (Cᵀ)⁻¹, under the hypotheses of TauCeti.gradedCartanMatrix_transpose_mul_diagonalExtPoincareMatrix_map_eq_diagonal, when all the idempotent diagonal dimensions are one.