~amiloradovsky/symbolic-dynamics

symbolic-dynamics/Topological.v -rw-r--r-- 11.4 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
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
(* * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * *
 * Topological spaces with algebraic structure: e.g. groups
 * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * *)

Require Import Topology.Continuity.
Require Import Topology.ProductTopology.
Require Import Symbolic_Dynamics.Algebra.
Require Import Symbolic_Dynamics.Uniform.
Require Import Relation_Definitions.

Section Topological_Group.

  Variable X : TopologicalSpace.

  Let A := point_set X.

  Variable op : A -> A -> A.
  Variable neutral : A.
  Variable inverse : A -> A.

  (* Admits a uniform structure *)

  Inductive entourage_base
            (U: Ensemble A) (H: open U) (G: U neutral): relation _ :=
  | entourage_base_intro: forall x y,
      U (op x (inverse y)) -> entourage_base U H G x y.
  Inductive fundamental_system: Ensemble (relation _) :=
  | fundamental_system_intro: forall U (H : open U) (G : U neutral),
      fundamental_system (entourage_base U H G).

  Definition uniformity :=
    uniformity_from_fundamental_system fundamental_system.

  Hypothesis group: is_a_group _ op neutral inverse.

  Lemma indeed_is_reflexive : is_reflexive _ uniformity.
  Proof.
    intros??.
    destruct H.
    destruct H as (V & HIV & HVFS).
    intro.
    apply (HIV x x).
    destruct HVFS as [S H].
    constructor.
    destruct group as [_ [li ri]].
    rewrite ri.
    assumption.
  Qed.

  Lemma indeed_is_upper_closed :
    is_upper_closed _ uniformity.
  Proof.
    intros ? ? HIUV HUU.
    destruct HUU as (? & U_ & []).
    constructor.
    exists U_.
    split.
    - intros a b U_ab.
      apply HIUV.
      apply (H a b); assumption.
    - assumption.
  Qed.

  Hypothesis continuous_inverse: continuous inverse.

  Lemma indeed_is_stable_by_symmetry :
    is_stable_by_symmetry _ uniformity.
  Proof.
    intros??.
    constructor.
    destruct H.
    destruct H as (V & HIUV & HFSV).
    exists (converse _ V).
    split.
    - intros???.
      constructor.
      destruct H.
      apply HIUV.
      assumption.
    - clear HIUV U.
      destruct HFSV.
      eassert (entourage_base (inverse_image inverse U) _ _ =
               converse A (entourage_base U H G)).
      {
        destruct group as [[? ?] ?].
        apply extensionality_relations; split.
        all: intros???.
        1: constructor.
        2: destruct H0.
        all: destruct H0; constructor.
        * destruct H0.
          rewrite inverse_of_product
            with (inverse := inverse) (neutral := neutral) in H0.
          rewrite double_inverse
            with (op := op)
                 (inverse := inverse) (neutral := neutral) in H0.
          all: assumption.
        * constructor.
          rewrite inverse_of_product
            with (inverse := inverse) (neutral := neutral).
          rewrite double_inverse
            with (op := op)
                 (inverse := inverse) (neutral := neutral).
          all: assumption.
      }
      rewrite <- H0.
      constructor.

      Unshelve.
      + apply continuous_inverse. assumption.
      + cbv.
        destruct group as [[? ?] ?].
        constructor.
        rewrite inverse_of_neutral
          with (op := op) (inverse := inverse) (neutral := neutral).
        all: assumption.
  Qed.

  Lemma intersection_of_entourages :
    forall U0 U1 H0 H1 G0 G1,
    exists U H G, entourage_base U H G =
                  intersection A
                               (entourage_base U0 H0 G0)
                               (entourage_base U1 H1 G1).
  Proof.
    intros.
    exists (Intersection U0 U1).
    exists (open_intersection2 _ _ H0 H1).
    exists (Intersection_intro _ _ _ neutral G0 G1).
    apply extensionality_relations; split.
    all: intros???.
    - induction H.
      inversion H as [z].
      constructor.
      all: constructor; assumption.
    - destruct H as [? ? H0' H1'].
      constructor.
      constructor.
      + destruct H0'. assumption.
      + destruct H1'. assumption.
  Qed.

  Lemma indeed_is_stable_by_intersection :
    is_stable_by_intersection _ uniformity.
  Proof.
    intros ? ? HUU HUV.
    constructor.
    destruct HUU as [U HU], HUV as [V HV].
    destruct HU as (U_ & HIU_U & HFSU_).
    destruct HV as (V_ & HIV_V & HFSV_).
    exists (intersection A U_ V_).
    split.
    - intros ?? ?.
      constructor.
      + destruct H. apply HIU_U. assumption.
      + destruct H. apply HIV_V. assumption.
    - destruct HFSU_ as [? H0 G0], HFSV_ as [? H1 G1].
      pose (RE := intersection_of_entourages U0 U1 H0 H1 G0 G1).
      destruct RE as (U_ & H_ & G_ & ?).
      rewrite <- H.
      constructor.
  Qed.

  (* here we employ booleans for the index of the product space,
     simply because they have two constructors, no other reasons *)

  Let X2 := fun _ : bool => X.
  Let X2PT := ProductTopology X2.
  Let A2 := point_set X2PT.
  Let op2 : A2 -> A := fun aa => op (aa false) (aa true).

  Hypothesis continuous_product: continuous op2.

  Let pj0 (a : A2) := a false.
  Let pj1 (a : A2) := a true.

  Definition rectangle : forall U V : Ensemble A, Ensemble A2.
  Proof.
    intros.
    pose (U' := inverse_image pj0 U).
    pose (V' := inverse_image pj1 V).
    exact (Intersection U' V').
  Defined.

  (* TODO: this is a very general lemma, should live somewhere else *)
  Lemma union_of_singleton :
    forall {T} S, @FamilyUnion T (Singleton S) = S.
  Proof.
      intros.
      apply Extensionality_Ensembles.
      split.
      - intros??.
        destruct H.
        destruct H.
        assumption.
      - intros??.
        econstructor.
        constructor.
        assumption.
  Qed.

  Lemma open_rectangle :
    forall U V : Ensemble A, open U -> open V -> open (rectangle U V).
  Proof.
    intros ? ? HU HV.
    unfold rectangle.
    remember (inverse_image pj0 U) as U'.
    remember (inverse_image pj1 V) as V'.
    pose (Z := weak_topology_subbasis product_space_proj (Y := X2)).
    eassert (FIU' := FiniteIntersections.intro_S Z U' _).
    eassert (FIV' := FiniteIntersections.intro_S Z V' _).
    pose (FI := FiniteIntersections.intro_intersection
                  Z U' V' FIU' FIV').
    replace (Intersection U' V') with
        (FamilyUnion (Singleton (Intersection U' V')))
      by apply union_of_singleton.
    constructor.
    intros??.
    destruct H.
    apply FI.

    Unshelve.
    - subst U'.
      replace pj0 with (product_space_proj false (X := X2))
        by reflexivity.
      constructor. assumption.
    - subst V'.
      replace pj1 with (product_space_proj true (X := X2))
        by reflexivity.
      constructor. assumption.
  Qed.

  Lemma finite_intersection_is_rectangle W :
    FiniteIntersections.finite_intersections
      (weak_topology_subbasis product_space_proj) W ->
    exists U V, open U /\ open V /\ rectangle U V = W.
  Proof.
    intros.
    induction H.

    - exists Full_set, Full_set.
      repeat split.
      1,2: apply open_full.
      apply Extensionality_Ensembles.
      split.
      all: repeat constructor.

    - destruct H.
      destruct a.
      + exists Full_set, V.
        repeat split.
        apply open_full. assumption.
        apply Extensionality_Ensembles; split.
        * intros??.
          destruct H0.
          apply H1.
        * intros??.
          repeat constructor.
          destruct H0.
          apply H0.
      + exists V, Full_set.
        repeat split.
        assumption. apply open_full.
        apply Extensionality_Ensembles; split.
        * intros??.
          destruct H0.
          apply H0.
        * intros??.
          repeat constructor.
          destruct H0.
          apply H0.

    - destruct IHfinite_intersections  as (UU & UV & HU).
      destruct IHfinite_intersections0 as (VU & VV & HV).
      exists (Intersection UU VU).
      exists (Intersection UV VV).
      destruct HU as (HUU & HUV & ?), HV as (HVU & HVV & ?).
      repeat split.
      apply open_intersection2. 1,2: assumption.
      apply open_intersection2. 1,2: assumption.
      subst U V.
      apply Extensionality_Ensembles; split.
      + intros??.
        destruct H1.
        destruct H1, H2.
        constructor.
        * constructor.
          inversion H1. constructor. assumption.
          inversion H2. constructor. assumption.
        * constructor.
          inversion H1. constructor. assumption.
          inversion H2. constructor. assumption.
      + intros??.
        destruct H1.
        destruct H1, H2.
        constructor.
        all: constructor.
        * constructor.
          inversion H1. assumption.
          inversion H2. assumption.
        * constructor.
          inversion H3. assumption.
          inversion H4. assumption.
  Qed.

  Let to_A2 x y : A2 := fun z => match z with
                                | false => x
                                | true => y end.
  Let nn := to_A2 neutral neutral.

  Lemma rectangular_subset (W : Ensemble A2) :
    open W -> W nn -> exists U V, open U /\ open V /\
                                  rectangle U V nn /\
                                  Included (rectangle U V) W.
  Proof.
    intros H Hnn.
    destruct H.
    destruct Hnn.
    specialize (H S H0).
    pose (finite_intersection_is_rectangle _ H).
    destruct e as (U & V & HU & HV & E).
    exists U, V.
    split. assumption.
    split. assumption.
    split.
    - rewrite E.
      assumption.
    - intros??.
      rewrite E in H2.
      econstructor.
      apply H0.
      assumption.
  Qed.

  Lemma square_root_set (U : Ensemble A) :
    open U -> U neutral -> exists V,
        open V /\ V neutral /\ forall x y, V x -> V y -> U (op x y).
  Proof.
    intros ? Un.
    pose (U_ := inverse_image op2 U).
    assert (H_ : open U_) by apply (continuous_product U H).
    inversion H_ as [? HF HUF].
    assert (U_nn : U_ nn).
    {
      subst U_.
      constructor.
      cbv.
      destruct group as [[_ [ln rn]] _].
      rewrite <- rn. assumption.
    }
    pose (rectangular_subset U_ H_ U_nn).
    destruct e as (V0 & V1 & HV0 & HV1 & Rnn & RI).
    exists (Intersection V0 V1).
    split.
    - apply open_intersection2. all: assumption.
    - split.
      + inversion Rnn. subst x.
        constructor; [ apply H0 | apply H1 ].
      + intros.
        subst U_.
        specialize (RI (to_A2 x y)).
        apply RI.
        constructor.
        all: constructor.
        * inversion H0; inversion H1. subst x0 x1.
          cbv. assumption.
        * inversion H0; inversion H1. subst x0 x1.
          cbv. assumption.
  Qed.

  Lemma indeed_there_exist_square_roots :
    there_exist_square_roots _ uniformity.
  Proof.
    intros??.
    destruct H.
    destruct H as (V & HIUV & HFSV).
    unfold square_is_in.
    unfold squared.
    destruct HFSV as [U' H' G'].
    destruct (square_root_set U' H' G') as (V & HV & HN & HI).
    exists (entourage_base V HV HN).
    split.
    - constructor.
      eexists.
      repeat split.
      destruct H.
      apply H.
      Unshelve.
      all: assumption.
    - intros???.
      destruct H.
      destruct H as (? & Uax & Uxc).
      apply HIUV.
      constructor.
      destruct group as [[HA [ln rn]] [li ri]].
      rewrite (rn a).
      rewrite <- (li x).
      rewrite HA.
      rewrite <- HA.
      unfold continuous in continuous_product.
      destruct Uax as [a x Hax], Uxc as [x c Hxc].
      apply HI.
      all: assumption.
  Qed.

  Lemma indeed_is_uniform_structure:
    is_uniform_structure _ uniformity.
  Proof.
    split. exact indeed_is_reflexive.
    split. exact indeed_is_upper_closed.
    split. exact indeed_is_stable_by_symmetry.
    split. exact indeed_is_stable_by_intersection.
    exact indeed_there_exist_square_roots.
  Qed.

End Topological_Group.