Supports in minimal lattice coordinates

The inverse coordinates of an integer lattice chart carry its generating support to a support that generates the full new coordinate lattice. The generation statement uses the finitely supported integer weights required by FlagDecomposition.IsMinimal.

theorem EGZ.exists_finsupp_affineCombination_of_mem_affineSpan {n : ℕ} {S : Finset (IntCoord n)} {z : IntCoord n} (hz : z ∈ affineSpan ℤ ↑S) : ∃ (c : IntCoord n →₀ ℤ), c.support ⊆ S ∧ ∑ q ∈ c.support, c q = 1 ∧ ∑ q ∈ c.support, c q • q = z

An integer point in an affine span admits finitely supported integer coefficients with sum one on the given generating support.

theorem EGZ.FlagDecomposition.affineIntSpans_iff_affineSpan_eq_top {n : ℕ} (S : Finset (IntCoord n)) : AffineIntSpans S ↔ affineSpan ℤ ↑S = ⊤

The finitely supported coefficient definition of minimality is equivalent to spanning the full integer affine space.

noncomputable def EGZ.IntegerLatticeChart.coordinates {n : ℕ} {S : Finset (IntCoord n)} (C : IntegerLatticeChart S) : IntCoord n → IntCoord C.rank

Inverse integer coordinates. Its values outside the chart range are irrelevant; the inverse laws below hold on the generated lattice.

Equations

• C.coordinates = Function.invFun ⇑C.map

@[simp]

theorem EGZ.IntegerLatticeChart.coordinates_map {n : ℕ} {S : Finset (IntCoord n)} (C : IntegerLatticeChart S) (q : IntCoord C.rank) : C.coordinates (C.map q) = q

theorem EGZ.IntegerLatticeChart.map_coordinates_of_mem_affineSpan {n : ℕ} {S : Finset (IntCoord n)} (C : IntegerLatticeChart S) {z : IntCoord n} (hz : z ∈ affineSpan ℤ ↑S) : C.map (C.coordinates z) = z

The inverse coordinates recover each point in the support-generated integer affine lattice.

theorem EGZ.IntegerLatticeChart.map_coordinates_of_mem {n : ℕ} {S : Finset (IntCoord n)} (C : IntegerLatticeChart S) {z : IntCoord n} (hz : z ∈ S) : C.map (C.coordinates z) = z

noncomputable def EGZ.IntegerLatticeChart.coordinateSupport {n : ℕ} {S : Finset (IntCoord n)} (C : IntegerLatticeChart S) : Finset (IntCoord C.rank)

The old generating support, expressed in the chart coordinates.

Equations

• C.coordinateSupport = Finset.image C.coordinates S

theorem EGZ.IntegerLatticeChart.coordinates_mem_coordinateSupport {n : ℕ} {S : Finset (IntCoord n)} (C : IntegerLatticeChart S) {z : IntCoord n} (hz : z ∈ S) : C.coordinates z ∈ C.coordinateSupport

@[simp]

theorem EGZ.IntegerLatticeChart.mem_coordinateSupport {n : ℕ} {S : Finset (IntCoord n)} (C : IntegerLatticeChart S) {q : IntCoord C.rank} : q ∈ C.coordinateSupport ↔ C.map q ∈ S

@[simp]

theorem EGZ.IntegerLatticeChart.image_coordinateSupport {n : ℕ} {S : Finset (IntCoord n)} (C : IntegerLatticeChart S) : Finset.image (⇑C.map) C.coordinateSupport = S

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

@[simp]

theorem EGZ.IntegerLatticeChart.card_coordinateSupport {n : ℕ} {S : Finset (IntCoord n)} (C : IntegerLatticeChart S) : C.coordinateSupport.card = S.card

theorem EGZ.IntegerLatticeChart.affineSpan_coordinateSupport {n : ℕ} {S : Finset (IntCoord n)} (C : IntegerLatticeChart S) : affineSpan ℤ ↑C.coordinateSupport = ⊤

The new support generates every integer coordinate point.

theorem EGZ.IntegerLatticeChart.coordinateSupport_affineIntSpans {n : ℕ} {S : Finset (IntCoord n)} (C : IntegerLatticeChart S) : FlagDecomposition.AffineIntSpans C.coordinateSupport

The transformed support satisfies exactly the lattice-generation field in the definition of a minimal flag decomposition.

theorem EGZ.IntegerLatticeChart.coordinateSupport_bound {n : ℕ} {S : Finset (IntCoord n)} (C : IntegerLatticeChart S) {K B : ℕ} (hS : ∀ z ∈ S, latticeSupNorm z ≤ K) (hC : ∀ (q : IntCoord C.rank), latticeSupNorm (C.map q) ≤ K → latticeSupNorm q ≤ B) (q : IntCoord C.rank) : q ∈ C.coordinateSupport → latticeSupNorm q ≤ B

An old support bound and a chart box bound give the new support bound.