Decompositions on a prescribed support diagram

An exact nonempty cumulative support at every node permits packaging a decomposition on the given flag itself. Integer transitions preserving these supports imply face visibility, so visibility is not an extra input.

theorem EGZ.RationalPolytope.Face.exists_mem_of_eq_convexHull {n : ℕ} {P : RationalPolytope n} (Γ : P.Face) (S : Finset (RealCoord n)) (hP : P.carrier = (convexHull ℝ) ↑S) : ∃ q ∈ S, q ∈ Γ.carrier

Every nonempty face of a finite hull contains one of its generators, even when that finite hull differs from the polytope's stored presentation.

theorem EGZ.FlagDecompositionRaw.localLift_le_hat {p d : ℕ} [NeZero p] {F : ConvexFlag} (R : FpRepresentation p d F) (pieces : F.Node → FpCoord p d → ℕ) (x : F.Node) (q : IntCoord (F.rank x)) : localLift R pieces x q ≤ hat R pieces x q

A local lifted fibre contributes to its cumulative lifted fibre.

structure EGZ.FlagDecompositionRaw.SupportData {p d : ℕ} [NeZero p] {F : ConvexFlag} (R : FpRepresentation p d F) (pieces : F.Node → FpCoord p d → ℕ) : Type u_1

Exact support data on the nodes of a prescribed flag.

• support (x : F.Node) : Finset (IntCoord (F.rank x))

  The finite set of integral coordinates where the node's cumulative centered lift is nonzero.

• support_spec (x : F.Node) (q : IntCoord (F.rank x)) : q ∈ self.support x ↔ hat R pieces x q ≠ 0
• support_nonempty (x : F.Node) : (self.support x).Nonempty
• polytope_eq (x : F.Node) : (F.polytope x).carrier = (convexHull ℝ) (IntCoord.real '' ↑(self.support x))
• transition_support {x y : F.Node} (h : x ≤ y) (q : IntCoord (F.rank x)) : q ∈ self.support x → (F.transition h).integer q ∈ self.support y
• local_supported (x : F.Node) (v : FpCoord p d) : pieces x v ≠ 0 → v ∈ R.space x

theorem EGZ.FlagDecompositionRaw.SupportData.support_centered {p d : ℕ} [NeZero p] {F : ConvexFlag} {R : FpRepresentation p d F} {pieces : F.Node → FpCoord p d → ℕ} (D : SupportData R pieces) (x : F.Node) (q : IntCoord (F.rank x)) (hq : q ∈ D.support x) : IsCenteredLift p q

theorem EGZ.FlagDecompositionRaw.SupportData.mem_support_of_localLift_ne_zero {p d : ℕ} [NeZero p] {F : ConvexFlag} {R : FpRepresentation p d F} {pieces : F.Node → FpCoord p d → ℕ} (D : SupportData R pieces) (x : F.Node) (q : IntCoord (F.rank x)) (hq : localLift R pieces x q ≠ 0) : q ∈ D.support x

theorem EGZ.FlagDecompositionRaw.SupportData.mem_polytope_of_localLift_ne_zero {p d : ℕ} [NeZero p] {F : ConvexFlag} {R : FpRepresentation p d F} {pieces : F.Node → FpCoord p d → ℕ} (D : SupportData R pieces) (x : F.Node) (q : IntCoord (F.rank x)) (hq : localLift R pieces x q ≠ 0) : q.real ∈ (F.polytope x).carrier

theorem EGZ.FlagDecompositionRaw.SupportData.transition_centered_of_localLift_ne_zero {p d : ℕ} [NeZero p] {F : ConvexFlag} {R : FpRepresentation p d F} {pieces : F.Node → FpCoord p d → ℕ} (D : SupportData R pieces) {x y : F.Node} (h : x ≤ y) (q : IntCoord (F.rank x)) (hq : localLift R pieces x q ≠ 0) : IsCenteredLift p ((F.transition h).integer q)

