Special morphisms in Iyama tau-categories

Iyama calls a radical morphism special when every perturbation by the square of the categorical radical is isomorphic to it. This file gives that invariant arrow-category definition and proves the basic seed result used in the right-ladder construction: the first map of every tau-approximation is special. In particular, every left mesh first map is special.

The nilpotence field of NilpotentRadicalData is not used here; the structure currently provides the project's chosen Hom-ideal realization of the categorical radical.

def QuotientSubmoduleEquidistribution.Iyama.IsSpecial {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (R : CategoricalRadical.NilpotentRadicalData C) {X Y : C} (a : X ⟶ Y) : Prop

A radical morphism is special when every perturbation by a radical-square morphism is isomorphic to it in the arrow category.

theorem QuotientSubmoduleEquidistribution.Iyama.IsSpecial.of_iso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (R : CategoricalRadical.NilpotentRadicalData C) {A B : CategoryTheory.Arrow C} (ha : IsSpecial R A.hom) (e : A ≅ B) : IsSpecial R B.hom

Specialness is invariant under isomorphism in the arrow category.

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

A special padded arrow absorbs a radical-square complementary component. This is the perturbation step in Iyama's special-arrow normal form; cancellation of the zero source summand is a separate theorem.

theorem QuotientSubmoduleEquidistribution.Iyama.IsSpecial.nonempty_iso_biprod_desc_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 : Z ⟶ Y} {q : U ⟶ Y} (ha : IsSpecial R a) (e : CategoryTheory.Arrow.mk a ≅ CategoryTheory.Arrow.mk (CategoryTheory.Limits.biprod.desc b q)) (hq : q ∈ (R.ideal.pow 2).hom U Y) : Nonempty (CategoryTheory.Arrow.mk a ≅ CategoryTheory.Arrow.mk (CategoryTheory.Limits.biprod.desc b 0))

Isomorphism-invariant form of complementary radical-square absorption.

theorem QuotientSubmoduleEquidistribution.Iyama.nonempty_arrow_iso_of_biprod_desc_zero_iso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {Z U Y Z' U' Y' : C} {b : Z ⟶ Y} {b' : Z' ⟶ Y'} (hb : IsRightMinimal b) (hb' : IsRightMinimal b') (e : CategoryTheory.Arrow.mk (CategoryTheory.Limits.biprod.desc b 0) ≅ CategoryTheory.Arrow.mk (CategoryTheory.Limits.biprod.desc b' 0)) : Nonempty (CategoryTheory.Arrow.mk b ≅ CategoryTheory.Arrow.mk b')

Zero-padded right-minimal arrows cancel their padded source summands. This is the categorical cancellation used in Iyama's special-arrow construction.

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

Specialness of a zero-padded arrow descends to its right-minimal essential component, provided all its radical-square perturbations remain right minimal.

theorem QuotientSubmoduleEquidistribution.Iyama.TauApproximation.exists_radical_factor_of_mem_square {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (R : CategoricalRadical.NilpotentRadicalData C) {S : CategoryTheory.ShortComplex C} (hS : TauApproximation S) {r : S.X₁ ⟶ S.X₂} (hr : r ∈ (R.ideal.pow 2).hom S.X₁ S.X₂) : ∃ b ∈ R.ideal.hom S.X₂ S.X₂, CategoryTheory.CategoryStruct.comp S.f b = r

Every radical-square perturbation of the first map of a tau-approximation factors through that first map with a radical endomorphism of the middle term.

theorem QuotientSubmoduleEquidistribution.Iyama.TauApproximation.exists_radical_factor_into_of_mem_square {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (R : CategoricalRadical.NilpotentRadicalData C) {S : CategoryTheory.ShortComplex C} (hS : TauApproximation S) {W : C} {r : W ⟶ S.X₃} (hr : r ∈ (R.ideal.pow 2).hom W S.X₃) : ∃ b ∈ R.ideal.hom W S.X₂, CategoryTheory.CategoryStruct.comp b S.g = r

Dually, every radical-square arrow into the right endpoint of a tau-approximation factors through its second map with a radical morphism.

theorem QuotientSubmoduleEquidistribution.Iyama.TauApproximation.isSpecial_f {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (R : CategoricalRadical.NilpotentRadicalData C) {S : CategoryTheory.ShortComplex C} (hS : TauApproximation S) : IsSpecial R S.f

The first map of every tau-approximation is special.

theorem QuotientSubmoduleEquidistribution.Iyama.LeftTauSequence.isSpecial_f {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (R : CategoricalRadical.NilpotentRadicalData C) {S : CategoryTheory.ShortComplex C} (hS : LeftTauSequence S) : IsSpecial R S.f

The first map of every left tau-sequence is special. This is the abstract seed μ⁻ used in Iyama's right-ladder existence theorem.