The canonical face flag of a rational polytope

Every nonempty exposed face is a node. All fibres use the ambient coordinates, transition maps are identities, and the lattice at a face is the affine integer span of the generators on that face. A physical point is represented at its least containing face.

The order-theoretic least-face formulation makes the construction independent of the analytic characterization by relative interior. That characterization is only needed when the final centerpoint is stated as lying in a relative interior.

structure EGZ.FaceFlagModel {d : ℕ} (P : RationalPolytope d) : Type 1

The face flag as a presentation of the points of a working polytope.

• flag : ConvexFlag

  Convex flag modeling the faces of the original polytope.

• proper : self.flag.ProperPointSet

  Proper point set of the face-flag model.

• properEquiv : { q : self.flag.Point // q ∈ self.proper } ≃ { x : RealCoord d // x ∈ P.carrier }

  Identify proper flag points with points of the original polytope.

def EGZ.FaceFlagModel.physical {d : ℕ} {P : RationalPolytope d} (A : FaceFlagModel P) (q : A.flag.Point) (hq : q ∈ A.proper) : RealCoord d

The physical point represented by a proper flag point.

Equations

• A.physical q hq = ↑(A.properEquiv ⟨q, hq⟩)

def EGZ.FaceFlagModel.lift {d : ℕ} {P : RationalPolytope d} (A : FaceFlagModel P) (q : RealCoord d) (hq : q ∈ P.carrier) : A.flag.Point

The proper flag point based at the least face containing a physical point.

Equations

• A.lift q hq = ↑(A.properEquiv.symm ⟨q, hq⟩)

theorem EGZ.FaceFlagModel.lift_proper {d : ℕ} {P : RationalPolytope d} (A : FaceFlagModel P) (q : RealCoord d) (hq : q ∈ P.carrier) : A.lift q hq ∈ A.proper

@[simp]

theorem EGZ.FaceFlagModel.physical_lift {d : ℕ} {P : RationalPolytope d} (A : FaceFlagModel P) (q : RealCoord d) (hq : q ∈ P.carrier) : A.physical (A.lift q hq) ⋯ = q

structure EGZ.FaceFlagCombinationLaws {d : ℕ} {P : RationalPolytope d} (A : FaceFlagModel P) : Prop

Compatibility of physical convex combinations with a face-flag model.

The second field records that an affine-integer-span certificate on the positive support makes the resulting flag point integral.

• combination_of_physical {n : ℕ} (points : Fin n → A.flag.Point) (hproper : ∀ (i : Fin n), points i ∈ A.proper) (weight : Fin n → ℝ) (result : A.flag.Point) (hresult : result ∈ A.proper) : (∀ (i : Fin n), 0 ≤ weight i) → ∑ i : Fin n, weight i = 1 → A.physical result hresult = ∑ i : Fin n, weight i • A.physical (points i) ⋯ → ConvexFlag.ConvexCombination points weight result
• integral_of_activeSpan {n : ℕ} (points : Fin n → A.flag.Point) (hproper : ∀ (i : Fin n), points i ∈ A.proper) (_hintegral : ∀ (i : Fin n), (points i).IsIntegral) (weight : Fin n → ℝ) (result : A.flag.Point) (hresult : result ∈ A.proper) : ConvexFlag.ConvexCombination points weight result → A.physical result hresult ∈ affineIntSpan ((fun (i : Fin n) => A.physical (points i) ⋯) '' {i : Fin n | 0 < weight i}) → result.IsIntegral

def EGZ.RationalPolytope.Face.restrict {d : ℕ} {P Q : RationalPolytope d} (F : P.Face) (hQP : Q.carrier ⊆ P.carrier) (hnonempty : (Q.carrier ∩ F.carrier).Nonempty) : Q.Face

Restrict a face of P to a subpolytope Q.

Equations

• F.restrict hQP hnonempty = { carrier := Q.carrier ∩ F.carrier, is_exposed := ⋯, nonempty := hnonempty }

@[simp]

theorem EGZ.RationalPolytope.Face.restrict_carrier {d : ℕ} {P Q : RationalPolytope d} (F : P.Face) (hQP : Q.carrier ⊆ P.carrier) (hnonempty : (Q.carrier ∩ F.carrier).Nonempty) : (F.restrict hQP hnonempty).carrier = Q.carrier ∩ F.carrier

noncomputable def EGZ.RationalPolytope.Face.asPolytope {d : ℕ} {P : RationalPolytope d} (F : P.Face) : RationalPolytope d

A face, regarded as a rational polytope in the ambient coordinates.

Equations

• F.asPolytope = EGZ.RationalPolytope.ofFiniteConvexHull ↑F.generatorFinset ⋯ ⋯ ⋯

@[simp]

theorem EGZ.RationalPolytope.Face.asPolytope_carrier {d : ℕ} {P : RationalPolytope d} (F : P.Face) : F.asPolytope.carrier = F.carrier

noncomputable def EGZ.RationalPolytope.Face.generatorLattice {d : ℕ} {P : RationalPolytope d} (F : P.Face) : AffineLattice d

The affine lattice generated by the vertices of a face.

Equations

• F.generatorLattice = EGZ.AffineLattice.span ↑F.generatorFinset ⋯ ⋯ ⋯

@[simp]

theorem EGZ.RationalPolytope.Face.generatorLattice_carrier {d : ℕ} {P : RationalPolytope d} (F : P.Face) : F.generatorLattice.carrier = affineIntSpan ↑F.generatorFinset

@[reducible, inline]

noncomputable abbrev EGZ.faceFlag {d : ℕ} (P : RationalPolytope d) : ConvexFlag

The canonical constant-rank flag indexed by the faces of P.

Equations

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

@[simp]

theorem EGZ.faceFlag_rank {d : ℕ} {P : RationalPolytope d} (F : P.Face) : (faceFlag P).rank F = d

theorem EGZ.faceFlag_polytope_carrier {d : ℕ} {P : RationalPolytope d} (F : P.Face) : ((faceFlag P).polytope F).carrier = F.carrier

@[simp]

theorem EGZ.faceFlag_lattice_carrier {d : ℕ} {P : RationalPolytope d} (F : P.Face) : ((faceFlag P).lattice F).carrier = affineIntSpan ↑F.generatorFinset

@[simp]

theorem EGZ.faceFlag_coord {d : ℕ} {P : RationalPolytope d} (q : (faceFlag P).Point) {F : P.Face} (h : q.base ≤ F) : q.coord h = q.val

def EGZ.faceProperCarrier {d : ℕ} (P : RationalPolytope d) : Set (faceFlag P).Point

Proper points are based at their order-theoretic least containing face.

Equations

• EGZ.faceProperCarrier P = {q : (EGZ.faceFlag P).Point | EGZ.RationalPolytope.Face.IsLeastFaceAt P q.val q.base}

@[reducible, inline]

noncomputable abbrev EGZ.faceProper {d : ℕ} (P : RationalPolytope d) : (faceFlag P).ProperPointSet

Least-face points form a proper-point set for the canonical face flag.

Equations

• EGZ.faceProper P = { carrier := EGZ.faceProperCarrier P, convex_closed := ⋯ }

def EGZ.facePhysical {d : ℕ} (P : RationalPolytope d) (q : { q : (faceFlag P).Point // q ∈ faceProper P }) : { x : RealCoord d // x ∈ P.carrier }

Send a proper face-flag point to its physical point in the polytope.

Equations

• EGZ.facePhysical P q = ⟨(↑q).val, ⋯⟩

noncomputable def EGZ.facePhysicalEquiv {d : ℕ} (P : RationalPolytope d) : { q : (faceFlag P).Point // q ∈ faceProper P } ≃ { x : RealCoord d // x ∈ P.carrier }

Identify proper face-flag points with points of the polytope.

Equations

• EGZ.facePhysicalEquiv P = Equiv.ofBijective (EGZ.facePhysical P) ⋯

@[reducible, inline]

noncomputable abbrev EGZ.canonicalFaceFlagModel {d : ℕ} (P : RationalPolytope d) : FaceFlagModel P

The canonical face-flag presentation of a rational polytope.

Equations

• EGZ.canonicalFaceFlagModel P = { flag := EGZ.faceFlag P, proper := EGZ.faceProper P, properEquiv := EGZ.facePhysicalEquiv P }

@[simp]

theorem EGZ.canonicalFaceFlagModel_physical {d : ℕ} {P : RationalPolytope d} (q : (faceFlag P).Point) (hq : q ∈ faceProper P) : (canonicalFaceFlagModel P).physical q hq = q.val

theorem EGZ.canonicalFaceFlagCombinationLaws {d : ℕ} (P : RationalPolytope d) : FaceFlagCombinationLaws (canonicalFaceFlagModel P)

The canonical face flag respects physical convex combinations and its face lattices absorb every active affine-integer-span certificate.