Occurrence bases over an algebraically closed field

For an indecomposable finite-dimensional module over an algebraically closed field, every endomorphism is scalar modulo the categorical radical. This is the precise form of Schur's lemma needed to identify repeated summands in an almost-split middle term with the dimension of the corresponding irreducible morphism space; the endomorphism itself need not be scalar.

@[instance_reducible]

def QuotientSubmoduleEquidistribution.IndecomposableSkeleton.restrictedModule {K R : Type u} [Field K] [Ring R] [Algebra K R] [IsNoetherianRing R] {Iota : Type v} (sigma : IndecomposableSkeleton R Iota) (i : Iota) : Module K ↑(sigma.obj i)

theorem QuotientSubmoduleEquidistribution.IndecomposableSkeleton.restrictedScalarTower {K R : Type u} [Field K] [Ring R] [Algebra K R] [IsNoetherianRing R] {Iota : Type v} (sigma : IndecomposableSkeleton R Iota) (i : Iota) : IsScalarTower K R ↑(sigma.obj i)

theorem QuotientSubmoduleEquidistribution.IndecomposableSkeleton.exists_scalar_sub_mem_radicalHom {K R : Type u} [Field K] [IsAlgClosed K] [Ring R] [Algebra K R] [FiniteDimensional K R] [IsNoetherianRing R] {Iota : Type v} (sigma : IndecomposableSkeleton R Iota) (x : Iota) (f : sigma.obj x ⟶ sigma.obj x) : ∃ (a : K), ModuleCat.Hom.hom f.hom - a • LinearMap.id ∈ sigma.radicalHom x x

Over an algebraically closed field, an endomorphism of an indecomposable finite-dimensional module differs from a scalar by a radical endomorphism.

theorem QuotientSubmoduleEquidistribution.IndecomposableSkeleton.exists_scalar_sub_isRadicalMorphism {K R : Type u} [Field K] [IsAlgClosed K] [Ring R] [Algebra K R] [FiniteDimensional K R] [IsNoetherianRing R] {Iota : Type v} (sigma : IndecomposableSkeleton R Iota) (x : Iota) (f : sigma.obj x ⟶ sigma.obj x) : ∃ (a : K), CategoricalRadical.IsRadicalMorphism (f - a • CategoryTheory.CategoryStruct.id (sigma.obj x))

Over an algebraically closed field, an endomorphism of a chosen indecomposable differs from a scalar identity by a categorical-radical morphism.

theorem QuotientSubmoduleEquidistribution.IndecomposableSkeleton.rightAROccurrenceToIrr_surjective_of_scalar_mod_radical {K R : Type u} [Field K] [Ring R] [Algebra K R] [IsNoetherianRing R] {Iota : Type v} (sigma : IndecomposableSkeleton R Iota) {z : Iota} (A : sigma.MinimalRightAlmostSplitDecomposition z) (x : Iota) (hscalar : ∀ (f : sigma.obj x ⟶ sigma.obj x), ∃ (a : K), ModuleCat.Hom.hom f.hom - a • LinearMap.id ∈ sigma.radicalHom x x) : Function.Surjective ⇑(sigma.rightAROccurrenceToIrr A x)

The right almost-split occurrence coordinates span Irr when source endomorphisms are scalar modulo the radical.

noncomputable def QuotientSubmoduleEquidistribution.IndecomposableSkeleton.rightAROccurrenceLinearEquivOfIsAlgClosed {K R : Type u} [Field K] [IsAlgClosed K] [Ring R] [Algebra K R] [FiniteDimensional K R] [IsNoetherianRing R] {Iota : Type v} (sigma : IndecomposableSkeleton R Iota) {z : Iota} (A : sigma.MinimalRightAlmostSplitDecomposition z) (x : Iota) : (sigma.RightAROccurrence A x → K) ≃ₗ[K] sigma.irreducibleHomSpace x z

Over an algebraically closed field, right almost-split occurrences form a basis of the corresponding irreducible-morphism space.

theorem QuotientSubmoduleEquidistribution.IndecomposableSkeleton.finrank_irreducibleHomSpace_eq_card_rightAROccurrence_of_isAlgClosed {K R : Type u} [Field K] [IsAlgClosed K] [Ring R] [Algebra K R] [FiniteDimensional K R] [IsNoetherianRing R] {Iota : Type v} (sigma : IndecomposableSkeleton R Iota) {z : Iota} (A : sigma.MinimalRightAlmostSplitDecomposition z) (x : Iota) : Module.finrank K (sigma.irreducibleHomSpace x z) = Nat.card (sigma.RightAROccurrence A x)

The dimension of Irr(x,z) is the number of occurrences of x in a minimal right almost-split middle term over an algebraically closed field.

theorem QuotientSubmoduleEquidistribution.IndecomposableSkeleton.leftAROccurrenceToIrr_surjective_of_scalar_mod_radical {K R : Type u} [Field K] [Ring R] [Algebra K R] [IsNoetherianRing R] {Iota : Type v} (sigma : IndecomposableSkeleton R Iota) {x : Iota} (A : sigma.MinimalLeftAlmostSplitDecomposition x) (y : Iota) (hscalar : ∀ (f : sigma.obj y ⟶ sigma.obj y), ∃ (a : K), ModuleCat.Hom.hom f.hom - a • LinearMap.id ∈ sigma.radicalHom y y) : Function.Surjective ⇑(sigma.leftAROccurrenceToIrr A y)

The left almost-split occurrence coordinates span Irr when target endomorphisms are scalar modulo the radical.

noncomputable def QuotientSubmoduleEquidistribution.IndecomposableSkeleton.leftAROccurrenceLinearEquivOfIsAlgClosed {K R : Type u} [Field K] [IsAlgClosed K] [Ring R] [Algebra K R] [FiniteDimensional K R] [IsNoetherianRing R] {Iota : Type v} (sigma : IndecomposableSkeleton R Iota) {x : Iota} (A : sigma.MinimalLeftAlmostSplitDecomposition x) (y : Iota) : (sigma.LeftAROccurrence A y → K) ≃ₗ[K] sigma.irreducibleHomSpace x y

Over an algebraically closed field, left almost-split occurrences form a basis of the corresponding irreducible-morphism space.

theorem QuotientSubmoduleEquidistribution.IndecomposableSkeleton.finrank_irreducibleHomSpace_eq_card_leftAROccurrence_of_isAlgClosed {K R : Type u} [Field K] [IsAlgClosed K] [Ring R] [Algebra K R] [FiniteDimensional K R] [IsNoetherianRing R] {Iota : Type v} (sigma : IndecomposableSkeleton R Iota) {x : Iota} (A : sigma.MinimalLeftAlmostSplitDecomposition x) (y : Iota) : Module.finrank K (sigma.irreducibleHomSpace x y) = Nat.card (sigma.LeftAROccurrence A y)

The dimension of Irr(x,y) is the number of occurrences of y in a minimal left almost-split middle term over an algebraically closed field.