Multiplicative bases

MBDVendor.Magnitude.CategoryTheory.ModuleIrreducibleSpaceComparison

Intrinsic irreducible spaces and the existing module multiplicity interface #

source
@[instance_reducible]
def MBDVendor.QSE.IndecomposableSkeleton.comparisonModule {k R : Type u} [Field k] [Ring R] [Algebra k R] [IsNoetherianRing R] {ι : Type v} (S : IndecomposableSkeleton R ι) (i : ι) :
Module k ↑(S.obj i)
Instances For
    source
    theorem MBDVendor.QSE.IndecomposableSkeleton.comparisonTower {k R : Type u} [Field k] [Ring R] [Algebra k R] [IsNoetherianRing R] {ι : Type v} (S : IndecomposableSkeleton R ι) (i : ι) :
    IsScalarTower k R ↑(S.obj i)
    source
    def MBDVendor.QSE.IndecomposableSkeleton.intrinsicRadicalEquiv {k R : Type u} [Field k] [Ring R] [Algebra k R] [IsNoetherianRing R] {ι : Type v} (S : IndecomposableSkeleton R ι) (x y : ι) :
    ↥(Magnitude.CategoricalIrreducible.radical k (S.obj x) (S.obj y)) ≃ₗ[k] ↥(S.radicalHom x y)

    The categorical radical numerator is the existing space of nonsplit linear maps between the chosen indecomposables.

    Instances For
      source
      theorem MBDVendor.QSE.IndecomposableSkeleton.intrinsicDenominator_map {k R : Type u} [Field k] [Ring R] [Algebra k R] [IsNoetherianRing R] {ι : Type v} (S : IndecomposableSkeleton R ι) (x y : ι) :
      Submodule.map (↑(S.intrinsicRadicalEquiv x y)) (Magnitude.CategoricalIrreducible.denominator k (S.obj x) (S.obj y)) = S.radicalSquareInRadicalSubmodule x y

      The numerator comparison identifies the two radical-square denominators.

      source
      def MBDVendor.QSE.IndecomposableSkeleton.intrinsicIrreducibleEquiv {k R : Type u} [Field k] [Ring R] [Algebra k R] [IsNoetherianRing R] {ι : Type v} (S : IndecomposableSkeleton R ι) (x y : ι) :
      Magnitude.CategoricalIrreducible.Space k (S.obj x) (S.obj y) ≃ₗ[k] S.irreducibleHomSpace x y

      The intrinsic categorical quotient is the established module irreducible space used by the almost-split occurrence-basis theorems.

      Instances For