Curtis–Hedlund–Lyndon theorem

TheoremCurtis–Hedlund–Lyndon theorem with an arbitrary discrete output alphabet#✓fully proved

Let \(A\) be a finite set and \(B\) any set, both with the discrete topology, and give \(A^{\mathbb{Z}}\) and \(B^{\mathbb{Z}}\) the product topology. For \(k \in \mathbb{Z}\) let \(\sigma^k\) be the shift on either space given by \((\sigma^k x)_n = x_{n+k}\) for all \(n \in \mathbb{Z}\). A map \(F : A^{\mathbb{Z}} \to B^{\mathbb{Z}}\) is a sliding block code, that is, there are a radius \(r \in \mathbb{N}\) and a local rule \(\varphi : A^{2r+1} \to B\) with \(F(x)_n = \varphi(x_{n-r}, \dots, x_{n+r})\) for all \(x \in A^{\mathbb{Z}}\) and \(n \in \mathbb{Z}\), if and only if \(F\) is continuous and commutes with every shift: \(F(\sigma^k x) = \sigma^k F(x)\) for all \(x \in A^{\mathbb{Z}}\) and \(k \in \mathbb{Z}\).

theorem curtis_hedlund_lyndon_general {A B : Type*} [TopologicalSpace A] [DiscreteTopology A]
    [Finite A] [TopologicalSpace B] [DiscreteTopology B] (F : (ℤ → A) → (ℤ → B)) :
    (∃ (r : ℕ) (φ : (Fin (2 * r + 1) → A) → B), ∀ (x : ℤ → A) (n : ℤ),
      F x n = φ (fun i => x (n + ((i.val : ℤ) - (r : ℤ))))) ↔
    (Continuous F ∧ ∀ (x : ℤ → A) (k : ℤ), F (fun n => x (n + k)) = fun n => F x (n + k))

Used by 1

Used byCurtis–Hedlund–Lyndon theorem

TheoremCurtis–Hedlund–Lyndon theorem#✓fully proved

Let \(A\) and \(B\) be finite sets with the discrete topology, and give \(A^{\mathbb{Z}}\) and \(B^{\mathbb{Z}}\) the product topology. For \(k \in \mathbb{Z}\) let \(\sigma^k\) be the shift on either space given by \((\sigma^k x)_n = x_{n+k}\) for all \(n \in \mathbb{Z}\). A map \(F : A^{\mathbb{Z}} \to B^{\mathbb{Z}}\) is a sliding block code, that is, there are a radius \(r \in \mathbb{N}\) and a local rule \(\varphi : A^{2r+1} \to B\) with \(F(x)_n = \varphi(x_{n-r}, \dots, x_{n+r})\) for all \(x \in A^{\mathbb{Z}}\) and \(n \in \mathbb{Z}\), if and only if \(F\) is continuous and commutes with every shift: \(F(\sigma^k x) = \sigma^k F(x)\) for all \(x \in A^{\mathbb{Z}}\) and \(k \in \mathbb{Z}\).

@[nolint unusedArguments]
theorem curtis_hedlund_lyndon {A B : Type*} [TopologicalSpace A] [DiscreteTopology A]
  [Finite A] [TopologicalSpace B] [DiscreteTopology B] [Finite B] (F : (ℤ → A) → (ℤ → B)) :
  (∃ (r : ℕ) (φ : (Fin (2 * r + 1) → A) → B), ∀ (x : ℤ → A) (n : ℤ), F x n = φ
  (fun i => x (n + ((i.val : ℤ) - (r : ℤ))))) ↔
  (Continuous F ∧ ∀ (x : ℤ → A) (k : ℤ), F (fun n => x (n + k)) = fun n => F x (n + k))

Sources

• https://en.wikipedia.org/wiki/Curtis%E2%80%93Hedlund%E2%80%93Lyndon_theorem (statement id curtis-hedlund-s1).

Uses 1

Proof usesCurtis–Hedlund–Lyndon theorem with an arbitrary discrete output alphabet

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.