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
Used by
Source code
( : Type) ( : quotType T) : Type := Q.Used by
- mathcomp.analysis.homotopy_theory.wedge_sigT
Source code
Section quotients.
Local Open Scope quotient_scope.
Section unpointed.
Context { : topologicalType} { : quotType T}.
Local Notation := (quotient_topology Q0).
.
instanceSource code
DefinitionSource code
QuotientSource code
.copy Q Q0..
instanceSource code
DefinitionSource code
[SubSource code
Q of T by %/]..
instanceSource code
DefinitionSource code
[ChoiceSource code
of Q by <:].Definition
quotient_open
Used by
Source code
:= open (\pi_Q @^-1` U).Used by
- mathcomp.analysis.homotopy_theory.wedge_sigT
Source code
Program Definition
quotient_topologicalType_mixin
Source code
:=Source code
@isOpenTopological.Build Q quotient_open _ _ _.
Next Obligation.
Next Obligation.
Next Obligation.
instanceSource code
DefinitionSource code
quotient_topologicalType_mixinSource code
.Lemma
pi_continuousUsed by
Source code
: continuous (\pi_Q : T -> Q).- mathcomp.analysis.homotopy_theory.wedge_sigT
Source code
Proof.
exact/continuousP. Qed.
Lemma
quotient_continuousSource code
{ : 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.
by rewrite comp_preimage; move/continuousP: pi_continuous; apply; exact: cts.
Qed.
Lemma
repr_comp_continuousUsed by
Source code
( : topologicalType) ( : T -> Z) :- mathcomp.analysis.homotopy_theory.wedge_sigT
Source code
continuous g -> {homo g : / \pi_Q a == \pi_Q b :> Q >-> a == b} ->
continuous (g \o repr : Q -> Z).
Proof.
End unpointed.
Section pointed.
Context { : ptopologicalType} { : quotType T}.
Local Notation := (quotient_topology Q0).
.
instanceSource code
DefinitionSource code
isPointedSource code
.Build Q (\pi_Q point : Q).End pointed.
End quotients.