Nakayama-pair extraction from Iyama's finite ladder comparison #
This file assembles the abstract categorical ingredients of the finite-ladder argument. A radical-power witness is restricted to an indecomposable summand, the reversed comparison identifies the terminal essential arrow, and the resulting positive-length certificate is truncated by one rung to produce a Nakayama pair.
theorem
QuotientSubmoduleEquidistribution.Iyama.FiniteTauCategoryData.exists_chosenSummand_radicalWitness
{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 W : C}
(n : ℕ)
(q : X ⟶ W)
(hq : q ∈ (T.radical.ideal.pow n).hom X W)
(hqne : q ≠ 0)
:
A nonzero radical-power morphism remains nonzero on some chosen indecomposable direct summand of its source.
theorem
QuotientSubmoduleEquidistribution.Iyama.TauSequenceComparison.ofInfiniteSpecialRightLadder_U_zero_eq
{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}
{a₀ : X₀ ⟶ Y₀}
(R : RightLadder.InfiniteSpecialRightLadder T.toFiniteRightTauCategoryData a₀)
(n : ℕ)
:
(ReversedRightPrefix.ofInfiniteSpecialRightLadder R n).U 0 = R.U n
The boundary object of the reversed prefix is the actual complementary object at the end of the finite right-ladder window.
theorem
QuotientSubmoduleEquidistribution.Iyama.TauSequenceComparison.terminalLeftDomain_not_isZero_of_radicalWitness
{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}
{a₀ : X₀ ⟶ Y₀}
(R : RightLadder.InfiniteSpecialRightLadder T.toFiniteRightTauCategoryData a₀)
(n : ℕ)
{W : C}
(q : R.U n ⟶ W)
(hq : q ∈ (T.radical.ideal.pow n).hom (R.U n) W)
(hqne : q ≠ 0)
:
¬CategoryTheory.Limits.IsZero
((LeftLadder.chosenFiniteSpecialLeftLadderFromZero T ((ReversedRightPrefix.ofInfiniteSpecialRightLadder R n).U 0)
n).Y
(Fin.last n))
A radical-power witness on the actual terminal complementary object transports to the zero boundary of the reversed prefix and forces the chosen left ladder to have nonzero terminal domain.
theorem
QuotientSubmoduleEquidistribution.Iyama.TauSequenceComparison.terminalEssentialArrow_iso_muMinus_of_boundaryEmbedding
{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)
(R : RightLadder.InfiniteSpecialRightLadder T.toFiniteRightTauCategoryData (T.muMinus A))
(n : ℕ)
(U₀ : C)
(E : BoundaryEmbedding (ReversedRightPrefix.ofInfiniteSpecialRightLadder R n) U₀)
(hY : ¬CategoryTheory.Limits.IsZero ((LeftLadder.chosenFiniteSpecialLeftLadderFromZero T U₀ n).Y (Fin.last n)))
:
Nonempty
(CategoryTheory.Arrow.mk ((LeftLadder.chosenFiniteSpecialLeftLadderFromZero T U₀ n).b (Fin.last n)) ≅ CategoryTheory.Arrow.mk (T.muMinus A))
The terminal essential left arrow is isomorphic to the initial
muMinus arrow when its boundary is a split subobject of the reversed right
complement.
theorem
QuotientSubmoduleEquidistribution.Iyama.TauSequenceComparison.terminalEssentialArrow_iso_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)
(R : RightLadder.InfiniteSpecialRightLadder T.toFiniteRightTauCategoryData (T.muMinus A))
(n : ℕ)
(hY :
¬CategoryTheory.Limits.IsZero
((LeftLadder.chosenFiniteSpecialLeftLadderFromZero T ((ReversedRightPrefix.ofInfiniteSpecialRightLadder R n).U 0)
n).Y
(Fin.last n)))
:
Nonempty
(CategoryTheory.Arrow.mk
((LeftLadder.chosenFiniteSpecialLeftLadderFromZero T ((ReversedRightPrefix.ofInfiniteSpecialRightLadder R n).U 0)
n).b
(Fin.last n)) ≅ CategoryTheory.Arrow.mk (T.muMinus A))
Whole-boundary specialization of the terminal endpoint theorem.
theorem
QuotientSubmoduleEquidistribution.Iyama.TauSequenceComparison.radicalWitness_index_ne_zero
{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)
(R : RightLadder.InfiniteSpecialRightLadder T.toFiniteRightTauCategoryData (T.muMinus A))
(n : ℕ)
{W : C}
(q : R.U n ⟶ W)
(hq : q ∈ (T.radical.ideal.pow n).hom (R.U n) W)
(hqne : q ≠ 0)
(hTheta : ¬CategoryTheory.Limits.IsZero (T.thetaMinus A))
:
n ≠ 0
Under the nonzero-middle hypothesis of the extraction theorem, a radical witness cannot occur at index zero.
theorem
QuotientSubmoduleEquidistribution.Iyama.NakayamaExtraction.indecomposable_of_iso
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
{X Y : C}
(hY : CategoryTheory.Indecomposable Y)
(e : X ≅ Y)
:
CategoryTheory.Indecomposable X
Indecomposability transports backwards across an object isomorphism.
def
QuotientSubmoduleEquidistribution.Iyama.NakayamaExtraction.certificatePrefix
{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}
{a₀ : X₀ ⟶ Y₀}
(R : RightLadder.InfiniteSpecialRightLadder T.toFiniteRightTauCategoryData a₀)
{n : ℕ}
{X Y : C}
{finish : X ⟶ Y}
(K : RightLadder.Comparison.Certificate R (n + 1) finish)
:
A comparison certificate can be truncated just before its last rung.
Instances For
theorem
QuotientSubmoduleEquidistribution.Iyama.NakayamaExtraction.certificatePrefix_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}
{X₀ Y₀ : C}
{a₀ : X₀ ⟶ Y₀}
(R : RightLadder.InfiniteSpecialRightLadder T.toFiniteRightTauCategoryData a₀)
{n : ℕ}
{X Y : C}
{finish : X ⟶ Y}
(K : RightLadder.Comparison.Certificate R (n + 1) finish)
:
The prefix of a length-n+1 comparison ends at the arrow immediately
before its terminal rung.
theorem
QuotientSubmoduleEquidistribution.Iyama.NakayamaExtraction.certificateStep
{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}
{a₀ : X₀ ⟶ Y₀}
(R : RightLadder.InfiniteSpecialRightLadder T.toFiniteRightTauCategoryData a₀)
{n : ℕ}
{X Y : C}
{finish : X ⟶ Y}
(K : RightLadder.Comparison.Certificate R n finish)
(i : Fin n)
:
Each certificate entry is the invertible step between the corresponding two padded arrows.
theorem
QuotientSubmoduleEquidistribution.Iyama.NakayamaExtraction.invertibleLadderOfDistance_finish_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}
{n : ℕ}
{X₀ Y₀ X Y X' Y' : C}
{start : X₀ ⟶ Y₀}
{finish : X ⟶ Y}
{finish' : X' ⟶ Y'}
(h : NakayamaLadder.InvertibleLadderOfDistance T n start finish)
(e : CategoryTheory.Arrow.mk finish ≅ CategoryTheory.Arrow.mk finish')
:
NakayamaLadder.InvertibleLadderOfDistance T n start finish'
The terminal endpoint of a finite ladder can be replaced by an arrow-isomorphic morphism without changing its distance.
theorem
QuotientSubmoduleEquidistribution.Iyama.NakayamaExtraction.exists_nonprojective_muPlus_predecessor_of_step_to_zeroTarget_of_indec
{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 : NakayamaLadder.InvertibleLadderStep T aPrev aNext)
(hXNext : CategoryTheory.Indecomposable XNext)
(hYNext : CategoryTheory.Limits.IsZero YNext)
:
∃ (B : Ind), ¬T.IsProjective B ∧ Nonempty (CategoryTheory.Arrow.mk aPrev ≅ CategoryTheory.Arrow.mk (T.muPlus B))
The terminal-boundary argument only needs the next source to be abstractly indecomposable.
theorem
QuotientSubmoduleEquidistribution.Iyama.NakayamaExtraction.exists_nakayamaPairOfDistance_of_succ_certificate
{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}
{a₀ : X₀ ⟶ Y₀}
(R : RightLadder.InfiniteSpecialRightLadder T.toFiniteRightTauCategoryData a₀)
{n : ℕ}
{U Z : C}
{finish : U ⟶ Z}
(K : RightLadder.Comparison.Certificate R (n + 1) finish)
(hZ : CategoryTheory.Limits.IsZero Z)
(hterminalSource : CategoryTheory.Indecomposable (R.Z (n + 1) ⊞ R.U (n + 1)))
:
∃ (B : Ind), ¬T.IsProjective B ∧ NakayamaLadder.InvertibleLadderOfDistance T n a₀ (T.muPlus B)
Deleting the last rung of a positive-length certificate gives the
required muPlus-ending Nakayama ladder. A witness at index n+1
therefore produces a Nakayama pair of distance n.
theorem
QuotientSubmoduleEquidistribution.Iyama.NakayamaExtraction.exists_nakayamaPairOfDistance_of_succ_certificate_to_leftBoundary
{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}
{a₀ : X₀ ⟶ Y₀}
(R : RightLadder.InfiniteSpecialRightLadder T.toFiniteRightTauCategoryData a₀)
{n : ℕ}
{U₀ : C}
(L : LeftLadder.FiniteSpecialLeftLadderFromZero T U₀ (n + 1))
(hU₀ : CategoryTheory.Indecomposable U₀)
(K : RightLadder.Comparison.Certificate R (n + 1) (L.b 0))
:
∃ (B : Ind), ¬T.IsProjective B ∧ NakayamaLadder.InvertibleLadderOfDistance T n a₀ (T.muPlus B)
If the certificate ends at a chosen indecomposable zero boundary, its terminal source is automatically indecomposable.
theorem
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)
:
Iyama's finite ladder construction extracts a Nakayama partner from
every nonzero nonmonic muMinus boundary map.