Bigraded Ext diagonality and the Cartan--Poincare identity

Let A be a finite-dimensional nonnegatively graded algebra, and let the S i be the simple-class basis used by a graded Cartan matrix, with the projective basis consisting of the corresponding idempotent projectives. If the full bigraded Ext Poincare matrix of the S i is diagonal, the general linear-resolution criterion shows that chosen minimal resolutions of the S i are linear. The Cartan--Poincare identity then gives

C^T * P(-q) = diagonal (fun i ↦ gdim(eᵢ • Sᵢ)).

The diagonal polynomial P forgets all off-diagonal Ext groups, while the q-Euler form can cancel groups in different cohomological degrees, so this identity alone is not asserted to imply linearity.

The converse does hold for the total Ext Poincaré matrix P_tot, whose (i, j) entry is ∑ n, dim_k Extⁿ(Sᵢ, ⨁ p, Sⱼ{p}) tⁿ: linearity of the minimal resolutions is equivalent to C^T * P_tot(-q) = diagonal (fun i ↦ gdim(eᵢ • Sᵢ)). Here P_tot(-q) is the matrix of Maslov-graded Euler characteristics TauCeti.Bigraded.maslovEuler of the full bigraded Ext Poincaré matrix. Comparing this identity with the conjugate-transpose relation for the q-Euler matrix gives TauCeti.Bigraded.euler = TauCeti.Bigraded.maslovEuler entrywise. Minimality places every Ext group on or above the diagonal. By TauCeti.Bigraded.euler_eq_maslovEuler_iff_isDiagonal no cancellation is then possible, and the bigraded matrix is diagonal.

Main results

• TauCeti.cartan_poincare_of_bigradedExtPoincareMatrix_isDiagonal: full bigraded diagonality implies the graded Cartan--Poincare identity.
• TauCeti.cartan_poincare_of_bigradedExtPoincareMatrix_isDiagonal_of_semisimple: the same implication over a semisimple degree-zero part, without chosen resolutions.
• TauCeti.forall_isLinear_iff_cartan_poincare_maslovEuler: chosen minimal resolutions are linear exactly when the Cartan--Poincaré identity holds for the total Ext Poincaré matrix.
• TauCeti.forall_exists_isLinear_iff_cartan_poincare_maslovEuler: the same equivalence over a semisimple degree-zero part, without chosen resolutions.

References

• A. Beilinson, V. Ginzburg and W. Soergel, Koszul duality patterns in representation theory, Sections 1.2 and 2.11, for diagonal bigraded Ext and the Cartan--Poincare identity.
• L. Positselski, The correspondence between Hilbert series of quadratically dual algebras does not imply their having the Koszul property, Funct. Anal. Appl. 29 (1995), 213--217, for quadratic algebras satisfying the diagonal identity without being Koszul.
• C. Nastasescu and F. Van Oystaeyen, Methods of Graded Rings, Section 2.3, for minimal graded projective resolutions and the diagonal Ext criterion.

theorem TauCeti.cartan_poincare_of_bigradedExtPoincareMatrix_isDiagonal {k : Type uk} [Field k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} [GradedAlgebra 𝒜] [CategoryTheory.HasExt (GradedModuleCat 𝒜)] {I : Type uI} [Module.Finite k A] [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 ≠ 0) (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 𝒜)) (r : (i : I) → GradedProjectiveResolution 𝒜 (S i).obj.grading) [∀ (i : I) (n : ℕ), Module.Finite k ((r i).X n)] (hr : ∀ (i : I), (r i).IsMinimal) (hneg : ∀ p < 0, 𝒜 p = ⊥) (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) (hdiag : ∀ (i j : I), Bigraded.IsDiagonal (bigradedExtPoincareMatrix (fun (i : I) => (S i).obj) ⋯ b i j)) : (gradedCartanMatrix 𝒜 bP (gradedSimpleClassBasisOfNeZero S he he₀ hne hself hS)).transpose * (diagonalExtPoincareMatrix k (fun (i : I) => (S i).obj) b).map ⇑(Polynomial.eval₂RingHom LaurentPolynomial.C (-LaurentPolynomial.T 1)) = Matrix.diagonal fun (i : I) => GradedModuleCat.smulGradedDimension (e i) (S i).obj

Full bigraded diagonality implies the Cartan--Poincare identity. If every entry of the full bigraded Ext Poincare matrix is diagonal, then the chosen minimal resolutions are linear and C^T * P(-q) = diagonal (fun i ↦ gdim(eᵢ • Sᵢ)) in the chosen projective and simple bases.

The hypothesis retains the off-diagonal Ext data needed to detect linearity. The conclusion uses the diagonal Poincare matrix because, after linearity is known, those are all the surviving Ext groups.

