Integral homogenization of rational polytope vertices

This module chooses one common denominator for the vertices of a rational polytope, embeds the resulting integral coordinates into one higher dimension with final coordinate 1, and forms the integer submodule generated by the vertices on each face. The final coordinate turns linear combinations in the homogenized module into affine combinations in the original polytope.

def EGZ.IntCoord.homogenize {d : ℕ} (z : IntCoord d) : IntCoord (d + 1)

Add a final affine coordinate equal to one.

Equations

• z.homogenize i = Fin.lastCases 1 z i

@[simp]

theorem EGZ.IntCoord.homogenize_last {d : ℕ} (z : IntCoord d) : z.homogenize (Fin.last d) = 1

@[simp]

theorem EGZ.IntCoord.homogenize_castSucc {d : ℕ} (z : IntCoord d) (i : Fin d) : z.homogenize i.castSucc = z i

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

A simultaneous choice of integral scaled coordinates for all vertices of P. Positivity of denominator is recorded so that scaling can be cancelled over the reals.

• denominator : ℕ

  Common positive denominator used to scale the rational vertices.

• denominator_pos : 0 < self.denominator
• scaledVertex : ↑P.vertexSet → IntCoord d

  Integer coordinates of the vertices after scaling by the common denominator.

• scaledVertex_real (q : ↑P.vertexSet) : (self.scaledVertex q).real = ↑self.denominator • ↑q

noncomputable def EGZ.RationalPolytope.vertexHomogenization {d : ℕ} (P : RationalPolytope d) : P.VertexHomogenization

The canonical common-denominator choice supplied by finiteness and rationality of the vertex set.

Equations

• P.vertexHomogenization = { denominator := Classical.choose ⋯, denominator_pos := ⋯, scaledVertex := fun (q : ↑P.vertexSet) => Classical.choose ⋯, scaledVertex_real := ⋯ }

def EGZ.RationalPolytope.VertexHomogenization.homogenizedVertex {d : ℕ} {P : RationalPolytope d} (H : P.VertexHomogenization) (q : ↑P.vertexSet) : IntCoord (d + 1)

Homogenized integral coordinate of a vertex.

Equations

• H.homogenizedVertex q = (H.scaledVertex q).homogenize

@[simp]

theorem EGZ.RationalPolytope.VertexHomogenization.homogenizedVertex_last {d : ℕ} {P : RationalPolytope d} (H : P.VertexHomogenization) (q : ↑P.vertexSet) : H.homogenizedVertex q (Fin.last d) = 1

@[simp]

theorem EGZ.RationalPolytope.VertexHomogenization.homogenizedVertex_castSucc {d : ℕ} {P : RationalPolytope d} (H : P.VertexHomogenization) (q : ↑P.vertexSet) (i : Fin d) : H.homogenizedVertex q i.castSucc = H.scaledVertex q i

def EGZ.RationalPolytope.VertexHomogenization.faceHomogenizedSet {d : ℕ} {P : RationalPolytope d} (H : P.VertexHomogenization) (F : P.Face) : Set (IntCoord (d + 1))

Homogenized vertices lying on a face.

Equations

• H.faceHomogenizedSet F = Set.range fun (q : { q : EGZ.RealCoord d // q ∈ P.vertexSet ∩ F.carrier }) => H.homogenizedVertex ⟨↑q, ⋯⟩

def EGZ.RationalPolytope.VertexHomogenization.faceSubmodule {d : ℕ} {P : RationalPolytope d} (H : P.VertexHomogenization) (F : P.Face) : Submodule ℤ (IntCoord (d + 1))

The integer submodule generated by homogenized vertices on a face.

Equations

• H.faceSubmodule F = Submodule.span ℤ (H.faceHomogenizedSet F)

theorem EGZ.RationalPolytope.VertexHomogenization.homogenizedVertex_mem_faceSubmodule {d : ℕ} {P : RationalPolytope d} (H : P.VertexHomogenization) (F : P.Face) (q : ↑P.vertexSet) (hqF : ↑q ∈ F.carrier) : H.homogenizedVertex q ∈ H.faceSubmodule F

A vertex lying on F is one of the generators of the face submodule.

theorem EGZ.RationalPolytope.VertexHomogenization.homogenize_mem_faceSubmodule_iff {d : ℕ} {P : RationalPolytope d} (H : P.VertexHomogenization) (F : P.Face) {q : RealCoord d} {z : IntCoord d} (hz : z.real = ↑H.denominator • q) : z.homogenize ∈ H.faceSubmodule F ↔ q ∈ affineIntSpan (P.vertexSet ∩ F.carrier)

Membership of an integral point with final coordinate 1 in the homogenized face submodule is equivalent to affine-integer-span membership of the corresponding real point.

theorem EGZ.RationalPolytope.VertexHomogenization.exists_uniform_face_saturation_bound {d : ℕ} {P : RationalPolytope d} (H : P.VertexHomogenization) : ∃ (B : ℕ), ∀ {p : ℕ}, Nat.Prime p → B < p → ∀ (F : P.Face) {x : IntCoord (d + 1)}, ↑p • x ∈ H.faceSubmodule F → x ∈ H.faceSubmodule F

A single threshold makes every face submodule p-saturated.