Occurrence bases for minimal left almost-split maps

This is the dual occurrence-coordinate construction for a chosen indecomposable decomposition of the middle term of a minimal left almost-split map. Left minimality proves linear independence in Irr = rad / rad², while scalar endomorphisms of the target prove spanning. Consequently, the multiplicity of a target indecomposable in the middle term is exactly the dimension of the corresponding irreducible-morphism space.

The construction is abstract and uses no quiver presentation or module classification.

@[reducible, inline]

abbrev QuotientSubmoduleEquidistribution.IndecomposableSkeleton.LeftAROccurrence {R : Type u} [Ring R] [IsNoetherianRing R] {Iota : Type v} (sigma : IndecomposableSkeleton R Iota) {x : Iota} (A : sigma.MinimalLeftAlmostSplitDecomposition x) (y : Iota) : Type

The occurrences of one fixed target indecomposable in a chosen minimal left almost-split middle decomposition.

noncomputable def QuotientSubmoduleEquidistribution.IndecomposableSkeleton.leftAROccurrenceMiddleArrow {R : Type u} [Ring R] [IsNoetherianRing R] {Iota : Type v} (sigma : IndecomposableSkeleton R Iota) {x : Iota} (A : sigma.MinimalLeftAlmostSplitDecomposition x) (y : Iota) (t : sigma.LeftAROccurrence A y) : A.middle ⟶ sigma.obj y

Projection from the middle term to one occurring copy of y.

noncomputable def QuotientSubmoduleEquidistribution.IndecomposableSkeleton.leftAROccurrenceArrow {R : Type u} [Ring R] [IsNoetherianRing R] {Iota : Type v} (sigma : IndecomposableSkeleton R Iota) {x : Iota} (A : sigma.MinimalLeftAlmostSplitDecomposition x) (y : Iota) (t : sigma.LeftAROccurrence A y) : sigma.obj x ⟶ sigma.obj y

The coordinate arrow from the left almost-split source to an occurring copy of y.

noncomputable def QuotientSubmoduleEquidistribution.IndecomposableSkeleton.leftAROccurrenceMiddleInclusion {R : Type u} [Ring R] [IsNoetherianRing R] {Iota : Type v} (sigma : IndecomposableSkeleton R Iota) {x : Iota} (A : sigma.MinimalLeftAlmostSplitDecomposition x) (y : Iota) (t : sigma.LeftAROccurrence A y) : sigma.obj y ⟶ A.middle

Inclusion of one occurring copy of y back into the middle term.

noncomputable def QuotientSubmoduleEquidistribution.IndecomposableSkeleton.leftAROccurrenceMiddleCombination {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) (c : sigma.LeftAROccurrence A y → K) : A.middle ⟶ sigma.obj y

The middle-term projection represented by a coefficient vector.

theorem QuotientSubmoduleEquidistribution.IndecomposableSkeleton.leftAROccurrenceMiddleInclusion_combination {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) (c : sigma.LeftAROccurrence A y → K) (t : sigma.LeftAROccurrence A y) : CategoryTheory.CategoryStruct.comp (sigma.leftAROccurrenceMiddleInclusion A y t) (sigma.leftAROccurrenceMiddleCombination A y c) = c t • CategoryTheory.CategoryStruct.id (sigma.obj y)

theorem QuotientSubmoduleEquidistribution.IndecomposableSkeleton.leftAROccurrenceMiddleCombination_isSplitEpi_of_ne_zero {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) (c : sigma.LeftAROccurrence A y → K) (hc : c ≠ 0) : CategoryTheory.IsSplitEpi (sigma.leftAROccurrenceMiddleCombination A y c)

noncomputable def QuotientSubmoduleEquidistribution.IndecomposableSkeleton.leftAROccurrenceArrowLinear {R : Type u} [Ring R] [IsNoetherianRing R] {Iota : Type v} (sigma : IndecomposableSkeleton R Iota) {x : Iota} (A : sigma.MinimalLeftAlmostSplitDecomposition x) (y : Iota) (t : sigma.LeftAROccurrence A y) : ↑(sigma.obj x) →ₗ[R] ↑(sigma.obj y)

