Reduced nodes of a flag decomposition

A base occurs in a flag convex hull precisely when it is a nonempty finite join of bases of generating points. In particular the reduced nodes are closed under joins. These are the order-theoretic facts used when removing inactive nodes in the reduced-decomposition lemma.

theorem EGZ.ConvexFlag.exists_mem_convexHull_base_sup' {F : ConvexFlag} {S : Set F.Point} (s : Finset F.Node) (hs : s.Nonempty) (hS : ∀ x ∈ s, ∃ q ∈ S, q.base = x) : ∃ q ∈ F.convexHull S, q.base = s.sup' hs id

Every nonempty finite join of generator bases occurs in the flag hull. The witnesses are combined with equal, strictly positive coefficients.

theorem EGZ.ConvexFlag.exists_mem_convexHull_base_iff {F : ConvexFlag} {S : Set F.Point} (x : F.Node) : (∃ q ∈ F.convexHull S, q.base = x) ↔ ∃ (s : Finset F.Node) (hs : s.Nonempty), (∀ y ∈ s, ∃ q ∈ S, q.base = y) ∧ s.sup' hs id = x

The bases occurring in a flag convex hull are exactly the nonempty finite joins of bases occurring in its generating set.

theorem EGZ.ConvexFlag.ProperPointSet.exists_mem_base_sup' {F : ConvexFlag} (Ω : F.ProperPointSet) (s : Finset F.Node) (hs : s.Nonempty) (hS : ∀ x ∈ s, ∃ q ∈ Ω.carrier, q.base = x) : ∃ q ∈ Ω.carrier, q.base = s.sup' hs id

Bases of proper points are closed under every nonempty finite join.

theorem EGZ.FlagDecomposition.localWeight_le_cumulativeWeight {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (x : Φ.flag.Node) (v : FpCoord p d) : Φ.localWeight x v ≤ Φ.cumulativeWeight x v

A local weight is bounded by the cumulative weight at its own node.

theorem EGZ.FlagDecomposition.localLift_le_hat {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (x : Φ.flag.Node) (z : IntCoord (Φ.flag.rank x)) : Φ.localLift x z ≤ Φ.hat x z

The local centered lift is bounded by the cumulative centered lift.

theorem EGZ.FlagDecomposition.mem_polytope_of_localLift_ne_zero {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (x : Φ.flag.Node) (z : IntCoord (Φ.flag.rank x)) (hz : Φ.localLift x z ≠ 0) : z.real ∈ (Φ.flag.polytope x).carrier

Every nonzero local lifted point belongs to its node polytope.

theorem EGZ.FlagDecomposition.isReducedElement_of_localLift_ne_zero {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (x : Φ.flag.Node) (z : IntCoord (Φ.flag.rank x)) (hz : Φ.localLift x z ≠ 0) : Φ.IsReducedElement x

A nonzero local lift supplies a generating point based at its node.

theorem EGZ.FlagDecomposition.isReducedElement_of_localWeight_ne_zero {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (hp : Odd p) (x : Φ.flag.Node) (v : FpCoord p d) (hv : Φ.localWeight x v ≠ 0) : Φ.IsReducedElement x

Over an odd modulus every nonzero local weight is detected by its centered lift, and therefore its node is reduced.

theorem EGZ.FlagDecomposition.localWeight_eq_zero_of_not_isReducedElement {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (hp : Odd p) {x : Φ.flag.Node} (hx : ¬Φ.IsReducedElement x) (v : FpCoord p d) : Φ.localWeight x v = 0

Deleting a non-reduced node deletes no local mass.

theorem EGZ.FlagDecomposition.isReducedElement_iff_sup'_omegaZero {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (x : Φ.flag.Node) : Φ.IsReducedElement x ↔ ∃ (s : Finset Φ.flag.Node) (hs : s.Nonempty), (∀ y ∈ s, ∃ q ∈ Φ.omegaZero, q.base = y) ∧ s.sup' hs id = x

Reduced nodes are exactly the nonempty finite joins of local generator bases, as in the paragraph preceding the reduced-decomposition lemma.

theorem EGZ.FlagDecomposition.isReducedElement_iff_sup'_localLift {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (x : Φ.flag.Node) : Φ.IsReducedElement x ↔ ∃ (s : Finset Φ.flag.Node) (hs : s.Nonempty), (∀ y ∈ s, ∃ (z : IntCoord (Φ.flag.rank y)), Φ.localLift y z ≠ 0) ∧ s.sup' hs id = x

The description of reduced nodes directly in terms of nonzero local lifts, matching the set displayed in the paper.

theorem EGZ.FlagDecomposition.isReducedElement_sup' {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (s : Finset Φ.flag.Node) (hs : s.Nonempty) (hred : ∀ x ∈ s, Φ.IsReducedElement x) : Φ.IsReducedElement (s.sup' hs id)

The reduced nodes form a set closed under nonempty finite joins.

theorem EGZ.FlagDecomposition.isReducedElement_sup {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) {x y : Φ.flag.Node} (hx : Φ.IsReducedElement x) (hy : Φ.IsReducedElement y) : Φ.IsReducedElement (x ⊔ y)

In particular the join of two reduced nodes is reduced.

theorem EGZ.FlagDecomposition.isReducedElement_faceIndex {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (x : Φ.flag.Node) (Γ : (Φ.flag.polytope x).Face) : Φ.IsReducedElement (Φ.faceIndex x Γ)

The index of any visible face is reduced, because it is a nonempty finite join of bases of proper points on that face.