Multiplicative bases

MultiplicativeBasisDeformations.Foundations.ARInjData

The labels P_x, S_x, I_x of k(Γ_A) #

The data used in the paragraph "Injectives in the image" of the proof of Proposition 2.10 (graded-category.tex): for a projective label P_x, the original simple S_x = P_x / rad P_x and the original injective I_x = D(Ae_x), with

all through eq:graded-hom-dimensions (finrank_meshHom).

source
theorem MultiplicativeBasisDeformations.IndSkeleton.finrank_meshHom_fg {k A : Type w} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : IndSkeleton k A) (b : S.ArrowBases) (x y : S.ARVertex) :
Module.finrank k (S.meshObj b x ⟶ S.meshObj b y) = Module.finrank k (S.fg (S.index x) ⟶ S.fg (S.index y))

eq:graded-hom-dimensions in mod A.

source
theorem MultiplicativeBasisDeformations.IndSkeleton.projective_of_proj {k A : Type w} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : IndSkeleton k A) (b : S.ArrowBases) (p : (S.arMeshData b).PV) :
CategoryTheory.Projective (S.fg (S.index ↑p))
source
noncomputable def MultiplicativeBasisDeformations.IndSkeleton.topLabel {k A : Type w} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : IndSkeleton k A) (b : S.ArrowBases) (p : (S.arMeshData b).PV) :
S.ARVertex

The label of the simple top of a projective label.

Instances For
    source
    noncomputable def MultiplicativeBasisDeformations.IndSkeleton.topLabelIso {k A : Type w} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : IndSkeleton k A) (b : S.ArrowBases) (p : (S.arMeshData b).PV) :
    S.top (S.index ↑p) ≅ S.fg (S.index (S.topLabel b p))
    Instances For
      source
      noncomputable def MultiplicativeBasisDeformations.IndSkeleton.injLabel {k A : Type w} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : IndSkeleton k A) (b : S.ArrowBases) (p : (S.arMeshData b).PV) :
      S.ARVertex

      The injective label I_x of a projective label.

      Instances For
        source
        theorem MultiplicativeBasisDeformations.IndSkeleton.finrank_hom_injLabel {k A : Type w} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : IndSkeleton k A) (b : S.ArrowBases) (p : (S.arMeshData b).PV) (M : ModCat A) :
        Module.finrank k (M ⟶ S.fg (S.index (S.injLabel b p))) = Module.finrank k (S.fg (S.index ↑p) ⟶ M)
        source
        theorem MultiplicativeBasisDeformations.IndSkeleton.pv_eq_iff {k A : Type w} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : IndSkeleton k A) (b : S.ArrowBases) (p q : (S.arMeshData b).PV) :
        q = p ↔ S.index ↑q = S.index ↑p
        source
        theorem MultiplicativeBasisDeformations.IndSkeleton.finrank_fg_top {k A : Type w} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : IndSkeleton k A) (b : S.ArrowBases) (p q : (S.arMeshData b).PV) :
        Module.finrank k (S.fg (S.index ↑q) ⟶ S.fg (S.index (S.topLabel b p))) = if q = p then 1 else 0
        source
        noncomputable def MultiplicativeBasisDeformations.IndSkeleton.arInjData {k A : Type w} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : IndSkeleton k A) (b : S.ArrowBases) :
        (S.arMeshData b).InjData

        The labels of Proposition 2.10 for k(Γ_A).

        Instances For