Projective/simple duality for the q-Euler pairing

For a finite-dimensional graded algebra, suppose the classes of the degree-zero idempotent projectives Aeᵢ form a Laurent basis, and the idempotents cut out an exhaustive family of graded simples Sᵢ with gdim(eᵢ Sⱼ) = 0 for i ≠ j and dᵢ = gdim(eᵢ Sᵢ) ≠ 0. Then the projective/module q-Euler pairing has matrix diagonal d in these bases: χ_q(x, [Sᵢ]) = dᵢ · bar(xᵢ), where xᵢ is the ith projective coordinate of x.

Since ℤ[q,q⁻¹] is a domain, both radicals of the pairing vanish. The pairing identifies the projective Grothendieck group semilinearly with the linear dual of the module Grothendieck group, or the module group linearly with the semilinear dual of the projective group, exactly when every dᵢ is a unit of ℤ[q,q⁻¹]. For the head Sᵢ = A eᵢ / A₊eᵢ of a primitive idempotent eᵢ of a nonnegatively graded algebra with semisimple degree-zero part, the diagonal entry dᵢ is the constant dim_k End_A(Sᵢ), so perfectness fails over a field that does not split the simple modules even though nondegeneracy survives (TauCeti.gradedProjectiveExtEuler_bijective_iff_finrank_end_eq_one).

When dᵢ = 1 for every i, the projective basis maps to the usual dual basis of the simple-class basis, and coordinates in the projective basis are recovered by pairing against simples and applying LaurentPolynomial.invert. No finite-global-dimension hypothesis is needed: only projectives occur in the first argument. The finite index hypothesis is needed for surjectivity onto the full dual.

Main results

• TauCeti.gradedProjectiveExtEuler_simple_eq_mul_invert_repr: χ_q(x, [Sᵢ]) = dᵢ · bar(xᵢ).
• TauCeti.gradedProjectiveExtEuler_nondegenerate: both radicals vanish when every dᵢ ≠ 0.
• TauCeti.gradedProjectiveExtEuler_bijective_iff and TauCeti.gradedProjectiveExtEuler_flip_bijective_iff: either side is identified with the dual of the other exactly when every dᵢ is a unit.
• TauCeti.gradedProjectiveExtEuler_basis_eq_dualBasis: for dᵢ = 1 the projective basis is the dual basis of the simple-class basis.

References

• Zsuzsanna Dancso and Anthony Licata, "Koszul algebras and flow lattices", Sections 2.2 and 3.1--3.2, for q-antilinearity and the distinction between left and right duals.
• Peter Webb, A Course in Finite Group Representation Theory, Proposition 7.4.1, for the factor dim_k End_A(Sᵢ) in the pairing of projective covers with simples over a general field.

The diagonal pairing of [A eᵢ] with [Sⱼ] is TauCeti.gradedProjectiveExtEuler_basis; dual bases use Mathlib's Module.Basis.dualBasis.

theorem TauCeti.gradedProjectiveExtEuler_simple_eq_mul_invert_repr {k : Type uk} [Field k] {A : Type uA} [Ring A] [Algebra k A] [Module.Finite k A] {𝒜 : ℤ → Submodule k A} [GradedAlgebra 𝒜] [CategoryTheory.HasExt (GradedModuleCat 𝒜)] {I : Type uI} [Finite 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 := ⋯ }) (x : LaurentK0 (gradedFiniteProjectiveModulesExactStructure 𝒜)) (i : I) : ((gradedProjectiveExtEuler 𝒜) x) (LaurentK0.of (gradedFiniteModulesExactStructure 𝒜) (S i)) = GradedModuleCat.smulGradedDimension (e i) (S i).obj * LaurentPolynomial.invert ((bP.repr x) i)

Pairing a projective class against a simple class. The q-Euler pairing of x with [Sᵢ] is the diagonal graded dimension gdim(eᵢ • Sᵢ) times the conjugate of the ith projective coordinate of x.

theorem TauCeti.smulGradedDimension_mul_repr_of_isGeneratedInDegree {k : Type uk} [Field k] {A : Type uA} [Ring A] [Algebra k A] [Module.Finite k A] {𝒜 : ℤ → Submodule k A} [GradedAlgebra 𝒜] [CategoryTheory.HasExt (GradedModuleCat 𝒜)] {I : Type uI} [Finite 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 := ⋯ }) (P : (gradedFiniteProjectiveModules 𝒜).FullSubcategory) {d : ℤ} (hP : P.obj.grading.IsGeneratedInDegree A d) (hconc : ∀ (i : I) (p : ℤ), p ≠ 0 → (S i).obj.grading.piece ℤ p = ⊥) (i : I) : GradedModuleCat.smulGradedDimension (e i) (S i).obj * (bP.repr (LaurentK0.of (gradedFiniteProjectiveModulesExactStructure 𝒜) P)) i = LaurentPolynomial.C ↑(Module.finrank k (P.obj ⟶ (S i).obj.shiftObj d)) * LaurentPolynomial.T d

