Coordinate models for the convex part of the paper

The paper works with rational affine spaces inside their real affine spans: convex coefficients are real, while lattice and transition data are rational. We make that distinction explicit. A rank-n fibre has real point space RealCoord n, integer lattice coordinates IntCoord n, and reduction modulo p in FpCoord p n.

Choosing affine lattice coordinates at each node loses no information and is particularly useful later: an integral-affine transition has compatible real, integer, and modulo-p realizations. This is the compatibility needed in the proof of Proposition 7.1.

@[reducible, inline]

abbrev EGZ.RealCoord (n : ℕ) : Type

Real points in a chosen rank-n affine-lattice coordinate system.

Equations

• EGZ.RealCoord n = (Fin n → ℝ)

@[reducible, inline]

abbrev EGZ.IntCoord (n : ℕ) : Type

Integer points in a chosen rank-n affine-lattice coordinate system.

Equations

• EGZ.IntCoord n = (Fin n → ℤ)

@[reducible, inline]

abbrev EGZ.FpCoord (p n : ℕ) : Type

Reduction of lattice coordinates modulo p.

Equations

• EGZ.FpCoord p n = (Fin n → ZMod p)

def EGZ.IntCoord.real {n : ℕ} (z : IntCoord n) : RealCoord n

Realification of an integer coordinate vector.

Equations

• z.real i = ↑(z i)

def EGZ.IntCoord.mod (p : ℕ) {n : ℕ} (z : IntCoord n) : FpCoord p n

Coordinatewise reduction modulo p.

Equations

• EGZ.IntCoord.mod p z i = ↑(z i)

@[simp]

theorem EGZ.IntCoord.real_apply {n : ℕ} (z : IntCoord n) (i : Fin n) : z.real i = ↑(z i)

@[simp]

theorem EGZ.IntCoord.mod_apply (p : ℕ) {n : ℕ} (z : IntCoord n) (i : Fin n) : mod p z i = ↑(z i)

theorem EGZ.IntCoord.isClosedEmbedding_real {n : ℕ} : Topology.IsClosedEmbedding real

Coordinatewise realification embeds the integer lattice as a closed discrete subset of finite-dimensional real coordinate space.

theorem EGZ.IntCoord.isClosed_range_real {n : ℕ} : IsClosed (Set.range real)

theorem EGZ.IntCoord.isDiscrete_range_real {n : ℕ} : IsDiscrete (Set.range real)

def EGZ.IsIntegral {n : ℕ} (q : RealCoord n) : Prop

A real coordinate vector represents a point of the distinguished affine integer lattice.

Equations

• EGZ.IsIntegral q = ∃ (z : EGZ.IntCoord n), z.real = q

def EGZ.IsRational {n : ℕ} (q : RealCoord n) : Prop

A real point has rational coordinate data.

Equations

• EGZ.IsRational q = ∀ (i : Fin n), ∃ (a : ℚ), ↑a = q i

structure EGZ.IntegralAffineMap (m n : ℕ) : Type

An integral affine map in chosen affine-lattice coordinates.

The integer realization makes preservation of the affine lattice explicit; the last two fields say that the real and modular realizations are obtained from it by scalar extension and reduction. In particular, the target modulo p is an affine space: no canonical origin for the original affine lattice is being assumed.

• real : RealCoord m →ᵃ[ℝ] RealCoord n

  Affine map on the real coordinate spaces.

• integer : IntCoord m → IntCoord n

  Map induced on integer coordinates.

• modp (p : ℕ) : FpCoord p m →ᵃ[ZMod p] FpCoord p n

  Affine map induced on coordinates modulo each natural modulus.

• real_integer (z : IntCoord m) : self.real z.real = (self.integer z).real
• mod_integer (p : ℕ) (z : IntCoord m) : (self.modp p) (IntCoord.mod p z) = IntCoord.mod p (self.integer z)

def EGZ.IntegralAffineMap.id (n : ℕ) : IntegralAffineMap n n

The identity integral-affine map.

Equations

