Primitive lattice directions and rational coordinates

This module supplies the primitive-direction coordinates of Section 1.1 of paper/nivat.tex, used in Proposition 3.5 (prop:tangent-period) and the proof of Theorem 5.1. The integer gcd and a Bézout identity extend every primitive direction to a lattice basis.

The main results are exists_lattice_basis_for_nonzero, latticeEquivRatLinear_compatible, and transverse_coordinate_ne_zero. The rational extension permits convex windows to be transported through the same coordinate change as the lattice configurations.

theorem Nivat.lattice_addEquiv_coordinates (e : Lattice ≃+ Lattice) (z : Lattice) : e z = z.1 • e (1, 0) + z.2 • e (0, 1)

An additive lattice map is determined by its two basis vectors, giving the primitive-direction coordinate formula used in Section 1.1.

def Nivat.bezoutLatticeEquiv (x y a b : ℤ) (h : x * a + y * b = 1) : Lattice ≃+ Lattice

A Bézout identity constructs an integer lattice basis containing the primitive vector (x,y), as in Section 1.1.

Equations

• One or more equations did not get rendered due to their size.

theorem Nivat.exists_lattice_basis_for_nonzero (h : Lattice) (hh : h ≠ 0) : ∃ (q : ℕ), 0 < q ∧ ∃ (e : Lattice ≃+ Lattice), e (↑q, 0) = h

Every nonzero integer direction is a positive multiple of the first vector of a lattice basis. This is the primitive-direction normalization of Section 1.1, used in Proposition 3.5 and Theorem 5.1.

def Nivat.latticeRatCast (z : Lattice) : ℚ × ℚ

The coordinate embedding of the integer lattice into the rational plane, used to express convexity in the coordinate normalization of Theorem 5.1.

Equations

• Nivat.latticeRatCast z = (↑z.1, ↑z.2)

def Nivat.latticeEquivRatLinear (e : Lattice ≃+ Lattice) : ℚ × ℚ →ₗ[ℚ] ℚ × ℚ

The rational linear extension of a lattice equivalence, used to transport convex windows in the proof of Theorem 5.1.

Equations

• Nivat.latticeEquivRatLinear e = { toFun := fun (z : ℚ × ℚ) => (↑(e (1, 0)).1 * z.1 + ↑(e (0, 1)).1 * z.2, ↑(e (1, 0)).2 * z.1 + ↑(e (0, 1)).2 * z.2), map_add' := ⋯, map_smul' := ⋯ }

theorem Nivat.latticeEquivRatLinear_compatible (e : Lattice ≃+ Lattice) (z : Lattice) : latticeRatCast (e z) = (latticeEquivRatLinear e) (latticeRatCast z)

The rational linear extension agrees with its lattice equivalence at every integer site. This is the compatibility needed by the convex-window coordinate change in Theorem 5.1.

theorem Nivat.transverse_coordinate_ne_zero (e : Lattice ≃+ Lattice) (q : ℕ) {h t : Lattice} (he : e (↑q, 0) = h) (hnonparallel : h.1 * t.2 ≠ h.2 * t.1) : (e.symm t).2 ≠ 0

Two nonparallel directions have a nonzero transverse coordinate after the first is made horizontal. This is the coordinate normalization in the nonparallel case of Theorem 5.1.