Occurrence bases for minimal right almost-split maps

For a chosen indecomposable decomposition of the middle term of a minimal right almost-split map, this file constructs the coordinate map from copies of one indecomposable to the linear irreducible-morphism space Irr = rad / rad². Right minimality proves linear independence, while scalar endomorphisms of the source prove spanning. Thus the multiplicity of an indecomposable middle summand is exactly the dimension of the corresponding irreducible-morphism space.

The construction is abstract: it uses no quiver presentation or module classification, and it applies to projective-boundary right almost-split maps as well as to almost-split sequences.

@[reducible, inline]

abbrev QuotientSubmoduleEquidistribution.IndecomposableSkeleton.RightAROccurrence {R : Type u} [Ring R] [IsNoetherianRing R] {Iota : Type v} (sigma : IndecomposableSkeleton R Iota) {z : Iota} (A : sigma.MinimalRightAlmostSplitDecomposition z) (x : Iota) : Type

The occurrences of one fixed indecomposable in a chosen right almost-split middle decomposition.

noncomputable def QuotientSubmoduleEquidistribution.IndecomposableSkeleton.rightAROccurrenceArrow {R : Type u} [Ring R] [IsNoetherianRing R] {Iota : Type v} (sigma : IndecomposableSkeleton R Iota) {z : Iota} (A : sigma.MinimalRightAlmostSplitDecomposition z) (x : Iota) (t : sigma.RightAROccurrence A x) : sigma.obj x ⟶ sigma.obj z

The coordinate map from an occurring copy of x to the right almost-split endpoint.

noncomputable def QuotientSubmoduleEquidistribution.IndecomposableSkeleton.rightAROccurrenceMiddleArrow {R : Type u} [Ring R] [IsNoetherianRing R] {Iota : Type v} (sigma : IndecomposableSkeleton R Iota) {z : Iota} (A : sigma.MinimalRightAlmostSplitDecomposition z) (x : Iota) (t : sigma.RightAROccurrence A x) : sigma.obj x ⟶ A.middle

The same coordinate before composing with the right almost-split map.

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

The middle-term morphism represented by a coefficient vector.

noncomputable def QuotientSubmoduleEquidistribution.IndecomposableSkeleton.rightAROccurrenceMiddleProjection {R : Type u} [Ring R] [IsNoetherianRing R] {Iota : Type v} (sigma : IndecomposableSkeleton R Iota) {z : Iota} (A : sigma.MinimalRightAlmostSplitDecomposition z) (x : Iota) (t : sigma.RightAROccurrence A x) : A.middle ⟶ sigma.obj x

Projection back from the middle term to one specified occurrence.

theorem QuotientSubmoduleEquidistribution.IndecomposableSkeleton.rightAROccurrenceMiddleCombination_projection {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) (c : sigma.RightAROccurrence A x → K) (t : sigma.RightAROccurrence A x) : CategoryTheory.CategoryStruct.comp (sigma.rightAROccurrenceMiddleCombination A x c) (sigma.rightAROccurrenceMiddleProjection A x t) = c t • CategoryTheory.CategoryStruct.id (sigma.obj x)

theorem QuotientSubmoduleEquidistribution.IndecomposableSkeleton.rightAROccurrenceMiddleCombination_isSplitMono_of_ne_zero {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) (c : sigma.RightAROccurrence A x → K) (hc : c ≠ 0) : CategoryTheory.IsSplitMono (sigma.rightAROccurrenceMiddleCombination A x c)

noncomputable def QuotientSubmoduleEquidistribution.IndecomposableSkeleton.rightAROccurrenceArrowLinear {R : Type u} [Ring R] [IsNoetherianRing R] {Iota : Type v} (sigma : IndecomposableSkeleton R Iota) {z : Iota} (A : sigma.MinimalRightAlmostSplitDecomposition z) (x : Iota) (t : sigma.RightAROccurrence A x) : ↑(sigma.obj x) →ₗ[R] ↑(sigma.obj z)

The same coordinate arrow as an R-linear map.

noncomputable def QuotientSubmoduleEquidistribution.IndecomposableSkeleton.rightAROccurrenceCombination {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)] {z : Iota} (A : sigma.MinimalRightAlmostSplitDecomposition z) (x : Iota) (c : sigma.RightAROccurrence A x → K) : ↑(sigma.obj x) →ₗ[R] ↑(sigma.obj z)

A finite linear combination of occurrence-coordinate arrows.

noncomputable def QuotientSubmoduleEquidistribution.IndecomposableSkeleton.rightAROccurrenceCombinationLinear {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)] {z : Iota} (A : sigma.MinimalRightAlmostSplitDecomposition z) (x : Iota) : (sigma.RightAROccurrence A x → K) →ₗ[K] ↑(sigma.obj x) →ₗ[R] ↑(sigma.obj z)

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

theorem QuotientSubmoduleEquidistribution.IndecomposableSkeleton.rightAROccurrenceMiddleCombination_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)] {z : Iota} (A : sigma.MinimalRightAlmostSplitDecomposition z) (x : Iota) (c : sigma.RightAROccurrence A x → K) : CategoryTheory.CategoryStruct.comp (sigma.rightAROccurrenceMiddleCombination A x c) A.map = CategoryTheory.ConcreteCategory.ofHom (sigma.rightAROccurrenceCombination A x c)