• EGZ.IntegralAffineMap.id n = { real := AffineMap.id ℝ (EGZ.RealCoord n), integer := id, modp := fun (p : ℕ) => AffineMap.id (ZMod p) (EGZ.FpCoord p n), real_integer := ⋯, mod_integer := ⋯ }

def EGZ.IntegralAffineMap.comp {l m n : ℕ} (f : IntegralAffineMap m n) (g : IntegralAffineMap l m) : IntegralAffineMap l n

Composition of integral-affine maps.

Equations

• f.comp g = { real := f.real.comp g.real, integer := f.integer ∘ g.integer, modp := fun (p : ℕ) => (f.modp p).comp (g.modp p), real_integer := ⋯, mod_integer := ⋯ }

@[simp]

theorem EGZ.IntegralAffineMap.id_real (n : ℕ) : (id n).real = AffineMap.id ℝ (RealCoord n)

@[simp]

theorem EGZ.IntegralAffineMap.id_integer (n : ℕ) : (id n).integer = _root_.id

@[simp]

theorem EGZ.IntegralAffineMap.id_modp (p n : ℕ) : (id n).modp p = AffineMap.id (ZMod p) (FpCoord p n)

structure EGZ.RationalPolytope (n : ℕ) : Type

A nonempty rational polytope in chosen affine-lattice coordinates.

finite_integral is mathematically redundant (bounded rational polytopes have finitely many lattice points), but recording it here keeps the Helly-constant API independent of analytic boundedness infrastructure. It can later be discharged once, by the constructor for a finite rational vertex set.

• carrier : Set (RealCoord n)

  Underlying convex set of the rational polytope.

• generators : Finset (RealCoord n)

  Finite rational generating set of the polytope.

• generators_nonempty : self.generators.Nonempty
• generators_rational (q : RealCoord n) : q ∈ self.generators → IsRational q
• carrier_eq_convexHull : self.carrier = (convexHull ℝ) ↑self.generators
• finite_integral : {q : RealCoord n | q ∈ self.carrier ∧ IsIntegral q}.Finite

theorem EGZ.RationalPolytope.convexHull_supportingLevel_eq {n : ℕ} (generators : Finset (RealCoord n)) (functional : RealCoord n →ᵃ[ℝ] ℝ) (level : ℝ) (hle : ∀ q ∈ generators, functional q ≤ level) : {q : RealCoord n | q ∈ (convexHull ℝ) ↑generators ∧ functional q = level} = (convexHull ℝ) ↑({q ∈ generators | functional q = level})

Intersecting a finite convex hull with a supporting level set simply takes the convex hull of the generators on that level. This is the finite polytope fact that makes exposed faces combinatorially finite.

theorem EGZ.RationalPolytope.finite_integral_of_isCompact {n : ℕ} {S : Set (RealCoord n)} (hS : IsCompact S) : {q : RealCoord n | q ∈ S ∧ IsIntegral q}.Finite

A compact subset of finite-dimensional real coordinate space contains only finitely many points of the standard integer lattice.

theorem EGZ.RationalPolytope.finite_integral_convexHull {n : ℕ} (generators : Finset (RealCoord n)) : {q : RealCoord n | q ∈ (convexHull ℝ) ↑generators ∧ IsIntegral q}.Finite

The convex hull of a finite set contains only finitely many standard integer points.

def EGZ.RationalPolytope.ofFinsetConvexHull {n : ℕ} (generators : Finset (RealCoord n)) (hnonempty : generators.Nonempty) (hrational : ∀ q ∈ generators, IsRational q) : RationalPolytope n

A nonempty finite rational set, presented as a finset, determines a RationalPolytope with exactly its ordinary real convex hull as carrier.

Equations

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

@[simp]

theorem EGZ.RationalPolytope.ofFinsetConvexHull_carrier {n : ℕ} (generators : Finset (RealCoord n)) (hnonempty : generators.Nonempty) (hrational : ∀ q ∈ generators, IsRational q) : (ofFinsetConvexHull generators hnonempty hrational).carrier = (convexHull ℝ) ↑generators

