Files

  • mathcomp

    • Top source

    Module mathcomp.analysis.topology_theory.quotient_topology

    From HB Require Import structures.
    From mathcomp Require Import boot order algebra all_classical.
    From mathcomp Require Import topology_structure.

    # quotient topology ``` quotient_topology Q == the quotient topology corresponding to quotient Q : quotType T where T has type topologicalType ```

    Unset SsrOldRewriteGoalsOrder.
    Set Implicit Arguments.
    Unset Strict Implicit.
    Unset Printing Implicit Defensive.

    Local Open Scope classical_set_scope.
    Local Open Scope ring_scope.

    Definition
    quotient_topology
    Source code
     (
    T
    Source code
     : Type) (
    Q
    Source code
     : quotType T) : Type := Q.

    Section quotients.
    Local Open Scope quotient_scope.
    Section unpointed.
    Context {
    T
    Source code
     : topologicalType} {
    Q0
    Source code
     : quotType T}.

    Local Notation
    Q
    Source code
     := (quotient_topology Q0).

    HB
    Source code
    .
    instance
    Source code
    Definition
    Source code
    _
    Source code
    :=
    Source code
    Quotient
    Source code
    .copy Q Q0.
    HB
    Source code
    .
    instance
    Source code
    Definition
    Source code
    _
    Source code
    :=
    Source code
    [Sub
    Source code
     Q of T by %/].
    HB
    Source code
    .
    instance
    Source code
    Definition
    Source code
    _
    Source code
    :=
    Source code
    [Choice
    Source code
     of Q by <:].

    Definition
    quotient_open

    entourage_ : forall {R : numDomainType} {T T' : Type}, (T -> R -> set T') -> set_system (T * T') entourage_ is not universe polymorphic Arguments entourage_ {R} {T T'}%_type_scope ball%_function_scope _ entourage_ is transparent Expands to: Constant mathcomp.analysis.topology_theory.pseudometric_structure.entourage_ Declared in library mathcomp.analysis.topology_theory.pseudometric_structure, line 60, characters 11-21

    Source code
    U
    Source code
     := open (\pi_Q @^-1` U).

    Program Definition
    quotient_topologicalType_mixin

    nbhs_ball_ : forall {R : numDomainType} {T T' : Type}, (T -> R -> set T') -> T -> set_system T' nbhs_ball_ is not universe polymorphic Arguments nbhs_ball_ {R} {T T'}%_type_scope ball%_function_scope x _ nbhs_ball_ is transparent Expands to: Constant mathcomp.analysis.topology_theory.pseudometric_structure.nbhs_ball_ Declared in library mathcomp.analysis.topology_theory.pseudometric_structure, line 162, characters 11-21

    Source code
     :=
      @isOpenTopological.Build Q quotient_open _ _ _.
    Next Obligation.
    by rewrite /quotient_open preimage_setT; exact: openT. Qed.
    Next Obligation.
    by move=> ? ? ? ?; exact: openI. Qed.
    Next Obligation.
    by move=> I f ofi; apply: bigcup_open => i _; exact: ofi. Qed.
    HB
    Source code
    .
    instance
    Source code
    Definition
    Source code
    _
    Source code
    :=
    Source code
    quotient_topologicalType_mixin
    Source code
    .

    Lemma
    pi_continuous
    Source code
     : continuous (\pi_Q : T -> Q).
    Proof.
    exact/continuousP. Qed.

    Lemma
    quotient_continuous
    Source code
     {
    Z
    Source code
     : topologicalType} (
    f
    Source code
     : Q -> Z) :
      continuous f <-> continuous (f \o \pi_Q).
    Proof.
    split => /continuousP /= cts; apply/continuousP => A oA; last exact: cts.
    by rewrite comp_preimage; move/continuousP: pi_continuous; apply; exact: cts.
    Qed.

    Lemma
    repr_comp_continuous
    Source code
     (
    Z
    Source code
     : topologicalType) (
    g
    Source code
     : T -> Z) :
      continuous g -> {homo g :
    a
    Source code
    b
    Source code
     / \pi_Q a == \pi_Q b :> Q >-> a == b} ->
      continuous (g \o repr : Q -> Z).
    Proof.
    move=> /continuousP ctsG rgE; apply/continuousP => A oA.
    rewrite /open/= /quotient_open (_ : _ @^-1` _ = g @^-1` A); last exact: ctsG.
    have greprE x : g (repr (\pi_Q x)) = g x by apply/eqP; rewrite rgE// reprK.
    by rewrite eqEsubset; split => x /=; rewrite greprE.
    Qed.

    End unpointed.

    Section pointed.
    Context {
    T
    Source code
     : ptopologicalType} {
    Q0
    Source code
     : quotType T}.
    Local Notation
    Q
    Source code
     := (quotient_topology Q0).
    HB
    Source code
    .
    instance
    Source code
    Definition
    Source code
    _
    Source code
    :=
    Source code
    isPointed
    Source code
    .Build Q (\pi_Q point : Q).
    End pointed.
    End quotients.
    Generated by rocqnavi