Finite tau-category data for Iyama's extraction theorem

This file records the finite Krull--Schmidt skeleton, chosen right and left tau-sequences, nilpotent radical, and mesh compatibility needed to state Iyama's Nakayama-pair extraction theorem. It then proves that the left-mesh form of that theorem formally implies the right-mesh form.

The relation NakayamaPair remains an external parameter here. Its genuine definition by finite invertible ladders belongs to the next layer.

structure QuotientSubmoduleEquidistribution.Iyama.FiniteRightTauCategoryData (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] : Type (max (max u v) w)

An idempotent-complete finite Krull--Schmidt skeleton equipped with chosen right tau-sequences.

The chosen categorical radical is globally aligned with CategoricalRadical.IsRadicalMorphism and nilpotent. Nilpotence is stronger than the separated-radical hypothesis in Iyama's general theorem, but is the finite input intended for the manuscript's acyclic word mesh category.

• obj : Ind → C

  Chosen representative of an indecomposable label.

• obj_indec (A : Ind) : CategoryTheory.Indecomposable (self.obj A)

  Every chosen representative is indecomposable.

• obj_end_local (A : Ind) : IsLocalRing (CategoryTheory.End (self.obj A))

  The chosen representatives have local endomorphism rings.

• obj_decomposition (X : C) : ∃ (n : ℕ) (label : Fin n → Ind), Nonempty (X ≅ ⨁ fun (i : Fin n) => self.obj (label i))

  Every object is a finite biproduct of chosen representatives.

• obj_complete (X : C) : CategoryTheory.Indecomposable X → ∃ (A : Ind), Nonempty (X ≅ self.obj A)

  The labels contain every indecomposable object up to isomorphism.

• obj_skeletal {A B : Ind} : Nonempty (self.obj A ≅ self.obj B) → A = B

  Distinct labels do not represent isomorphic objects.

• radical : CategoricalRadical.NilpotentRadicalData C

  A nilpotent Hom ideal realizing the categorical radical.

• rightMesh : C → CategoryTheory.ShortComplex C

  Chosen right mesh ending at every object.

• rightTermIso (X : C) : (self.rightMesh X).X₃ ≅ X

  The right endpoint really is the supplied object.

• rightTau (X : C) : RightTauSequence (self.rightMesh X)

  Every chosen right mesh is a right tau-sequence.

structure QuotientSubmoduleEquidistribution.Iyama.FiniteTauCategoryData (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] extends QuotientSubmoduleEquidistribution.Iyama.FiniteRightTauCategoryData C Ind : Type (max (max u v) w)

A finite right tau-category together with compatible chosen left tau-sequences and the two-sided Auslander--Reiten translation.

• obj : Ind → C
• obj_indec (A : Ind) : CategoryTheory.Indecomposable (self.obj A)
• obj_end_local (A : Ind) : IsLocalRing (CategoryTheory.End (self.obj A))
• obj_decomposition (X : C) : ∃ (n : ℕ) (label : Fin n → Ind), Nonempty (X ≅ ⨁ fun (i : Fin n) => self.obj (label i))
• obj_complete (X : C) : CategoryTheory.Indecomposable X → ∃ (A : Ind), Nonempty (X ≅ self.obj A)
• obj_skeletal {A B : Ind} : Nonempty (self.obj A ≅ self.obj B) → A = B
• radical : CategoricalRadical.NilpotentRadicalData C
• rightMesh : C → CategoryTheory.ShortComplex C
• rightTermIso (X : C) : (self.rightMesh X).X₃ ≅ X
• rightTau (X : C) : RightTauSequence (self.rightMesh X)
• leftMesh : C → CategoryTheory.ShortComplex C

  Chosen left mesh starting at every object.

• leftTermIso (A : C) : (self.leftMesh A).X₁ ≅ A

  The left endpoint really is the supplied object.

• leftTau (A : C) : LeftTauSequence (self.leftMesh A)

  Every chosen left mesh is a left tau-sequence.

