Transition maps in support-generated lattice coordinates

An affine map taking the source generators into the target generated lattice factors uniquely through their integer coordinate charts. Uniqueness then supplies the identity and composition laws for recharted flag transitions.

theorem EGZ.IntegerLatticeChart.existsUnique_lift {n k : ℕ} {T : Finset (IntCoord n)} (C : IntegerLatticeChart T) (g : IntCoord k →ᵃ[ℤ] IntCoord n) (hg : ∀ (q : IntCoord k), g q ∈ affineSpan ℤ ↑T) : ∃! B : IntCoord k →ᵃ[ℤ] IntCoord C.rank, C.map.comp B = g

An affine map into a chart's generated lattice has a unique affine lift to the chart coordinates.

noncomputable def EGZ.IntegerLatticeChart.lift {n k : ℕ} {T : Finset (IntCoord n)} (C : IntegerLatticeChart T) (g : IntCoord k →ᵃ[ℤ] IntCoord n) (hg : ∀ (q : IntCoord k), g q ∈ affineSpan ℤ ↑T) : IntCoord k →ᵃ[ℤ] IntCoord C.rank

The canonical lift is characterized by composition with the chart map.

Equations

• C.lift g hg = Classical.choose ⋯

@[simp]

theorem EGZ.IntegerLatticeChart.map_comp_lift {n k : ℕ} {T : Finset (IntCoord n)} (C : IntegerLatticeChart T) (g : IntCoord k →ᵃ[ℤ] IntCoord n) (hg : ∀ (q : IntCoord k), g q ∈ affineSpan ℤ ↑T) : C.map.comp (C.lift g hg) = g

theorem EGZ.IntegerLatticeChart.lift_unique {n k : ℕ} {T : Finset (IntCoord n)} (C : IntegerLatticeChart T) (g : IntCoord k →ᵃ[ℤ] IntCoord n) (hg : ∀ (q : IntCoord k), g q ∈ affineSpan ℤ ↑T) (B : IntCoord k →ᵃ[ℤ] IntCoord C.rank) (hB : C.map.comp B = g) : B = C.lift g hg

theorem EGZ.IntegerLatticeChart.map_chart_mem_affineSpan {m n : ℕ} {S : Finset (IntCoord m)} {T : Finset (IntCoord n)} (C : IntegerLatticeChart S) (A : IntCoord m →ᵃ[ℤ] IntCoord n) (hA : ∀ z ∈ S, A z ∈ affineSpan ℤ ↑T) (q : IntCoord C.rank) : A (C.map q) ∈ affineSpan ℤ ↑T

It suffices to check membership in the target generated lattice on the source generators.

noncomputable def EGZ.IntegerLatticeChart.transition {m n : ℕ} {S : Finset (IntCoord m)} {T : Finset (IntCoord n)} (C : IntegerLatticeChart S) (D : IntegerLatticeChart T) (A : IntCoord m →ᵃ[ℤ] IntCoord n) (hA : ∀ z ∈ S, A z ∈ affineSpan ℤ ↑T) : IntCoord C.rank →ᵃ[ℤ] IntCoord D.rank

Express an ambient affine transition in the support-generated coordinates.

Equations

• C.transition D A hA = D.lift (A.comp C.map) ⋯

@[simp]

theorem EGZ.IntegerLatticeChart.map_comp_transition {m n : ℕ} {S : Finset (IntCoord m)} {T : Finset (IntCoord n)} (C : IntegerLatticeChart S) (D : IntegerLatticeChart T) (A : IntCoord m →ᵃ[ℤ] IntCoord n) (hA : ∀ z ∈ S, A z ∈ affineSpan ℤ ↑T) : D.map.comp (C.transition D A hA) = A.comp C.map

@[simp]

theorem EGZ.IntegerLatticeChart.map_transition {m n : ℕ} {S : Finset (IntCoord m)} {T : Finset (IntCoord n)} (C : IntegerLatticeChart S) (D : IntegerLatticeChart T) (A : IntCoord m →ᵃ[ℤ] IntCoord n) (hA : ∀ z ∈ S, A z ∈ affineSpan ℤ ↑T) (q : IntCoord C.rank) : D.map ((C.transition D A hA) q) = A (C.map q)

theorem EGZ.IntegerLatticeChart.transition_unique {m n : ℕ} {S : Finset (IntCoord m)} {T : Finset (IntCoord n)} (C : IntegerLatticeChart S) (D : IntegerLatticeChart T) (A : IntCoord m →ᵃ[ℤ] IntCoord n) (hA : ∀ z ∈ S, A z ∈ affineSpan ℤ ↑T) (B : IntCoord C.rank →ᵃ[ℤ] IntCoord D.rank) (hB : D.map.comp B = A.comp C.map) : B = C.transition D A hA

@[simp]

theorem EGZ.IntegerLatticeChart.transition_id {m : ℕ} {S : Finset (IntCoord m)} (C : IntegerLatticeChart S) (h : ∀ z ∈ S, (AffineMap.id ℤ (IntCoord m)) z ∈ affineSpan ℤ ↑S) : C.transition C (AffineMap.id ℤ (IntCoord m)) h = AffineMap.id ℤ (IntCoord C.rank)

Recharting the identity transition gives the identity map.

theorem EGZ.IntegerLatticeChart.transition_comp {m n : ℕ} {S : Finset (IntCoord m)} {T : Finset (IntCoord n)} {r : ℕ} {U : Finset (IntCoord r)} (C : IntegerLatticeChart S) (D : IntegerLatticeChart T) (E : IntegerLatticeChart U) (A : IntCoord m →ᵃ[ℤ] IntCoord n) (B : IntCoord n →ᵃ[ℤ] IntCoord r) (hA : ∀ z ∈ S, A z ∈ affineSpan ℤ ↑T) (hB : ∀ z ∈ T, B z ∈ affineSpan ℤ ↑U) (hBA : ∀ z ∈ S, (B.comp A) z ∈ affineSpan ℤ ↑U) : C.transition E (B.comp A) hBA = (D.transition E B hB).comp (C.transition D A hA)

Uniqueness gives the cocycle law for consecutive recharted transitions.