Target split--radical normal form

This is the categorical dual of the source normal form used in Iyama's right-ladder construction. No concrete algebra or module classification is used.

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

An elementary lower shear of a binary biproduct.

theorem QuotientSubmoduleEquidistribution.Iyama.LeftLadder.lift_biprodTargetShear_hom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {M Z U : C} (c : Z ⟶ U) (p : M ⟶ Z) (r : M ⟶ U) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.lift p r) (biprodTargetShear c).hom = CategoryTheory.Limits.biprod.lift p (CategoryTheory.CategoryStruct.comp p c + r)

theorem QuotientSubmoduleEquidistribution.Iyama.LeftLadder.lift_biprodTargetShear_hom_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {M Z U : C} (c : Z ⟶ U) (p : M ⟶ Z) (r : M ⟶ U) {Z✝ : C} (h : Z ⊞ U ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.lift p r) (CategoryTheory.CategoryStruct.comp (biprodTargetShear c).hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.lift p (CategoryTheory.CategoryStruct.comp p c + r)) h

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

Target-side counterpart of moveLeftPastFirstIso_inv_desc.

theorem QuotientSubmoduleEquidistribution.Iyama.LeftLadder.lift_lift_associator_inv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {M Z P U : C} (p : M ⟶ Z) (a : M ⟶ P) (r : M ⟶ U) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.lift p (CategoryTheory.Limits.biprod.lift a r)) (CategoryTheory.Limits.biprod.associator Z P U).inv = CategoryTheory.Limits.biprod.lift (CategoryTheory.Limits.biprod.lift p a) r

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

A target split--radical form: after changing the target by an isomorphism, a morphism is a column consisting of a split epimorphism and a categorical-radical morphism.

• Z : C
• U : C
• e : Y ≅ self.Z ⊞ self.U
• p : M ⟶ self.Z
• r : M ⟶ self.U
• s : self.Z ⟶ M
• s_p : CategoryTheory.CategoryStruct.comp self.s self.p = CategoryTheory.CategoryStruct.id self.Z
• s_r : CategoryTheory.CategoryStruct.comp self.s self.r = 0
• r_mem : self.r ∈ R.ideal.hom M self.U
• map_eq : CategoryTheory.CategoryStruct.comp k self.e.hom = CategoryTheory.Limits.biprod.lift self.p self.r

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

Transport a target split--radical form along an isomorphism of targets.

theorem QuotientSubmoduleEquidistribution.Iyama.LeftLadder.FiniteTauCategoryData.isRadicalMorphism_iff_not_isSplitEpi_to_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 : FiniteTauCategoryData C Ind) {x : Ind} {M : C} (f : M ⟶ T.obj x) : CategoricalRadical.IsRadicalMorphism f ↔ ¬CategoryTheory.IsSplitEpi f

A morphism into a chosen indecomposable is radical exactly when it is not a split epimorphism.

noncomputable def QuotientSubmoduleEquidistribution.Iyama.LeftLadder.cosplitRadicalForm_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 : FiniteTauCategoryData C Ind) (x : Ind) {M Q : C} (f : M ⟶ T.obj x) (q : M ⟶ Q) (hq : CosplitRadicalForm T.radical q) : CosplitRadicalForm T.radical (CategoryTheory.Limits.biprod.lift f q)

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

noncomputable def QuotientSubmoduleEquidistribution.Iyama.LeftLadder.cosplitRadicalForm_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 : FiniteTauCategoryData C Ind) (n : ℕ) (label : Fin n → Ind) (M : C) (k : M ⟶ ⨁ fun (i : Fin n) => T.obj (label i)) : CosplitRadicalForm T.radical k

Target split--radical normal form for a morphism whose target is a displayed finite biproduct of chosen indecomposables.

noncomputable def QuotientSubmoduleEquidistribution.Iyama.LeftLadder.FiniteTauCategoryData.cosplitRadicalForm {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 : FiniteTauCategoryData C Ind) {M Y : C} (k : M ⟶ Y) : CosplitRadicalForm T.radical k

Every morphism in a finite tau-category has a target split--radical normal form.

theorem QuotientSubmoduleEquidistribution.Iyama.LeftLadder.FiniteTauCategoryData.exists_splitEpi_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 : FiniteTauCategoryData C Ind) {M Y : C} (k : M ⟶ Y) : ∃ (Z : C) (U : C) (e : Y ≅ Z ⊞ U) (p : M ⟶ Z) (r : M ⟶ U), CategoryTheory.IsSplitEpi p ∧ CategoricalRadical.IsRadicalMorphism r ∧ CategoryTheory.CategoryStruct.comp k e.hom = CategoryTheory.Limits.biprod.lift p r

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