Magnitude conjecture

QuotientSubmoduleEquidistribution.RepresentationTheory.LinearIrreducibleHomSpace

The linear irreducible-morphism space #

This file upgrades the field-free quotient rad(X,Y) / rad²(X,Y) to a vector-space quotient over a central ground field. It supplies the exact object whose finrank occurs in the multiplicity-one theorem for a representation-finite algebra.

No finite-dimensionality, directedness, algebra presentation, or module classification is used in the construction.

source
def QuotientSubmoduleEquidistribution.IndecomposableSkeleton.radicalSquareHomSubmodule {K R : Type u} [Field K] [Ring R] [Algebra K R] [IsNoetherianRing R] {Iota : Type uIota} (sigma : IndecomposableSkeleton R Iota) [(i : Iota) → Module K ↑(sigma.obj i)] [∀ (i : Iota), IsScalarTower K R ↑(sigma.obj i)] (x y : Iota) :
Submodule K (↑(sigma.obj x) →ₗ[R] ↑(sigma.obj y))

The square of the categorical radical as a K-subspace of the R-linear Hom-space.

Instances For
    source
    @[simp]
    theorem QuotientSubmoduleEquidistribution.IndecomposableSkeleton.mem_radicalSquareHomSubmodule_iff {K R : Type u} [Field K] [Ring R] [Algebra K R] [IsNoetherianRing R] {Iota : Type uIota} (sigma : IndecomposableSkeleton R Iota) [(i : Iota) → Module K ↑(sigma.obj i)] [∀ (i : Iota), IsScalarTower K R ↑(sigma.obj i)] {x y : Iota} (f : ↑(sigma.obj x) →ₗ[R] ↑(sigma.obj y)) :
    f ∈ sigma.radicalSquareHomSubmodule x y ↔ sigma.HasRadicalSquareFactorization (CategoryTheory.ConcreteCategory.ofHom f)
    source
    def QuotientSubmoduleEquidistribution.IndecomposableSkeleton.radicalSquareInRadicalSubmodule {K R : Type u} [Field K] [Ring R] [Algebra K R] [IsNoetherianRing R] {Iota : Type uIota} (sigma : IndecomposableSkeleton R Iota) [(i : Iota) → Module K ↑(sigma.obj i)] [∀ (i : Iota), IsScalarTower K R ↑(sigma.obj i)] (x y : Iota) :
    Submodule K ↥(sigma.radicalHom x y)

    The linear denominator rad²(X,Y) regarded as a subspace of rad(X,Y).

    Instances For
      source
      @[reducible, inline]
      abbrev QuotientSubmoduleEquidistribution.IndecomposableSkeleton.irreducibleHomSpace {K R : Type u} [Field K] [Ring R] [Algebra K R] [IsNoetherianRing R] {Iota : Type uIota} (sigma : IndecomposableSkeleton R Iota) [(i : Iota) → Module K ↑(sigma.obj i)] [∀ (i : Iota), IsScalarTower K R ↑(sigma.obj i)] (x y : Iota) :
      Type u

      The manuscript's K-linear irreducible-morphism space Irr(X,Y) = rad(X,Y) / rad²(X,Y).

      Instances For
        source
        theorem QuotientSubmoduleEquidistribution.IndecomposableSkeleton.nontrivial_irreducibleHomSpace_iff_hasIrreducibleMorphism {K R : Type u} [Field K] [Ring R] [Algebra K R] [IsNoetherianRing R] {Iota : Type uIota} (sigma : IndecomposableSkeleton R Iota) [(i : Iota) → Module K ↑(sigma.obj i)] [∀ (i : Iota), IsScalarTower K R ↑(sigma.obj i)] (x y : Iota) :
        Nontrivial (sigma.irreducibleHomSpace x y) ↔ HasIrreducibleMorphism (sigma.obj x) (sigma.obj y)

        The linear irreducible-morphism space is nontrivial exactly when there is an irreducible morphism between the two indecomposables.

        source
        theorem QuotientSubmoduleEquidistribution.IndecomposableSkeleton.hasIrreducibleMorphism_iff_nontrivial_irreducibleHomSpace {K R : Type u} [Field K] [Ring R] [Algebra K R] [IsNoetherianRing R] {Iota : Type uIota} (sigma : IndecomposableSkeleton R Iota) [(i : Iota) → Module K ↑(sigma.obj i)] [∀ (i : Iota), IsScalarTower K R ↑(sigma.obj i)] (x y : Iota) :
        HasIrreducibleMorphism (sigma.obj x) (sigma.obj y) ↔ Nontrivial (sigma.irreducibleHomSpace x y)

        Manuscript-style orientation of the nonzero-space criterion.