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 ( : Type) ( : quotType T) : Type := Q.

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

Local Notation := (quotient_topology Q0).

..copy Q Q0.
. Q of T by %/].
. of Q by <:].

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

Program Definition :=
@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.

..

Lemma : continuous (\pi_Q : T -> Q).

Proof.

exact/continuousP. Qed.

Lemma { : topologicalType} ( : 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 ( : topologicalType) ( : T -> Z) :
continuous g -> {homo g : / \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 { : ptopologicalType} { : quotType T}.
Local Notation := (quotient_topology Q0).
..Build Q (\pi_Q point : Q).
End pointed.
End quotients.

Files

Module mathcomp.analysis.topology_theory.quotient_topology