mathlib documentation

topology.discrete_quotient

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 #

  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 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:

  1. discrete_quotient.eq_of_proj_eq which states that when X is compact, t2 and totally disconnected, any two elements of X agree 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_1) [topological_space X] :
Type u_1

The type of discrete quotients of a topological space.

Instances for discrete_quotient
theorem discrete_quotient.ext_iff {X : Type u_1} {_inst_1 : topological_space X} (x y : discrete_quotient X) :
x = y x.rel = y.rel
theorem discrete_quotient.ext {X : Type u_1} {_inst_1 : topological_space X} (x y : discrete_quotient X) (h : x.rel = y.rel) :
x = y
def discrete_quotient.of_clopen {X : Type u_1} [topological_space X] {A : set X} (h : is_clopen A) :

Construct a discrete quotient from a clopen set.

Equations
theorem discrete_quotient.refl {X : Type u_1} [topological_space X] (S : discrete_quotient X) (x : X) :
S.rel x x
theorem discrete_quotient.symm {X : Type u_1} [topological_space X] (S : discrete_quotient X) (x y : X) :
S.rel x yS.rel y x
theorem discrete_quotient.trans {X : Type u_1} [topological_space X] (S : discrete_quotient X) (x y z : X) :
S.rel x yS.rel y zS.rel x z

The setoid whose quotient yields the discrete quotient.

Equations
@[protected, instance]
Equations
def discrete_quotient.proj {X : Type u_1} [topological_space X] (S : discrete_quotient X) :
X → S

The projection from X to the given discrete quotient.

Equations
theorem discrete_quotient.fiber_eq {X : Type u_1} [topological_space X] (S : discrete_quotient X) (x : X) :
S.proj ⁻¹' {S.proj x} = set_of (S.rel x)
theorem discrete_quotient.fiber_open {X : Type u_1} [topological_space X] (S : discrete_quotient X) (A : set S) :
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
def discrete_quotient.comap {X : Type u_1} [topological_space X] (S : discrete_quotient X) {Y : Type u_2} [topological_space Y] {f : Y → X} (cont : continuous f) :

Comap a discrete quotient along a continuous map.