• tauPlusEquiv : { X : Ind // ¬CategoryTheory.Limits.IsZero (self.rightMesh (self.obj X)).X₁ } ≃ { A : Ind // ¬CategoryTheory.Limits.IsZero (self.leftMesh (self.obj A)).X₃ }

  Positive and negative translation are mutually inverse between the nonprojective and noninjective indecomposable labels.

• rightLeftMeshIso (X : { X : Ind // ¬CategoryTheory.Limits.IsZero (self.rightMesh (self.obj X)).X₁ }) : self.rightMesh (self.obj ↑X) ≅ self.leftMesh (self.obj ↑(self.tauPlusEquiv X))

  Iyama's compatibility (X] ≅ [tauPlus X) between the chosen right and left meshes.

structure QuotientSubmoduleEquidistribution.Iyama.FiniteTauCategoryExtension {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 : FiniteRightTauCategoryData C Ind) : Type (max (max u v) w)

A two-sided finite tau-category structure extending fixed chosen right tau-category data. This is the source-faithful interface for results, such as Iyama, Tau-categories II, 1.4(2), which promote an ideal quotient with specified right meshes to a tau-category.

• data : FiniteTauCategoryData C Ind
• right_eq : self.data.toFiniteRightTauCategoryData = T

@[instance_reducible]

instance QuotientSubmoduleEquidistribution.Iyama.instCoeFiniteTauCategoryDataFiniteRightTauCategoryData {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] : Coe (FiniteTauCategoryData C Ind) (FiniteRightTauCategoryData C Ind)

theorem QuotientSubmoduleEquidistribution.Iyama.FiniteRightTauCategoryData.nonempty_rightMesh_iso_shortComplexBiproduct_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 : FiniteRightTauCategoryData C Ind) {J : Type x} [Fintype J] (F : J → C) (X : C) (e : X ≅ ⨁ F) : Nonempty (T.rightMesh X ≅ shortComplexBiproduct fun (j : J) => T.rightMesh (F j))

The chosen right mesh of an object is, up to isomorphism, the componentwise biproduct of the chosen right meshes in any displayed finite biproduct decomposition of that object.

theorem QuotientSubmoduleEquidistribution.Iyama.FiniteRightTauCategoryData.nonempty_rightMesh_biproduct_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 : FiniteRightTauCategoryData C Ind) {J : Type x} [Fintype J] (F : J → C) : Nonempty (T.rightMesh (⨁ F) ≅ shortComplexBiproduct fun (j : J) => T.rightMesh (F j))

The chosen right mesh commutes with every finite biproduct, up to a nonempty type of isomorphisms of short complexes.

theorem QuotientSubmoduleEquidistribution.Iyama.FiniteRightTauCategoryData.exists_rightMesh_decomposition {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 : FiniteRightTauCategoryData C Ind) (X : C) : ∃ (n : ℕ) (label : Fin n → Ind), Nonempty (T.rightMesh X ≅ shortComplexBiproduct fun (i : Fin n) => T.rightMesh (T.obj (label i)))

Every recorded indecomposable decomposition of an object induces the corresponding decomposition of its chosen right mesh.

theorem QuotientSubmoduleEquidistribution.Iyama.FiniteTauCategoryData.nonempty_rightMesh_iso_shortComplexBiproduct_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) {J : Type x} [Fintype J] (F : J → C) (X : C) (e : X ≅ ⨁ F) : Nonempty (T.rightMesh X ≅ shortComplexBiproduct fun (j : J) => T.rightMesh (F j))

The chosen right mesh of an object is, up to isomorphism, the componentwise biproduct of the chosen right meshes in any displayed finite biproduct decomposition of that object.

theorem QuotientSubmoduleEquidistribution.Iyama.FiniteTauCategoryData.nonempty_rightMesh_biproduct_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) {J : Type x} [Fintype J] (F : J → C) : Nonempty (T.rightMesh (⨁ F) ≅ shortComplexBiproduct fun (j : J) => T.rightMesh (F j))

The chosen right mesh commutes with every finite biproduct, up to a nonempty type of isomorphisms of short complexes.

theorem QuotientSubmoduleEquidistribution.Iyama.FiniteTauCategoryData.exists_rightMesh_decomposition {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) : ∃ (n : ℕ) (label : Fin n → Ind), Nonempty (T.rightMesh X ≅ shortComplexBiproduct fun (i : Fin n) => T.rightMesh (T.obj (label i)))

Every recorded indecomposable decomposition of an object induces the corresponding decomposition of its chosen right mesh.

theorem QuotientSubmoduleEquidistribution.Iyama.FiniteTauCategoryData.nonempty_leftMesh_iso_shortComplexBiproduct_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) {J : Type x} [Fintype J] (F : J → C) (X : C) (e : X ≅ ⨁ F) : Nonempty (T.leftMesh X ≅ shortComplexBiproduct fun (j : J) => T.leftMesh (F j))

