Coordinates for support-generated integer lattices

Every nonempty finite integer support admits affine integer coordinates in its own generated lattice. Finiteness of the collection of bounded supports then makes coordinate and prime-saturation bounds uniform in the support.

def EGZ.IntCoord.realLinearMap (n : ℕ) : IntCoord n →ₗ[ℤ] RealCoord n

Realification as an integer-linear map.

Equations

• EGZ.IntCoord.realLinearMap n = { toFun := EGZ.IntCoord.real, map_add' := ⋯, map_smul' := ⋯ }

structure EGZ.IntegerLatticeChart {n : ℕ} (S : Finset (IntCoord n)) : Type

Integer coordinates on precisely the affine lattice generated by S. The ambient dimension need not equal the rank of that lattice.

• rank : ℕ

  The number of integer coordinates needed for the affine lattice chart.

• rank_le : self.rank ≤ n
• map : IntCoord self.rank →ᵃ[ℤ] IntCoord n

  The injective integer affine parametrization of the support's affine span.

• injective : Function.Injective ⇑self.map
• range_eq : Set.range ⇑self.map = ↑(affineSpan ℤ ↑S)

theorem EGZ.exists_integerLatticeChart {n : ℕ} (S : Finset (IntCoord n)) (hS : S.Nonempty) : Nonempty (IntegerLatticeChart S)

A nonempty finite support has affine integer coordinates, including when its affine span has smaller dimension than its ambient space.

theorem EGZ.IntegerLatticeChart.range_real_eq {n : ℕ} {S : Finset (IntCoord n)} (C : IntegerLatticeChart S) : (Set.range fun (q : IntCoord C.rank) => (C.map q).real) = affineIntSpan (IntCoord.real '' ↑S)

The real images of chart coordinates are exactly the support-generated affine lattice used by the convex flag definitions.

theorem EGZ.IntegerLatticeChart.linear_range_eq {n : ℕ} {S : Finset (IntCoord n)} (C : IntegerLatticeChart S) : C.map.linear.range = vectorSpan ℤ ↑S

The linear part of a chart parametrizes the direction lattice.

theorem EGZ.IntegerLatticeChart.exists_map_eq {n : ℕ} {S : Finset (IntCoord n)} (C : IntegerLatticeChart S) {z : IntCoord n} (hz : z ∈ S) : ∃ (q : IntCoord C.rank), C.map q = z

Every generator has coordinates in its generated lattice.

theorem EGZ.IntegerLatticeChart.exists_support_bound {n : ℕ} {S : Finset (IntCoord n)} (C : IntegerLatticeChart S) : ∃ (B : ℕ), ∀ z ∈ S, ∃ (q : IntCoord C.rank), C.map q = z ∧ latticeSupNorm q ≤ B

The finitely many generators have a common coordinate bound in any chosen chart.

theorem EGZ.IntegerLatticeChart.exists_box_bound {n : ℕ} {S : Finset (IntCoord n)} (C : IntegerLatticeChart S) (K : ℕ) : ∃ (B : ℕ), ∀ (q : IntCoord C.rank), latticeSupNorm (C.map q) ≤ K → latticeSupNorm q ≤ B

All lattice points in an old coordinate box have bounded new coordinates. This controls an entire node polytope, not just its generators.

theorem EGZ.exists_bounded_integerLatticeChart (n K : ℕ) : ∃ (B : ℕ), ∀ (S : Finset (IntCoord n)), S.Nonempty → (∀ z ∈ S, latticeSupNorm z ≤ K) → ∃ (C : IntegerLatticeChart S), ∀ (q : IntCoord C.rank), latticeSupNorm (C.map q) ≤ K → latticeSupNorm q ≤ B

In a fixed ambient dimension there are only finitely many possible supports in a fixed box, so one chart bound works for all of them.

theorem EGZ.exists_uniform_integerLatticeChart_bound (d : ℕ) : ∃ (A : ℕ → ℕ), Monotone A ∧ (∀ (K : ℕ), K ≤ A K) ∧ ∀ (K n : ℕ), n ≤ d → ∀ (S : Finset (IntCoord n)), S.Nonempty → (∀ z ∈ S, latticeSupNorm z ≤ K) → ∃ (C : IntegerLatticeChart S), ∀ (q : IntCoord C.rank), latticeSupNorm (C.map q) ≤ K → latticeSupNorm q ≤ A K

A monotone coordinate bound depending only on the upper dimension and the old coordinate bound, as required by the minimal decomposition lemma.

theorem EGZ.exists_uniform_bounded_direction_saturation (d K : ℕ) : ∃ (B : ℕ), ∀ {p : ℕ}, Nat.Prime p → B < p → ∀ n ≤ d, ∀ (S : Finset (IntCoord n)), (∀ z ∈ S, latticeSupNorm z ≤ K) → ∀ {v : IntCoord n}, ↑p • v ∈ vectorSpan ℤ ↑S → v ∈ vectorSpan ℤ ↑S

One prime threshold excludes torsion in the quotients by all lattices generated by supports in a fixed box, simultaneously in every rank at most d. There is no dependence on the support or on the number of flag nodes.

theorem EGZ.exists_uniform_integerLatticeChart_mod_injective (d K : ℕ) : ∃ (B : ℕ), ∀ {p : ℕ}, Nat.Prime p → B < p → ∀ n ≤ d, ∀ (S : Finset (IntCoord n)), (∀ z ∈ S, latticeSupNorm z ≤ K) → ∀ (C : IntegerLatticeChart S) (q r : IntCoord C.rank), IntCoord.mod p (C.map q) = IntCoord.mod p (C.map r) → IntCoord.mod p q = IntCoord.mod p r

For sufficiently large primes, congruence of ambient coordinates reflects congruence in any chart of a bounded support-generated lattice. This is the injectivity assertion for the natural map of lattice quotients in the minimal decomposition lemma.