~amiloradovsky/symbolic-dynamics

symbolic-dynamics/Prodiscrete.v -rw-r--r-- 2.5 KiB View raw
5857f238Andrew Miloradovsky .build.yml: continuous integration for SourceHut 7 months ago
                                                                                
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
(* * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * *
 * Pro-discrete (Tychonoff) topology on the space of configurations
 * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * *)

(*
  There is a technical distinction to be made, between (point-set
  of) the full shift space and configurations / full patterns:
  The former view is convenient / necessary when dealing with the
  topological properties of the space, interaction with the library.
  The latter is when dealing with supports, patterns, and restrictions.
  Thus, some convertibility needs to be proven before we can proceed.
 *)

Require Export Topology.ProductTopology.
Require Export Symbolic_Dynamics.Patterns.

Section Prodiscrete_Topology.

  Variable 𝕄 : Type.  (* the "time" domain, e.g. N^d or Z^d (d: nat) *)
  Variable 𝔸 : Set.  (* the alphabet, the space of the symbols,
                        the equality of symbols is proof-irrelevant *)

  Definition Constant {U V: Type} (C: V) := fun _: U => C.
  Definition Discrete (X: Type): TopologicalSpace.
    refine (Build_TopologicalSpace X (fun _ => True) _ _ _).
    all: trivial.
  Defined.

  Definition Full_shift_space := @ProductTopology
                                   𝕄 (Constant (Discrete 𝔸)).
  (* point-set of the space is just the space of maps 𝕄 -> 𝔸 *)

  Definition full_shift_space_to_configurations:
    point_set (Full_shift_space) -> configuration 𝕄 𝔸.
  Proof. intros X x. destruct x. exact (X x). Defined.
  Definition configurations_to_full_shift_space:
    configuration 𝕄 𝔸 -> point_set (Full_shift_space).
  Proof. intros X i. apply X. now exists i. Defined.
  Lemma full_shift_space_is_made_of_configurations_0:
    forall x, configurations_to_full_shift_space
                (full_shift_space_to_configurations x) = x.
  Proof. cbv. intros. trivial. Qed.
  Lemma full_shift_space_is_made_of_configurations_1:
    forall y, full_shift_space_to_configurations
                (configurations_to_full_shift_space y) = y.
  Proof. intros.
         apply FunctionalExtensionality.functional_extensionality;
           intro. destruct x. destruct f. reflexivity. Qed.
  (* TODO: Here should be a lemma about the equivalence of the types *)

  Hypothesis compact_alphabet : compact (Discrete 𝔸).
  (* could be derived from finiteness, but I don't know how *)

  Lemma compact_full_shift_space: compact Full_shift_space.
  Proof. now apply TychonoffProductTheorem. Qed.

End Prodiscrete_Topology.