Affine lattice coordinates

Coordinate transport for Lemma 5.5 (lem:boundary-window) and Theorem 5.1 (thm:twofactor) in paper/nivat.tex.

A configuration and its window are transported together. The affine map s acts on sites, while its additive part t acts on translation and period vectors.

theorem Nivat.FiniteRange.precomp {A : Type u_1} {c : Configuration A} (hc : FiniteRange c) (f : Lattice → Lattice) : FiniteRange (c ∘ f)

Reindexing lattice sites preserves finite range (Section 1.1).

theorem Nivat.complexity_affine_reindex {A : Type u_1} (c : Configuration A) (s : Lattice ≃ Lattice) (t : Lattice ≃+ Lattice) (hst : ∀ (z u : Lattice), s (z + u) = s z + t u) (D : Finset Lattice) : complexity (c ∘ ⇑s) D = complexity c (Finset.map s.toEmbedding D)

Transport both a configuration and its window along affine lattice coordinates. This is the basis-and-origin change in Lemma 5.5 (lem:boundary-window); s is the affine bijection and t its linear part.

theorem Nivat.isPeriod_affine_reindex_iff {A : Type u_1} (c : Configuration A) (s : Lattice ≃ Lattice) (t : Lattice ≃+ Lattice) (hst : ∀ (z u : Lattice), s (z + u) = s z + t u) (h : Lattice) : IsPeriod (c ∘ ⇑s) h ↔ IsPeriod c (t h)

A period in affine coordinates transports through the linear part. This is the return to the original lattice in Theorem 5.1 (thm:twofactor).

theorem Nivat.difference_affine_reindex {A : Type u_1} [AddCommGroup A] (c : Configuration A) (s : Lattice ≃ Lattice) (t : Lattice ≃+ Lattice) (hst : ∀ (z u : Lattice), s (z + u) = s z + t u) (h : Lattice) : difference h (c ∘ ⇑s) = difference (t h) c ∘ ⇑s

Difference operators transport with their lattice direction. This is the mixed-difference coordinate change in Theorem 5.1 (thm:twofactor).