Projective-free ladder support and the Nakayama boundary

This file proves the projective-free right support of every finite invertible ladder directly from its left-mesh identifications. It also identifies the vertical arrow immediately before a zero-target terminal rung with a genuine muPlus boundary map. These are the abstract support and truncation inputs in Iyama's Nakayama-pair extraction; no concrete algebra or classification is used.

theorem QuotientSubmoduleEquidistribution.Iyama.FiniteTauCategoryData.rightMesh_components_isZero_of_isZero {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) (Y : C) (hY : CategoryTheory.Limits.IsZero Y) : CategoryTheory.Limits.IsZero (T.rightMesh Y).X₁ ∧ CategoryTheory.Limits.IsZero (T.rightMesh Y).X₂ ∧ CategoryTheory.Limits.IsZero (T.rightMesh Y).X₃

A chosen right mesh ending at a zero object is componentwise zero.

theorem QuotientSubmoduleEquidistribution.Iyama.FiniteTauCategoryData.leftMesh_components_isZero_of_isZero {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 : C) (hX : CategoryTheory.Limits.IsZero X) : CategoryTheory.Limits.IsZero (T.leftMesh X).X₁ ∧ CategoryTheory.Limits.IsZero (T.leftMesh X).X₂ ∧ CategoryTheory.Limits.IsZero (T.leftMesh X).X₃

A chosen left mesh starting at a zero object is componentwise zero.

def QuotientSubmoduleEquidistribution.Iyama.FiniteTauCategoryData.secondMapIso {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 : T.Noninjective) : CategoryTheory.Arrow.mk (T.nuMinus ↑A) ≅ CategoryTheory.Arrow.mk (T.muPlus (T.tauMinus A))

Compatibility identifies the second map of a noninjective left mesh with the terminal map of the right mesh at its negative translate.

theorem QuotientSubmoduleEquidistribution.Iyama.FiniteTauCategoryData.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 : FiniteTauCategoryData C Ind) {p q : Ind} (f : T.obj p ⟶ T.obj q) [CategoryTheory.IsSplitMono f] : CategoryTheory.IsIso f

A split monomorphism between two chosen indecomposables is an isomorphism.

theorem QuotientSubmoduleEquidistribution.Iyama.FiniteTauCategoryData.exists_isSplitMono_component_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) (p : Ind) (n : ℕ) (F : Fin n → C) (j : T.obj p ⟶ ⨁ F) [CategoryTheory.IsSplitMono j] : ∃ (i : Fin n), CategoryTheory.IsSplitMono (CategoryTheory.CategoryStruct.comp j (CategoryTheory.Limits.biproduct.π F i))

A split embedding of a chosen indecomposable into a finite biproduct has a split-monic coordinate. This is the local-ring form of finite Krull--Schmidt support detection, and does not require the target factors to be indecomposable.

theorem QuotientSubmoduleEquidistribution.Iyama.FiniteTauCategoryData.exists_label_eq_of_isSplitMono_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) (p : Ind) (n : ℕ) (label : Fin n → Ind) (j : T.obj p ⟶ ⨁ fun (i : Fin n) => T.obj (label i)) [CategoryTheory.IsSplitMono j] : ∃ (i : Fin n), label i = p

A split embedding of a chosen indecomposable into a displayed finite biproduct forces its label to occur among the displayed factors. This is the finite-skeleton support detector needed by the projective-free-prefix argument.

theorem QuotientSubmoduleEquidistribution.Iyama.FiniteTauCategoryData.SupportedOnNonprojectives.of_iso {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} (hX : T.SupportedOnNonprojectives X) (e : Y ≅ X) : T.SupportedOnNonprojectives Y

Support on nonprojective labels is invariant under object isomorphism.

theorem QuotientSubmoduleEquidistribution.Iyama.FiniteTauCategoryData.not_isProjective_of_isSplitMono_to_leftMesh_X₃ {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) (p : Ind) (X : C) (j : T.obj p ⟶ (T.leftMesh X).X₃) [CategoryTheory.IsSplitMono j] : ¬T.IsProjective p

