Real affine dimension of support-generated lattice coordinates #
Integer affine generation implies full real affine span. Consequently a support-generated chart has rank equal to the real affine dimension of its support polytope. A chart for support in a proper face of a minimal node has strictly smaller rank.
theorem
EGZ.real_mem_affineSpan_of_mem_int_affineSpan
{n : ℕ}
{S : Set (IntCoord n)}
{q : IntCoord n}
(hq : q ∈ affineSpan ℤ S)
:
Real affine hulls contain real realizations of integer affine spans.
The integer coordinate lattice spans the entire real affine space.
theorem
EGZ.FlagDecomposition.AffineIntSpans.affineSpan_real_eq_top
{n : ℕ}
{S : Finset (IntCoord n)}
(hS : AffineIntSpans S)
:
theorem
EGZ.FlagDecomposition.Rechart.polytope_affineSpan_eq_top
{p d : ℕ}
[NeZero p]
{f : FpCoord p d → ℕ}
(Φ : FlagDecomposition p d f)
(C : (x : Φ.flag.Node) → IntegerLatticeChart (Φ.liftedSupport x))
(x : Φ.flag.Node)
:
theorem
EGZ.FlagDecomposition.Rechart.rank_eq_polytope_dimension
{p d : ℕ}
[NeZero p]
{f : FpCoord p d → ℕ}
(Φ : FlagDecomposition p d f)
(C : (x : Φ.flag.Node) → IntegerLatticeChart (Φ.liftedSupport x))
(x : Φ.flag.Node)
:
The new lattice rank is exactly the real affine dimension of the old support polytope, including when the old coordinates were not minimal.
theorem
EGZ.FlagDecomposition.Rechart.rank_eq_of_isMinimal
{p d : ℕ}
[NeZero p]
{f : FpCoord p d → ℕ}
(Φ : FlagDecomposition p d f)
(C : (x : Φ.flag.Node) → IntegerLatticeChart (Φ.liftedSupport x))
(hΦ : Φ.IsMinimal)
(x : Φ.flag.Node)
: