Almost-split morphisms for a finite indecomposable skeleton

For a finite complete skeleton of finite-length indecomposable modules over a finite-dimensional algebra, this file constructs right and left almost-split morphisms by finite radical evaluation. It then combines those morphisms with the finite-length minimalization theorem in AlmostSplitCofinite.

The construction is intrinsic: it uses only the radical Hom-spaces between the chosen indecomposables and their finite biproducts. No presentation or classification of the algebra or its modules enters.

def QuotientSubmoduleEquidistribution.IndecomposableSkeleton.radicalHom {K : Type uK} [Field K] {R : Type uR} [Ring R] [Algebra K R] [IsNoetherianRing R] {ι : Type uι} (σ : IndecomposableSkeleton R ι) [(i : ι) → Module K ↑(σ.obj i)] [∀ (i : ι), IsScalarTower K R ↑(σ.obj i)] (x z : ι) : Submodule K (↑(σ.obj x) →ₗ[R] ↑(σ.obj z))

The K-linear radical Hom-space between two chosen indecomposables, realized as the maps which are not split epimorphisms.

@[simp]

theorem QuotientSubmoduleEquidistribution.IndecomposableSkeleton.mem_radicalHom_iff_not_isSplitEpi {K : Type uK} [Field K] {R : Type uR} [Ring R] [Algebra K R] [IsNoetherianRing R] {ι : Type uι} (σ : IndecomposableSkeleton R ι) [(i : ι) → Module K ↑(σ.obj i)] [∀ (i : ι), IsScalarTower K R ↑(σ.obj i)] {x z : ι} (f : ↑(σ.obj x) →ₗ[R] ↑(σ.obj z)) : f ∈ σ.radicalHom x z ↔ ¬CategoryTheory.IsSplitEpi (have this := CategoryTheory.ConcreteCategory.ofHom f; this)

theorem QuotientSubmoduleEquidistribution.IndecomposableSkeleton.mem_radicalHom_iff_not_isSplitMono {K : Type uK} [Field K] {R : Type uR} [Ring R] [Algebra K R] [IsNoetherianRing R] {ι : Type uι} (σ : IndecomposableSkeleton R ι) [(i : ι) → Module K ↑(σ.obj i)] [∀ (i : ι), IsScalarTower K R ↑(σ.obj i)] {x z : ι} (f : ↑(σ.obj x) →ₗ[R] ↑(σ.obj z)) : f ∈ σ.radicalHom x z ↔ ¬CategoryTheory.IsSplitMono (have this := CategoryTheory.ConcreteCategory.ofHom f; this)

On the duplicate-free indecomposable skeleton, the same radical Hom-space consists of the maps which are not split monomorphisms.

theorem QuotientSubmoduleEquidistribution.IndecomposableSkeleton.biproductDesc_not_isSplitEpi {R : Type uR} [Ring R] [IsNoetherianRing R] {ι : Type uι} (σ : IndecomposableSkeleton R ι) {z : ι} {J : Type} [Fintype J] (F : J → FGModuleCat R) (component : (j : J) → F j ⟶ σ.obj z) (hnonsplit : ∀ (j : J), ¬CategoryTheory.IsSplitEpi (component j)) : ¬CategoryTheory.IsSplitEpi (CategoryTheory.Limits.biproduct.desc component)

A finite biproduct map into a chosen indecomposable cannot split if none of its components splits.

theorem QuotientSubmoduleEquidistribution.IndecomposableSkeleton.biproductLift_not_isSplitMono {R : Type uR} [Ring R] [IsNoetherianRing R] {ι : Type uι} (σ : IndecomposableSkeleton R ι) {z : ι} {J : Type} [Fintype J] (F : J → FGModuleCat R) (component : (j : J) → σ.obj z ⟶ F j) (hnonsplit : ∀ (j : J), ¬CategoryTheory.IsSplitMono (component j)) : ¬CategoryTheory.IsSplitMono (CategoryTheory.Limits.biproduct.lift component)

Dually, a finite biproduct map out of a chosen indecomposable cannot split if none of its component maps splits.

theorem QuotientSubmoduleEquidistribution.IndecomposableSkeleton.exists_finiteLength_rightAlmostSplit {K : Type uK} [Field K] {R : Type uR} [Ring R] [Algebra K R] [IsNoetherianRing R] {ι : Type uι} (σ : IndecomposableSkeleton R ι) [(i : ι) → Module K ↑(σ.obj i)] [∀ (i : ι), IsScalarTower K R ↑(σ.obj i)] [Finite ι] [∀ (i : ι), FiniteDimensional K ↑(σ.obj i)] (z : ι) : ∃ (E : FGModuleCat R) (f : E ⟶ σ.obj z), IsFiniteLength R ↑E ∧ IsRightAlmostSplit f

Finite radical evaluation gives a finite-length right almost-split map into every representative of a finite indecomposable skeleton.

theorem QuotientSubmoduleEquidistribution.IndecomposableSkeleton.exists_finiteLength_leftAlmostSplit {K : Type uK} [Field K] {R : Type uR} [Ring R] [Algebra K R] [IsNoetherianRing R] {ι : Type uι} (σ : IndecomposableSkeleton R ι) [(i : ι) → Module K ↑(σ.obj i)] [∀ (i : ι), IsScalarTower K R ↑(σ.obj i)] [Finite ι] [∀ (i : ι), FiniteDimensional K ↑(σ.obj i)] (z : ι) : ∃ (E : FGModuleCat R) (f : σ.obj z ⟶ E), IsFiniteLength R ↑E ∧ IsLeftAlmostSplit f

Finite radical evaluation gives a finite-length left almost-split map out of every representative of a finite indecomposable skeleton.

theorem QuotientSubmoduleEquidistribution.IndecomposableSkeleton.minimalRightAlmostSplitDecomposition_nonempty {K : Type uK} [Field K] {R : Type uR} [Ring R] [Algebra K R] [IsNoetherianRing R] {ι : Type uι} (σ : IndecomposableSkeleton R ι) [(i : ι) → Module K ↑(σ.obj i)] [∀ (i : ι), IsScalarTower K R ↑(σ.obj i)] [Finite ι] [∀ (i : ι), FiniteDimensional K ↑(σ.obj i)] (z : ι) : Nonempty (σ.MinimalRightAlmostSplitDecomposition z)

Finite radical evaluation followed by finite-length minimalization gives a minimal right almost-split decomposition at every skeleton vertex.

theorem QuotientSubmoduleEquidistribution.IndecomposableSkeleton.minimalLeftAlmostSplitDecomposition_nonempty {K : Type uK} [Field K] {R : Type uR} [Ring R] [Algebra K R] [IsNoetherianRing R] {ι : Type uι} (σ : IndecomposableSkeleton R ι) [(i : ι) → Module K ↑(σ.obj i)] [∀ (i : ι), IsScalarTower K R ↑(σ.obj i)] [Finite ι] [∀ (i : ι), FiniteDimensional K ↑(σ.obj i)] (z : ι) : Nonempty (σ.MinimalLeftAlmostSplitDecomposition z)

The left-hand finite radical evaluation likewise has a minimal finite-length representative.

theorem QuotientSubmoduleEquidistribution.IndecomposableSkeleton.qClosed_compl_pair_iff_hasIrreducible_of_finiteSkeleton {K : Type uK} [Field K] {R : Type uR} [Ring R] [Algebra K R] [IsNoetherianRing R] {ι : Type uι} (σ : IndecomposableSkeleton R ι) [(i : ι) → Module K ↑(σ.obj i)] [∀ (i : ι), IsScalarTower K R ↑(σ.obj i)] [Finite ι] [∀ (i : ι), FiniteDimensional K ↑(σ.obj i)] {p z : ι} (hpz : p ≠ z) (hp : σ.IsRelativeSplitProjective Set.univ p) (hz : ¬σ.IsRelativeSplitProjective Set.univ z) : σ.qClosure.IsClosed {p, z}ᶜ ↔ HasIrreducibleMorphism (σ.obj p) (σ.obj z)

In the finite-skeleton setting, the quotient-side mixed criterion no longer needs an almost-split existence hypothesis.

theorem QuotientSubmoduleEquidistribution.IndecomposableSkeleton.sClosed_compl_pair_iff_hasIrreducible_of_finiteSkeleton {K : Type uK} [Field K] {R : Type uR} [Ring R] [Algebra K R] [IsNoetherianRing R] {ι : Type uι} (σ : IndecomposableSkeleton R ι) [(i : ι) → Module K ↑(σ.obj i)] [∀ (i : ι), IsScalarTower K R ↑(σ.obj i)] [Finite ι] [∀ (i : ι), FiniteDimensional K ↑(σ.obj i)] {z i : ι} (hzi : z ≠ i) (hz : ¬σ.IsRelativeSplitInjective Set.univ z) (hi : σ.IsRelativeSplitInjective Set.univ i) : σ.sClosure.IsClosed {z, i}ᶜ ↔ HasIrreducibleMorphism (σ.obj z) (σ.obj i)

