Magnitude conjecture

MagnitudeConjecture.CategoryTheory.FiniteTauIrreducible

Irreducible components of finite tau meshes #

The middle term of a chosen right tau mesh is decomposed into the selected indecomposable representatives when its arrow multiplicities are defined. This file proves that every resulting summand-to-endpoint component is an irreducible morphism. The argument is intrinsic to a finite tau-category: right almost-split factorization comes from the tau approximation, while minimality of the second mesh map follows from its minimal weak kernel.

source
noncomputable def MagnitudeConjecture.FiniteTauMatrix.rightMiddleDecompositionIso {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 : QuotientSubmoduleEquidistribution.Iyama.FiniteTauCategoryData C Ind) (Y : Ind) :
(T.rightMesh (T.obj Y)).X₂ ≅ ⨁ fun (i : Fin (rightMiddleArity T.toFiniteRightTauCategoryData Y)) => T.obj (rightMiddleLabel T.toFiniteRightTauCategoryData Y i)

A fixed representative of the chosen decomposition of a right-mesh middle term.

Instances For
    source
    noncomputable def MagnitudeConjecture.FiniteTauMatrix.rightMiddleInclusion {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 : QuotientSubmoduleEquidistribution.Iyama.FiniteTauCategoryData C Ind) (Y : Ind) (i : Fin (rightMiddleArity T.toFiniteRightTauCategoryData Y)) :
    T.obj (rightMiddleLabel T.toFiniteRightTauCategoryData Y i) ⟶ (T.rightMesh (T.obj Y)).X₂

    Inclusion of one chosen indecomposable occurrence into the right-mesh middle term.

    Instances For
      source
      noncomputable def MagnitudeConjecture.FiniteTauMatrix.rightMiddleProjection {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 : QuotientSubmoduleEquidistribution.Iyama.FiniteTauCategoryData C Ind) (Y : Ind) (i : Fin (rightMiddleArity T.toFiniteRightTauCategoryData Y)) :
      (T.rightMesh (T.obj Y)).X₂ ⟶ T.obj (rightMiddleLabel T.toFiniteRightTauCategoryData Y i)

      Projection from the right-mesh middle term onto one chosen occurrence.

      Instances For
        source
        noncomputable def MagnitudeConjecture.FiniteTauMatrix.rightMiddleComponent {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 : QuotientSubmoduleEquidistribution.Iyama.FiniteTauCategoryData C Ind) (Y : Ind) (i : Fin (rightMiddleArity T.toFiniteRightTauCategoryData Y)) :
        T.obj (rightMiddleLabel T.toFiniteRightTauCategoryData Y i) ⟶ T.obj Y

        The actual morphism from one displayed middle occurrence to the selected endpoint representative.

        Instances For
          source
          @[simp]
          theorem MagnitudeConjecture.FiniteTauMatrix.rightMiddleInclusion_projection {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 : QuotientSubmoduleEquidistribution.Iyama.FiniteTauCategoryData C Ind) (Y : Ind) (i : Fin (rightMiddleArity T.toFiniteRightTauCategoryData Y)) :
          CategoryTheory.CategoryStruct.comp (rightMiddleInclusion T Y i) (rightMiddleProjection T Y i) = CategoryTheory.CategoryStruct.id (T.obj (rightMiddleLabel T.toFiniteRightTauCategoryData Y i))
          source
          theorem MagnitudeConjecture.FiniteTauMatrix.rightMiddleComponent_isIrreducible {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 : QuotientSubmoduleEquidistribution.Iyama.FiniteTauCategoryData C Ind) (Y : Ind) (i : Fin (rightMiddleArity T.toFiniteRightTauCategoryData Y)) :
          QuotientSubmoduleEquidistribution.IsIrreducibleMorphism (rightMiddleComponent T Y i)

          Every occurrence counted by arrowMultiplicity is represented by an irreducible morphism between the corresponding selected indecomposables.

          source
          theorem MagnitudeConjecture.FiniteTauMatrix.rightMesh_f_isLeftMinimal {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 : QuotientSubmoduleEquidistribution.Iyama.FiniteTauCategoryData C Ind) (Y : T.Nonprojective) :
          QuotientSubmoduleEquidistribution.IsLeftMinimal (T.rightMesh (T.obj ↑Y)).f

          For a nonprojective endpoint, compatibility with the corresponding left mesh makes the first map of the right mesh left minimal as well.

          source
          noncomputable def MagnitudeConjecture.FiniteTauMatrix.rightMiddleSourceComponent {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 : QuotientSubmoduleEquidistribution.Iyama.FiniteTauCategoryData C Ind) (Y : T.Nonprojective) (i : Fin (rightMiddleArity T.toFiniteRightTauCategoryData ↑Y)) :
          T.obj (T.tauPlus Y) ⟶ T.obj (rightMiddleLabel T.toFiniteRightTauCategoryData (↑Y) i)

          The component of the first right-mesh map from its translated source to one occurrence of the chosen middle decomposition.

          Instances For
            source
            theorem MagnitudeConjecture.FiniteTauMatrix.rightMiddleSourceComponent_isIrreducible {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 : QuotientSubmoduleEquidistribution.Iyama.FiniteTauCategoryData C Ind) (Y : T.Nonprojective) (i : Fin (rightMiddleArity T.toFiniteRightTauCategoryData ↑Y)) :
            QuotientSubmoduleEquidistribution.IsIrreducibleMorphism (rightMiddleSourceComponent T Y i)

            At a nonprojective endpoint, the translated-source component to every chosen middle occurrence is irreducible.

            source
            theorem MagnitudeConjecture.FiniteTauMatrix.rightMiddleArity_pos_of_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 : QuotientSubmoduleEquidistribution.Iyama.FiniteTauCategoryData C Ind) (Y : T.Nonprojective) :
            0 < rightMiddleArity T.toFiniteRightTauCategoryData ↑Y

            A nonprojective right mesh has at least one occurrence in its chosen middle decomposition.