Magnitude conjecture

MagnitudeConjecture.Algebra.RightModuleStandardFormUniversalNilpotence

Uniform path nilpotence on the standard-form universal mesh #

Path evaluation sends a string of arrows in a Hom ideal into the corresponding ideal power. Applied to the normalized universal-cover realization and the nilpotent categorical radical of a representation-finite module category, this gives one uniform length bound above which all universal mesh paths vanish.

source
@[instance_reducible]
def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversalNilpotenceQuiver {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) :
Quiver (Fin S.n)
Instances For
    source
    @[instance_reducible]
    noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversalNilpotenceArrowFintype {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x y : Fin S.n) :
    Fintype (x ⟶ y)
    Instances For
      source
      @[instance_reducible]
      noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversalNilpotenceStarFintype {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x₀ : Fin S.n) (W : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀) :
      Fintype (Quiver.Star W)
      Instances For
        source
        theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.exists_standardFormUniversal_pathHom_eq_zero {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x₀ : Fin S.n) :
        ∃ (N : ℕ), ∀ {Y Z : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀} (p : Quiver.Path Y Z), N ≤ p.length → (MeshCategory.quotientFunctor (MeshCategory.RightMeshData.UniversalCover.rightMeshData S.standardFormRightMeshData x₀)).map (LinearPathCategory.pathHom p) = 0

        Paths in the normalized universal-cover mesh category vanish above one uniform length bound.