Discrete quotients of a topological space. #
This file defines the type of discrete quotients of a topological space,
denoted discrete_quotient X
. To avoid quantifying over types, we model such
quotients as setoids whose equivalence classes are clopen.
Definitions #
discrete_quotient X
is the type of discrete quotients ofX
. It is endowed with a coercion toType
, which is defined as the quotient associated to the setoid in question, and each such quotient is endowed with the discrete topology.- Given
S : discrete_quotient X
, the projectionX → S
is denotedS.proj
. - When
X
is compact andS : discrete_quotient X
, the spaceS
is endowed with afintype
instance.
Order structure #
The type discrete_quotient X
is endowed with an instance of a semilattice_inf
with order_top
.
The partial ordering A ≤ B
mathematically means that B.proj
factors through A.proj
.
The top element ⊤
is the trivial quotient, meaning that every element of X
is collapsed
to a point. Given h : A ≤ B
, the map A → B
is discrete_quotient.of_le h
.
Whenever X
is discrete, the type discrete_quotient X
is also endowed with an instance of a
semilattice_inf
with order_bot
, where the bot element ⊥
is X
itself.
Given f : X → Y
and h : continuous f
, we define a predicate le_comap h A B
for
A : discrete_quotient X
and B : discrete_quotient Y
, asserting that f
descends to A → B
.
If cond : le_comap h A B
, the function A → B
is obtained by discrete_quotient.map cond
.
Theorems #
The two main results proved in this file are:
discrete_quotient.eq_of_proj_eq
which states that whenX
is compact, t2 and totally disconnected, any two elements ofX
agree if their projections inQ
agree for allQ : discrete_quotient X
.discrete_quotient.exists_of_compat
which states that whenX
is compact, then any system of elements ofQ
asQ : discrete_quotient X
varies, which is compatible with respect todiscrete_quotient.of_le
, must arise from some element ofX
.
Remarks #
The constructions in this file will be used to show that any profinite space is a limit of finite discrete spaces.
- rel : X → X → Prop
- equiv : equivalence self.rel
- clopen : ∀ (x : X), is_clopen (set_of (self.rel x))
The type of discrete quotients of a topological space.
Instances for discrete_quotient
Construct a discrete quotient from a clopen set.
The setoid whose quotient yields the discrete quotient.
Equations
- discrete_quotient.has_coe_to_sort = {coe := λ (S : discrete_quotient X), quotient S.setoid}
Equations
The projection from X
to the given discrete quotient.
Equations
Equations
- discrete_quotient.partial_order = {le := λ (A B : discrete_quotient X), ∀ (x y : X), A.rel x y → B.rel x y, lt := preorder.lt._default (λ (A B : discrete_quotient X), ∀ (x y : X), A.rel x y → B.rel x y), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _}
Equations
- discrete_quotient.semilattice_inf = {inf := λ (A B : discrete_quotient X), {rel := λ (x y : X), A.rel x y ∧ B.rel x y, equiv := _, clopen := _}, le := partial_order.le discrete_quotient.partial_order, lt := partial_order.lt discrete_quotient.partial_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, inf_le_left := _, inf_le_right := _, le_inf := _}
Equations
Comap a discrete quotient along a continuous map.
The map induced by a refinement of a discrete quotient.
Equations
- discrete_quotient.of_le h = λ (a : ↥A), quotient.lift_on' a (λ (x : X), B.proj x) _
When X is discrete, there is a order_bot
instance on discrete_quotient X
Given cont : continuous f
, le_comap cont A B
is defined as A ≤ B.comap f
.
Mathematically this means that f
descends to a morphism A → B
.
Equations
- discrete_quotient.le_comap cont A B = (A ≤ B.comap cont)
Map a discrete quotient along a continuous map.
Equations
- discrete_quotient.map cond = quotient.map' f cond
Any locally constant function induces a discrete quotient.
The function from the discrete quotient associated to a locally constant function.
Equations
- f.lift = λ (a : ↥(f.discrete_quotient)), quotient.lift_on' a ⇑f _
A locally constant version of locally_constant.lift
.
Equations
- f.locally_constant_lift = {to_fun := f.lift, is_locally_constant := _}