Affine lattices generated by rational points

A finite rational set has a common denominator. Consequently its affine integer span is contained in a rescaled copy of the standard integer lattice, so its intersection with a compact set is finite.

theorem EGZ.affineIntSpan_eq_affineSpan_int {d : ℕ} (S : Set (RealCoord d)) : affineIntSpan S = ↑(affineSpan ℤ S)

The explicit finite-combination definition of affineIntSpan agrees with Mathlib's affine span over ℤ. This characterization supplies the closure laws of the support-generated lattices used by the face flag.

theorem EGZ.affineIntSpan_mono {d : ℕ} {S T : Set (RealCoord d)} (hST : S ⊆ T) : affineIntSpan S ⊆ affineIntSpan T

Affine integer span is monotone.

theorem EGZ.affineIntSpan_idempotent {d : ℕ} (S : Set (RealCoord d)) : affineIntSpan (affineIntSpan S) = affineIntSpan S

Taking the affine integer span twice does not enlarge it.

theorem EGZ.subset_affineIntSpan {d : ℕ} (S : Set (RealCoord d)) : S ⊆ affineIntSpan S

Every generator belongs to its affine integer span.

theorem EGZ.isRational_of_mem_affineIntSpan {d : ℕ} {S : Set (RealCoord d)} (hS : ∀ q ∈ S, IsRational q) {q : RealCoord d} (hq : q ∈ affineIntSpan S) : IsRational q

Integer affine combinations of rational points are rational.

theorem EGZ.IsRational.exists_integral_nsmul {d : ℕ} {q : RealCoord d} (hq : IsRational q) : ∃ (D : ℕ), 0 < D ∧ IsIntegral (↑D • q)

A rational point becomes integral after multiplication by one positive integer.

theorem EGZ.IsIntegral.nat_smul {d : ℕ} {q : RealCoord d} (hq : IsIntegral q) (m : ℕ) : IsIntegral (↑m • q)

Integral points remain integral after multiplication by a natural number.

theorem EGZ.Set.Finite.exists_common_integral_nsmul {d : ℕ} {S : Set (RealCoord d)} (hS : S.Finite) (hSrational : ∀ q ∈ S, IsRational q) : ∃ (D : ℕ), 0 < D ∧ ∀ q ∈ S, IsIntegral (↑D • q)

A finite set of rational points admits one positive common denominator in every coordinate.

theorem EGZ.isIntegral_nsmul_of_mem_affineIntSpan {d D : ℕ} {S : Set (RealCoord d)} (hS : ∀ q ∈ S, IsIntegral (↑D • q)) {q : RealCoord d} (hq : q ∈ affineIntSpan S) : IsIntegral (↑D • q)

A common denominator for the generators is also a common denominator for every integer affine combination of them.

theorem EGZ.finite_inter_affineIntSpan_of_isCompact {d : ℕ} {S K : Set (RealCoord d)} (hSfinite : S.Finite) (hSrational : ∀ q ∈ S, IsRational q) (hK : IsCompact K) : (K ∩ affineIntSpan S).Finite

A compact set meets the affine integer span of a finite rational set in only finitely many points. No affine independence or full-dimensionality is required.

theorem EGZ.RationalPolytope.isCompact {d : ℕ} (P : RationalPolytope d) : IsCompact P.carrier

A finitely generated rational polytope is compact.

Abstract affine lattices

For convex flags we only need the carrier of an affine lattice, closure under integer affine combinations, and local finiteness. Packaging precisely those properties lets a flag use a different lattice in every fibre without first choosing bases which identify all of them with standard integer coordinates.

structure EGZ.AffineLattice (d : ℕ) : Type

A locally finite affine ℤ-lattice in real coordinate space.

The carrier is required to be nonempty and closed under finite integer affine combinations. finite_inter_compact is the operational discreteness property used to make the population of integral points in a bounded flag fibre finite.

• carrier : Set (RealCoord d)

  Underlying set of points in the affine lattice.

• nonempty : self.carrier.Nonempty
• affineIntSpan_closed : affineIntSpan self.carrier ⊆ self.carrier
• finite_inter_compact {K : Set (RealCoord d)} : IsCompact K → (K ∩ self.carrier).Finite

@[instance_reducible]

instance EGZ.AffineLattice.instMembershipRealCoord {d : ℕ} : Membership (RealCoord d) (AffineLattice d)

Equations

• EGZ.AffineLattice.instMembershipRealCoord = { mem := fun (L : EGZ.AffineLattice d) (q : EGZ.RealCoord d) => q ∈ L.carrier }

@[simp]

theorem EGZ.AffineLattice.mem_carrier {d : ℕ} (L : AffineLattice d) (q : RealCoord d) : q ∈ L.carrier ↔ q ∈ L

Membership in an affine lattice is membership in its carrier.

theorem EGZ.AffineLattice.finite_mem_of_isCompact {d : ℕ} (L : AffineLattice d) {K : Set (RealCoord d)} (hK : IsCompact K) : {q : RealCoord d | q ∈ K ∧ q ∈ L}.Finite

Only finitely many points of an affine lattice lie in a compact set.

def EGZ.AffineLattice.standard (d : ℕ) : AffineLattice d

The standard integer lattice in the chosen coordinates.

Equations

• EGZ.AffineLattice.standard d = { carrier := {q : EGZ.RealCoord d | EGZ.IsIntegral q}, nonempty := ⋯, affineIntSpan_closed := ⋯, finite_inter_compact := ⋯ }

noncomputable def EGZ.AffineLattice.span {d : ℕ} (S : Set (RealCoord d)) (hfinite : S.Finite) (hnonempty : S.Nonempty) (hrational : ∀ q ∈ S, IsRational q) : AffineLattice d

The affine lattice generated by a finite nonempty rational set.

Equations

• EGZ.AffineLattice.span S hfinite hnonempty hrational = { carrier := EGZ.affineIntSpan S, nonempty := ⋯, affineIntSpan_closed := ⋯, finite_inter_compact := ⋯ }