Documentation

TauCeti.Algebra.Category.GradedModuleCat.CartanMap.ExtEuler.Basic

The q-Euler form between graded projectives and finite graded modules #

Let A be a finite-dimensional algebra over a field k, graded by π’œ : β„€ β†’ Submodule k A. A finitely generated graded projective P has no higher Ext, and its graded maps into the shifts M{j} of a finite graded module M vanish for all but finitely many j. Hence every such pair is graded Euler-admissible, and the q-Euler characteristic descends to a form

Ο‡_q : Kβ‚€^gr(proj A) Γ— Gβ‚€^gr(mod A) ⟢ β„€[q,q⁻¹],

q-antilinear in the first variable and q-linear in the second. It is defined on the same Laurent Grothendieck groups as the graded Cartan map TauCeti.gradedCartanMap.

For an idempotent f of degree zero, a graded map Af ⟢ M is determined by the image of f, which can be any vector of f β€’ Mβ‚€. Therefore Ο‡_q(Af, M) = βˆ‘β±Ό q⁻ʲ dim_k(f β€’ Mβ‚‹β±Ό) = βˆ‘β‚š dim_k(f β€’ Mβ‚š) qα΅–: pairing against [Af] is the idempotent coordinate TauCeti.gradedIdempotentCoordinate. In particular, if the degree-zero idempotents eα΅’ cut out graded simples Sα΅’ with gdim(eα΅’ β€’ Sβ±Ό) = 0 for i β‰  j, then Ο‡_q([A eα΅’], [Sβ±Ό]) is gdim(eα΅’ β€’ Sα΅’) on the diagonal and 0 off it. When moreover every gdim(eα΅’ β€’ Sα΅’) = 1, the classes [A eα΅’] pair with Gβ‚€^gr(mod A) as the coordinate functionals of the graded simple-class basis. This is the graded form of the duality between projective covers and simples.

Main definitions #

Main results #

References #

source
theorem TauCeti.gradedExtEuler_directSumObj {k : Type uk} [Field k] {A : Type uA} [Ring A] [Algebra k A] {π’œ : β„€ β†’ Submodule k A} [CategoryTheory.HasExt (GradedModuleCat π’œ)] {J : Type uJ} [Fintype J] (e : GradedModuleCat π’œ β‰Œ GradedModuleCat π’œ) (M : J β†’ GradedModuleCat π’œ) [βˆ€ (j : J), CategoryTheory.Projective (M j)] (Y : GradedModuleCat π’œ) (h : IsGradedEulerAdmissible k e (GradedModuleCat.directSumObj M) Y) (hj : βˆ€ (j : J), IsGradedEulerAdmissible k e (M j) Y) :
gradedExtEuler k e h = βˆ‘ j : J, gradedExtEuler k e β‹―

The q-Euler characteristic of a finite direct sum of projective graded modules is the sum of the characteristics of the summands, for any grading-shift autoequivalence and admissible pairs.

Evaluation against Af #

source
@[simp]
theorem TauCeti.gradedExtEuler_ofIdeal_span_singleton {k : Type uk} [Field k] {A : Type uA} [Ring A] [Algebra k A] {π’œ : β„€ β†’ Submodule k A} [GradedAlgebra π’œ] [CategoryTheory.HasExt (GradedModuleCat π’œ)] {f : A} (hf : IsIdempotentElem f) (hfβ‚€ : f ∈ π’œ 0) (hI : Ideal.IsHomogeneous π’œ (Ideal.span {f})) (M : GradedModuleCat π’œ) [Module.Finite k M.carrier] (h : IsGradedEulerAdmissible k (GradedModuleCat.shift π’œ) (GradedModuleCat.ofIdeal π’œ (Ideal.span {f}) hI) M) :
gradedExtEuler k (GradedModuleCat.shift π’œ) h = GradedModuleCat.smulGradedDimension f M

The q-Euler characteristic against Af is the idempotent graded dimension: for an idempotent f of degree zero and a finite-dimensional graded module M, Ο‡_q(Af, M) = βˆ‘β‚š dim_k(f β€’ Mβ‚š) qα΅–. This holds for every admissibility witness and every HasExt instance.

Graded Euler-admissibility of projective pairs #

