Magnitude conjecture

MagnitudeConjecture.Algebra.StringButlerRingelCount

Numerical assembly of the Butler--Ringel correspondence #

The arrow-cokernel construction gives an injective map from displayed quiver arrows to one-middle meshes. Literal unary boundary classification gives an injective map in the reverse direction. Finite cardinality therefore makes the arrow-cokernel map surjective. Together with the two-middle bound, this proves E₁ = |Q₁| and vanishing of the Auslander--Reiten surplus.

source
theorem MagnitudeConjecture.BoundQuiver.StringPresentation.butlerRingelCountAlgebraFiniteDimensional {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : StringPresentation k A Q) :
FiniteDimensional k P.quotientCategoryAlgebra
source
theorem MagnitudeConjecture.BoundQuiver.StringPresentation.butlerRingelCountAlgebraOppositeIsNoetherian {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : StringPresentation k A Q) :
IsNoetherianRing P.quotientCategoryAlgebraᵐᵒᵖ
source
theorem MagnitudeConjecture.BoundQuiver.StringPresentation.butlerRingelCountFGHasFiniteBiproducts {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : StringPresentation k A Q) :
CategoryTheory.Limits.HasFiniteBiproducts (FGModuleCat P.quotientCategoryAlgebraᵐᵒᵖ)
source
theorem MagnitudeConjecture.BoundQuiver.StringPresentation.butlerRingelCountFGHasBinaryBiproducts {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : StringPresentation k A Q) :
CategoryTheory.Limits.HasBinaryBiproducts (FGModuleCat P.quotientCategoryAlgebraᵐᵒᵖ)
source
@[instance_reducible]
noncomputable def MagnitudeConjecture.BoundQuiver.StringPresentation.butlerRingelCountProjectiveDecidablePred {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : StringPresentation k A Q) (S : RightModule.FiniteIndecomposableSkeleton k P.quotientCategoryAlgebra) :
DecidablePred S.finiteTauCategoryData.IsProjective
Instances For
    source
    theorem MagnitudeConjecture.BoundQuiver.StringPresentation.displayedArrowOneMiddleMesh_surjective {k A Q : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : StringPresentation k A Q) (S : P.ArrowPolarization) (T : RightModule.FiniteIndecomposableSkeleton k P.quotientCategoryAlgebra) :
    Function.Surjective (P.displayedArrowOneMiddleMesh T)

    The Butler--Ringel arrow-cokernel map is surjective. Its proved injectivity and the injective reverse choice of a unary-boundary arrow force equality of the two finite cardinalities.

    source
    noncomputable def MagnitudeConjecture.BoundQuiver.StringPresentation.displayedArrowOneMiddleMeshEquiv {k A Q : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : StringPresentation k A Q) (S : P.ArrowPolarization) (T : RightModule.FiniteIndecomposableSkeleton k P.quotientCategoryAlgebra) :
    DisplayedArrow Q ≃ FiniteTauMatrix.OneMiddleMesh T.finiteTauCategoryData

    The displayed-arrow/one-middle-mesh Butler--Ringel equivalence.

    Instances For
      source
      theorem MagnitudeConjecture.BoundQuiver.StringPresentation.oneMiddleMeshCount_eq_natCard_displayedArrow {k A Q : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : StringPresentation k A Q) (S : P.ArrowPolarization) (T : RightModule.FiniteIndecomposableSkeleton k P.quotientCategoryAlgebra) :
      FiniteTauMatrix.oneMiddleMeshCount T.finiteTauCategoryData = Nat.card (DisplayedArrow Q)

      The converse Butler--Ringel classification gives the manuscript's count E₁ = |Q₁|.

      source
      theorem MagnitudeConjecture.BoundQuiver.StringPresentation.quotientCategoryAlgebra_surplus_eq_zero {k A Q : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : StringPresentation k A Q) (S : P.ArrowPolarization) (T : RightModule.FiniteIndecomposableSkeleton k P.quotientCategoryAlgebra) :
      ARCount.surplus (FiniteTauMatrix.arrowMultiplicity T.finiteTauCategoryData.toFiniteRightTauCategoryData) T.finiteTauCategoryData.IsProjective = 0

      The exact string-algebra numerical endpoint: literal boundary classification and the two-middle bound force the quotient-algebra Auslander--Reiten surplus to vanish.