# mathlib3documentation

topology.discrete_quotient

# Discrete quotients of a topological space. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 #

1. discrete_quotient X is the type of discrete quotients of X. It is endowed with a coercion to Type, which is defined as the quotient associated to the setoid in question, and each such quotient is endowed with the discrete topology.
2. Given S : discrete_quotient X, the projection X → S is denoted S.proj.
3. When X is compact and S : discrete_quotient X, the space S is endowed with a fintype 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 a locally connected space, the type discrete_quotient X is also endowed with an instance of a order_bot, where the bot element ⊥ is given by the connectedComponentSetoid, i.e., x ~ y means that x and y belong to the same connected component. In particular, if X is a discrete topological space, then x ~ y is equivalent (propositionally, not definitionally) to x = y.

Given f : C(X, Y), we define a predicate discrete_quotient.le_comap f A B for A : discrete_quotient X and B : discrete_quotient Y, asserting that f descends to A → B. If cond : discrete_quotient.le_comap h A B, the function A → B is obtained by discrete_quotient.map f cond.

## Theorems #

The two main results proved in this file are:

1. discrete_quotient.eq_of_forall_proj_eq which states that when X is compact, T₂, and totally disconnected, any two elements of X are equal if their projections in Q agree for all Q : discrete_quotient X.

2. discrete_quotient.exists_of_compat which states that when X is compact, then any system of elements of Q as Q : discrete_quotient X varies, which is compatible with respect to discrete_quotient.of_le, must arise from some element of X.

## Remarks #

The constructions in this file will be used to show that any profinite space is a limit of finite discrete spaces.

@[ext]
structure discrete_quotient (X : Type u_5)  :
Type u_5

The type of discrete quotients of a topological space.

Instances for discrete_quotient
theorem discrete_quotient.ext_iff {X : Type u_5} {_inst_4 : topological_space X} (x y : discrete_quotient X) :
x = y
theorem discrete_quotient.ext {X : Type u_5} {_inst_4 : topological_space X} (x y : discrete_quotient X) (h : x.to_setoid = y.to_setoid) :
x = y
def discrete_quotient.of_clopen {X : Type u_2} {A : set X} (h : is_clopen A) :

Construct a discrete quotient from a clopen set.

Equations
theorem discrete_quotient.refl {X : Type u_2} (S : discrete_quotient X) (x : X) :
theorem discrete_quotient.symm {X : Type u_2} (S : discrete_quotient X) {x y : X} :
theorem discrete_quotient.trans {X : Type u_2} (S : discrete_quotient X) {x y z : X} :
@[protected, instance]
def discrete_quotient.has_coe_to_sort {X : Type u_2}  :
(Type u_2)
Equations
@[protected, instance]
Equations
def discrete_quotient.proj {X : Type u_2} (S : discrete_quotient X) :
X S

The projection from X to the given discrete quotient.

Equations
theorem discrete_quotient.fiber_eq {X : Type u_2} (S : discrete_quotient X) (x : X) :
@[protected, instance]
@[protected, instance]
def discrete_quotient.has_inf {X : Type u_2}  :
Equations
@[protected, instance]
Equations
@[protected, instance]
def discrete_quotient.order_top {X : Type u_2}  :
Equations
@[protected, instance]
def discrete_quotient.inhabited {X : Type u_2}  :
Equations
@[protected, instance]
Equations
@[protected, instance]
def discrete_quotient.comap {X : Type u_2} {Y : Type u_3} (f : C(X, Y)) (S : discrete_quotient Y) :

Comap a discrete quotient along a continuous map.

Equations
@[simp]
theorem discrete_quotient.comap_id {X : Type u_2} (S : discrete_quotient X) :
@[simp]
theorem discrete_quotient.comap_comp {X : Type u_2} {Y : Type u_3} {Z : Type u_4} (g : C(Y, Z)) (f : C(X, Y)) (S : discrete_quotient Z) :
theorem discrete_quotient.comap_mono {X : Type u_2} {Y : Type u_3} (f : C(X, Y)) {A B : discrete_quotient Y} (h : A B) :
def discrete_quotient.of_le {X : Type u_2} {A B : discrete_quotient X} (h : A B) :

The map induced by a refinement of a discrete quotient.

Equations
@[simp]
theorem discrete_quotient.of_le_refl {X : Type u_2} {A : discrete_quotient X} :
@[simp]
theorem discrete_quotient.of_le_of_le {X : Type u_2} {A B C : discrete_quotient X} (h₁ : A B) (h₂ : B C) (x : A) :
@[simp]
theorem discrete_quotient.of_le_comp_of_le {X : Type u_2} {A B C : discrete_quotient X} (h₁ : A B) (h₂ : B C) :
theorem discrete_quotient.of_le_continuous {X : Type u_2} {A B : discrete_quotient X} (h : A B) :
@[simp]
theorem discrete_quotient.of_le_proj {X : Type u_2} {A B : discrete_quotient X} (h : A B) (x : X) :
(A.proj x) = B.proj x
@[simp]
theorem discrete_quotient.of_le_comp_proj {X : Type u_2} {A B : discrete_quotient X} (h : A B) :
@[protected, instance]
def discrete_quotient.order_bot {X : Type u_2}  :

