Documentation

TauCeti.Algebra.Category.GradedModuleCat.Idempotent.GradedDimension

Idempotent graded dimensions of graded modules #

Let A be a k-algebra with homogeneous pieces π’œ : β„€ β†’ Submodule k A, and let e ∈ π’œ 0 be an idempotent of degree zero. For a graded A-module M, a morphism restricts degreewise to the subspaces e β€’ Mβ‚š. These restrictions preserve exactness, and hence the Laurent-polynomial-valued graded dimension

gdim_e(M) = βˆ‘β‚š dim_k(e β€’ Mβ‚š) qα΅–

is additive on short exact sequences of finite-dimensional graded modules. Shifting the grading by n multiplies this dimension by qⁿ.

Main definitions #

Main results #

References #

The subspaces e β€’ Mβ‚š #

source
def TauCeti.GradedModuleCat.smulPieceMap {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] {π’œ : β„€ β†’ Submodule k A} (e : A) {M N : GradedModuleCat π’œ} (f : M ⟢ N) (p : β„€) :
β†₯(e β€’ M.grading.piece β„€ p) β†’β‚—[k] β†₯(e β€’ N.grading.piece β„€ p)

A morphism of graded modules restricts to the subspaces e β€’ Mβ‚š ⟢ e β€’ Nβ‚š.