Equations
@[simp]
@[simp]
theorem discrete_quotient.comap_comp {X : Type u_1} [topological_space X] (S : discrete_quotient X) {Y : Type u_2} [topological_space Y] {f : Y → X} (cont : continuous f) {Z : Type u_3} [topological_space Z] {g : Z → Y} (cont' : continuous g) :
S.comap _ = (S.comap cont).comap cont'
theorem discrete_quotient.comap_mono {X : Type u_1} [topological_space X] {Y : Type u_2} [topological_space Y] {f : Y → X} (cont : continuous f) {A B : discrete_quotient X} (h : A B) :
A.comap cont B.comap cont
def discrete_quotient.of_le {X : Type u_1} [topological_space X] {A B : discrete_quotient X} (h : A B) :
A → B

The map induced by a refinement of a discrete quotient.

Equations
@[simp]
@[simp]
theorem discrete_quotient.of_le_proj_apply {X : Type u_1} [topological_space X] {A B : discrete_quotient X} (h : A B) (x : X) :
@[protected, instance]

When X is discrete, there is a order_bot instance on discrete_quotient X

Equations
def discrete_quotient.le_comap {X : Type u_1} [topological_space X] {Y : Type u_2} [topological_space Y] {f : Y → X} (cont : continuous f) (A : discrete_quotient Y) (B : discrete_quotient X) :
Prop

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
theorem discrete_quotient.le_comap_comp {X : Type u_1} [topological_space X] {Y : Type u_2} [topological_space Y] {f : Y → X} {cont : continuous f} {A : discrete_quotient Y} {B : discrete_quotient X} {Z : Type u_3} [topological_space Z] {g : Z → Y} {cont' : continuous g} {C : discrete_quotient Z} :
theorem discrete_quotient.le_comap_trans {X : Type u_1} [topological_space X] {Y : Type u_2} [topological_space Y] {f : Y → X} {cont : continuous f} {A : discrete_quotient Y} {B C : discrete_quotient X} :
def discrete_quotient.map {X : Type u_1} [topological_space X] {Y : Type u_2} [topological_space Y] {f : Y → X} {cont : continuous f} {A : discrete_quotient Y} {B : discrete_quotient X} (cond : discrete_quotient.le_comap cont A B) :
A → B

Map a discrete quotient along a continuous map.

Equations
theorem discrete_quotient.map_continuous {X : Type u_1} [topological_space X] {Y : Type u_2} [topological_space Y] {f : Y → X} {cont : continuous f} {A : discrete_quotient Y} {B : discrete_quotient X} (cond : discrete_quotient.le_comap cont A B) :
@[simp]
theorem discrete_quotient.map_proj {X : Type u_1} [topological_space X] {Y : Type u_2} [topological_space Y] {f : Y → X} {cont : continuous f} {A : discrete_quotient Y} {B : discrete_quotient X} (cond : discrete_quotient.le_comap cont A B) :
@[simp]
theorem discrete_quotient.map_proj_apply {X : Type u_1} [topological_space X] {Y : Type u_2} [topological_space Y] {f : Y → X} {cont : continuous f} {A : discrete_quotient Y} {B : discrete_quotient X} (cond : discrete_quotient.le_comap cont A B) (y : Y) :
discrete_quotient.map cond (A.proj y) = B.proj (f y)
@[simp]
theorem discrete_quotient.map_comp {X : Type u_1} [topological_space X] {Y : Type u_2} [topological_space Y] {f : Y → X} {cont : continuous f} {A : discrete_quotient Y} {B : discrete_quotient X} {Z : Type u_3} [topological_space Z] {g : Z → Y} {cont' : continuous g} {C : discrete_quotient Z} (h1 : discrete_quotient.le_comap cont' C A) (h2 : discrete_quotient.le_comap cont A B) :
@[simp]
theorem discrete_quotient.of_le_map {X : Type u_1} [topological_space X] {Y : Type u_2} [topological_space Y] {f : Y → X} {cont : continuous f} {A : discrete_quotient Y} {B C : discrete_quotient X} (cond : discrete_quotient.le_comap cont A B) (h : B C) :
@[simp]
theorem discrete_quotient.of_le_map_apply {X : Type u_1} [topological_space X] {Y : Type u_2} [topological_space Y] {f : Y → X} {cont : continuous f} {A : discrete_quotient Y} {B C : discrete_quotient X} (cond : discrete_quotient.le_comap cont A B) (h : B C) (a : A) :
@[simp]
theorem discrete_quotient.map_of_le {X : Type u_1} [topological_space X] {Y : Type u_2} [topological_space Y] {f : Y → X} {cont : continuous f} {A : discrete_quotient Y} {B : discrete_quotient X} {C : discrete_quotient Y} (cond : discrete_quotient.le_comap cont A B) (h : C A) :
@[simp]
theorem discrete_quotient.map_of_le_apply {X : Type u_1} [topological_space X] {Y : Type u_2} [topological_space Y] {f : Y → X} {cont : continuous f} {A : discrete_quotient Y} {B : discrete_quotient X} {C : discrete_quotient Y} (cond : discrete_quotient.le_comap cont A B) (h : C A) (c : C) :
theorem discrete_quotient.eq_of_proj_eq {X : Type u_1} [topological_space X] [t2_space X] [compact_space X] [disc : totally_disconnected_space X] {x y : X} :
(∀ (Q : discrete_quotient X), Q.proj x = Q.proj y)x = y
theorem discrete_quotient.fiber_le_of_le {X : Type u_1} [topological_space X] {A B : discrete_quotient X} (h : A B) (a : A) :
theorem discrete_quotient.exists_of_compat {X : Type u_1} [topological_space X] [compact_space X] (Qs : Π (Q : discrete_quotient X), Q) (compat : ∀ (A B : discrete_quotient X) (h : A B), discrete_quotient.of_le h (Qs A) = Qs B) :
∃ (x : X), ∀ (Q : discrete_quotient X), Q.proj x = Qs Q
@[protected, instance]
noncomputable def discrete_quotient.fintype {X : Type u_1} [topological_space X] (S : discrete_quotient X) [compact_space X] :
Equations
def locally_constant.discrete_quotient {X : Type u_1} [topological_space X] {α : Type u_2} (f : locally_constant X α) :

Any locally constant function induces a discrete quotient.

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

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

Equations

A locally constant version of locally_constant.lift.

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