Irreducible morphisms and the categorical radical quotient

This file formalizes the manuscript convention Irr(X,Y) = rad(X,Y) / rad²(X,Y) for two representatives in a complete indecomposable skeleton. The construction uses additive Hom-groups and is therefore independent of a ground field.

Between indecomposable finite-length objects, a radical map is equivalently a nonsplit epimorphism, or equivalently a nonsplit monomorphism. The square is expressed by one factorization through an arbitrary finitely generated module: finite sums of radical composites consolidate into such a factorization through a finite biproduct. Thus this is the square of the categorical radical ideal, not the square of either endpoint endomorphism ring.

No algebra presentation or classification of modules is used.

def QuotientSubmoduleEquidistribution.IndecomposableSkeleton.radicalHomAddSubgroup {R : Type uR} [Ring R] [IsNoetherianRing R] {ι : Type uι} (σ : IndecomposableSkeleton R ι) (x y : ι) : AddSubgroup (σ.obj x ⟶ σ.obj y)

The field-free radical Hom-group between two chosen indecomposables, realized as the morphisms which are not split epimorphisms.

@[simp]

theorem QuotientSubmoduleEquidistribution.IndecomposableSkeleton.mem_radicalHomAddSubgroup_iff_not_isSplitEpi {R : Type uR} [Ring R] [IsNoetherianRing R] {ι : Type uι} (σ : IndecomposableSkeleton R ι) {x y : ι} (f : σ.obj x ⟶ σ.obj y) : f ∈ σ.radicalHomAddSubgroup x y ↔ ¬CategoryTheory.IsSplitEpi f

theorem QuotientSubmoduleEquidistribution.IndecomposableSkeleton.mem_radicalHomAddSubgroup_iff_not_isSplitMono {R : Type uR} [Ring R] [IsNoetherianRing R] {ι : Type uι} (σ : IndecomposableSkeleton R ι) {x y : ι} (f : σ.obj x ⟶ σ.obj y) : f ∈ σ.radicalHomAddSubgroup x y ↔ ¬CategoryTheory.IsSplitMono f

On the duplicate-free indecomposable skeleton, the same radical group consists of the morphisms which are not split monomorphisms.

theorem QuotientSubmoduleEquidistribution.IndecomposableSkeleton.isRadicalMorphism_iff_not_isSplitMono_from_obj {R : Type uR} [Ring R] [IsNoetherianRing R] {ι : Type uι} (σ : IndecomposableSkeleton R ι) {x : ι} {M : FGModuleCat R} (g : σ.obj x ⟶ M) : CategoricalRadical.IsRadicalMorphism g ↔ ¬CategoryTheory.IsSplitMono g

A morphism out of a chosen indecomposable is categorical-radical exactly when it is not a split monomorphism, even when its target is an arbitrary finitely generated module.

theorem QuotientSubmoduleEquidistribution.IndecomposableSkeleton.isRadicalMorphism_iff_not_isSplitEpi_to_obj {R : Type uR} [Ring R] [IsNoetherianRing R] {ι : Type uι} (σ : IndecomposableSkeleton R ι) {M : FGModuleCat R} {y : ι} (h : M ⟶ σ.obj y) : CategoricalRadical.IsRadicalMorphism h ↔ ¬CategoryTheory.IsSplitEpi h

A morphism into a chosen indecomposable is categorical-radical exactly when it is not a split epimorphism, even when its source is an arbitrary finitely generated module.

theorem QuotientSubmoduleEquidistribution.IndecomposableSkeleton.mem_radicalHomAddSubgroup_iff_isRadicalMorphism {R : Type uR} [Ring R] [IsNoetherianRing R] {ι : Type uι} (σ : IndecomposableSkeleton R ι) {x y : ι} (f : σ.obj x ⟶ σ.obj y) : f ∈ σ.radicalHomAddSubgroup x y ↔ CategoricalRadical.IsRadicalMorphism f

On chosen indecomposables, the nonsplit-epimorphism description agrees with the intrinsic categorical Jacobson radical, in its source-object convention.

def QuotientSubmoduleEquidistribution.IndecomposableSkeleton.HasRadicalSquareFactorization {R : Type uR} [Ring R] [IsNoetherianRing R] {ι : Type uι} (σ : IndecomposableSkeleton R ι) {x y : ι} (f : σ.obj x ⟶ σ.obj y) : Prop

A morphism between chosen indecomposables has a radical-square factorization if it factors through an arbitrary finitely generated module, with a nonsplit-monic first factor and a nonsplit-epic second factor.

