Multiplicative bases

MultiplicativeBasisDeformations.Foundations.EvaluationDim

Proposition 2.10(3): dimensions of evaluated modules #

graded-category.tex (prop:projective-evaluation(3)): "If X₀ is the evaluation of the object labelled by an indecomposable A-module X, then dim_k X₀e_x = dim_k Xe_x […] dim X₀e_x = dim C(P_x, X) = dim Xe_x."

The evaluation at the projective label P_x is C(P_x, X), of dimension dim Hom_A(P_x, X) (finrank_meshHom, eq. graded-hom-dimensions); for P_x ≅ e_xA, Hom_A(e_xA, X) ≅ Xe_x by evaluation at e_x (homIdealEquiv).

source
def MultiplicativeBasisDeformations.fixSub {k A : Type u} [Field k] [Ring A] [Algebra k A] {e : A} (M : RightModuleCat A) :
Submodule k ↑M

The subspace Me = {m | m e = m}.

Instances For
    source
    theorem MultiplicativeBasisDeformations.gen_smul {A : Type u} [Ring A] {e : A} (he : IsIdempotentElem e) (x : ↥(MBDVendor.Magnitude.RightModule.rightIdeal e)) :
    MulOpposite.op ↑x • MBDVendor.Magnitude.RightModule.rightIdealGenerator e = x
    source
    def MultiplicativeBasisDeformations.homIdealEquiv {k A : Type u} [Field k] [Ring A] [Algebra k A] {e : A} (he : IsIdempotentElem e) (M : RightModuleCat A) :
    (idealMod e ⟶ M) ≃ₗ[k] ↥(fixSub M)

    Hom_A(eA, M) ≅ Me, by evaluation at e.

    Instances For
      source
      noncomputable def MultiplicativeBasisDeformations.IndSkeleton.inclHomEquiv {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : IndSkeleton k A) (X Y : S.Ind) :
      (X ⟶ Y) ≃ₗ[k] S.incl.obj X ⟶ S.incl.obj Y

      Hom in ind(mod A) is Hom of right modules.

      Instances For
        source
        theorem MultiplicativeBasisDeformations.IndSkeleton.finrank_evaluation {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : IndSkeleton k A) (b : S.ArrowBases) (p y : S.ARVertex) {e : A} (he : IsIdempotentElem e) (i : S.obj p ≅ idealMod e) :
        Module.finrank k (S.meshObj b p ⟶ S.meshObj b y) = Module.finrank k ↥(fixSub (S.obj y))

        Proposition 2.10(3) (prop:projective-evaluation(3)): for a projective label P_x ≅ eA, the evaluation X₀e_x = C(P_x, X) of the object labelled by X has the dimension of Xe.