Magnitude conjecture

QuotientSubmoduleEquidistribution.CategoryTheory.IyamaFiniteLadderComparison

Finite Krull--Schmidt specialization of ladder comparison #

This is the exact bridge from the general terminal cycle to the categorical finiteness recorded in FiniteTauCategoryData.

source
theorem QuotientSubmoduleEquidistribution.Iyama.TauSequenceComparison.initialPreviousCancellation_of_terminalEssentialIso_finite {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 : ℕ) (L : LeftLadder.FiniteSpecialLeftLadderFromZero T ((ReversedRightPrefix.ofInfiniteSpecialRightLadder R (n + 1)).U 0) (n + 1)) (hterminal : Nonempty (CategoryTheory.Arrow.mk (L.b (Fin.last (n + 1))) ≅ CategoryTheory.Arrow.mk a₀)) :
Nonempty (RightLadder.Comparison.PreviousCancellation R 0)

In a finite tau-category, a terminal essential-arrow identification canonically supplies the first cancellation datum for the genuine right ladder.

source
theorem QuotientSubmoduleEquidistribution.Iyama.TauSequenceComparison.nonempty_certificate_to_leftZeroBoundary_finite {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₀ U₀ : C} {a₀ : X₀ ⟶ Y₀} (R : RightLadder.InfiniteSpecialRightLadder T.toFiniteRightTauCategoryData a₀) (n : ℕ) (L : LeftLadder.FiniteSpecialLeftLadderFromZero T U₀ n) (E : BoundaryEmbedding (ReversedRightPrefix.ofInfiniteSpecialRightLadder R n) U₀) (hlast : Nonempty (CategoryTheory.Arrow.mk (L.b (Fin.last n)) ≅ CategoryTheory.Arrow.mk ((ReversedRightPrefix.ofInfiniteSpecialRightLadder R n).paddedArrow (Fin.last n)))) :
Nonempty (RightLadder.Comparison.Certificate R n (L.b 0))

Finite Krull--Schmidt specialization of the full comparison-certificate constructor.

source
theorem QuotientSubmoduleEquidistribution.Iyama.TauSequenceComparison.nonempty_certificate_to_leftZeroBoundary_of_terminalEssentialIso_finite {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₀ U₀ : C} {a₀ : X₀ ⟶ Y₀} (R : RightLadder.InfiniteSpecialRightLadder T.toFiniteRightTauCategoryData a₀) (n : ℕ) (L : LeftLadder.FiniteSpecialLeftLadderFromZero T U₀ n) (E : BoundaryEmbedding (ReversedRightPrefix.ofInfiniteSpecialRightLadder R n) U₀) (hterminal : Nonempty (CategoryTheory.Arrow.mk (L.b (Fin.last n)) ≅ CategoryTheory.Arrow.mk a₀)) :
Nonempty (RightLadder.Comparison.Certificate R n (L.b 0))

More directly usable endpoint form: identifying the terminal essential left arrow with the genuine initial right-ladder arrow automatically closes the reversed last diagonal via R.initialIso.