Magnitude conjecture

QuotientSubmoduleEquidistribution.CategoryTheory.IyamaLadderComparisonAssembly

Categorical assembly of Iyama's finite ladder comparison #

This file contains only the diagrammatic assembly which remains after Iyama, Tau-categories I, Lemma 6.3.1(2)(i) has supplied the comparison isomorphisms. It converts those isomorphisms into the literal finite invertible-ladder relation used for Nakayama pairs.

source
noncomputable def QuotientSubmoduleEquidistribution.Iyama.RightLadder.Comparison.paddedArrow {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₀} (L : InfiniteSpecialRightLadder T.toFiniteRightTauCategoryData a₀) (i : ℕ) :
L.Z i ⊞ L.U i ⟶ L.Y i

The actual right-ladder arrow before its zero source summand is cancelled.

Instances For
    source
    def QuotientSubmoduleEquidistribution.Iyama.RightLadder.Comparison.negIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (X : C) :
    X ≅ X

    Negation of the identity as an automorphism.

    Instances For
      source
      structure QuotientSubmoduleEquidistribution.Iyama.RightLadder.Comparison.PreviousCancellation {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₀} (L : InfiniteSpecialRightLadder T.toFiniteRightTauCategoryData a₀) (i : ℕ) :
      Type v

      Explicit cancellation data for the zero-padded previous vertical arrow. Keeping the component isomorphisms explicit avoids dependent Arrow projection noise in the matrix calculation.

      • sourceIso : L.Z i ⊞ L.U i ≅ L.Z i
      • targetIso : L.Y i ≅ L.Y i
      • inv_comm : CategoryTheory.CategoryStruct.comp self.sourceIso.inv (paddedArrow L i) = CategoryTheory.CategoryStruct.comp (L.b i) self.targetIso.inv
      Instances For
        source
        noncomputable def QuotientSubmoduleEquidistribution.Iyama.RightLadder.Comparison.PreviousCancellation.ofArrowIso {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₀} (L : InfiniteSpecialRightLadder T.toFiniteRightTauCategoryData a₀) (i : ℕ) (e : CategoryTheory.Arrow.mk (paddedArrow L i) ≅ CategoryTheory.Arrow.mk (L.b i)) :
        PreviousCancellation L i

        Extract explicit cancellation data from an arrow-category isomorphism.

        Instances For
          source
          def QuotientSubmoduleEquidistribution.Iyama.RightLadder.Comparison.squareF {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₀} (L : InfiniteSpecialRightLadder T.toFiniteRightTauCategoryData a₀) (i : ℕ) (p : PreviousCancellation L i) :
          L.Y i.succ ⟶ L.Y i

          Horizontal target map in the invariant square obtained after cancelling the previous zero-padded source summand.

          Instances For
            source
            noncomputable def QuotientSubmoduleEquidistribution.Iyama.RightLadder.Comparison.squareG {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₀} (L : InfiniteSpecialRightLadder T.toFiniteRightTauCategoryData a₀) (i : ℕ) (p : PreviousCancellation L i) :
            L.Z i.succ ⊞ L.U i.succ ⟶ L.Z i ⊞ L.U i

            Horizontal source map in the same invariant square. The signs are forced by the convention in NakayamaLadder.stepComplex.

            Instances For
              source
              theorem QuotientSubmoduleEquidistribution.Iyama.RightLadder.Comparison.square_comm {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₀} (L : InfiniteSpecialRightLadder T.toFiniteRightTauCategoryData a₀) (i : ℕ) (p : PreviousCancellation L i) :
              CategoryTheory.CategoryStruct.comp (paddedArrow L i.succ) (squareF L i p) = CategoryTheory.CategoryStruct.comp (squareG L i p) (paddedArrow L i)

              The transformed square commutes.

              source
              noncomputable def QuotientSubmoduleEquidistribution.Iyama.RightLadder.Comparison.squareComplex {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₀} (L : InfiniteSpecialRightLadder T.toFiniteRightTauCategoryData a₀) (i : ℕ) (p : PreviousCancellation L i) :
              CategoryTheory.ShortComplex C

              The common short complex used by one candidate invertible-ladder square.

              Instances For
                source
                noncomputable def QuotientSubmoduleEquidistribution.Iyama.RightLadder.Comparison.rightStepIsoSquareComplex {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₀} (L : InfiniteSpecialRightLadder T.toFiniteRightTauCategoryData a₀) (i : ℕ) (p : PreviousCancellation L i) :
                stepComplex (L.b i) (L.b i.succ) (L.f i) (L.g i) (L.h i) ⋯ ⋯ ≅ squareComplex L i p

                Cancelling the previous padded summand turns the explicit constructed right rung into the common Nakayama-ladder square.

                Instances For

                  Finite assembly after the comparison theorem #

                  source
                  structure QuotientSubmoduleEquidistribution.Iyama.RightLadder.Comparison.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₀} (L : InfiniteSpecialRightLadder T.toFiniteRightTauCategoryData a₀) (n : ℕ) {Xₙ Yₙ : C} (finish : Xₙ ⟶ Yₙ) :
                  Type v

                  The exact categorical output needed from Iyama's comparison argument.

                  For step i, previousCancellation i cancels the zero summand in the constructed right arrow a_i. The leftSquareIso field says that the same square is a chosen left mesh at the source of a_(i+1). In an application to a length-n left ladder, this field is obtained from its rung n-i-1, so the left ladder is read in reverse. Finally, terminalIso identifies the right terminal arrow a_n with the left zero boundary.

                  The nonzero endpoint part of Tau I, 6.3.1(2)(i) is proved separately in IyamaLadderComparisonEndpoint. Constructing the remaining reversed cross-mesh isomorphisms is kept explicit in this certificate.

                  Instances For
                    source
                    theorem QuotientSubmoduleEquidistribution.Iyama.RightLadder.Comparison.Certificate.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₀} (L : InfiniteSpecialRightLadder T.toFiniteRightTauCategoryData a₀) (n : ℕ) {Xₙ Yₙ : C} {finish : Xₙ ⟶ Yₙ} (K : Certificate L n finish) :
                    NakayamaLadder.InvertibleLadderOfDistance T n a₀ finish

                    A comparison certificate assembles the constructed right prefix into an invertible ladder of the same distance.

                    source
                    theorem QuotientSubmoduleEquidistribution.Iyama.RightLadder.Comparison.Certificate.invertibleLadderOfDistance_and_terminalIso {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₀} (L : InfiniteSpecialRightLadder T.toFiniteRightTauCategoryData a₀) (n : ℕ) {Xₙ Yₙ : C} {finish : Xₙ ⟶ Yₙ} (K : Certificate L n finish) :
                    NakayamaLadder.InvertibleLadderOfDistance T n a₀ finish ∧ Nonempty (CategoryTheory.Arrow.mk (paddedArrow L n) ≅ CategoryTheory.Arrow.mk finish)

                    The assembly retains the terminal arrow-category isomorphism explicitly, which is useful when the caller needs both conclusions of Tau I, 6.3.1.