When X is a locally connected space, there is an order_bot instance on discrete_quotient X. The bottom element is given by connected_component_setoid X

Equations
@[simp]
theorem discrete_quotient.proj_bot_eq {X : Type u_2} {x y : X} :
theorem discrete_quotient.proj_bot_inj {X : Type u_2} {x y : X} :
.proj x = .proj y x = y
def discrete_quotient.le_comap {X : Type u_2} {Y : Type u_3} (f : C(X, Y)) (A : discrete_quotient X) (B : discrete_quotient Y) :
Prop

Given f : C(X, Y), le_comap cont A B is defined as A ≤ B.comap f. Mathematically this means that f descends to a morphism A → B.

Equations
@[simp]
theorem discrete_quotient.le_comap_id_iff {X : Type u_2} {A A' : discrete_quotient X} :
A A'
theorem discrete_quotient.le_comap.comp {X : Type u_2} {Y : Type u_3} {Z : Type u_4} {f : C(X, Y)} {A : discrete_quotient X} {B : discrete_quotient Y} {g : C(Y, Z)} {C : discrete_quotient Z} :
A C
theorem discrete_quotient.le_comap.mono {X : Type u_2} {Y : Type u_3} {f : C(X, Y)} {A A' : discrete_quotient X} {B B' : discrete_quotient Y} (h : B) (hA : A' A) (hB : B B') :
B'
def discrete_quotient.map {X : Type u_2} {Y : Type u_3} {A : discrete_quotient X} {B : discrete_quotient Y} (f : C(X, Y)) (cond : B) :

Map a discrete quotient along a continuous map.

Equations
• cond = cond
theorem discrete_quotient.map_continuous {X : Type u_2} {Y : Type u_3} {f : C(X, Y)} {A : discrete_quotient X} {B : discrete_quotient Y} (cond : B) :
@[simp]
theorem discrete_quotient.map_comp_proj {X : Type u_2} {Y : Type u_3} {f : C(X, Y)} {A : discrete_quotient X} {B : discrete_quotient Y} (cond : B) :
cond A.proj = B.proj f
@[simp]
theorem discrete_quotient.map_proj {X : Type u_2} {Y : Type u_3} {f : C(X, Y)} {A : discrete_quotient X} {B : discrete_quotient Y} (cond : B) (x : X) :
cond (A.proj x) = B.proj (f x)
@[simp]
theorem discrete_quotient.map_id {X : Type u_2} {A : discrete_quotient X} :
@[simp]
theorem discrete_quotient.map_comp {X : Type u_2} {Y : Type u_3} {Z : Type u_4} {f : C(X, Y)} {A : discrete_quotient X} {B : discrete_quotient Y} {g : C(Y, Z)} {C : discrete_quotient Z} (h1 : C) (h2 : B) :
_ =
@[simp]
theorem discrete_quotient.of_le_map {X : Type u_2} {Y : Type u_3} {f : C(X, Y)} {A : discrete_quotient X} {B B' : discrete_quotient Y} (cond : B) (h : B B') (a : A) :
cond a) =
@[simp]
theorem discrete_quotient.of_le_comp_map {X : Type u_2} {Y : Type u_3} {f : C(X, Y)} {A : discrete_quotient X} {B B' : discrete_quotient Y} (cond : B) (h : B B') :
@[simp]
theorem discrete_quotient.map_of_le {X : Type u_2} {Y : Type u_3} {f : C(X, Y)} {A A' : discrete_quotient X} {B : discrete_quotient Y} (cond : B) (h : A' A) (c : A') :
cond =
@[simp]
theorem discrete_quotient.map_comp_of_le {X : Type u_2} {Y : Type u_3} {f : C(X, Y)} {A A' : discrete_quotient X} {B : discrete_quotient Y} (cond : B) (h : A' A) :
theorem discrete_quotient.eq_of_forall_proj_eq {X : Type u_2} [t2_space X] [disc : totally_disconnected_space X] {x y : X} (h : (Q : , Q.proj x = Q.proj y) :
x = y
theorem discrete_quotient.fiber_subset_of_le {X : Type u_2} {A B : discrete_quotient X} (h : A B) (a : A) :
theorem discrete_quotient.exists_of_compat {X : Type u_2} (Qs : Π (Q : , Q) (compat : (A B : (h : A B), (Qs A) = Qs B) :
(x : X), (Q : , Q.proj x = Qs Q
@[protected, instance]
def discrete_quotient.finite {X : Type u_2} (S : discrete_quotient X)  :
def locally_constant.discrete_quotient {α : Type u_1} {X : Type u_2} (f : α) :

Any locally constant function induces a discrete quotient.

Equations
def locally_constant.lift {α : Type u_1} {X : Type u_2} (f : α) :

The (locally constant) function from the discrete quotient associated to a locally constant function.

Equations
@[simp]
theorem locally_constant.lift_comp_proj {α : Type u_1} {X : Type u_2} (f : α) :