The chosen left mesh of an object is, up to isomorphism, the componentwise biproduct of the chosen left meshes in any displayed finite biproduct decomposition of that object.

theorem QuotientSubmoduleEquidistribution.Iyama.FiniteTauCategoryData.nonempty_leftMesh_biproduct_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) {J : Type x} [Fintype J] (F : J → C) : Nonempty (T.leftMesh (⨁ F) ≅ shortComplexBiproduct fun (j : J) => T.leftMesh (F j))

The chosen left mesh commutes with every finite biproduct, up to a nonempty type of isomorphisms of short complexes.

theorem QuotientSubmoduleEquidistribution.Iyama.FiniteTauCategoryData.exists_leftMesh_decomposition {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) : ∃ (n : ℕ) (label : Fin n → Ind), Nonempty (T.leftMesh X ≅ shortComplexBiproduct fun (i : Fin n) => T.leftMesh (T.obj (label i)))

Every recorded indecomposable decomposition of an object induces the corresponding decomposition of its chosen left mesh.

@[reducible, inline]

abbrev QuotientSubmoduleEquidistribution.Iyama.FiniteTauCategoryData.IsProjective {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 : Ind) : Prop

Projective labels are exactly those whose right mesh has zero left term.

@[reducible, inline]

abbrev QuotientSubmoduleEquidistribution.Iyama.FiniteTauCategoryData.Nonprojective {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) : Type w

The finite type of nonprojective labels.

@[reducible, inline]

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

Injective labels are exactly those whose left mesh has zero right term.

@[reducible, inline]

abbrev QuotientSubmoduleEquidistribution.Iyama.FiniteTauCategoryData.Noninjective {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) : Type w

The finite type of noninjective labels.

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

An object is supported on nonprojectives when it has a finite biproduct decomposition using only nonprojective labels. The zero object is allowed through the empty decomposition.

@[reducible, inline]

abbrev QuotientSubmoduleEquidistribution.Iyama.FiniteTauCategoryData.tauPlus {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 : T.Nonprojective) : Ind

Positive translation on a nonprojective label.

@[reducible, inline]

abbrev QuotientSubmoduleEquidistribution.Iyama.FiniteTauCategoryData.tauMinus {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) : Ind

Negative translation on a noninjective label.

@[simp]

theorem QuotientSubmoduleEquidistribution.Iyama.FiniteTauCategoryData.tauMinus_tauPlus {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 : T.Nonprojective) : T.tauMinus (T.tauPlusEquiv X) = ↑X

Positive and negative translation cancel on nonprojective labels.

@[simp]

theorem QuotientSubmoduleEquidistribution.Iyama.FiniteTauCategoryData.tauPlus_tauMinus {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) : T.tauPlus (T.tauPlusEquiv.symm A) = ↑A

Negative and positive translation cancel on noninjective labels.

def QuotientSubmoduleEquidistribution.Iyama.FiniteTauCategoryData.tauPlusIso {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 : T.Nonprojective) : (T.rightMesh (T.obj ↑X)).X₁ ≅ T.obj (T.tauPlus X)

The left term of a nonprojective right mesh is the chosen representative of its positive translate. This identification is derived from mesh compatibility, rather than stored as a second potentially incoherent choice.

def QuotientSubmoduleEquidistribution.Iyama.FiniteTauCategoryData.leftRightMeshIso {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) : T.leftMesh (T.obj ↑A) ≅ T.rightMesh (T.obj (T.tauMinus A))

Compatibility read in the reverse direction: the left mesh at a noninjective label is the right mesh at its negative translate.

def QuotientSubmoduleEquidistribution.Iyama.FiniteTauCategoryData.tauMinusIso {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) : (T.leftMesh (T.obj ↑A)).X₃ ≅ T.obj (T.tauMinus A)

The right term of a noninjective left mesh is the chosen representative of its negative translate.

@[reducible, inline]

abbrev QuotientSubmoduleEquidistribution.Iyama.FiniteTauCategoryData.nuPlus {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 : Ind) : (T.rightMesh (T.obj X)).X₁ ⟶ (T.rightMesh (T.obj X)).X₂

First and second maps of the chosen right mesh.

@[reducible, inline]

