Quotient topology (#786)

* quotient topology

* docs

* trying to fix build

* cleaning up proof

* more general quotients

* docs

* trying to fix build

* nitpicks

* quotType alias

* fix changelog

* fixing changelog again

---------

Co-authored-by: Reynald Affeldt <[email protected]>

Author: 2 people

CHANGELOG_UNRELEASED.md

@@ -64,6 +64,11 @@
   + lemmas `adde_def_doppeD`, `adde_def_doppeB`
   + lemma `fin_num_sume_distrr`
 
+- in file `topology.v`,
+  + new definitions `quotient_topology`, and `quotient_open`.
+  + new lemmas `pi_continuous`, `quotient_continuous`, and
+    `repr_comp_continuous`.
+
 ### Changed
 
 - in `fsbigop.v`:

theories/topology.v

@@ -1,6 +1,6 @@
 (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              *)
 From HB Require Import structures.
-From mathcomp Require Import all_ssreflect all_algebra finmap.
+From mathcomp Require Import all_ssreflect all_algebra finmap generic_quotient.
 From mathcomp.classical Require Import boolp classical_sets functions.
 From mathcomp.classical Require Import cardinality mathcomp_extra fsbigop.
 Require Import reals signed.
@@ -303,6 +303,9 @@ Require Import reals signed.
 (*                     close x y <-> x and y are arbitrarily close w.r.t. to  *)
 (*                                   balls.                                   *)
 (*          weak_pseudoMetricType == the metric space for weak topologies     *)
+(*            quotient_topology Q == the quotient topology corresponding to   *)
+(*                                   quotient Q : quotType T. where T has     *)
+(*                                   type topologicalType                     *)
 (*                                                                            *)
 (* * Complete uniform spaces :                                                *)
 (*                      cauchy F <-> the set of sets F is a cauchy filter     *)
@@ -4707,6 +4710,49 @@ HB.instance Definition _ := Uniform_isPseudoMetric.Build R (T -> U)
   fct_ball_center fct_ball_sym fct_ball_triangle fct_entourage.
 End fct_PseudoMetric.
 
+Definition quotient_topology (T : topologicalType) (Q : quotType T) : Type := Q.
+
+Section quotients.
+Local Open Scope quotient_scope.
+Context {T : topologicalType} {Q0 : quotType T}.
+
+Local Notation Q := (quotient_topology Q0).
+
+HB.instance Definition _ := gen_eqMixin Q.
+HB.instance Definition _ := gen_choiceMixin Q.
+HB.instance Definition _ := isPointed.Build Q (\pi_Q point).
+
+Definition quotient_open U := open (\pi_Q @^-1` U).
+
+Program Definition quotient_topologicalType_mixin :=
+  @Pointed_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.instance Definition _ := quotient_topologicalType_mixin.
+
+Lemma pi_continuous : continuous (\pi_Q : T -> Q).
+Proof. exact/continuousP. Qed.
+
+Lemma quotient_continuous {Z : topologicalType} (f : 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 (Z : topologicalType) (g : T -> Z) :
+  continuous g -> {homo g : a b / \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); first 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 quotients.
+
 (** ** Complete uniform spaces *)
 
 Definition cauchy {T : uniformType} (F : set_system T) := (F, F) --> entourage.