source
theorem TauCeti.isGradedEulerAdmissibleOn_gradedFiniteProjectiveModules_gradedFiniteModules {k : Type uk} [Field k] {A : Type uA} [Ring A] [Algebra k A] {π’œ : β„€ β†’ Submodule k A} [GradedAlgebra π’œ] [Module.Finite k A] [CategoryTheory.HasExt (GradedModuleCat π’œ)] :
IsGradedEulerAdmissibleOn (gradedFiniteProjectiveModules π’œ) (gradedFiniteModules π’œ)

Finite graded projectives and finite graded modules form graded Euler-admissible pairs: higher Ext out of a projective vanishes, and its graded Hom spaces into the shifts of a finite graded module have finite Laurent support.

The q-Euler form on graded Grothendieck groups #

source
noncomputable def TauCeti.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 π’œ)] :
LaurentK0 (gradedFiniteProjectiveModulesExactStructure π’œ) β†’β‚›β‚—[LaurentPolynomial.invert.toRingEquiv.toRingHom] LaurentK0 (gradedFiniteModulesExactStructure π’œ) β†’β‚—[LaurentPolynomial β„€] LaurentPolynomial β„€

The q-Euler form between graded projectives and finite graded modules, Kβ‚€^gr(proj A) Γ— Gβ‚€^gr(mod A) β†’ β„€[q,q⁻¹]. It is q-antilinear in the first variable and q-linear in the second, and its value on two classes is the graded Ext-Euler characteristic.

