Krull--Schmidt split--radical normal form

In the finite Krull--Schmidt skeleton recorded by FiniteTauCategoryData, every morphism becomes, after an isomorphism of its source, a row consisting of a split monomorphism and a categorical-radical morphism. The proof is a finite induction over a chosen indecomposable decomposition. Elementary biproduct shears add each indecomposable either to the split part or to the radical remainder.

This is the classification-free normal-form input in Iyama's special-arrow right-ladder construction.

noncomputable def QuotientSubmoduleEquidistribution.Iyama.finTailProjection {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] {n : ℕ} (F : Fin (n + 1) → C) : ⨁ F ⟶ ⨁ fun (i : Fin n) => F i.succ

noncomputable def QuotientSubmoduleEquidistribution.Iyama.finTailInclusion {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] {n : ℕ} (F : Fin (n + 1) → C) : (⨁ fun (i : Fin n) => F i.succ) ⟶ ⨁ F

@[simp]

theorem QuotientSubmoduleEquidistribution.Iyama.fin_head_tailProjection {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] {n : ℕ} (F : Fin (n + 1) → C) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.ι F 0) (finTailProjection F) = 0

@[simp]

theorem QuotientSubmoduleEquidistribution.Iyama.fin_head_tailProjection_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] {n : ℕ} (F : Fin (n + 1) → C) {Z : C} (h : (⨁ fun (i : Fin n) => F i.succ) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.ι F 0) (CategoryTheory.CategoryStruct.comp (finTailProjection F) h) = CategoryTheory.CategoryStruct.comp 0 h

@[simp]

theorem QuotientSubmoduleEquidistribution.Iyama.fin_tailComponent_tailProjection {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] {n : ℕ} (F : Fin (n + 1) → C) (j : Fin n) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.ι F j.succ) (finTailProjection F) = CategoryTheory.Limits.biproduct.ι (fun (i : Fin n) => F i.succ) j

@[simp]

theorem QuotientSubmoduleEquidistribution.Iyama.fin_tailComponent_tailProjection_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] {n : ℕ} (F : Fin (n + 1) → C) (j : Fin n) {Z : C} (h : (⨁ fun (i : Fin n) => F i.succ) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.ι F j.succ) (CategoryTheory.CategoryStruct.comp (finTailProjection F) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.ι (fun (i : Fin n) => F i.succ) j) h

@[simp]

theorem QuotientSubmoduleEquidistribution.Iyama.fin_tailInclusion_head {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] {n : ℕ} (F : Fin (n + 1) → C) : CategoryTheory.CategoryStruct.comp (finTailInclusion F) (CategoryTheory.Limits.biproduct.π F 0) = 0

@[simp]

theorem QuotientSubmoduleEquidistribution.Iyama.fin_tailInclusion_head_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] {n : ℕ} (F : Fin (n + 1) → C) {Z : C} (h : F 0 ⟶ Z) : CategoryTheory.CategoryStruct.comp (finTailInclusion F) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.π F 0) h) = CategoryTheory.CategoryStruct.comp 0 h

@[simp]

theorem QuotientSubmoduleEquidistribution.Iyama.fin_tailInclusion_component {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] {n : ℕ} (F : Fin (n + 1) → C) (j : Fin n) : CategoryTheory.CategoryStruct.comp (finTailInclusion F) (CategoryTheory.Limits.biproduct.π F j.succ) = CategoryTheory.Limits.biproduct.π (fun (i : Fin n) => F i.succ) j

@[simp]

theorem QuotientSubmoduleEquidistribution.Iyama.fin_tailInclusion_component_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] {n : ℕ} (F : Fin (n + 1) → C) (j : Fin n) {Z : C} (h : F j.succ ⟶ Z) : CategoryTheory.CategoryStruct.comp (finTailInclusion F) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.π F j.succ) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.π (fun (i : Fin n) => F i.succ) j) h

@[simp]

