A reduced representative with the same cumulative weight

The face index of the whole polytope is the join of all proper bases below the node. Every nonzero local summand has such a base, so passing to this reduced node preserves the entire cumulative function.

theorem EGZ.FlagDecomposition.localWeight_base_le_faceIndex_top {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (hp : Odd p) {y x : Φ.flag.Node} (h : y ≤ x) (v : FpCoord p d) (hv : Φ.localWeight y v ≠ 0) : y ≤ Φ.faceIndex x ⊤

theorem EGZ.FlagDecomposition.cumulativeWeight_faceIndex_top {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (hp : Odd p) (x : Φ.flag.Node) : Φ.cumulativeWeight (Φ.faceIndex x ⊤) = Φ.cumulativeWeight x

theorem EGZ.FlagDecomposition.exists_reducedRepresentative {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (hp : Odd p) (x : Φ.flag.Node) : ∃ y ≤ x, Φ.IsReducedElement y ∧ Φ.cumulativeWeight y = Φ.cumulativeWeight x

Every node has a reduced node below it carrying the same cumulative function. In a minimal decomposition their finite-field spaces also agree.

theorem EGZ.FlagDecomposition.space_faceIndex_top {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (hp : Odd p) (hminimal : Φ.IsMinimal) (x : Φ.flag.Node) : Φ.representation.space (Φ.faceIndex x ⊤) = Φ.representation.space x

theorem EGZ.FlagDecomposition.isCompleteElement_faceIndex_top {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (hp : Odd p) (hminimal : Φ.IsMinimal) (x : Φ.flag.Node) {t : ℕ} {δ : ℝ} (hc : Φ.IsCompleteElement x t δ) : Φ.IsCompleteElement (Φ.faceIndex x ⊤) t δ

With minimal spaces, completeness passes to the reduced representative: its finer representation can only make the fibre condition weaker.