Instances For
    source
    @[simp]
    theorem TauCeti.GradedModuleCat.coe_smulPieceMap_apply {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] {π’œ : β„€ β†’ Submodule k A} (e : A) {M N : GradedModuleCat π’œ} (f : M ⟢ N) (p : β„€) (x : β†₯(e β€’ M.grading.piece β„€ p)) :
    ↑((smulPieceMap e f p) x) = f.hom ↑x
    source
    @[simp]
    theorem TauCeti.GradedModuleCat.smulPieceMap_id {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] {π’œ : β„€ β†’ Submodule k A} (e : A) (M : GradedModuleCat π’œ) (p : β„€) :
    smulPieceMap e (CategoryTheory.CategoryStruct.id M) p = LinearMap.id
    source
    @[simp]
    theorem TauCeti.GradedModuleCat.smulPieceMap_comp {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] {π’œ : β„€ β†’ Submodule k A} (e : A) {M N P : GradedModuleCat π’œ} (f : M ⟢ N) (g : N ⟢ P) (p : β„€) :
    smulPieceMap e (CategoryTheory.CategoryStruct.comp f g) p = smulPieceMap e g p βˆ˜β‚— smulPieceMap e f p
    source
    theorem TauCeti.GradedModuleCat.smulPieceMap_injective {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] {π’œ : β„€ β†’ Submodule k A} {e : A} {M N : GradedModuleCat π’œ} {f : M ⟢ N} (hf : Function.Injective ⇑f.hom) (p : β„€) :
    Function.Injective ⇑(smulPieceMap e f p)

    Restriction to e β€’ Mβ‚š preserves injectivity.

    source
    theorem TauCeti.GradedModuleCat.smulPieceMap_surjective {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] {π’œ : β„€ β†’ Submodule k A} {e : A} {N P : GradedModuleCat π’œ} {g : N ⟢ P} (hg : Function.Surjective ⇑g.hom) (p : β„€) :
    Function.Surjective ⇑(smulPieceMap e g p)

    Restriction to e β€’ Mβ‚š preserves surjectivity: a preimage can be chosen of degree p.

    source
    theorem TauCeti.GradedModuleCat.smul_grading_piece_le {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] {π’œ : β„€ β†’ Submodule k A} {e : A} (heβ‚€ : e ∈ π’œ 0) (M : GradedModuleCat π’œ) (p : β„€) :
    e β€’ M.grading.piece β„€ p ≀ M.grading.piece β„€ p

    An element of degree zero carries Mβ‚š into itself.

    source
    theorem TauCeti.GradedModuleCat.mem_smul_grading_piece_iff {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] {π’œ : β„€ β†’ Submodule k A} {e : A} (he : IsIdempotentElem e) (heβ‚€ : e ∈ π’œ 0) {M : GradedModuleCat π’œ} {p : β„€} {x : M.carrier} :
    x ∈ e β€’ M.grading.piece β„€ p ↔ x ∈ M.grading.piece β„€ p ∧ e β€’ x = x

    For an idempotent e of degree zero, e β€’ Mβ‚š consists of the elements of Mβ‚š fixed by e.

    source
    theorem TauCeti.GradedModuleCat.exact_smulPieceMap {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] {π’œ : β„€ β†’ Submodule k A} {e : A} {M N P : GradedModuleCat π’œ} (he : IsIdempotentElem e) (heβ‚€ : e ∈ π’œ 0) {f : M ⟢ N} {g : N ⟢ P} (hfg : Function.Exact ⇑f.hom ⇑g.hom) (p : β„€) :
    Function.Exact ⇑(smulPieceMap e f p) ⇑(smulPieceMap e g p)

    Restriction to e β€’ Mβ‚š preserves exactness when e is an idempotent of degree zero.

    The graded dimension of e β€’ M #

    source
    theorem TauCeti.GradedModuleCat.hasFiniteLaurentSupport_smul_grading_piece {k : Type uk} [Field k] {A : Type uA} [Ring A] [Algebra k A] {π’œ : β„€ β†’ Submodule k A} (e : A) (M : GradedModuleCat π’œ) [Module.Finite k M.carrier] :
    HasFiniteLaurentSupport k fun (p : β„€) => β†₯(e β€’ M.grading.piece β„€ p)

    A graded module that is finite-dimensional over k has finitely many nonzero subspaces e β€’ Mβ‚š, all finite-dimensional.

    source
    noncomputable def TauCeti.GradedModuleCat.smulGradedDimension {k : Type uk} [Field k] {A : Type uA} [Ring A] [Algebra k A] {π’œ : β„€ β†’ Submodule k A} (e : A) (M : GradedModuleCat π’œ) [Module.Finite k M.carrier] :
    LaurentPolynomial β„€

    The graded dimension of e β€’ M, βˆ‘β‚š dim_k(e β€’ Mβ‚š) qα΅–, for a graded module that is finite-dimensional over k.

    Instances For
      source
      @[simp]
      theorem TauCeti.GradedModuleCat.coeff_smulGradedDimension {k : Type uk} [Field k] {A : Type uA} [Ring A] [Algebra k A] {π’œ : β„€ β†’ Submodule k A} (e : A) (M : GradedModuleCat π’œ) [Module.Finite k M.carrier] (p : β„€) :
      (smulGradedDimension e M).coeff p = ↑(Module.finrank k β†₯(e β€’ M.grading.piece β„€ p))
      source
      theorem TauCeti.GradedModuleCat.smulGradedDimension_eq_C_of_concentrated {k : Type uk} [Field k] {A : Type uA} [Ring A] [Algebra k A] {π’œ : β„€ β†’ Submodule k A} (e : A) (M : GradedModuleCat π’œ) [Module.Finite k M.carrier] (hM : βˆ€ (p : β„€), p β‰  0 β†’ M.grading.piece β„€ p = βŠ₯) :
      smulGradedDimension e M = LaurentPolynomial.C ↑(Module.finrank k β†₯(e β€’ M.grading.piece β„€ 0))

      If a graded module is concentrated in degree zero, the graded dimension of e β€’ M is constant. No idempotence assumption on e is needed.

      source
      theorem TauCeti.GradedModuleCat.finrank_smul_piece_zero_pos_of_concentrated {k : Type uk} [Field k] {A : Type uA} [Ring A] [Algebra k A] {π’œ : β„€ β†’ Submodule k A} (e : A) (M : GradedModuleCat π’œ) [Module.Finite k M.carrier] (hM : βˆ€ (p : β„€), p β‰  0 β†’ M.grading.piece β„€ p = βŠ₯) (h : smulGradedDimension e M β‰  0) :
      0 < Module.finrank k β†₯(e β€’ M.grading.piece β„€ 0)

      A nonzero idempotent graded dimension of a degree-zero module has positive degree-zero dimension. No idempotence assumption on e is needed.

      source
      theorem TauCeti.GradedModuleCat.smulGradedDimension_congr {k : Type uk} [Field k] {A : Type uA} [Ring A] [Algebra k A] {π’œ : β„€ β†’ Submodule k A} (e : A) {M N : GradedModuleCat π’œ} [Module.Finite k M.carrier] [Module.Finite k N.carrier] (i : M β‰… N) :
      smulGradedDimension e M = smulGradedDimension e N

      Isomorphic graded modules have the same graded dimension of e β€’ M.

      source
      @[simp]
      theorem TauCeti.GradedModuleCat.smulGradedDimension_shiftObj {k : Type uk} [Field k] {A : Type uA} [Ring A] [Algebra k A] {π’œ : β„€ β†’ Submodule k A} (e : A) (M : GradedModuleCat π’œ) [Module.Finite k M.carrier] (n : β„€) :
      smulGradedDimension e (M.shiftObj n) = LaurentPolynomial.T n * smulGradedDimension e M

      Shifting the grading multiplies the graded dimension of e β€’ M by a power of q: gdim_e(M{n}) = qⁿ gdim_e(M).

      source
      theorem TauCeti.GradedModuleCat.smulGradedDimension_one_ne_zero {k : Type uk} [Field k] {A : Type uA} [Ring A] [Algebra k A] {π’œ : β„€ β†’ Submodule k A} (M : GradedModuleCat π’œ) [Module.Finite k M.carrier] [Nontrivial M.carrier] :
      smulGradedDimension 1 M β‰  0

      A nonzero finite-dimensional graded module has nonzero graded dimension, the case e = 1: some homogeneous piece of M is nonzero.

      source
      @[simp]
      theorem TauCeti.GradedModuleCat.laurentEval_one_smulGradedDimension {k : Type uk} [Field k] {A : Type uA} [Ring A] [Algebra k A] {π’œ : β„€ β†’ Submodule k A} {e : A} (M : GradedModuleCat π’œ) (heβ‚€ : e ∈ π’œ 0) [Module.Finite k M.carrier] :
      (laurentEval 1) (smulGradedDimension e M) = ↑(Module.finrank k β†₯(e β€’ ⊀))

      At q = 1 the graded dimension of e β€’ M is the dimension of e β€’ M, for e of degree zero: the subspaces e β€’ Mβ‚š form an internal direct sum decomposition of e β€’ M. No idempotence is needed.

      source
      theorem TauCeti.GradedModuleCat.eq_zero_of_iso_shiftObj {k : Type uk} [Field k] {A : Type uA} [Ring A] [Algebra k A] {π’œ : β„€ β†’ Submodule k A} (M : GradedModuleCat π’œ) [Module.Finite k M.carrier] [Nontrivial M.carrier] {n : β„€} (i : M β‰… M.shiftObj n) :
      n = 0

      A nonzero finite-dimensional graded module is isomorphic to no nontrivial shift of itself: shifting by n multiplies its nonzero graded dimension by qⁿ.

      source
      theorem TauCeti.GradedModuleCat.smulGradedDimension_shortExact {k : Type uk} [Field k] {A : Type uA} [Ring A] [Algebra k A] {π’œ : β„€ β†’ Submodule k A} {e : A} (he : IsIdempotentElem e) (heβ‚€ : e ∈ π’œ 0) {S : CategoryTheory.ShortComplex (GradedModuleCat π’œ)} (hS : S.ShortExact) [Module.Finite k S.X₁.carrier] [Module.Finite k S.Xβ‚‚.carrier] [Module.Finite k S.X₃.carrier] :
      smulGradedDimension e S.Xβ‚‚ = smulGradedDimension e S.X₁ + smulGradedDimension e S.X₃

      The graded dimension of e β€’ M is additive on short exact sequences of graded modules when e is an idempotent of degree zero.