Magnitude conjecture

MagnitudeConjecture.Algebra.RightModuleStandardInteriorArrowDimension

Interior supported irreducible dimensions count ordinary arrows #

source
@[instance_reducible]
def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.interiorArrowQuiver {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.interiorArrowFintype {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
      def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormSupported_interior_arrowDimension {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {m : ℕ} (a b : S.standardFormSupportedLabel m) (ht0 : 0 ≤ ↑b.snd) (htm : ↑b.snd ≤ ↑m - 2 * ↑S.standardFormIntervalControlHeight) :
      Module.finrank k (CategoricalIrreducible.Space k (S.standardFormSupportedFamily m a) (S.standardFormSupportedFamily m b)) = if ↑a.snd = ↑b.snd + 1 then FiniteTauMatrix.arrowMultiplicity S.finiteTauCategoryData.toFiniteRightTauCategoryData (MeshCategory.obj S.standardFormRightMeshData a.fst).as (MeshCategory.obj S.standardFormRightMeshData b.fst).as else 0

      At an interior target, the supported quotient retains exactly the ordinary arrows from source labels whose shift is one higher.

      Instances For
        source
        theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormSupported_interior_nextShift {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {m : ℕ} (b : S.standardFormSupportedLabel m) (ht0 : 0 ≤ ↑b.snd) (htm : ↑b.snd ≤ ↑m - 2 * ↑S.standardFormIntervalControlHeight) (i : Fin S.n) :
        ↑b.snd + 1 ∈ GradedInterval.allowedShifts m (S.standardFormSupportWindow i).lower (S.standardFormSupportWindow i).upper

        Every ordinary source label has its degree-one shift inside an interior interval, whether or not that particular label contributes an arrow.