abbrev QuotientSubmoduleEquidistribution.Iyama.FiniteTauCategoryData.muPlus {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 : Ind) : (T.rightMesh (T.obj X)).X₂ ⟶ (T.rightMesh (T.obj X)).X₃

@[reducible, inline]

abbrev QuotientSubmoduleEquidistribution.Iyama.FiniteTauCategoryData.muMinus {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) : (T.leftMesh (T.obj A)).X₁ ⟶ (T.leftMesh (T.obj A)).X₂

First and second maps of the chosen left mesh.

@[reducible, inline]

abbrev QuotientSubmoduleEquidistribution.Iyama.FiniteTauCategoryData.nuMinus {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) : (T.leftMesh (T.obj A)).X₂ ⟶ (T.leftMesh (T.obj A)).X₃

@[reducible, inline]

abbrev QuotientSubmoduleEquidistribution.Iyama.FiniteTauCategoryData.thetaPlus {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 : Ind) : C

Middle objects of the chosen right and left meshes.

@[reducible, inline]

abbrev QuotientSubmoduleEquidistribution.Iyama.FiniteTauCategoryData.thetaMinus {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) : C

theorem QuotientSubmoduleEquidistribution.Iyama.FiniteTauCategoryData.not_isZero_thetaPlus {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 : T.Nonprojective) : ¬CategoryTheory.Limits.IsZero (T.thetaPlus ↑X)

The middle term of the chosen right mesh at a nonprojective label is nonzero. This follows from minimality of the first mesh map.

def QuotientSubmoduleEquidistribution.Iyama.FiniteTauCategoryData.firstMapIso {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 : T.Nonprojective) : CategoryTheory.Arrow.mk (T.nuPlus ↑X) ≅ CategoryTheory.Arrow.mk (T.muMinus (T.tauPlus X))

Compatibility identifies the first maps of the right mesh at X and the left mesh at tauPlus X as objects of the arrow category.

def QuotientSubmoduleEquidistribution.Iyama.FiniteTauCategoryData.middleIso {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 : T.Nonprojective) : T.thetaPlus ↑X ≅ T.thetaMinus (T.tauPlus X)

Compatibility identifies the two middle terms.

theorem QuotientSubmoduleEquidistribution.Iyama.FiniteTauCategoryData.mono_nuPlus_iff_mono_muMinus {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 : T.Nonprojective) : CategoryTheory.Mono (T.nuPlus ↑X) ↔ CategoryTheory.Mono (T.muMinus (T.tauPlus X))

Monicity of the two compatible first mesh maps is equivalent.

theorem QuotientSubmoduleEquidistribution.Iyama.FiniteTauCategoryData.not_isZero_thetaMinus_of_not_isZero_thetaPlus {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 : T.Nonprojective) (hX : ¬CategoryTheory.Limits.IsZero (T.thetaPlus ↑X)) : ¬CategoryTheory.Limits.IsZero (T.thetaMinus (T.tauPlus X))

A nonzero right middle term remains nonzero after mesh compatibility.

theorem QuotientSubmoduleEquidistribution.Iyama.FiniteTauCategoryData.not_mono_muMinus_of_not_mono_nuPlus {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 : T.Nonprojective) (hX : ¬CategoryTheory.Mono (T.nuPlus ↑X)) : ¬CategoryTheory.Mono (T.muMinus (T.tauPlus X))

Nonmonicity of nuPlus X transports to muMinus (tauPlus X).

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

The exact theorem boundary supplied by Iyama's ladder argument.

No ladder theorem is assumed as a field of FiniteTauCategoryData; instead, this proposition can later be proved for the actual ladder-defined NakayamaPair relation.

theorem QuotientSubmoduleEquidistribution.Iyama.FiniteTauCategoryData.exists_nakayamaPair_of_not_mono_nuPlus {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) (NakayamaPair : Ind → Ind → Prop) (hExtract : T.MuMinusNakayamaExtraction NakayamaPair) (X : T.Nonprojective) (hMiddle : ¬CategoryTheory.Limits.IsZero (T.thetaPlus ↑X)) (hmono : ¬CategoryTheory.Mono (T.nuPlus ↑X)) : ∃ (B : Ind), ¬T.IsProjective B ∧ NakayamaPair (T.tauPlus X) B

The right-mesh formulation follows formally from the muMinus theorem and right/left mesh compatibility.