Files

  • mathcomp

    • Top

    Module mathcomp.analysis.topology_theory.subtype_topology

    From HB Require Import structures.
    From mathcomp Require Import all_ssreflect_compat all_algebra all_classical.
    From mathcomp Require Import reals topology_structure uniform_structure compact.
    From mathcomp Require Import pseudometric_structure connected initial_topology.
    From mathcomp Require Import product_topology subspace_topology.

    # Subtypes of topological spaces We have two distinct ways of building topologies as subsets of a topological space `X`. One is the `subspace topology`, which is defined in `subspace_topology.v`. It builds a topology on X which 'isolates' a set A. The other, defined in this file, defines a topology on the sigma type `set_type` in the initial topology by the inclusion. Note `subspace A` has the advantage that it preserves all the algebraic structure on X, but only the local behavior A (in particular, continuity). On the other hand `set_type A` has the right global properties you'd expect for the subset topology. But you can't easily add two elements of `set_val [0, 1]`. Note the implicit coercion from sets to `set_val` from `classical_sets.v`. This file provides `set_type` with a topology, and some theory. ``` sigT_of_setX == commutes `set_type` and product topologies setX_of_sigT == commutes product and `set_type` topologies ```

    Unset SsrOldRewriteGoalsOrder.

    Local Open Scope classical_set_scope.
    Local Open Scope ring_scope.

    HB.instance Definition _ {X : topologicalType} (A : set X) :=
      Topological.copy (set_type A) (initial_topology set_val).

    HB.instance Definition _ {X : uniformType} (A : set X) :=
      Uniform.copy (A : Type) (@initial_topology (A : Type) X set_val).

    HB.instance Definition _ {R : realType} {X : pseudoMetricType R} (A : set X) :=
      PseudoMetric.copy (A : Type) (@initial_topology (A : Type) X set_val).

    Section subspace_sig.
    Context {X : topologicalType} (A : set X).

    Lemma subspace_subtypeP (x : A) (U : set A) :
      nbhs x U <-> nbhs (set_val x : subspace A) (set_val @` U).
    Proof.
    rewrite /nbhs /= -nbhs_subspace_in //.
      by case: x; rewrite set_valE => //= ? /set_mem.
    split.
      case=> _ /= [] [W oW <- /= Wx sWU]; move: oW; rewrite openE /= /interior.
      move=> /(_ _ Wx); apply: filter_app; apply: nearW => w /= Ww /mem_set Aw.
      by exists (@exist _ _ w Aw) => //; exact: sWU.
    rewrite withinE => -[V + UAVA]; rewrite nbhsE => -[V' [oV' V'x V'V]].
    exists (sval @^-1` V'); split => //=; first by exists V'.
    move=> w /= /V'V Vsw; have : (V `&` A) (\val w).
      by split => //; case: w Vsw => //= ? /set_mem.
    by rewrite -UAVA => -[[v ? /eq_sig_hprop] <-].
    Qed.

    Lemma subspace_sigL_continuousP {Y : topologicalType} (f : X -> Y) :
      {within A, continuous f} <-> continuous (sigL A f).
    Proof.
    split.
      have /continuous_subspaceT/subspaceT_continuous :=
        @initial_continuous A X set_val.
      move=> svf ctsf; apply/continuous_subspace_setT => x.
      apply: (@continuous_comp (subspace _) (subspace A)); last exact: ctsf.
      by move=> U nfU; exact: svf.
    rewrite continuous_subspace_in => + x Ax U nfxU.
    move=> /(_ (@exist _ _ x Ax) U) /= []; first exact: nfxU.
    move=> _ [/= [W + <- /=]] Wx svWU; rewrite nbhs_simpl/=.
    rewrite /nbhs /= -nbhs_subspace_in; first exact/set_mem.
    rewrite openE /= /interior=> /(_ _ Wx); rewrite {1}set_valE/=.
    apply: filter_app; apply: nearW => w Ww /= /mem_set Aw.
    by have /= := svWU (@exist _ _ w Aw); rewrite ?set_valE /=; exact.
    Qed.

    Lemma subspace_valL_continuousP' {Y : topologicalType} (y : Y) (f : A -> Y) :
      {within A, continuous (valL_ y f)} <-> continuous f.
    Proof.
    rewrite -{2}[f](@valLK _ _ y A); split=> [/subspace_sigL_continuousP//|cf].
    exact/subspace_sigL_continuousP.
    Qed.

    Lemma subspace_valL_continuousP {Y : ptopologicalType} (f : A -> Y) :
      {within A, continuous (valL f)} <-> continuous f.
    Proof.
    exact: (@subspace_valL_continuousP' _ point). Qed.

    End subspace_sig.

    Lemma within_continuous_comp {U V W : topologicalType}
      (A : set V) (f : V -> U) (g : U -> W) :
      {in f @` A, continuous g} ->
      {within A, continuous f} ->
      {within A, continuous (g \o f)}.
    Proof.
    move=> cg /subspace_sigL_continuousP cf; apply/subspace_sigL_continuousP.
    rewrite /sigL -compA => /= x; apply: continuous_comp; first exact: cf.
    by apply/cg/image_f; rewrite inE; exact/set_valP.
    Qed.

    Section subtype_setX.
    Context {X Y : topologicalType} (A : set X) (B : set Y).

    Program Definition
    setX_of_sigT

    setX_of_sigT : forall {X Y : topology_structure.Topological.type} (A : set (topology_structure.Topological.sort X)) (B : set (topology_structure.Topological.sort Y)), (A `*` B)%classic -> A * B setX_of_sigT is not universe polymorphic Arguments setX_of_sigT {X Y} (A B)%_classical_set_scope ab setX_of_sigT is transparent Expands to: Constant mathcomp.analysis.topology_theory.subtype_topology.setX_of_sigT Declared in library mathcomp.analysis.topology_theory.subtype_topology, line 108, characters 19-31

    (ab : A `*` B) : (A * B)%type :=
      (@exist _ _ ab.1 _, @exist _ _ ab.2 _).
    Next Obligation.
    by case; case => a b /= /set_mem [] ? ?; exact/mem_set. Qed.
    Next Obligation.
    by case; case => a b /= /set_mem [] ? ?; exact/mem_set. Qed.

    Program Definition
    sigT_of_setX

    sigT_of_setX : forall {X Y : topology_structure.Topological.type} (A : set (topology_structure.Topological.sort X)) (B : set (topology_structure.Topological.sort Y)), A * B -> (A `*` B)%classic sigT_of_setX is not universe polymorphic Arguments sigT_of_setX {X Y} (A B)%_classical_set_scope ab sigT_of_setX is transparent Expands to: Constant mathcomp.analysis.topology_theory.subtype_topology.sigT_of_setX Declared in library mathcomp.analysis.topology_theory.subtype_topology, line 113, characters 19-31

    (ab : (A * B)%type) : A `*` B :=
      (@exist _ _ (\val ab.1, \val ab.2) _).
    Next Obligation.
    by move=> [[x/= /set_mem Ax] [y/= /set_mem By]]; exact/mem_set.
    Qed.

    Lemma sigT_of_setXK : cancel sigT_of_setX setX_of_sigT.
    Proof.
    by move=> [[x ?] [y ?]]; congr (( _, _)); exact: eq_sig_hprop. Qed.

    Lemma setX_of_sigTK : cancel setX_of_sigT sigT_of_setX.
    Proof.
    by move=> [[a b] ?]; exact: eq_sig_hprop. Qed.

    Lemma setX_of_sigT_continuous : continuous setX_of_sigT.
    Proof.
    move=> [[x y] p] U [/= [P Q]] /= [nxP nyQ] pqU.
    case: nxP => _ [/= [] P' oP' <- /=]; rewrite set_valE /= => P'x P'P.
    case: nyQ => _ [/= [] Q' oQ' <- /=]; rewrite set_valE /= => Q'x Q'Q.
    pose PQ : set (A `*` B) := \val @^-1` (P' `*` Q').
    exists PQ; split => //=.
      exists (P' `*` Q') => //; rewrite openE => -[a b /=] [P'a Q'b].
      exists (P', Q') => //; split.
      - by move: oP'; rewrite openE; exact.
      - by move: oQ'; rewrite openE; exact.
    by move=> [[a b]/= abAB [P'a Q'b]]; apply/pqU; split; [exact: P'P|exact: Q'Q].
    Qed.

    Lemma sigT_of_setX_continuous : continuous sigT_of_setX.
    Proof.
    move=> [[x Ax] [y By]] U [? [] [W + <-] /=]; rewrite set_valE/=.
    rewrite openE /= => /[apply] [][][] P Q /=; rewrite (nbhsE x) (nbhsE y) => -[].
    move=> [P' [oP' P'x P'P]] [Q' [oQ' Q'y Q'Q]] PQW WU.
    exists (val @^-1` P', \val @^-1` Q') => /=; first split.
    - by exists (\val@^-1` P'); split => //=; exists P'.
    - by exists (\val @^-1` Q'); split => //=; exists Q'.
    - by move=> [[p Ap] [q Bq]]/= [P'p Q'q]; apply/WU/PQW;
        split; [exact: P'P|exact: Q'Q].
    Qed.

    End subtype_setX.
    Generated by rocqnavi