theorem TauCeti.cartan_poincare_of_bigradedExtPoincareMatrix_isDiagonal_of_semisimple {k : Type uk} [Field k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} [GradedAlgebra 𝒜] [CategoryTheory.HasExt (GradedModuleCat 𝒜)] {I : Type uI} [Module.Finite k A] [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 ≠ 0) (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 := ⋯ }) [IsSemisimpleRing ↥(𝒜 0)] (h : IsGradedEulerAdmissibleOn (gradedFiniteModules 𝒜) (gradedFiniteModules 𝒜)) (hneg : ∀ p < 0, 𝒜 p = ⊥) (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) (hdiag : ∀ (i j : I), Bigraded.IsDiagonal (bigradedExtPoincareMatrix (fun (i : I) => (S i).obj) ⋯ b i j)) : (gradedCartanMatrix 𝒜 bP (gradedSimpleClassBasisOfNeZero S he he₀ hne hself hS)).transpose * (diagonalExtPoincareMatrix k (fun (i : I) => (S i).obj) b).map ⇑(Polynomial.eval₂RingHom LaurentPolynomial.C (-LaurentPolynomial.T 1)) = Matrix.diagonal fun (i : I) => GradedModuleCat.smulGradedDimension (e i) (S i).obj

The Cartan--Poincare identity over a semisimple degree-zero part. If A is finite-dimensional and nonnegatively graded, its degree-zero part is semisimple, the chosen simples are concentrated in degree zero, and their full bigraded Ext Poincare matrix is diagonal, then C^T * P(-q) = diagonal (fun i ↦ gdim(eᵢ • Sᵢ)).

The diagonal entries are nonzero and need not be one; for projective covers of degree-zero simples they are the constants dim_k End_A(Sᵢ). The semisimplicity hypothesis supplies minimal projective resolutions with finite-dimensional terms, so no resolutions or minimality witnesses occur in the public statement.

theorem TauCeti.forall_isLinear_iff_cartan_poincare_maslovEuler {k : Type uk} [Field k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} [GradedAlgebra 𝒜] [CategoryTheory.HasExt (GradedModuleCat 𝒜)] {I : Type uI} [Module.Finite k A] [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 ≠ 0) (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 𝒜)) (r : (i : I) → GradedProjectiveResolution 𝒜 (S i).obj.grading) [∀ (i : I) (n : ℕ), Module.Finite k ((r i).X n)] (hr : ∀ (i : I), (r i).IsMinimal) (hneg : ∀ p < 0, 𝒜 p = ⊥) (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) : (∀ (i : I), (r i).IsLinear) ↔ (gradedCartanMatrix 𝒜 bP (gradedSimpleClassBasisOfNeZero S he he₀ hne hself hS)).transpose * (bigradedExtPoincareMatrix (fun (i : I) => (S i).obj) ⋯ b).map ⇑Bigraded.maslovEuler = Matrix.diagonal fun (i : I) => GradedModuleCat.smulGradedDimension (e i) (S i).obj

Linearity is the Cartan--Poincaré identity for the total Ext Poincaré series. Let P be the full bigraded Ext Poincaré matrix of the Sᵢ, and apply the Maslov-graded Euler characteristic to each entry. The result is P_tot(-q), where P_tot has (i, j) entry ∑ n, dim_k Extⁿ(Sᵢ, ⨁ p, Sⱼ{p}) tⁿ. Chosen minimal resolutions with finite-dimensional terms are all linear exactly when Cᵀ · P_tot(-q) = diagonal (fun i ↦ gdim(eᵢ • Sᵢ)).

The diagonal Poincaré matrix TauCeti.diagonalExtPoincareMatrix cannot replace P_tot here: it discards the off-diagonal Ext groups, whose contributions to the q-Euler form can cancel.

theorem TauCeti.forall_exists_isLinear_iff_cartan_poincare_maslovEuler {k : Type uk} [Field k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} [GradedAlgebra 𝒜] [CategoryTheory.HasExt (GradedModuleCat 𝒜)] {I : Type uI} [Module.Finite k A] [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 ≠ 0) (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 := ⋯ }) [IsSemisimpleRing ↥(𝒜 0)] (h : IsGradedEulerAdmissibleOn (gradedFiniteModules 𝒜) (gradedFiniteModules 𝒜)) (hneg : ∀ p < 0, 𝒜 p = ⊥) (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) : (∀ (i : I), ∃ (r : GradedProjectiveResolution 𝒜 (S i).obj.grading), r.IsLinear) ↔ (gradedCartanMatrix 𝒜 bP (gradedSimpleClassBasisOfNeZero S he he₀ hne hself hS)).transpose * (bigradedExtPoincareMatrix (fun (i : I) => (S i).obj) ⋯ b).map ⇑Bigraded.maslovEuler = Matrix.diagonal fun (i : I) => GradedModuleCat.smulGradedDimension (e i) (S i).obj

Linearity is the Cartan--Poincaré identity over a semisimple degree-zero part. If A is finite-dimensional and nonnegatively graded with semisimple degree-zero part, every Sᵢ has a linear graded projective resolution exactly when Cᵀ · P_tot(-q) = diagonal (fun i ↦ gdim(eᵢ • Sᵢ)) for the total Ext Poincaré matrix P_tot, as in TauCeti.forall_isLinear_iff_cartan_poincare_maslovEuler.