Separated packing and equality for actual standard-form interval surpluses #
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.intervalPackingBaseFinite
{k A : Type u}
[Field k]
[IsAlgClosed k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
(S : FiniteIndecomposableSkeleton k A)
:
FiniteDimensional k (S.standardFormAlgebra ⋯)
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.intervalPackingAlgebraFinite
{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)
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.intervalPackingAlgebraNoetherian
{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)ᵐᵒᵖ
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormInterval_surplus_packing
{k A : Type u}
[Field k]
[IsAlgClosed k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
(S : FiniteIndecomposableSkeleton k A)
(r q : ℕ)
:
Separated copies of the actual small interval cannot have greater surplus than the ambient interval containing them.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormInterval_surplus_le_length_mul
{k A : Type u}
[Field k]
[IsAlgClosed k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
(S : FiniteIndecomposableSkeleton k A)
(r : ℕ)
:
(S.standardFormIntervalSkeleton r).ambientARSurplus ≤ (↑r + ↑S.standardFormIntervalControlHeight + 1) * S.ambientARSurplus
Packing and the uniform interval error bound give the manuscript's upper surplus bound.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormInterval_surplus_eq_zero_of_ambient_eq_zero
{k A : Type u}
[Field k]
[IsAlgClosed k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
(S : FiniteIndecomposableSkeleton k A)
(hz : S.ambientARSurplus = 0)
(r : ℕ)
:
(S.standardFormIntervalSkeleton r).ambientARSurplus = 0
At zero ambient surplus, every actual finite interval has zero surplus.