Bounding hollow rational polytopes

This module isolates the exact bridge from Proposition wl to boundedness of the vertex counts defining hollowPolytopeNumber. It also develops the Smith-normal-form saturation lemma needed to prove that bridge.

def EGZ.RationalPolytope.HasPrimeHollowReduction {d : ℕ} (P : RationalPolytope d) : Prop

The weakest consequence of Proposition wl needed for bounding one hollow polytope: its vertices have a p-hollow reduction for at least one prime.

Equations

• P.HasPrimeHollowReduction = ∃ (p : ℕ), Nat.Prime p ∧ EGZ.AdmitsPHollowLength p d P.vertexSet.ncard

def EGZ.HollowReductionBridge (d : ℕ) : Prop

Dimensionwise form of the reduction bridge. Proposition wl proves a stronger eventual-prime statement, while this existential form is all that the polynomial bound needs.

Equations

• EGZ.HollowReductionBridge d = ∀ (P : EGZ.RationalPolytope d), P.IsHollow → P.HasPrimeHollowReduction

theorem EGZ.bddAbove_hollowPolytopeVertexCount_of_reductionBridge {d : ℕ} (hd : 1 ≤ d) (hbridge : HollowReductionBridge d) : BddAbove {n : ℕ | AdmitsHollowPolytopeVertexCount d n}

Conditional global boundedness of hollow-polytope vertex counts. The bound is exactly the prime-independent polynomial bound.

theorem Module.Basis.SmithNormalForm.mem_of_smul_mem_of_isCoprime {M : Type u_1} [AddCommGroup M] {N : Submodule ℤ M} {ι : Type u_2} {r : ℕ} (snf : SmithNormalForm N ι r) (c : ℤ) (hc : c ≠ 0) (hcoprime : ∀ (i : Fin r), IsCoprime (snf.a i) c) {x : M} (hx : c • x ∈ N) : x ∈ N

If a scalar is nonzero and coprime to every diagonal coefficient in a Smith normal form for N, then membership in N can be cancelled across multiplication by that scalar. This is the algebraic core of the "all but finitely many primes are good" step in Proposition wl.

theorem Module.Basis.SmithNormalForm.coeff_ne_zero {M : Type u_1} [AddCommGroup M] {N : Submodule ℤ M} {ι : Type u_2} {r : ℕ} (snf : SmithNormalForm N ι r) (i : Fin r) : snf.a i ≠ 0

Every diagonal coefficient in a Smith normal form is nonzero.

theorem Submodule.exists_prime_saturation_bound {M : Type u_1} [AddCommGroup M] {ι : Type u_2} [Finite ι] (b : Module.Basis ι ℤ M) (N : Submodule ℤ M) : ∃ (B : ℕ), ∀ {p : ℕ}, Nat.Prime p → B < p → ∀ {x : M}, ↑p • x ∈ N → x ∈ N

A submodule of a finite free abelian group is saturated with respect to every sufficiently large prime. The bound is the maximum absolute value of the diagonal entries in a Smith normal form.

theorem Submodule.exists_uniform_prime_saturation_bound {α : Type u_1} {M : Type u_2} [AddCommGroup M] {ι : Type u_3} [Finite ι] (b : Module.Basis ι ℤ M) (s : Finset α) (L : α → Submodule ℤ M) : ∃ (B : ℕ), ∀ {p : ℕ}, Nat.Prime p → B < p → ∀ a ∈ s, ∀ {x : M}, ↑p • x ∈ L a → x ∈ L a

A single threshold works simultaneously for a finite indexed family of integer submodules. This is the facewise p-saturation package needed after assigning one homogenized lattice to every face of a polytope.

theorem Submodule.exists_finite_exceptional_primes {α : Type u_1} {M : Type u_2} [AddCommGroup M] {ι : Type u_3} [Finite ι] (b : Module.Basis ι ℤ M) (s : Finset α) (L : α → Submodule ℤ M) : ∃ (bad : Finset ℕ), ∀ {p : ℕ}, Nat.Prime p → p ∉ bad → ∀ a ∈ s, ∀ {x : M}, ↑p • x ∈ L a → x ∈ L a

Equivalent finite-bad-prime form of exists_uniform_prime_saturation_bound.