mathlib3 documentation

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 #

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.
Given S : discrete_quotient X, the projection X → S is denoted S.proj.
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:

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.
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) [topological_space X] :

Type u_5

to_setoid : setoid X
is_open_set_of_rel : ∀ (x : X), is_open (set_of (self.to_setoid.rel x))

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 ↔ x.to_setoid = y.to_setoid

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} [topological_space X] {A : set X} (h : is_clopen A) :

discrete_quotient X

Construct a discrete quotient from a clopen set.

Equations

discrete_quotient.of_clopen h = {to_setoid := {r := λ (x y : X), x ∈ A ↔ y ∈ A, iseqv := _}, is_open_set_of_rel := _}

theorem discrete_quotient.refl {X : Type u_2} [topological_space X] (S : discrete_quotient X) (x : X) :

S.to_setoid.rel x x

theorem discrete_quotient.symm {X : Type u_2} [topological_space X] (S : discrete_quotient X) {x y : X} :

S.to_setoid.rel x y → S.to_setoid.rel y x

theorem discrete_quotient.trans {X : Type u_2} [topological_space X] (S : discrete_quotient X) {x y z : X} :

S.to_setoid.rel x y → S.to_setoid.rel y z → S.to_setoid.rel x z

@[protected, instance]

def discrete_quotient.has_coe_to_sort {X : Type u_2} [topological_space X] :

has_coe_to_sort (discrete_quotient X) (Type u_2)

Equations

discrete_quotient.has_coe_to_sort = {coe := λ (S : discrete_quotient X), quotient S.to_setoid}

@[protected, instance]

def discrete_quotient.topological_space {X : Type u_2} [topological_space X] (S : discrete_quotient X) :

topological_space ↥S

Equations

S.topological_space = quotient.topological_space

def discrete_quotient.proj {X : Type u_2} [topological_space X] (S : discrete_quotient X) :

The projection from X to the given discrete quotient.

Equations

S.proj = quotient.mk'

theorem discrete_quotient.fiber_eq {X : Type u_2} [topological_space X] (S : discrete_quotient X) (x : X) :

S.proj ⁻¹' {S.proj x} = set_of (S.to_setoid.rel x)

theorem discrete_quotient.proj_surjective {X : Type u_2} [topological_space X] (S : discrete_quotient X) :

function.surjective S.proj

theorem discrete_quotient.proj_quotient_map {X : Type u_2} [topological_space X] (S : discrete_quotient X) :

quotient_map S.proj

theorem discrete_quotient.proj_continuous {X : Type u_2} [topological_space X] (S : discrete_quotient X) :

continuous S.proj

@[protected, instance]

def discrete_quotient.discrete_topology {X : Type u_2} [topological_space X] (S : discrete_quotient X) :

discrete_topology ↥S

theorem discrete_quotient.proj_is_locally_constant {X : Type u_2} [topological_space X] (S : discrete_quotient X) :

is_locally_constant S.proj

theorem discrete_quotient.is_clopen_preimage {X : Type u_2} [topological_space X] (S : discrete_quotient X) (A : set ↥S) :

