Magnitude conjecture

MagnitudeConjecture.Algebra.RightModuleStandardIntervalControlHeight

One height controlling both support and Hom degrees #

source
noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormIntervalControlHeight {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) :
ℕ

A common height for the interval's support and incoming-Hom estimates.

Instances For
    source
    theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormIntervalControlHeight_pos {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) :
    1 ≤ S.standardFormIntervalControlHeight
    source
    theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormSupportWindow_upper_le_control {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (i : Fin S.n) :
    (S.standardFormSupportWindow i).upper ≤ S.standardFormIntervalControlHeight
    source
    theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormIntervalControlHeight_hom_bound {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (X Y : S.StandardFormMeshCategory) (d : ℤ) (hd : d < 0 ∨ ↑S.standardFormIntervalControlHeight < d) :
    S.standardFormIntegerHomGrading.component X Y d = ⊥

    Degrees outside the common height vanish in every mesh Hom space.