The submodule-side mixed criterion is unconditionally available under the same finite-skeleton hypotheses.

theorem QuotientSubmoduleEquidistribution.IndecomposableSkeleton.exists_finiteLength_rightAlmostSplit_of_finiteDimensional {R : Type uR} [Ring R] [IsNoetherianRing R] {ι : Type uι} (σ : IndecomposableSkeleton R ι) (K : Type uK) [Field K] [Algebra K R] [FiniteDimensional K R] [Finite ι] (z : ι) : ∃ (E : FGModuleCat R) (f : E ⟶ σ.obj z), IsFiniteLength R ↑E ∧ IsRightAlmostSplit f

The usual finite-dimensional-algebra hypotheses supply all pointwise scalar and finiteness instances required by right radical evaluation.

theorem QuotientSubmoduleEquidistribution.IndecomposableSkeleton.exists_finiteLength_leftAlmostSplit_of_finiteDimensional {R : Type uR} [Ring R] [IsNoetherianRing R] {ι : Type uι} (σ : IndecomposableSkeleton R ι) (K : Type uK) [Field K] [Algebra K R] [FiniteDimensional K R] [Finite ι] (z : ι) : ∃ (E : FGModuleCat R) (f : σ.obj z ⟶ E), IsFiniteLength R ↑E ∧ IsLeftAlmostSplit f

The corresponding finite-dimensional-algebra wrapper for left radical evaluation.

theorem QuotientSubmoduleEquidistribution.IndecomposableSkeleton.minimalRightAlmostSplitDecomposition_nonempty_of_finiteDimensional {R : Type uR} [Ring R] [IsNoetherianRing R] {ι : Type uι} (σ : IndecomposableSkeleton R ι) (K : Type uK) [Field K] [Algebra K R] [FiniteDimensional K R] [Finite ι] (z : ι) : Nonempty (σ.MinimalRightAlmostSplitDecomposition z)

A finite-dimensional algebra with a finite complete indecomposable skeleton has minimal right almost-split decompositions at every vertex.

theorem QuotientSubmoduleEquidistribution.IndecomposableSkeleton.minimalLeftAlmostSplitDecomposition_nonempty_of_finiteDimensional {R : Type uR} [Ring R] [IsNoetherianRing R] {ι : Type uι} (σ : IndecomposableSkeleton R ι) (K : Type uK) [Field K] [Algebra K R] [FiniteDimensional K R] [Finite ι] (z : ι) : Nonempty (σ.MinimalLeftAlmostSplitDecomposition z)

The left-dual minimal decomposition exists under the same hypotheses.

theorem QuotientSubmoduleEquidistribution.IndecomposableSkeleton.qClosed_compl_pair_iff_hasIrreducible_of_finiteDimensional {R : Type uR} [Ring R] [IsNoetherianRing R] {ι : Type uι} (σ : IndecomposableSkeleton R ι) (K : Type uK) [Field K] [Algebra K R] [FiniteDimensional K R] [Finite ι] {p z : ι} (hpz : p ≠ z) (hp : σ.IsRelativeSplitProjective Set.univ p) (hz : ¬σ.IsRelativeSplitProjective Set.univ z) : σ.qClosure.IsClosed {p, z}ᶜ ↔ HasIrreducibleMorphism (σ.obj p) (σ.obj z)

Paper-facing finite-dimensional-algebra form of the quotient-side mixed criterion.

theorem QuotientSubmoduleEquidistribution.IndecomposableSkeleton.sClosed_compl_pair_iff_hasIrreducible_of_finiteDimensional {R : Type uR} [Ring R] [IsNoetherianRing R] {ι : Type uι} (σ : IndecomposableSkeleton R ι) (K : Type uK) [Field K] [Algebra K R] [FiniteDimensional K R] [Finite ι] {z i : ι} (hzi : z ≠ i) (hz : ¬σ.IsRelativeSplitInjective Set.univ z) (hi : σ.IsRelativeSplitInjective Set.univ i) : σ.sClosure.IsClosed {z, i}ᶜ ↔ HasIrreducibleMorphism (σ.obj z) (σ.obj i)

Paper-facing finite-dimensional-algebra form of the dual mixed criterion.