noncomputable def EGZ.RationalPolytope.ofFiniteConvexHull {n : ℕ} (S : Set (RealCoord n)) (hfinite : S.Finite) (hnonempty : S.Nonempty) (hrational : ∀ q ∈ S, IsRational q) : RationalPolytope n

Set-based constructor used for the support hull in Theorem 1.12.

Equations

• EGZ.RationalPolytope.ofFiniteConvexHull S hfinite hnonempty hrational = EGZ.RationalPolytope.ofFinsetConvexHull hfinite.toFinset ⋯ ⋯

@[simp]

theorem EGZ.RationalPolytope.ofFiniteConvexHull_carrier {n : ℕ} (S : Set (RealCoord n)) (hfinite : S.Finite) (hnonempty : S.Nonempty) (hrational : ∀ q ∈ S, IsRational q) : (ofFiniteConvexHull S hfinite hnonempty hrational).carrier = (convexHull ℝ) S

theorem EGZ.RationalPolytope.ofFiniteConvexHull_subset {n : ℕ} (S : Set (RealCoord n)) (hfinite : S.Finite) (hnonempty : S.Nonempty) (hrational : ∀ q ∈ S, IsRational q) {C : Set (RealCoord n)} (hSC : S ⊆ C) (hC : Convex ℝ C) : (ofFiniteConvexHull S hfinite hnonempty hrational).carrier ⊆ C

The finite convex hull is contained in every convex set containing its generating set.

theorem EGZ.RationalPolytope.convex {n : ℕ} (P : RationalPolytope n) : Convex ℝ P.carrier

The carrier of a rational polytope is convex.

theorem EGZ.RationalPolytope.nonempty {n : ℕ} (P : RationalPolytope n) : P.carrier.Nonempty

A rational polytope is nonempty.

def EGZ.RationalPolytope.vertexSet {n : ℕ} (P : RationalPolytope n) : Set (RealCoord n)

The actual vertices are the extreme points of the carrier. They are kept separate from an arbitrary finite generating set, which may be redundant.

Equations

• P.vertexSet = Set.extremePoints ℝ P.carrier

theorem EGZ.RationalPolytope.vertexSet_subset_generators {n : ℕ} (P : RationalPolytope n) : P.vertexSet ⊆ ↑P.generators

theorem EGZ.RationalPolytope.finite_vertexSet {n : ℕ} (P : RationalPolytope n) : P.vertexSet.Finite

theorem EGZ.RationalPolytope.rational_of_mem_vertexSet {n : ℕ} (P : RationalPolytope n) {q : RealCoord n} (hq : q ∈ P.vertexSet) : IsRational q

structure EGZ.RationalPolytope.Face {n : ℕ} (P : RationalPolytope n) : Type

A (nonempty) face, represented as an exposed face. Every face of a polytope has such a presentation.

• carrier : Set (RealCoord n)

  Underlying set of points in the exposed face.

• is_exposed : ∃ (functional : RealCoord n →ᵃ[ℝ] ℝ) (level : ℝ), (∀ q ∈ P.carrier, functional q ≤ level) ∧ self.carrier = {q : RealCoord n | q ∈ P.carrier ∧ functional q = level}
• nonempty : self.carrier.Nonempty

theorem EGZ.RationalPolytope.Face.subset_polytope {n : ℕ} {P : RationalPolytope n} (F : P.Face) : F.carrier ⊆ P.carrier

theorem EGZ.RationalPolytope.Face.ext {n : ℕ} {P : RationalPolytope n} {F G : P.Face} (h : F.carrier = G.carrier) : F = G

theorem EGZ.RationalPolytope.Face.ext_iff {n : ℕ} {P : RationalPolytope n} {F G : P.Face} : F = G ↔ F.carrier = G.carrier

def EGZ.RationalPolytope.Face.relInterior {n : ℕ} {P : RationalPolytope n} (F : P.Face) : Set (RealCoord n)

Relative interior, called simply "interior of a face" in the paper.

Equations

• F.relInterior = intrinsicInterior ℝ F.carrier