theorem QuotientSubmoduleEquidistribution.IndecomposableSkeleton.rightAROccurrenceArrow_not_isSplitEpi {R : Type u} [Ring R] [IsNoetherianRing R] {Iota : Type v} (sigma : IndecomposableSkeleton R Iota) {z : Iota} (A : sigma.MinimalRightAlmostSplitDecomposition z) (x : Iota) (t : sigma.RightAROccurrence A x) : ¬CategoryTheory.IsSplitEpi (sigma.rightAROccurrenceArrow A x t)

Every displayed occurrence-coordinate is radical: if that single coordinate split epimorphically, then the whole right almost-split map would split epimorphically.

theorem QuotientSubmoduleEquidistribution.IndecomposableSkeleton.rightAROccurrenceArrowLinear_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)] {z : Iota} (A : sigma.MinimalRightAlmostSplitDecomposition z) (x : Iota) (t : sigma.RightAROccurrence A x) : sigma.rightAROccurrenceArrowLinear A x t ∈ sigma.radicalHom x z

theorem QuotientSubmoduleEquidistribution.IndecomposableSkeleton.rightAROccurrenceCombination_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)] {z : Iota} (A : sigma.MinimalRightAlmostSplitDecomposition z) (x : Iota) (c : sigma.RightAROccurrence A x → K) : sigma.rightAROccurrenceCombination A x c ∈ sigma.radicalHom x z

noncomputable def QuotientSubmoduleEquidistribution.IndecomposableSkeleton.rightAROccurrenceToRadical {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)] {z : Iota} (A : sigma.MinimalRightAlmostSplitDecomposition z) (x : Iota) : (sigma.RightAROccurrence A x → K) →ₗ[K] ↥(sigma.radicalHom x z)

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

noncomputable def QuotientSubmoduleEquidistribution.IndecomposableSkeleton.rightAROccurrenceToIrr {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)] {z : Iota} (A : sigma.MinimalRightAlmostSplitDecomposition z) (x : Iota) : (sigma.RightAROccurrence A x → K) →ₗ[K] sigma.irreducibleHomSpace x z

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

theorem QuotientSubmoduleEquidistribution.IndecomposableSkeleton.rightAROccurrenceToIrr_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)] {z : Iota} (A : sigma.MinimalRightAlmostSplitDecomposition z) (x : Iota) (c : sigma.RightAROccurrence A x → K) : (sigma.rightAROccurrenceToIrr A x) c = 0 ↔ CategoryTheory.ConcreteCategory.ofHom (sigma.rightAROccurrenceCombination A x c) ∈ sigma.radicalSquareHomAddSubgroup x z

theorem QuotientSubmoduleEquidistribution.IndecomposableSkeleton.rightAROccurrenceToIrr_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)] {z : Iota} (A : sigma.MinimalRightAlmostSplitDecomposition z) (x : Iota) (c : sigma.RightAROccurrence A x → K) (hzero : (sigma.rightAROccurrenceToIrr A x) c = 0) : c = 0

Occurrence classes are linearly independent for every minimal right almost-split decomposition. Right minimality alone eliminates a hypothetical radical-square relation, so this argument also covers projective boundary maps and needs no AR kernel or translation data.

theorem QuotientSubmoduleEquidistribution.IndecomposableSkeleton.rightAROccurrenceToIrr_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)] {z : Iota} (A : sigma.MinimalRightAlmostSplitDecomposition z) (x : Iota) : Function.Injective ⇑(sigma.rightAROccurrenceToIrr A x)

theorem QuotientSubmoduleEquidistribution.IndecomposableSkeleton.rightAROccurrenceToIrr_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)] {z : Iota} (A : sigma.MinimalRightAlmostSplitDecomposition z) (x : Iota) (hscalar : ∀ (f : sigma.obj x ⟶ sigma.obj x), ∃ (a : K), a • CategoryTheory.CategoryStruct.id (sigma.obj x) = f) : Function.Surjective ⇑(sigma.rightAROccurrenceToIrr A x)

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

noncomputable def QuotientSubmoduleEquidistribution.IndecomposableSkeleton.rightAROccurrenceLinearEquivOfScalarEndomorphisms {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)] {z : Iota} (A : sigma.MinimalRightAlmostSplitDecomposition z) (x : Iota) (hscalar : ∀ (f : sigma.obj x ⟶ sigma.obj x), ∃ (a : K), a • CategoryTheory.CategoryStruct.id (sigma.obj x) = f) : (sigma.RightAROccurrence A x → K) ≃ₗ[K] sigma.irreducibleHomSpace x z

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

theorem QuotientSubmoduleEquidistribution.IndecomposableSkeleton.finrank_irreducibleHomSpace_eq_card_rightAROccurrence {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)] {z : Iota} (A : sigma.MinimalRightAlmostSplitDecomposition z) (x : Iota) (hscalar : ∀ (f : sigma.obj x ⟶ sigma.obj x), ∃ (a : K), a • CategoryTheory.CategoryStruct.id (sigma.obj x) = f) : Module.finrank K (sigma.irreducibleHomSpace x z) = Nat.card (sigma.RightAROccurrence A x)