theorem QuotientSubmoduleEquidistribution.Iyama.fin_tailInclusion_tailProjection {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] {n : ℕ} (F : Fin (n + 1) → C) : CategoryTheory.CategoryStruct.comp (finTailInclusion F) (finTailProjection F) = CategoryTheory.CategoryStruct.id (⨁ fun (i : Fin n) => F i.succ)

@[simp]

theorem QuotientSubmoduleEquidistribution.Iyama.fin_tailInclusion_tailProjection_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] {n : ℕ} (F : Fin (n + 1) → C) {Z : C} (h : (⨁ fun (i : Fin n) => F i.succ) ⟶ Z) : CategoryTheory.CategoryStruct.comp (finTailInclusion F) (CategoryTheory.CategoryStruct.comp (finTailProjection F) h) = h

noncomputable def QuotientSubmoduleEquidistribution.Iyama.finBiproductConsIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasBinaryBiproducts C] {n : ℕ} (F : Fin (n + 1) → C) : ⨁ F ≅ F 0 ⊞ ⨁ fun (i : Fin n) => F i.succ

Split off the first factor of a Fin (n+1)-indexed biproduct.

noncomputable def QuotientSubmoduleEquidistribution.Iyama.biprodShear {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {Z U : C} (c : U ⟶ Z) : Z ⊞ U ≅ Z ⊞ U

An elementary upper shear of a binary biproduct.

theorem QuotientSubmoduleEquidistribution.Iyama.biprodShear_hom_desc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {Z U M : C} (c : U ⟶ Z) (j : Z ⟶ M) (r : U ⟶ M) : CategoryTheory.CategoryStruct.comp (biprodShear c).hom (CategoryTheory.Limits.biprod.desc j r) = CategoryTheory.Limits.biprod.desc j (CategoryTheory.CategoryStruct.comp c j + r)

theorem QuotientSubmoduleEquidistribution.Iyama.biprodShear_hom_desc_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {Z U M : C} (c : U ⟶ Z) (j : Z ⟶ M) (r : U ⟶ M) {Z✝ : C} (h : M ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (biprodShear c).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.desc j r) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.desc j (CategoryTheory.CategoryStruct.comp c j + r)) h

noncomputable def QuotientSubmoduleEquidistribution.Iyama.moveLeftPastFirstIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {P Q Z U : C} (e : Q ≅ Z ⊞ U) : P ⊞ Q ≅ Z ⊞ P ⊞ U

Move the left factor past the first factor of a decomposed right term.

theorem QuotientSubmoduleEquidistribution.Iyama.moveLeftPastFirstIso_inv_desc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {P Q Z U M : C} (e : Q ≅ Z ⊞ U) (f : P ⟶ M) (q : Q ⟶ M) (j : Z ⟶ M) (r : U ⟶ M) (hq : CategoryTheory.CategoryStruct.comp e.inv q = CategoryTheory.Limits.biprod.desc j r) : CategoryTheory.CategoryStruct.comp (moveLeftPastFirstIso e).inv (CategoryTheory.Limits.biprod.desc f q) = CategoryTheory.Limits.biprod.desc j (CategoryTheory.Limits.biprod.desc f r)

structure QuotientSubmoduleEquidistribution.Iyama.SplitRadicalForm {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] (R : CategoricalRadical.NilpotentRadicalData C) {X M : C} (k : X ⟶ M) : Type (max u v)

• Z : C
• U : C
• e : X ≅ self.Z ⊞ self.U
• j : self.Z ⟶ M
• r : self.U ⟶ M
• s : M ⟶ self.Z
• j_s : CategoryTheory.CategoryStruct.comp self.j self.s = CategoryTheory.CategoryStruct.id self.Z
• r_s : CategoryTheory.CategoryStruct.comp self.r self.s = 0
• r_mem : self.r ∈ R.ideal.hom self.U M
• map_eq : CategoryTheory.CategoryStruct.comp self.e.inv k = CategoryTheory.Limits.biprod.desc self.j self.r