theorem EGZ.FlagDecompositionRaw.SupportData.exists_localLift_of_hat_ne_zero {p d : ℕ} [NeZero p] {F : ConvexFlag} {R : FpRepresentation p d F} {pieces : F.Node → FpCoord p d → ℕ} (D : SupportData R pieces) (hp : Odd p) (x : F.Node) (q : IntCoord (F.rank x)) (hq : hat R pieces x q ≠ 0) : ∃ (y : F.Node) (h : y ≤ x) (z : IntCoord (F.rank y)), localLift R pieces y z ≠ 0 ∧ (F.transition h).integer z = q

A cumulative support atom has a local antecedent with exact integer transition coordinates.

theorem EGZ.FlagDecompositionRaw.SupportData.faces_visible {p d : ℕ} [NeZero p] {F : ConvexFlag} {R : FpRepresentation p d F} {pieces : F.Node → FpCoord p d → ℕ} (D : SupportData R pieces) (hp : Odd p) (x : F.Node) (Γ : (F.polytope x).Face) : VisibleFace R pieces x Γ

Support generation and transition compatibility imply that every face contains a proper point.

@[reducible, inline]

noncomputable abbrev EGZ.FlagDecompositionRaw.SupportData.decomposition {p d : ℕ} [NeZero p] {F : ConvexFlag} {R : FpRepresentation p d F} {pieces : F.Node → FpCoord p d → ℕ} (D : SupportData R pieces) (hp : Odd p) (f : FpCoord p d → ℕ) (hretained : ∀ (v : FpCoord p d), retainedWeight pieces v ≤ f v) : FlagDecomposition p d f

Package a decomposition while retaining the prescribed flag, its nodes, its representation, and all local weights definitionally.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem EGZ.FlagDecompositionRaw.SupportData.decomposition_retainedWeight {p d : ℕ} [NeZero p] {F : ConvexFlag} {R : FpRepresentation p d F} {pieces : F.Node → FpCoord p d → ℕ} (D : SupportData R pieces) (hp : Odd p) (f : FpCoord p d → ℕ) (hretained : ∀ (v : FpCoord p d), retainedWeight pieces v ≤ f v) : (D.decomposition hp f hretained).retainedWeight = retainedWeight pieces

@[simp]

theorem EGZ.FlagDecompositionRaw.SupportData.decomposition_cumulativeWeight {p d : ℕ} [NeZero p] {F : ConvexFlag} {R : FpRepresentation p d F} {pieces : F.Node → FpCoord p d → ℕ} (D : SupportData R pieces) (hp : Odd p) (f : FpCoord p d → ℕ) (hretained : ∀ (v : FpCoord p d), retainedWeight pieces v ≤ f v) (x : F.Node) : (D.decomposition hp f hretained).cumulativeWeight x = cumulativeWeight pieces x

@[simp]

theorem EGZ.FlagDecompositionRaw.SupportData.decomposition_hat {p d : ℕ} [NeZero p] {F : ConvexFlag} {R : FpRepresentation p d F} {pieces : F.Node → FpCoord p d → ℕ} (D : SupportData R pieces) (hp : Odd p) (f : FpCoord p d → ℕ) (hretained : ∀ (v : FpCoord p d), retainedWeight pieces v ≤ f v) (x : F.Node) : (D.decomposition hp f hretained).hat x = hat R pieces x

@[simp]

theorem EGZ.FlagDecompositionRaw.SupportData.decomposition_localLift {p d : ℕ} [NeZero p] {F : ConvexFlag} {R : FpRepresentation p d F} {pieces : F.Node → FpCoord p d → ℕ} (D : SupportData R pieces) (hp : Odd p) (f : FpCoord p d → ℕ) (hretained : ∀ (v : FpCoord p d), retainedWeight pieces v ≤ f v) (x : F.Node) : (D.decomposition hp f hretained).localLift x = localLift R pieces x