Instances For
    source
    theorem TauCeti.gradedProjectiveExtEuler_def {k : Type uk} [Field k] {A : Type uA} [Ring A] [Algebra k A] {π’œ : β„€ β†’ Submodule k A} [GradedAlgebra π’œ] [Module.Finite k A] [CategoryTheory.HasExt (GradedModuleCat π’œ)] :
    gradedProjectiveExtEuler π’œ = gradedExtEulerSesquilinear β‹― β‹― β‹― β‹― β‹―

    The projective/module q-Euler form is the generic graded Ext-Euler sesquilinear form for the two induced graded abelian exact subcategories.

    source
    @[simp]
    theorem TauCeti.gradedProjectiveExtEuler_of_of {k : Type uk} [Field k] {A : Type uA} [Ring A] [Algebra k A] {π’œ : β„€ β†’ Submodule k A} [GradedAlgebra π’œ] [Module.Finite k A] [CategoryTheory.HasExt (GradedModuleCat π’œ)] (P : (gradedFiniteProjectiveModules π’œ).FullSubcategory) (M : (gradedFiniteModules π’œ).FullSubcategory) :
    ((gradedProjectiveExtEuler π’œ) (LaurentK0.of (gradedFiniteProjectiveModulesExactStructure π’œ) P)) (LaurentK0.of (gradedFiniteModulesExactStructure π’œ) M) = gradedExtEuler k (GradedModuleCat.shift π’œ) β‹―

    The q-Euler form evaluates on two classes as the graded Ext-Euler characteristic.

    source
    @[simp]
    theorem TauCeti.gradedProjectiveExtEuler_ofIdeal_span_singleton {k : Type uk} [Field k] {A : Type uA} [Ring A] [Algebra k A] {π’œ : β„€ β†’ Submodule k A} [GradedAlgebra π’œ] [Module.Finite k A] [CategoryTheory.HasExt (GradedModuleCat π’œ)] {f : A} (hf : IsIdempotentElem f) (hfβ‚€ : f ∈ π’œ 0) (hI : Ideal.IsHomogeneous π’œ (Ideal.span {f})) :
    (gradedProjectiveExtEuler π’œ) (LaurentK0.of (gradedFiniteProjectiveModulesExactStructure π’œ) { obj := GradedModuleCat.ofIdeal π’œ (Ideal.span {f}) hI, property := β‹― }) = gradedIdempotentCoordinate hf hfβ‚€

    Pairing against [Af] is the idempotent coordinate of f: for an idempotent f of degree zero, Ο‡_q([Af], -) is the β„€[q,q⁻¹]-linear map sending [M] to βˆ‘β‚š dim_k(f β€’ Mβ‚š) qα΅–.

    source
    @[simp]
    theorem TauCeti.gradedExtEulerSesquilinear_gradedCartanMap {k : Type uk} [Field k] {A : Type uA} [Ring A] [Algebra k A] {π’œ : β„€ β†’ Submodule k A} [GradedAlgebra π’œ] [Module.Finite k A] [CategoryTheory.HasExt (GradedModuleCat π’œ)] (h : IsGradedEulerAdmissibleOn (gradedFiniteModules π’œ) (gradedFiniteModules π’œ)) (x : LaurentK0 (gradedFiniteProjectiveModulesExactStructure π’œ)) (y : LaurentK0 (gradedFiniteModulesExactStructure π’œ)) :
    ((gradedExtEulerSesquilinear β‹― β‹― β‹― β‹― h) ((gradedCartanMap π’œ) x)) y = ((gradedProjectiveExtEuler π’œ) x) y

    The q-Euler form is compatible with the graded Cartan map: if every pair of finite graded modules is graded Euler-admissible, then pairing the image of a projective class x under the graded Cartan map against y gives the projective/module q-Euler form Ο‡_q(x, y).

    Duality with graded simples #

    source
    @[simp]
    theorem TauCeti.gradedProjectiveExtEuler_basis {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} (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) [DecidableEq I] (i j : I) :
    ((gradedProjectiveExtEuler π’œ) (LaurentK0.of (gradedFiniteProjectiveModulesExactStructure π’œ) { obj := GradedModuleCat.ofIdeal π’œ (Ideal.span {e i}) β‹―, property := β‹― })) (LaurentK0.of (gradedFiniteModulesExactStructure π’œ) (S j)) = if i = j then GradedModuleCat.smulGradedDimension (e i) (S i).obj else 0

    Diagonal pairing under the q-Euler form: if the finite graded modules Sβ±Ό and the degree-zero idempotents eα΅’ satisfy gdim(eα΅’ β€’ Sβ±Ό) = 0 for i β‰  j, then Ο‡_q([A eα΅’], [Sβ±Ό]) is gdim(eα΅’ β€’ Sα΅’) for i = j and 0 otherwise.

    source
    theorem TauCeti.gradedProjectiveExtEuler_ofIdeal_span_singleton_eq_mul_repr {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} (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) (i : I) (x : LaurentK0 (gradedFiniteModulesExactStructure π’œ)) :
    ((gradedProjectiveExtEuler π’œ) (LaurentK0.of (gradedFiniteProjectiveModulesExactStructure π’œ) { obj := GradedModuleCat.ofIdeal π’œ (Ideal.span {e i}) β‹―, property := β‹― })) x = GradedModuleCat.smulGradedDimension (e i) (S i).obj * ((gradedSimpleClassBasisOfNeZero S he heβ‚€ hne hself hS).repr x) i

    Pairing against [A eα΅’] is a multiple of the ith simple-class coordinate: for an exhaustive family of graded simples Sα΅’ cut out by degree-zero idempotents eα΅’ with nonzero diagonal graded dimensions, Ο‡_q([A eα΅’], x) is gdim(eα΅’ β€’ Sα΅’) times the ith coordinate of x in the graded simple-class basis of Gβ‚€^gr(mod A).

    source
    @[simp]
    theorem TauCeti.gradedProjectiveExtEuler_ofIdeal_span_singleton_eq_repr {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} (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) (i : I) (x : LaurentK0 (gradedFiniteModulesExactStructure π’œ)) :
    ((gradedProjectiveExtEuler π’œ) (LaurentK0.of (gradedFiniteProjectiveModulesExactStructure π’œ) { obj := GradedModuleCat.ofIdeal π’œ (Ideal.span {e i}) β‹―, property := β‹― })) x = ((gradedSimpleClassBasis S he heβ‚€ hne hself hS).repr x) i

    Pairing against [A eα΅’] is the ith simple-class coordinate: for an exhaustive family of graded simples Sα΅’ cut out by degree-zero idempotents eα΅’ with gdim(eα΅’ β€’ Sβ±Ό) = Ξ΄α΅’β±Ό, the form Ο‡_q([A eα΅’], -) is the ith coordinate functional of the graded simple-class basis of Gβ‚€^gr(mod A).