noncomputable def QuotientSubmoduleEquidistribution.Iyama.SplitRadicalForm.precomposeIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {R : CategoricalRadical.NilpotentRadicalData C} {X Y M : C} {q : Y ⟶ M} (h : SplitRadicalForm R q) (e₀ : X ≅ Y) (k : X ⟶ M) (hk : CategoryTheory.CategoryStruct.comp e₀.inv k = q) : SplitRadicalForm R k

Transport a split--radical form along an isomorphism of source objects.

theorem QuotientSubmoduleEquidistribution.Iyama.associator_hom_desc_desc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {Z P U M : C} (j : Z ⟶ M) (a : P ⟶ M) (r : U ⟶ M) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.associator Z P U).hom (CategoryTheory.Limits.biprod.desc j (CategoryTheory.Limits.biprod.desc a r)) = CategoryTheory.Limits.biprod.desc (CategoryTheory.Limits.biprod.desc j a) r

theorem QuotientSubmoduleEquidistribution.Iyama.FiniteRightTauCategoryData.isIso_of_isSplitMono_obj_obj {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.IsIdempotentComplete C] {Ind : Type w} [Fintype Ind] (T : FiniteRightTauCategoryData C Ind) {p q : Ind} (f : T.obj p ⟶ T.obj q) [CategoryTheory.IsSplitMono f] : CategoryTheory.IsIso f

A split monomorphism between two representatives in the finite right tau skeleton is an isomorphism.

noncomputable def QuotientSubmoduleEquidistribution.Iyama.splitRadicalForm_biprod_obj {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.IsIdempotentComplete C] {Ind : Type w} [Fintype Ind] (T : FiniteRightTauCategoryData C Ind) (p : Ind) {Q M : C} (f : T.obj p ⟶ M) (q : Q ⟶ M) (hq : SplitRadicalForm T.radical q) : SplitRadicalForm T.radical (CategoryTheory.Limits.biprod.desc f q)

Add one chosen indecomposable source summand to a split--radical normal form.

noncomputable def QuotientSubmoduleEquidistribution.Iyama.splitRadicalForm_finBiproduct {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.IsIdempotentComplete C] {Ind : Type w} [Fintype Ind] (T : FiniteRightTauCategoryData C Ind) (n : ℕ) (label : Fin n → Ind) (M : C) (k : (⨁ fun (i : Fin n) => T.obj (label i)) ⟶ M) : SplitRadicalForm T.radical k

Split--radical normal form for a morphism whose source is a displayed finite biproduct of chosen indecomposables.

noncomputable def QuotientSubmoduleEquidistribution.Iyama.FiniteRightTauCategoryData.splitRadicalForm {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.IsIdempotentComplete C] {Ind : Type w} [Fintype Ind] (T : FiniteRightTauCategoryData C Ind) {X M : C} (k : X ⟶ M) : SplitRadicalForm T.radical k

Every morphism in a finite tau-category has a Krull--Schmidt split--radical normal form on its source.

theorem QuotientSubmoduleEquidistribution.Iyama.FiniteRightTauCategoryData.exists_splitMono_radical_normalForm {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.IsIdempotentComplete C] {Ind : Type w} [Fintype Ind] (T : FiniteRightTauCategoryData C Ind) {X M : C} (k : X ⟶ M) : ∃ (Z : C) (U : C) (e : X ≅ Z ⊞ U) (j : Z ⟶ M) (r : U ⟶ M), CategoryTheory.IsSplitMono j ∧ CategoricalRadical.IsRadicalMorphism r ∧ CategoryTheory.CategoryStruct.comp e.inv k = CategoryTheory.Limits.biprod.desc j r

Existential form: after an isomorphism X ≅ Z ⨞ U, the map is the pair of a split monomorphism and a categorical-radical morphism.