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