~amiloradovsky/symbolic-dynamics

960accf8aead565646ace0b9854004a969724944 — Andrew Miloradovsky 6 months ago c05bff3
Topological: uniform structure on topological groups
3 files changed, 441 insertions(+), 0 deletions(-)

M Algebra.v
A Topological.v
M _CoqProject
M Algebra.v => Algebra.v +23 -0
@@ 63,6 63,13 @@ Hypothesis invertibility: is_inverse.

Notation "/ x" := (inverse x).

Lemma inverse_of_neutral : / neutral = neutral.
Proof.
  destruct invertibility as [li ri].
  destruct neutrality as [ln rn].
  congruence.
Qed.

Lemma inverse_of_product (a b: A): (/ (op a b)) = (op (/ b) (/ a)).
Proof.
  case invertibility. intros li ri. case neutrality. intros ln rn.


@@ 73,6 80,22 @@ Proof.
  rewrite ri. rewrite <- rn. rewrite ri. reflexivity.
Qed.

Lemma double_inverse : forall x, / (/ x) = x.
Proof.
  cbv in *.
  destruct invertibility as [li ri].
  destruct neutrality as [ln rn].
  intro.
  apply left_and_right_inverse with (b := / x).
  - cbv.
    rewrite <- inverse_of_product.
    rewrite ri.
    apply inverse_of_neutral.
  - cbv.
    rewrite li.
    reflexivity.
Qed.

Definition is_a_monoid := is_associative /\ is_neutral.
Definition is_a_group := is_a_monoid /\ is_inverse.
Definition is_commutative := forall x y: A, op x y = op y x.

A Topological.v => Topological.v +417 -0
@@ 0,0 1,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.

M _CoqProject => _CoqProject +1 -0
@@ 18,3 18,4 @@ Prodiscrete.v
Dynamical.v
Metric_Space.v
Decidable.v
Topological.v