The nonzero endpoint in Iyama's finite ladder comparison

This file proves the normalized endpoint step in Iyama, Tau-categories I, 6.3.1(2)(i), directly from the finite tau-category axioms. A split-dominant essential factor at a nonzero left-ladder domain is arrow-isomorphic to the initial muMinus map. The proof uses indecomposability, left-mesh uniqueness, weak-cokernel exactness, and radical perturbation; it requires neither a functor-category construction nor a concrete module classification.

theorem QuotientSubmoduleEquidistribution.Iyama.LeftLadder.Comparison.isIso_of_isSplitMono_to_indecomposable {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.IsIdempotentComplete C] {X Y : C} (hY : CategoryTheory.Indecomposable Y) (j : X ⟶ Y) [CategoryTheory.IsSplitMono j] (hX : ¬CategoryTheory.Limits.IsZero X) : CategoryTheory.IsIso j

A split subobject of an indecomposable object is the whole object as soon as its source is nonzero.

theorem QuotientSubmoduleEquidistribution.Iyama.LeftLadder.Comparison.exists_middle_iso_lifting_left_endpoint_iso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {S T : CategoryTheory.ShortComplex C} (hS : LeftTauSequence S) (hT : LeftTauSequence T) (e₁ : S.X₁ ≅ T.X₁) : ∃ (e₂ : S.X₂ ≅ T.X₂), CategoryTheory.CategoryStruct.comp e₁.hom T.f = CategoryTheory.CategoryStruct.comp S.f e₂.hom

The middle component of the uniqueness isomorphism between two left tau-sequences can be chosen above any prescribed left-endpoint isomorphism.

theorem QuotientSubmoduleEquidistribution.Iyama.LeftLadder.Comparison.isIso_of_isSplitEpi_of_isIso_comp {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : C} (p : X ⟶ Y) [CategoryTheory.IsSplitEpi p] (t : Y ⟶ Z) [CategoryTheory.IsIso (CategoryTheory.CategoryStruct.comp p t)] : CategoryTheory.IsIso p

A split epimorphism whose composite with a second map is invertible is itself invertible.

theorem QuotientSubmoduleEquidistribution.Iyama.LeftLadder.Comparison.nonempty_essentialArrow_iso_muMinus_of_leftDominance {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) (A : Ind) {Y Z : C} (p : (T.leftMesh Y).X₂ ⟶ Z) [CategoryTheory.IsSplitEpi p] (s : Y ⟶ (T.leftMesh (T.obj A)).X₁) [CategoryTheory.IsSplitMono s] (t : Z ⟶ (T.leftMesh (T.obj A)).X₂) (hY : ¬CategoryTheory.Limits.IsZero Y) (hdom : CategoryTheory.CategoryStruct.comp s (T.muMinus A) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (T.leftTermIso Y).inv (CategoryTheory.CategoryStruct.comp (T.leftMesh Y).f p)) t) : Nonempty (CategoryTheory.Arrow.mk (CategoryTheory.CategoryStruct.comp (T.leftTermIso Y).inv (CategoryTheory.CategoryStruct.comp (T.leftMesh Y).f p)) ≅ CategoryTheory.Arrow.mk (T.muMinus A))

Direct normalized form of the load-bearing endpoint step in Iyama 6.3.1(2)(i).

If a split-epi essential factor of the left mesh at a nonzero object is left-dominated by muMinus A, then it is already arrow-isomorphic to muMinus A. The proof avoids a functor-category detour: the split source map is invertible by indecomposability, and weak-cokernel exactness makes the target composite an isomorphism modulo the categorical radical.