The occurrence-coordinate arrow as an R-linear map.

noncomputable def QuotientSubmoduleEquidistribution.IndecomposableSkeleton.leftAROccurrenceCombination {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)] [∀ (i : Iota), IsScalarTower K R ↑(sigma.obj i)] {x : Iota} (A : sigma.MinimalLeftAlmostSplitDecomposition x) (y : Iota) (c : sigma.LeftAROccurrence A y → K) : ↑(sigma.obj x) →ₗ[R] ↑(sigma.obj y)

A finite linear combination of occurrence-coordinate arrows.

noncomputable def QuotientSubmoduleEquidistribution.IndecomposableSkeleton.leftAROccurrenceCombinationLinear {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)] [∀ (i : Iota), IsScalarTower K R ↑(sigma.obj i)] {x : Iota} (A : sigma.MinimalLeftAlmostSplitDecomposition x) (y : Iota) : (sigma.LeftAROccurrence A y → K) →ₗ[K] ↑(sigma.obj x) →ₗ[R] ↑(sigma.obj y)

Occurrence-coordinate combination is K-linear in its coefficients.

theorem QuotientSubmoduleEquidistribution.IndecomposableSkeleton.leftAROccurrenceCombination_eq_comp {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)] [∀ (i : Iota), IsScalarTower K R ↑(sigma.obj i)] {x : Iota} (A : sigma.MinimalLeftAlmostSplitDecomposition x) (y : Iota) (c : sigma.LeftAROccurrence A y → K) : CategoryTheory.CategoryStruct.comp A.map (sigma.leftAROccurrenceMiddleCombination A y c) = CategoryTheory.ConcreteCategory.ofHom (sigma.leftAROccurrenceCombination A y c)

theorem QuotientSubmoduleEquidistribution.IndecomposableSkeleton.leftAROccurrenceArrow_not_isSplitMono {R : Type u} [Ring R] [IsNoetherianRing R] {Iota : Type v} (sigma : IndecomposableSkeleton R Iota) {x : Iota} (A : sigma.MinimalLeftAlmostSplitDecomposition x) (y : Iota) (t : sigma.LeftAROccurrence A y) : ¬CategoryTheory.IsSplitMono (sigma.leftAROccurrenceArrow A y t)

Every displayed left occurrence-coordinate is radical.

theorem QuotientSubmoduleEquidistribution.IndecomposableSkeleton.leftAROccurrenceArrowLinear_mem_radical {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)] [∀ (i : Iota), IsScalarTower K R ↑(sigma.obj i)] {x : Iota} (A : sigma.MinimalLeftAlmostSplitDecomposition x) (y : Iota) (t : sigma.LeftAROccurrence A y) : sigma.leftAROccurrenceArrowLinear A y t ∈ sigma.radicalHom x y

theorem QuotientSubmoduleEquidistribution.IndecomposableSkeleton.leftAROccurrenceCombination_mem_radical {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)] [∀ (i : Iota), IsScalarTower K R ↑(sigma.obj i)] {x : Iota} (A : sigma.MinimalLeftAlmostSplitDecomposition x) (y : Iota) (c : sigma.LeftAROccurrence A y → K) : sigma.leftAROccurrenceCombination A y c ∈ sigma.radicalHom x y

noncomputable def QuotientSubmoduleEquidistribution.IndecomposableSkeleton.leftAROccurrenceToRadical {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)] [∀ (i : Iota), IsScalarTower K R ↑(sigma.obj i)] {x : Iota} (A : sigma.MinimalLeftAlmostSplitDecomposition x) (y : Iota) : (sigma.LeftAROccurrence A y → K) →ₗ[K] ↥(sigma.radicalHom x y)

The canonical linear map from left-occurrence coefficients to the linear radical Hom-space.

noncomputable def QuotientSubmoduleEquidistribution.IndecomposableSkeleton.leftAROccurrenceToIrr {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)] [∀ (i : Iota), IsScalarTower K R ↑(sigma.obj i)] {x : Iota} (A : sigma.MinimalLeftAlmostSplitDecomposition x) (y : Iota) : (sigma.LeftAROccurrence A y → K) →ₗ[K] sigma.irreducibleHomSpace x y

