Special-arrow target conormalization

This is the dual of Iyama's source-padded special normalization. The file uses the target split--radical normal form and produces the exact SpecialConormalization expected by the finite left-ladder builder.

theorem QuotientSubmoduleEquidistribution.Iyama.LeftLadder.IsSpecial.nonempty_iso_biprod_lift_zero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] (R : CategoricalRadical.NilpotentRadicalData C) {X Z U : C} {b : X ⟶ Z} {q : X ⟶ U} (ha : IsSpecial R (CategoryTheory.Limits.biprod.lift b q)) (hq : q ∈ (R.ideal.pow 2).hom X U) : Nonempty (CategoryTheory.Arrow.mk (CategoryTheory.Limits.biprod.lift b q) ≅ CategoryTheory.Arrow.mk (CategoryTheory.Limits.biprod.lift b 0))

A special arrow with a radical-square complementary target component is isomorphic to the same arrow with that component zeroed.

theorem QuotientSubmoduleEquidistribution.Iyama.LeftLadder.IsSpecial.nonempty_iso_biprod_lift_zero_of_iso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] (R : CategoricalRadical.NilpotentRadicalData C) {X Y Z U : C} {a : X ⟶ Y} {b : X ⟶ Z} {q : X ⟶ U} (ha : IsSpecial R a) (e : CategoryTheory.Arrow.mk a ≅ CategoryTheory.Arrow.mk (CategoryTheory.Limits.biprod.lift b q)) (hq : q ∈ (R.ideal.pow 2).hom X U) : Nonempty (CategoryTheory.Arrow.mk a ≅ CategoryTheory.Arrow.mk (CategoryTheory.Limits.biprod.lift b 0))

Isomorphism-invariant target-padding absorption.

theorem QuotientSubmoduleEquidistribution.Iyama.LeftLadder.nonempty_arrow_iso_of_biprod_lift_zero_iso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {X Z U X' Z' U' : C} {b : X ⟶ Z} {b' : X' ⟶ Z'} (hb : IsLeftMinimal b) (hb' : IsLeftMinimal b') (e : CategoryTheory.Arrow.mk (CategoryTheory.Limits.biprod.lift b 0) ≅ CategoryTheory.Arrow.mk (CategoryTheory.Limits.biprod.lift b' 0)) : Nonempty (CategoryTheory.Arrow.mk b ≅ CategoryTheory.Arrow.mk b')

Zero-padded left-minimal arrows cancel their padded target summands.

theorem QuotientSubmoduleEquidistribution.Iyama.LeftLadder.IsSpecial.cancel_biprod_lift_zero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] (R : CategoricalRadical.NilpotentRadicalData C) {X Z U : C} {b : X ⟶ Z} (hpadded : IsSpecial R (CategoryTheory.Limits.biprod.lift b 0)) (hb : IsLeftMinimal b) (hpert : ∀ r ∈ (R.ideal.pow 2).hom X Z, IsLeftMinimal (b + r)) : IsSpecial R b

Specialness of a target-padded arrow descends to its left-minimal essential component when its radical-square perturbations stay left minimal.

theorem QuotientSubmoduleEquidistribution.Iyama.LeftLadder.IsLeftMinimal.precomp_iso {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : C} {g : Y ⟶ Z} (e : X ≅ Y) (hg : IsLeftMinimal g) : IsLeftMinimal (CategoryTheory.CategoryStruct.comp e.hom g)

Precomposition by an isomorphism preserves left minimality.