The projective coordinate of a module generated in degree d is a single monomial, scaled by the idempotent dimension of its degree-zero simple target.

theorem TauCeti.gradedProjectiveExtEuler_injective {k : Type uk} [Field k] {A : Type uA} [Ring A] [Algebra k A] [Module.Finite k A] {𝒜 : ℤ → Submodule k A} [GradedAlgebra 𝒜] [CategoryTheory.HasExt (GradedModuleCat 𝒜)] {I : Type uI} [Finite 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 ≠ 0) : Function.Injective ⇑(gradedProjectiveExtEuler 𝒜)

The q-Euler pairing separates projective classes when every diagonal graded dimension gdim(eᵢ • Sᵢ) is nonzero.

theorem TauCeti.gradedProjectiveExtEuler_flip_injective {k : Type uk} [Field k] {A : Type uA} [Ring A] [Algebra k A] [Module.Finite k A] {𝒜 : ℤ → Submodule k A} [GradedAlgebra 𝒜] [CategoryTheory.HasExt (GradedModuleCat 𝒜)] {I : Type uI} (S : I → (gradedFiniteModules 𝒜).FullSubcategory) {e : I → A} (he : ∀ (i : I), IsIdempotentElem (e i)) (he₀ : ∀ (i : I), e i ∈ 𝒜 0) (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) : Function.Injective ⇑(gradedProjectiveExtEuler 𝒜).flip

The q-Euler pairing separates module classes when every diagonal graded dimension gdim(eᵢ • Sᵢ) is nonzero: pairing against [A eᵢ] reads gdim(eᵢ • Sᵢ) times the ith simple-class coordinate.

theorem TauCeti.gradedProjectiveExtEuler_nondegenerate {k : Type uk} [Field k] {A : Type uA} [Ring A] [Algebra k A] [Module.Finite k A] {𝒜 : ℤ → Submodule k A} [GradedAlgebra 𝒜] [CategoryTheory.HasExt (GradedModuleCat 𝒜)] {I : Type uI} [Finite 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 ≠ 0) (hS : IsExhaustiveGradedSimpleFamily S) : (gradedProjectiveExtEuler 𝒜).Nondegenerate

Both radicals of the projective/module q-Euler pairing vanish when every diagonal graded dimension gdim(eᵢ • Sᵢ) is nonzero. This does not identify either side with the dual of the other; see TauCeti.gradedProjectiveExtEuler_bijective_iff.

theorem TauCeti.gradedProjectiveExtEuler_bijective_iff {k : Type uk} [Field k] {A : Type uA} [Ring A] [Algebra k A] [Module.Finite k A] {𝒜 : ℤ → Submodule k A} [GradedAlgebra 𝒜] [CategoryTheory.HasExt (GradedModuleCat 𝒜)] {I : Type uI} [Finite 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 ≠ 0) (hS : IsExhaustiveGradedSimpleFamily S) : Function.Bijective ⇑(gradedProjectiveExtEuler 𝒜) ↔ ∀ (i : I), IsUnit (GradedModuleCat.smulGradedDimension (e i) (S i).obj)

The q-Euler pairing identifies the projective group with the dual of the module group exactly when every diagonal graded dimension is a unit. Every linear functional on G₀^gr(mod A) is χ_q(x, -) for exactly one projective class x if and only if each gdim(eᵢ • Sᵢ) is a unit of ℤ[q,q⁻¹].

theorem TauCeti.gradedProjectiveExtEuler_flip_bijective_iff {k : Type uk} [Field k] {A : Type uA} [Ring A] [Algebra k A] [Module.Finite k A] {𝒜 : ℤ → Submodule k A} [GradedAlgebra 𝒜] [CategoryTheory.HasExt (GradedModuleCat 𝒜)] {I : Type uI} [Finite 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 ≠ 0) (hS : IsExhaustiveGradedSimpleFamily S) : Function.Bijective ⇑(gradedProjectiveExtEuler 𝒜).flip ↔ ∀ (i : I), IsUnit (GradedModuleCat.smulGradedDimension (e i) (S i).obj)

The q-Euler pairing identifies the module group with the semilinear dual of the projective group exactly when every diagonal graded dimension is a unit. Every q ↦ q⁻¹ semilinear functional on K₀^gr(proj A) is χ_q(-, y) for exactly one module class y if and only if each gdim(eᵢ • Sᵢ) is a unit of ℤ[q,q⁻¹].

Kronecker diagonal

theorem TauCeti.gradedProjectiveExtEuler_basis_eq_dualBasis {k : Type uk} [Field k] {A : Type uA} [Ring A] [Algebra k A] [Module.Finite k A] {𝒜 : ℤ → Submodule k A} [GradedAlgebra 𝒜] [CategoryTheory.HasExt (GradedModuleCat 𝒜)] {I : Type uI} [Finite 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) (i : I) : (gradedProjectiveExtEuler 𝒜) (bP i) = (gradedSimpleClassBasis S he he₀ hne hself hS).dualBasis i

The projective basis vectors are the linear dual basis of the graded simple classes under the q-Euler pairing.