The basis-candidate map from left-AR occurrences to rad(x,y) / rad²(x,y).

theorem QuotientSubmoduleEquidistribution.IndecomposableSkeleton.leftAROccurrenceToIrr_eq_zero_iff {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)] [∀ (i : Iota), IsScalarTower K R ↑(sigma.obj i)] {x : Iota} (A : sigma.MinimalLeftAlmostSplitDecomposition x) (y : Iota) (c : sigma.LeftAROccurrence A y → K) : (sigma.leftAROccurrenceToIrr A y) c = 0 ↔ CategoryTheory.ConcreteCategory.ofHom (sigma.leftAROccurrenceCombination A y c) ∈ sigma.radicalSquareHomAddSubgroup x y

theorem QuotientSubmoduleEquidistribution.IndecomposableSkeleton.leftAROccurrenceToIrr_eq_zero {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)] [∀ (i : Iota), IsScalarTower K R ↑(sigma.obj i)] {x : Iota} (A : sigma.MinimalLeftAlmostSplitDecomposition x) (y : Iota) (c : sigma.LeftAROccurrence A y → K) (hzero : (sigma.leftAROccurrenceToIrr A y) c = 0) : c = 0

Occurrence classes are linearly independent for every minimal left almost-split decomposition. This is the left-minimal dual of the standard right occurrence argument.

theorem QuotientSubmoduleEquidistribution.IndecomposableSkeleton.leftAROccurrenceToIrr_injective {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)] [∀ (i : Iota), IsScalarTower K R ↑(sigma.obj i)] {x : Iota} (A : sigma.MinimalLeftAlmostSplitDecomposition x) (y : Iota) : Function.Injective ⇑(sigma.leftAROccurrenceToIrr A y)

theorem QuotientSubmoduleEquidistribution.IndecomposableSkeleton.leftAROccurrenceToIrr_surjective_of_scalar_endomorphisms {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)] [∀ (i : Iota), IsScalarTower K R ↑(sigma.obj i)] {x : Iota} (A : sigma.MinimalLeftAlmostSplitDecomposition x) (y : Iota) (hscalar : ∀ (f : sigma.obj y ⟶ sigma.obj y), ∃ (a : K), a • CategoryTheory.CategoryStruct.id (sigma.obj y) = f) : Function.Surjective ⇑(sigma.leftAROccurrenceToIrr A y)

The coordinate classes span Irr as soon as endomorphisms of the target are scalar. This is the left-minimal approximation half of the standard occurrence--Irr basis theorem.

noncomputable def QuotientSubmoduleEquidistribution.IndecomposableSkeleton.leftAROccurrenceLinearEquivOfScalarEndomorphisms {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)] [∀ (i : Iota), IsScalarTower K R ↑(sigma.obj i)] {x : Iota} (A : sigma.MinimalLeftAlmostSplitDecomposition x) (y : Iota) (hscalar : ∀ (f : sigma.obj y ⟶ sigma.obj y), ∃ (a : K), a • CategoryTheory.CategoryStruct.id (sigma.obj y) = f) : (sigma.LeftAROccurrence A y → K) ≃ₗ[K] sigma.irreducibleHomSpace x y

The general left-side occurrence--Irr equivalence, assuming only the scalar-endomorphism conclusion needed for spanning.

theorem QuotientSubmoduleEquidistribution.IndecomposableSkeleton.finrank_irreducibleHomSpace_eq_card_leftAROccurrence {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)] [∀ (i : Iota), IsScalarTower K R ↑(sigma.obj i)] {x : Iota} (A : sigma.MinimalLeftAlmostSplitDecomposition x) (y : Iota) (hscalar : ∀ (f : sigma.obj y ⟶ sigma.obj y), ∃ (a : K), a • CategoryTheory.CategoryStruct.id (sigma.obj y) = f) : Module.finrank K (sigma.irreducibleHomSpace x y) = Nat.card (sigma.LeftAROccurrence A y)