is_clopen (S.proj ⁻¹' A)

theorem discrete_quotient.is_open_preimage {X : Type u_2} [topological_space X] (S : discrete_quotient X) (A : set ↥S) :

is_open (S.proj ⁻¹' A)

theorem discrete_quotient.is_closed_preimage {X : Type u_2} [topological_space X] (S : discrete_quotient X) (A : set ↥S) :

is_closed (S.proj ⁻¹' A)

theorem discrete_quotient.is_clopen_set_of_rel {X : Type u_2} [topological_space X] (S : discrete_quotient X) (x : X) :

is_clopen (set_of (S.to_setoid.rel x))

@[protected, instance]

def discrete_quotient.has_inf {X : Type u_2} [topological_space X] :

has_inf (discrete_quotient X)

Equations

discrete_quotient.has_inf = {inf := λ (S₁ S₂ : discrete_quotient X), {to_setoid := S₁.to_setoid ⊓ S₂.to_setoid, is_open_set_of_rel := _}}

@[protected, instance]

def discrete_quotient.semilattice_inf {X : Type u_2} [topological_space X] :

semilattice_inf (discrete_quotient X)

Equations

discrete_quotient.semilattice_inf = function.injective.semilattice_inf discrete_quotient.to_setoid discrete_quotient.ext discrete_quotient.semilattice_inf._proof_1

@[protected, instance]

def discrete_quotient.order_top {X : Type u_2} [topological_space X] :

order_top (discrete_quotient X)

Equations

discrete_quotient.order_top = {top := {to_setoid := ⊤, is_open_set_of_rel := _}, le_top := _}

@[protected, instance]

def discrete_quotient.inhabited {X : Type u_2} [topological_space X] :

inhabited (discrete_quotient X)

Equations

discrete_quotient.inhabited = {default := ⊤}

@[protected, instance]

def discrete_quotient.inhabited_quotient {X : Type u_2} [topological_space X] (S : discrete_quotient X) [inhabited X] :

Equations

S.inhabited_quotient = {default := S.proj inhabited.default}

@[protected, instance]

def discrete_quotient.nonempty {X : Type u_2} [topological_space X] (S : discrete_quotient X) [nonempty X] :

def discrete_quotient.comap {X : Type u_2} {Y : Type u_3} [topological_space X] [topological_space Y] (f : C(X, Y)) (S : discrete_quotient Y) :

discrete_quotient X

Comap a discrete quotient along a continuous map.

Equations

discrete_quotient.comap f S = {to_setoid := setoid.comap ⇑f S.to_setoid, is_open_set_of_rel := _}

@[simp]

theorem discrete_quotient.comap_id {X : Type u_2} [topological_space X] (S : discrete_quotient X) :

discrete_quotient.comap (continuous_map.id X) S = S

@[simp]

theorem discrete_quotient.comap_comp {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [topological_space X] [topological_space Y] [topological_space Z] (g : C(Y, Z)) (f : C(X, Y)) (S : discrete_quotient Z) :

discrete_quotient.comap (g.comp f) S = discrete_quotient.comap f (discrete_quotient.comap g S)

theorem discrete_quotient.comap_mono {X : Type u_2} {Y : Type u_3} [topological_space X] [topological_space Y] (f : C(X, Y)) {A B : discrete_quotient Y} (h : A ≤ B) :

discrete_quotient.comap f A ≤ discrete_quotient.comap f B

def discrete_quotient.of_le {X : Type u_2} [topological_space X] {A B : discrete_quotient X} (h : A ≤ B) :

The map induced by a refinement of a discrete quotient.

Equations

discrete_quotient.of_le h = quotient.map' (λ (x : X), x) h

@[simp]

theorem discrete_quotient.of_le_refl {X : Type u_2} [topological_space X] {A : discrete_quotient X} :

discrete_quotient.of_le _ = id

theorem discrete_quotient.of_le_refl_apply {X : Type u_2} [topological_space X] {A : discrete_quotient X} (a : ↥A) :

discrete_quotient.of_le _ a = a

@[simp]

theorem discrete_quotient.of_le_of_le {X : Type u_2} [topological_space X] {A B C : discrete_quotient X} (h₁ : A ≤ B) (h₂ : B ≤ C) (x : ↥A) :

discrete_quotient.of_le h₂ (discrete_quotient.of_le h₁ x) = discrete_quotient.of_le _ x

@[simp]

theorem discrete_quotient.of_le_comp_of_le {X : Type u_2} [topological_space X] {A B C : discrete_quotient X} (h₁ : A ≤ B) (h₂ : B ≤ C) :

discrete_quotient.of_le h₂ ∘ discrete_quotient.of_le h₁ = discrete_quotient.of_le _

theorem discrete_quotient.of_le_continuous {X : Type u_2} [topological_space X] {A B : discrete_quotient X} (h : A ≤ B) :

continuous (discrete_quotient.of_le h)

@[simp]

theorem discrete_quotient.of_le_proj {X : Type u_2} [topological_space X] {A B : discrete_quotient X} (h : A ≤ B) (x : X) :

discrete_quotient.of_le h (A.proj x) = B.proj x

@[simp]

theorem discrete_quotient.of_le_comp_proj {X : Type u_2} [topological_space X] {A B : discrete_quotient X} (h : A ≤ B) :

discrete_quotient.of_le h ∘ A.proj = B.proj

@[protected, instance]

def discrete_quotient.order_bot {X : Type u_2} [topological_space X] [locally_connected_space X] :

order_bot (discrete_quotient X)

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

discrete_quotient.order_bot = {bot := {to_setoid := connected_component_setoid X _inst_1, is_open_set_of_rel := _}, bot_le := _}

@[simp]

theorem discrete_quotient.proj_bot_eq {X : Type u_2} [topological_space X] [locally_connected_space X] {x y : X} :

⊥.proj x = ⊥.proj y ↔ connected_component x = connected_component y

theorem discrete_quotient.proj_bot_inj {X : Type u_2} [topological_space X] [discrete_topology X] {x y : X} :

⊥.proj x = ⊥.proj y ↔ x = y

theorem discrete_quotient.proj_bot_injective {X : Type u_2} [topological_space X] [discrete_topology X] :

function.injective ⊥.proj

theorem discrete_quotient.proj_bot_bijective {X : Type u_2} [topological_space X] [discrete_topology X] :

function.bijective ⊥.proj

def discrete_quotient.le_comap {X : Type u_2} {Y : Type u_3} [topological_space X] [topological_space Y] (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

discrete_quotient.le_comap f A B = (A ≤ discrete_quotient.comap f B)

theorem discrete_quotient.le_comap_id {X : Type u_2} [topological_space X] (A : discrete_quotient X) :

discrete_quotient.le_comap (continuous_map.id X) A A

@[simp]

theorem discrete_quotient.le_comap_id_iff {X : Type u_2} [topological_space X] {A A' : discrete_quotient X} :

discrete_quotient.le_comap (continuous_map.id X) A A' ↔ A ≤ A'

theorem discrete_quotient.le_comap.comp {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [topological_space X] [topological_space Y] [topological_space Z] {f : C(X, Y)} {A : discrete_quotient X} {B : discrete_quotient Y} {g : C(Y, Z)} {C : discrete_quotient Z} :

discrete_quotient.le_comap g B C → discrete_quotient.le_comap f A B → discrete_quotient.le_comap (g.comp f) A C

theorem discrete_quotient.le_comap.mono {X : Type u_2} {Y : Type u_3} [topological_space X] [topological_space Y] {f : C(X, Y)} {A A' : discrete_quotient X} {B B' : discrete_quotient Y} (h : discrete_quotient.le_comap f A B) (hA : A' ≤ A) (hB : B ≤ B') :

discrete_quotient.le_comap f A' B'

def discrete_quotient.map {X : Type u_2} {Y : Type u_3} [topological_space X] [topological_space Y] {A : discrete_quotient X} {B : discrete_quotient Y} (f : C(X, Y)) (cond : discrete_quotient.le_comap f A B) :

Map a discrete quotient along a continuous map.

Equations

discrete_quotient.map f cond = quotient.map' ⇑f cond

theorem discrete_quotient.map_continuous {X : Type u_2} {Y : Type u_3} [topological_space X] [topological_space Y] {f : C(X, Y)} {A : discrete_quotient X} {B : discrete_quotient Y} (cond : discrete_quotient.le_comap f A B) :

continuous (discrete_quotient.map f cond)

@[simp]

theorem discrete_quotient.map_comp_proj {X : Type u_2} {Y : Type u_3} [topological_space X] [topological_space Y] {f : C(X, Y)} {A : discrete_quotient X} {B : discrete_quotient Y} (cond : discrete_quotient.le_comap f A B) :

discrete_quotient.map f cond ∘ A.proj = B.proj ∘ ⇑f

@[simp]

theorem discrete_quotient.map_proj {X : Type u_2} {Y : Type u_3} [topological_space X] [topological_space Y] {f : C(X, Y)} {A : discrete_quotient X} {B : discrete_quotient Y} (cond : discrete_quotient.le_comap f A B) (x : X) :

discrete_quotient.map f cond (A.proj x) = B.proj (⇑f x)

@[simp]

theorem discrete_quotient.map_id {X : Type u_2} [topological_space X] {A : discrete_quotient X} :

discrete_quotient.map (continuous_map.id X) _ = id

@[simp]

theorem discrete_quotient.map_comp {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [topological_space X] [topological_space Y] [topological_space Z] {f : C(X, Y)} {A : discrete_quotient X} {B : discrete_quotient Y} {g : C(Y, Z)} {C : discrete_quotient Z} (h1 : discrete_quotient.le_comap g B C) (h2 : discrete_quotient.le_comap f A B) :

discrete_quotient.map (g.comp f) _ = discrete_quotient.map g h1 ∘ discrete_quotient.map f h2

@[simp]

theorem discrete_quotient.of_le_map {X : Type u_2} {Y : Type u_3} [topological_space X] [topological_space Y] {f : C(X, Y)} {A : discrete_quotient X} {B B' : discrete_quotient Y} (cond : discrete_quotient.le_comap f A B) (h : B ≤ B') (a : ↥A) :

discrete_quotient.of_le h (discrete_quotient.map f cond a) = discrete_quotient.map f _ a

@[simp]

theorem discrete_quotient.of_le_comp_map {X : Type u_2} {Y : Type u_3} [topological_space X] [topological_space Y] {f : C(X, Y)} {A : discrete_quotient X} {B B' : discrete_quotient Y} (cond : discrete_quotient.le_comap f A B) (h : B ≤ B') :

discrete_quotient.of_le h ∘ discrete_quotient.map f cond = discrete_quotient.map f _

@[simp]

theorem discrete_quotient.map_of_le {X : Type u_2} {Y : Type u_3} [topological_space X] [topological_space Y] {f : C(X, Y)} {A A' : discrete_quotient X} {B : discrete_quotient Y} (cond : discrete_quotient.le_comap f A B) (h : A' ≤ A) (c : ↥A') :

discrete_quotient.map f cond (discrete_quotient.of_le h c) = discrete_quotient.map f _ c

@[simp]

theorem discrete_quotient.map_comp_of_le {X : Type u_2} {Y : Type u_3} [topological_space X] [topological_space Y] {f : C(X, Y)} {A A' : discrete_quotient X} {B : discrete_quotient Y} (cond : discrete_quotient.le_comap f A B) (h : A' ≤ A) :

discrete_quotient.map f cond ∘ discrete_quotient.of_le h = discrete_quotient.map f _

theorem discrete_quotient.eq_of_forall_proj_eq {X : Type u_2} [topological_space X] [t2_space X] [compact_space X] [disc : totally_disconnected_space X] {x y : X} (h : ∀ (Q : discrete_quotient X), Q.proj x = Q.proj y) :

x = y

theorem discrete_quotient.fiber_subset_of_le {X : Type u_2} [topological_space X] {A B : discrete_quotient X} (h : A ≤ B) (a : ↥A) :

A.proj ⁻¹' {a} ⊆ B.proj ⁻¹' {discrete_quotient.of_le h a}

theorem discrete_quotient.exists_of_compat {X : Type u_2} [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]

def discrete_quotient.finite {X : Type u_2} [topological_space X] (S : discrete_quotient X) [compact_space X] :

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

discrete_quotient X

Any locally constant function induces a discrete quotient.

Equations

f.discrete_quotient = {to_setoid := setoid.comap ⇑f ⊥, is_open_set_of_rel := _}

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

locally_constant ↥(f.discrete_quotient) α

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

Equations

f.lift = {to_fun := λ (a : ↥(f.discrete_quotient)), quotient.lift_on' a ⇑f _, is_locally_constant := _}

@[simp]

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

⇑(f.lift) ∘ f.discrete_quotient.proj = ⇑f