No projective chosen indecomposable can split-embed into the third term of a chosen left mesh. After decomposing the mesh, a nonzero split component is either impossible (injective label, hence zero third term) or lands in the negative translate, which is nonprojective.

theorem QuotientSubmoduleEquidistribution.Iyama.FiniteTauCategoryData.supportedOnNonprojectives_leftMesh_X₃ {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 : C) : T.SupportedOnNonprojectives (T.leftMesh X).X₃

The third term of every chosen left mesh is supported entirely on nonprojective labels.

noncomputable def QuotientSubmoduleEquidistribution.Iyama.NakayamaLadder.biprodDescIsoRightOfIsZero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {Y X Z : C} (hY : CategoryTheory.Limits.IsZero Y) (f : Y ⟶ Z) (a : X ⟶ Z) : CategoryTheory.Arrow.mk (CategoryTheory.Limits.biprod.desc f a) ≅ CategoryTheory.Arrow.mk a

Removing a zero source summand from a binary-biproduct arrow.

theorem QuotientSubmoduleEquidistribution.Iyama.NakayamaLadder.hasNonprojectiveRightSupport {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} : HasNonprojectiveRightSupport T

Iyama 6.2.1's projective-free-prefix consequence, derived directly from the left-mesh identification in each invertible rung.

theorem QuotientSubmoduleEquidistribution.Iyama.NakayamaLadder.not_isZero_previousTarget_of_step {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} {XPrev YPrev XNext YNext : C} {aPrev : XPrev ⟶ YPrev} {aNext : XNext ⟶ YNext} (hstep : InvertibleLadderStep T aPrev aNext) (hXNext : ¬CategoryTheory.Limits.IsZero XNext) : ¬CategoryTheory.Limits.IsZero YPrev

In an invertible rung, a nonzero next source forces the previous right endpoint to be nonzero.

theorem QuotientSubmoduleEquidistribution.Iyama.NakayamaLadder.nonempty_predecessor_iso_nuMinus_of_step_to_zeroTarget {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} {XPrev YPrev YNext : C} {I : Ind} {aPrev : XPrev ⟶ YPrev} {aNext : T.obj I ⟶ YNext} (hstep : InvertibleLadderStep T aPrev aNext) (hYNext : CategoryTheory.Limits.IsZero YNext) : Nonempty (CategoryTheory.Arrow.mk aPrev ≅ CategoryTheory.Arrow.mk (T.nuMinus I))

If the next source is a chosen indecomposable and the next target is zero, the previous vertical arrow is the second map of that source's left mesh, up to arrow isomorphism.

theorem QuotientSubmoduleEquidistribution.Iyama.NakayamaLadder.not_isInjective_of_step_to_zeroTarget {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} {XPrev YPrev YNext : C} {I : Ind} {aPrev : XPrev ⟶ YPrev} {aNext : T.obj I ⟶ YNext} (hstep : InvertibleLadderStep T aPrev aNext) : ¬T.IsInjective I

The chosen indecomposable source of an invertible rung is noninjective. The proof uses both mesh identifications in the rung.

theorem QuotientSubmoduleEquidistribution.Iyama.NakayamaLadder.exists_nonprojective_muPlus_predecessor_of_step_to_zeroTarget {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} {XPrev YPrev YNext : C} {I : Ind} {aPrev : XPrev ⟶ YPrev} {aNext : T.obj I ⟶ YNext} (hstep : InvertibleLadderStep T aPrev aNext) (hYNext : CategoryTheory.Limits.IsZero YNext) : ∃ (B : Ind), ¬T.IsProjective B ∧ Nonempty (CategoryTheory.Arrow.mk aPrev ≅ CategoryTheory.Arrow.mk (T.muPlus B))

A terminal rung with chosen indecomposable source canonically exposes the nonprojective label at the preceding vertical arrow.