theorem QuotientSubmoduleEquidistribution.Iyama.LeftLadder.IsLeftMinimal.postcomp_splitEpi {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {X Y Z : C} {g : X ⟶ Y} (hg : IsLeftMinimal g) (p : Y ⟶ Z) [CategoryTheory.IsSplitEpi p] : IsLeftMinimal (CategoryTheory.CategoryStruct.comp g p)

Postcomposing a left-minimal map by a split epimorphism preserves left minimality.

theorem QuotientSubmoduleEquidistribution.Iyama.LeftLadder.isLeftMinimal_splitCofactor_chosen_leftMesh {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 Z : C} (p : (T.leftMesh X).X₂ ⟶ Z) [CategoryTheory.IsSplitEpi p] : IsLeftMinimal (CategoryTheory.CategoryStruct.comp (T.leftTermIso X).inv (CategoryTheory.CategoryStruct.comp (T.leftMesh X).f p))

A split-epimorphic cofactor of a chosen left mesh map is left minimal.

theorem QuotientSubmoduleEquidistribution.Iyama.LeftLadder.isLeftMinimal_add_mem_square_splitCofactor_chosen_leftMesh {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 Z : C} (p : (T.leftMesh X).X₂ ⟶ Z) [CategoryTheory.IsSplitEpi p] (r : X ⟶ Z) (hr : r ∈ (T.radical.ideal.pow 2).hom X Z) : IsLeftMinimal (CategoryTheory.CategoryStruct.comp (T.leftTermIso X).inv (CategoryTheory.CategoryStruct.comp (T.leftMesh X).f p) + r)

Radical-square perturbations of a split-epimorphic chosen-left-mesh cofactor remain left minimal.

theorem QuotientSubmoduleEquidistribution.Iyama.LeftLadder.isSpecial_splitCofactor_of_isSpecial_padded {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 Z U : C} (p : (T.leftMesh X).X₂ ⟶ Z) [CategoryTheory.IsSplitEpi p] (hpadded : IsSpecial T.radical (CategoryTheory.Limits.biprod.lift (CategoryTheory.CategoryStruct.comp (T.leftTermIso X).inv (CategoryTheory.CategoryStruct.comp (T.leftMesh X).f p)) 0)) : IsSpecial T.radical (CategoryTheory.CategoryStruct.comp (T.leftTermIso X).inv (CategoryTheory.CategoryStruct.comp (T.leftMesh X).f p))

If a target-padded arrow defined by a split left-mesh cofactor is special, its essential component is special.

theorem QuotientSubmoduleEquidistribution.Iyama.LeftLadder.exists_factor_through_chosen_leftMesh {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 Y : C} (a : X ⟶ Y) (ha : CategoricalRadical.IsRadicalMorphism a) : ∃ (k : (T.leftMesh X).X₂ ⟶ Y), CategoryTheory.CategoryStruct.comp (T.leftTermIso X).inv (CategoryTheory.CategoryStruct.comp (T.leftMesh X).f k) = a

Every radical arrow out of X factors through the first map of the chosen left mesh at X, after the recorded endpoint isomorphism.

theorem QuotientSubmoduleEquidistribution.Iyama.LeftLadder.exists_special_splitCofactor_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) {X Y : C} (a : X ⟶ Y) (ha : IsSpecial T.radical a) : ∃ (Z : C) (U : C) (p : (T.leftMesh X).X₂ ⟶ Z), CategoryTheory.IsSplitEpi p ∧ IsSpecial T.radical (CategoryTheory.CategoryStruct.comp (T.leftTermIso X).inv (CategoryTheory.CategoryStruct.comp (T.leftMesh X).f p)) ∧ Nonempty (CategoryTheory.Arrow.mk a ≅ CategoryTheory.Arrow.mk (CategoryTheory.Limits.biprod.lift (CategoryTheory.CategoryStruct.comp (T.leftTermIso X).inv (CategoryTheory.CategoryStruct.comp (T.leftMesh X).f p)) 0))

Iyama's special-arrow target normalization: every special arrow is isomorphic to a target-zero-padded split cofactor of the chosen left mesh, and its essential component remains special.

noncomputable def QuotientSubmoduleEquidistribution.Iyama.LeftLadder.chooseSpecialConormalization {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 Y : C} (a : X ⟶ Y) (ha : IsSpecial T.radical a) : SpecialConormalization T a

Choose the target conormalization of an arbitrary special arrow.