Configurations and translation operators

The configuration, period and operator notation of Section 1.1 of paper/nivat.tex. All configurations have the full integer lattice as their domain.

IsPeriod c h permits the zero vector; Periodic c requires one nonzero period. The forward-shift convention is shared by the Laurent action and pattern pairing.

@[reducible, inline]

abbrev Nivat.Lattice : Type

The integer lattice ℤ² on which configurations are defined (Section 1).

Equations

• Nivat.Lattice = (ℤ × ℤ)

@[reducible, inline]

abbrev Nivat.Configuration (A : Type u_1) : Type u_1

A configuration with alphabet A, as in Section 1.

Equations

• Nivat.Configuration A = (Nivat.Lattice → A)

def Nivat.shift {A : Type u_1} (h : Lattice) (c : Configuration A) : Configuration A

The forward translation Tʰc, with (Tʰc)(z) = c(z + h) (Section 1.1).

Equations

• Nivat.shift h c z = c (z + h)

def Nivat.FiniteRange {A : Type u_1} (c : Configuration A) : Prop

A configuration takes values in a finite set (Section 1.1).

Equations

• Nivat.FiniteRange c = (Set.range c).Finite

def Nivat.IsPeriod {A : Type u_1} (c : Configuration A) (h : Lattice) : Prop

A vector fixes the configuration at every lattice site (Section 1). This predicate allows zero; Periodic requires a nonzero witness.

Equations

• Nivat.IsPeriod c h = ∀ (z : Nivat.Lattice), c (z + h) = c z

def Nivat.Periodic {A : Type u_1} (c : Configuration A) : Prop

Existence of one nonzero global period, the conclusion of Theorem 1.1 (thm:main).

Equations

• Nivat.Periodic c = ∃ (h : Nivat.Lattice), h ≠ 0 ∧ Nivat.IsPeriod c h

def Nivat.difference {A : Type u_1} [AddCommGroup A] (h : Lattice) (c : Configuration A) : Configuration A

The difference operator Δₕ = Tʰ - I from Section 1.1.

Equations

• Nivat.difference h c = Nivat.shift h c - c

@[simp]

theorem Nivat.shift_apply {A : Type u_1} (h : Lattice) (c : Configuration A) (z : Lattice) : shift h c z = c (z + h)

Evaluation of the forward shift from Section 1.1.

@[simp]

theorem Nivat.shift_zero {A : Type u_1} (c : Configuration A) : shift 0 c = c

The zero translation acts as the identity (Section 1.1).

theorem Nivat.shift_add {A : Type u_1} (h t : Lattice) (c : Configuration A) : shift (h + t) c = shift h (shift t c)

Composition of the shift operators from Section 1.1.

theorem Nivat.shift_comm {A : Type u_1} (h t : Lattice) (c : Configuration A) : shift h (shift t c) = shift t (shift h c)

Shift operators commute, as used throughout Section 1.1.

theorem Nivat.isPeriod_iff_shift_eq {A : Type u_1} (c : Configuration A) (h : Lattice) : IsPeriod c h ↔ shift h c = c

The pointwise period condition is equivalent to Tʰc = c (Section 1.1).

theorem Nivat.IsPeriod.zero {A : Type u_1} (c : Configuration A) : IsPeriod c 0

The zero vector fixes every configuration (Section 1.1).

theorem Nivat.IsPeriod.add {A : Type u_1} {c : Configuration A} {h t : Lattice} (hh : IsPeriod c h) (ht : IsPeriod c t) : IsPeriod c (h + t)

The sum of two periods is a period (Section 1.1).

theorem Nivat.IsPeriod.neg {A : Type u_1} {c : Configuration A} {h : Lattice} (hh : IsPeriod c h) : IsPeriod c (-h)

Reversing a period preserves periodicity (Section 1.1).

theorem Nivat.IsPeriod.nsmul {A : Type u_1} {c : Configuration A} {h : Lattice} (hh : IsPeriod c h) (n : ℕ) : IsPeriod c (n • h)

Every natural multiple of a period is a period (Section 1.1).

theorem Nivat.IsPeriod.zsmul {A : Type u_1} {c : Configuration A} {h : Lattice} (hh : IsPeriod c h) (n : ℤ) : IsPeriod c (n • h)

Every integer multiple of a period is a period (Section 1.1).

theorem Nivat.isPeriod_shift_iff {A : Type u_1} (c : Configuration A) (h t : Lattice) : IsPeriod (shift t c) h ↔ IsPeriod c h

A configuration and any translate have the same periods (Section 1.1).

theorem Nivat.periodic_shift_iff {A : Type u_1} (c : Configuration A) (t : Lattice) : Periodic (shift t c) ↔ Periodic c

Periodicity is invariant under translation (Section 1.1).

theorem Nivat.FiniteRange.map {A : Type u_1} {B : Type u_2} {c : Configuration A} (hc : FiniteRange c) (f : A → B) : FiniteRange (f ∘ c)

Applying a function to a finite alphabet preserves finite range (Section 1.1).

theorem Nivat.FiniteRange.shift {A : Type u_1} {c : Configuration A} (hc : FiniteRange c) (h : Lattice) : FiniteRange (Nivat.shift h c)

Translations preserve finite range (Section 1.1).

theorem Nivat.finiteRange_of_finite {A : Type u_1} [Finite A] (c : Configuration A) : FiniteRange c

A configuration over a finite alphabet has finite range (Section 1.1).

theorem Nivat.isPeriod_map_iff {A : Type u_1} {B : Type u_2} (c : Configuration A) {f : A → B} (hf : Function.Injective f) (h : Lattice) : IsPeriod (f ∘ c) h ↔ IsPeriod c h

Injective alphabet labels preserve each period vector (Section 1.1).

theorem Nivat.periodic_map_iff {A : Type u_1} {B : Type u_2} (c : Configuration A) {f : A → B} (hf : Function.Injective f) : Periodic (f ∘ c) ↔ Periodic c

Injective alphabet labels preserve periodicity (Section 1.1).

@[simp]

theorem Nivat.difference_apply {A : Type u_1} [AddCommGroup A] (h : Lattice) (c : Configuration A) (z : Lattice) : difference h c z = c (z + h) - c z

The pointwise formula for Δₕc in Section 1.1.

theorem Nivat.difference_eq_zero_iff {A : Type u_1} [AddCommGroup A] (h : Lattice) (c : Configuration A) : difference h c = 0 ↔ IsPeriod c h

Vanishing of Δₕc is exactly the period condition (Section 1.1).

theorem Nivat.difference_comm {A : Type u_1} [AddCommGroup A] (h t : Lattice) (c : Configuration A) : difference h (difference t c) = difference t (difference h c)

Difference operators commute (Section 1.1).