Intrinsic irreducible spaces and the existing module multiplicity interface #
@[instance_reducible]
def
QuotientSubmoduleEquidistribution.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
theorem
QuotientSubmoduleEquidistribution.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)
def
QuotientSubmoduleEquidistribution.IndecomposableSkeleton.intrinsicRadicalEquiv
{k R : Type u}
[Field k]
[Ring R]
[Algebra k R]
[IsNoetherianRing R]
{ι : Type v}
(S : IndecomposableSkeleton R ι)
(x y : ι)
:
↥(MagnitudeConjecture.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
theorem
QuotientSubmoduleEquidistribution.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))
(MagnitudeConjecture.CategoricalIrreducible.denominator k (S.obj x) (S.obj y)) = S.radicalSquareInRadicalSubmodule x y
The numerator comparison identifies the two radical-square denominators.
def
QuotientSubmoduleEquidistribution.IndecomposableSkeleton.intrinsicIrreducibleEquiv
{k R : Type u}
[Field k]
[Ring R]
[Algebra k R]
[IsNoetherianRing R]
{ι : Type v}
(S : IndecomposableSkeleton R ι)
(x y : ι)
:
MagnitudeConjecture.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.