Finite invertible ladders and Nakayama pairs

This file formalizes the diagrammatic definition in Iyama, Tau-categories II, Definition 2.1. A step from aPrev : XPrev ⟶ YPrev to aNext : XNext ⟶ YNext consists of maps

f : YNext ⟶ YPrev, g : XNext ⟶ XPrev

making the square commute, such that

XNext ⟶ YNext ⨁ XPrev ⟶ YPrev

with maps (-aNext, g) and (f, aPrev) is simultaneously the right tau-sequence ending at YPrev and the left tau-sequence starting at XNext.

The endpoints of a finite ladder are identified in the arrow category. This is the invariant form of Iyama's literal equalities a₀ = muMinus A and aₙ = muPlus B, and accommodates the chosen representatives in FiniteTauCategoryData.

noncomputable def QuotientSubmoduleEquidistribution.Iyama.NakayamaLadder.stepComplex {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] (aPrev aNext : CategoryTheory.Arrow C) (f : aNext.right ⟶ aPrev.right) (g : aNext.left ⟶ aPrev.left) (comm : CategoryTheory.CategoryStruct.comp aNext.hom f = CategoryTheory.CategoryStruct.comp g aPrev.hom) : CategoryTheory.ShortComplex C

The short complex in one square of Iyama's invertible-ladder diagram.

The sign convention is exactly the one in Tau-categories II, Definition 2.1: the first map has components (-aNext, g), and the second has components (f, aPrev).

def QuotientSubmoduleEquidistribution.Iyama.NakayamaLadder.InvertibleLadderStep {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) : Prop

One invertible ladder step in the chosen meshes of T.

The two explicit short-complex isomorphisms are the literal categorical rendering of Iyama's (YPrev] = [XNext) condition. The facts that the source complexes are a right and a left tau-sequence are supplied by T.rightTau and T.leftTau; they need not be duplicated in this predicate.

def QuotientSubmoduleEquidistribution.Iyama.NakayamaLadder.InvertibleLadderOfDistance {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 : ℕ) {X₀ Y₀ Xₙ Yₙ : C} (start : X₀ ⟶ Y₀) (finish : Xₙ ⟶ Yₙ) : Prop

An invertible ladder of a specified distance.

The family has n + 1 vertical arrows. For i : Fin n, castSucc i is the previous arrow and succ i is the next arrow. The first and last arrows are only required to be isomorphic to the supplied endpoints in Arrow C, which is invariant under choices of representatives.

def QuotientSubmoduleEquidistribution.Iyama.NakayamaLadder.InvertibleLadder {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₀ Xₙ Yₙ : C} (start : X₀ ⟶ Y₀) (finish : Xₙ ⟶ Yₙ) : Prop

Two arrows are connected by a finite invertible ladder.

def 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) : Prop

The exact projective-support consequence of Iyama's invertible-ladder theory: every right mesh used by a finite ladder ends at an object supported on nonprojective indecomposables.

For a family indexed by Fin (n + 1), step i : Fin n uses the right mesh ending at Y i.castSucc; the terminal object Y (Fin.last n) is deliberately absent. In Tau-categories I, 6.2.1 this is the implication from an invertible ladder to Y_i|ind⁺₁ C = 0 for i < n.

theorem QuotientSubmoduleEquidistribution.Iyama.NakayamaLadder.invertibleLadderOfDistance_zero_of_arrowIso {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₀ Xₙ Yₙ : C} {start : X₀ ⟶ Y₀} {finish : Xₙ ⟶ Yₙ} (e : CategoryTheory.Arrow.mk start ≅ CategoryTheory.Arrow.mk finish) : InvertibleLadderOfDistance T 0 start finish

Distance zero is precisely the endpoint-isomorphism case needed by the finite definition.

theorem QuotientSubmoduleEquidistribution.Iyama.NakayamaLadder.invertibleLadder_of_arrowIso {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₀ Xₙ Yₙ : C} {start : X₀ ⟶ Y₀} {finish : Xₙ ⟶ Yₙ} (e : CategoryTheory.Arrow.mk start ≅ CategoryTheory.Arrow.mk finish) : InvertibleLadder T start finish

Arrow-isomorphic endpoints are connected by an invertible ladder.

def QuotientSubmoduleEquidistribution.Iyama.FiniteTauCategoryData.NakayamaPairOfDistance {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 B : Ind) (n : ℕ) : Prop

Iyama's diagrammatic Nakayama-pair relation at a fixed distance.

def QuotientSubmoduleEquidistribution.Iyama.FiniteTauCategoryData.NakayamaPair {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 B : Ind) : Prop

A Nakayama pair is a pair of indecomposable labels whose boundary mesh maps are connected by a finite invertible ladder.

theorem QuotientSubmoduleEquidistribution.Iyama.FiniteTauCategoryData.nakayamaPair_iff_exists_distance {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 B : Ind) : T.NakayamaPair A B ↔ ∃ (n : ℕ), T.NakayamaPairOfDistance A B n

def QuotientSubmoduleEquidistribution.Iyama.FiniteTauCategoryData.HasMuMinusNakayamaExtraction {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) : Prop

The still-open extraction theorem, specialized to the genuine finite ladder relation. This is a proposition, not an assumed field.