Magnitude conjecture

MagnitudeConjecture.Algebra.RightModuleIntervalInequality

The magnitude surplus inequality from finite graded intervals #

source
theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.intervalInequalityFinite {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (m : ℕ) :
FiniteDimensional k (S.standardFormIntervalAlgebra m)
source
theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.intervalInequalityNoetherian {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (m : ℕ) :
IsNoetherianRing (S.standardFormIntervalAlgebra m)ᵐᵒᵖ
source
theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormInterval_surplus_nonnegative {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (m : ℕ) :
0 ≤ (S.standardFormIntervalSkeleton m).ambientARSurplus

Every finite interval has nonnegative surplus by directed deletion.

source
theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.ambientARSurplus_nonnegative_by_intervals {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) :
0 ≤ S.ambientARSurplus

The uniform interval estimate proves the ambient inequality, without a covering average.