theorem QuotientSubmoduleEquidistribution.IndecomposableSkeleton.hasRadicalSquareFactorization_iff_categoricalRadical {R : Type uR} [Ring R] [IsNoetherianRing R] {ι : Type uι} (σ : IndecomposableSkeleton R ι) {x y : ι} (f : σ.obj x ⟶ σ.obj y) : σ.HasRadicalSquareFactorization f ↔ ∃ (M : FGModuleCat R) (g : σ.obj x ⟶ M) (h : M ⟶ σ.obj y), CategoricalRadical.IsRadicalMorphism g ∧ CategoricalRadical.IsRadicalMorphism h ∧ CategoryTheory.CategoryStruct.comp g h = f

The arbitrary-middle predicate is literally one composite of two categorical-radical morphisms.

def QuotientSubmoduleEquidistribution.IndecomposableSkeleton.radicalSquareHomAddSubgroup {R : Type uR} [Ring R] [IsNoetherianRing R] {ι : Type uι} (σ : IndecomposableSkeleton R ι) (x y : ι) : AddSubgroup (σ.obj x ⟶ σ.obj y)

The field-free square of the categorical radical between two chosen indecomposables. Closure under addition consolidates two factorizations through their biproduct.

@[simp]

theorem QuotientSubmoduleEquidistribution.IndecomposableSkeleton.mem_radicalSquareHomAddSubgroup_iff {R : Type uR} [Ring R] [IsNoetherianRing R] {ι : Type uι} (σ : IndecomposableSkeleton R ι) {x y : ι} (f : σ.obj x ⟶ σ.obj y) : f ∈ σ.radicalSquareHomAddSubgroup x y ↔ σ.HasRadicalSquareFactorization f

theorem QuotientSubmoduleEquidistribution.IndecomposableSkeleton.radicalSquareHomAddSubgroup_le_radicalHomAddSubgroup {R : Type uR} [Ring R] [IsNoetherianRing R] {ι : Type uι} (σ : IndecomposableSkeleton R ι) (x y : ι) : σ.radicalSquareHomAddSubgroup x y ≤ σ.radicalHomAddSubgroup x y

Every radical-square morphism is radical.

def QuotientSubmoduleEquidistribution.IndecomposableSkeleton.radicalSquareInRadical {R : Type uR} [Ring R] [IsNoetherianRing R] {ι : Type uι} (σ : IndecomposableSkeleton R ι) (x y : ι) : AddSubgroup ↥(σ.radicalHomAddSubgroup x y)

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

@[reducible, inline]

abbrev QuotientSubmoduleEquidistribution.IndecomposableSkeleton.irreducibleHomQuotient {R : Type uR} [Ring R] [IsNoetherianRing R] {ι : Type uι} (σ : IndecomposableSkeleton R ι) (x y : ι) : Type w

The manuscript's field-free quotient Irr(X,Y) = rad(X,Y) / rad²(X,Y).

theorem QuotientSubmoduleEquidistribution.IndecomposableSkeleton.isIrreducibleMorphism_iff_mem_radical_not_mem_radicalSquare {R : Type uR} [Ring R] [IsNoetherianRing R] {ι : Type uι} (σ : IndecomposableSkeleton R ι) {x y : ι} (f : σ.obj x ⟶ σ.obj y) : IsIrreducibleMorphism f ↔ f ∈ σ.radicalHomAddSubgroup x y ∧ f ∉ σ.radicalSquareHomAddSubgroup x y

Between chosen indecomposables, categorical irreducibility is exactly membership in rad but not in rad².

theorem QuotientSubmoduleEquidistribution.IndecomposableSkeleton.nontrivial_irreducibleHomQuotient_iff_hasIrreducibleMorphism {R : Type uR} [Ring R] [IsNoetherianRing R] {ι : Type uι} (σ : IndecomposableSkeleton R ι) (x y : ι) : Nontrivial (σ.irreducibleHomQuotient x y) ↔ HasIrreducibleMorphism (σ.obj x) (σ.obj y)

The quotient rad(X,Y) / rad²(X,Y) is nontrivial exactly when there is an irreducible morphism from X to Y.

theorem QuotientSubmoduleEquidistribution.IndecomposableSkeleton.hasIrreducibleMorphism_iff_nontrivial_irreducibleHomQuotient {R : Type uR} [Ring R] [IsNoetherianRing R] {ι : Type uι} (σ : IndecomposableSkeleton R ι) (x y : ι) : HasIrreducibleMorphism (σ.obj x) (σ.obj y) ↔ Nontrivial (σ.irreducibleHomQuotient x y)

Manuscript-style orientation of the nonzero-quotient criterion.