# Documentation

Mathlib.Topology.DiscreteQuotient

# Discrete quotients of a topological space. #

This file defines the type of discrete quotients of a topological space, denoted DiscreteQuotient X. To avoid quantifying over types, we model such quotients as setoids whose equivalence classes are clopen.

## Definitions #

1. DiscreteQuotient 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 : DiscreteQuotient X, the projection X → S is denoted S.proj.
3. When X is compact and S : DiscreteQuotient X, the space S is endowed with a Fintype instance.

## Order structure #

The type DiscreteQuotient X is endowed with an instance of a SemilatticeInf with OrderTop. 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 DiscreteQuotient.ofLE h.

Whenever X is a locally connected space, the type DiscreteQuotient X is also endowed with an instance of an OrderBot, 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 DiscreteQuotient.LEComap f A B for A : DiscreteQuotient X and B : DiscreteQuotient Y, asserting that f descends to A → B. If cond : DiscreteQuotient.LEComap h A B, the function A → B is obtained by DiscreteQuotient.map f cond.

## Theorems #

The two main results proved in this file are:

1. DiscreteQuotient.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 : DiscreteQuotient X.

2. DiscreteQuotient.exists_of_compat which states that when X is compact, then any system of elements of Q as Q : DiscreteQuotient X varies, which is compatible with respect to DiscreteQuotient.ofLE, 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.

theorem DiscreteQuotient.ext_iff {X : Type u_5} :
∀ {inst : } (x y : ), x = y Setoid.r = Setoid.r
theorem DiscreteQuotient.ext {X : Type u_5} :
∀ {inst : } (x y : ), Setoid.r = Setoid.rx = y
structure DiscreteQuotient (X : Type u_5) [] extends :
Type u_5
• r : XXProp
• iseqv : Equivalence Setoid.r
• isOpen_setOf_rel : ∀ (x : X), IsOpen (setOf (Setoid.Rel s.toSetoid x))

For every point x, the set { y | Rel x y } is a clopen set.

The type of discrete quotients of a topological space.

Instances For
theorem DiscreteQuotient.toSetoid_injective {X : Type u_2} [] :
Function.Injective DiscreteQuotient.toSetoid
def DiscreteQuotient.ofClopen {X : Type u_2} [] {A : Set X} (h : ) :

Construct a discrete quotient from a clopen set.

Instances For
theorem DiscreteQuotient.refl {X : Type u_2} [] (S : ) (x : X) :
Setoid.Rel S.toSetoid x x
theorem DiscreteQuotient.symm {X : Type u_2} [] (S : ) (x : X) (y : X) :
Setoid.Rel S.toSetoid x ySetoid.Rel S.toSetoid y x
theorem DiscreteQuotient.trans {X : Type u_2} [] (S : ) (x : X) (y : X) (z : X) :
Setoid.Rel S.toSetoid x ySetoid.Rel S.toSetoid y zSetoid.Rel S.toSetoid x z
def DiscreteQuotient.proj {X : Type u_2} [] (S : ) :
XQuotient S.toSetoid

The projection from X to the given discrete quotient.

Instances For
theorem DiscreteQuotient.fiber_eq {X : Type u_2} [] (S : ) (x : X) :
= setOf (Setoid.Rel S.toSetoid x)
theorem DiscreteQuotient.proj_surjective {X : Type u_2} [] (S : ) :
theorem DiscreteQuotient.proj_quotientMap {X : Type u_2} [] (S : ) :
theorem DiscreteQuotient.proj_continuous {X : Type u_2} [] (S : ) :
theorem DiscreteQuotient.isClopen_preimage {X : Type u_2} [] (S : ) (A : Set (Quotient S.toSetoid)) :
theorem DiscreteQuotient.isOpen_preimage {X : Type u_2} [] (S : ) (A : Set (Quotient S.toSetoid)) :
theorem DiscreteQuotient.isClosed_preimage {X : Type u_2} [] (S : ) (A : Set (Quotient S.toSetoid)) :
theorem DiscreteQuotient.isClopen_setOf_rel {X : Type u_2} [] (S : ) (x : X) :
IsClopen (setOf (Setoid.Rel S.toSetoid x))
instance DiscreteQuotient.inhabitedQuotient {X : Type u_2} [] (S : ) [] :
Inhabited (Quotient S.toSetoid)
instance DiscreteQuotient.instNonemptyQuotientToSetoid {X : Type u_2} [] (S : ) [] :
Nonempty (Quotient S.toSetoid)

The quotient by ⊤ : DiscreteQuotient X is a Subsingleton.

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

Comap a discrete quotient along a continuous map.

Instances For
@[simp]
theorem DiscreteQuotient.comap_id {X : Type u_2} [] (S : ) :
@[simp]
theorem DiscreteQuotient.comap_comp {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [] [] [] (g : C(Y, Z)) (f : C(X, Y)) (S : ) :
theorem DiscreteQuotient.comap_mono {X : Type u_2} {Y : Type u_3} [] [] (f : C(X, Y)) {A : } {B : } (h : A B) :
def DiscreteQuotient.ofLE {X : Type u_2} [] {A : } {B : } (h : A B) :
Quotient A.toSetoidQuotient B.toSetoid

The map induced by a refinement of a discrete quotient.

Instances For
@[simp]
theorem DiscreteQuotient.ofLE_refl {X : Type u_2} [] {A : } :
theorem DiscreteQuotient.ofLE_refl_apply {X : Type u_2} [] {A : } (a : Quotient A.toSetoid) :
@[simp]
theorem DiscreteQuotient.ofLE_ofLE {X : Type u_2} [] {A : } {B : } {C : } (h₁ : A B) (h₂ : B C) (x : Quotient A.toSetoid) :
@[simp]
theorem DiscreteQuotient.ofLE_comp_ofLE {X : Type u_2} [] {A : } {B : } {C : } (h₁ : A B) (h₂ : B C) :
theorem DiscreteQuotient.ofLE_continuous {X : Type u_2} [] {A : } {B : } (h : A B) :
@[simp]
theorem DiscreteQuotient.ofLE_proj {X : Type u_2} [] {A : } {B : } (h : A B) (x : X) :
@[simp]
theorem DiscreteQuotient.ofLE_comp_proj {X : Type u_2} [] {A : } {B : } (h : A B) :

When X is a locally connected space, there is an OrderBot instance on DiscreteQuotient X. The bottom element is given by connectedComponentSetoid X

@[simp]
theorem DiscreteQuotient.proj_bot_eq {X : Type u_2} [] {x : X} {y : X} :
theorem DiscreteQuotient.proj_bot_inj {X : Type u_2} [] [] {x : X} {y : X} :
x = y
def DiscreteQuotient.LEComap {X : Type u_2} {Y : Type u_3} [] [] (f : C(X, Y)) (A : ) (B : ) :

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

Instances For
theorem DiscreteQuotient.leComap_id {X : Type u_2} [] (A : ) :
@[simp]
theorem DiscreteQuotient.leComap_id_iff {X : Type u_2} [] {A : } {A' : } :
A A'
theorem DiscreteQuotient.LEComap.comp {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [] [] [] {f : C(X, Y)} {A : } {B : } {g : C(Y, Z)} {C : } :
theorem DiscreteQuotient.LEComap.mono {X : Type u_2} {Y : Type u_3} [] [] {f : C(X, Y)} {A : } {A' : } {B : } {B' : } (h : ) (hA : A' A) (hB : B B') :
def DiscreteQuotient.map {X : Type u_2} {Y : Type u_3} [] [] {A : } {B : } (f : C(X, Y)) (cond : ) :
Quotient A.toSetoidQuotient B.toSetoid

Map a discrete quotient along a continuous map.

Instances For
theorem DiscreteQuotient.map_continuous {X : Type u_2} {Y : Type u_3} [] [] {f : C(X, Y)} {A : } {B : } (cond : ) :
@[simp]
theorem DiscreteQuotient.map_comp_proj {X : Type u_2} {Y : Type u_3} [] [] {f : C(X, Y)} {A : } {B : } (cond : ) :
=
@[simp]
theorem DiscreteQuotient.map_proj {X : Type u_2} {Y : Type u_3} [] [] {f : C(X, Y)} {A : } {B : } (cond : ) (x : X) :
@[simp]
theorem DiscreteQuotient.map_id {X : Type u_2} [] {A : } :
DiscreteQuotient.map () (_ : ) = id
theorem DiscreteQuotient.map_comp {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [] [] [] {f : C(X, Y)} {A : } {B : } {g : C(Y, Z)} {C : } (h1 : ) (h2 : ) :
@[simp]
theorem DiscreteQuotient.ofLE_map {X : Type u_2} {Y : Type u_3} [] [] {f : C(X, Y)} {A : } {B : } {B' : } (cond : ) (h : B B') (a : Quotient A.toSetoid) :
@[simp]
theorem DiscreteQuotient.ofLE_comp_map {X : Type u_2} {Y : Type u_3} [] [] {f : C(X, Y)} {A : } {B : } {B' : } (cond : ) (h : B B') :
@[simp]
theorem DiscreteQuotient.map_ofLE {X : Type u_2} {Y : Type u_3} [] [] {f : C(X, Y)} {A : } {A' : } {B : } (cond : ) (h : A' A) (c : Quotient A'.toSetoid) :
@[simp]
theorem DiscreteQuotient.map_comp_ofLE {X : Type u_2} {Y : Type u_3} [] [] {f : C(X, Y)} {A : } {A' : } {B : } (cond : ) (h : A' A) :
theorem DiscreteQuotient.eq_of_forall_proj_eq {X : Type u_2} [] [] [] [disc : ] {x : X} {y : X} (h : ∀ (Q : ), ) :
x = y
theorem DiscreteQuotient.fiber_subset_ofLE {X : Type u_2} [] {A : } {B : } (h : A B) (a : Quotient A.toSetoid) :
theorem DiscreteQuotient.exists_of_compat {X : Type u_2} [] [] (Qs : (Q : ) → Quotient Q.toSetoid) (compat : ∀ (A B : ) (h : A B), DiscreteQuotient.ofLE h (Qs A) = Qs B) :
x, ∀ (Q : ), = Qs Q
instance DiscreteQuotient.instFiniteQuotientToSetoid {X : Type u_2} [] (S : ) [] :
Finite (Quotient S.toSetoid)

If X is a compact space, then any discrete quotient of X is finite.

def LocallyConstant.discreteQuotient {α : Type u_1} {X : Type u_2} [] (f : ) :

Any locally constant function induces a discrete quotient.

Instances For
def LocallyConstant.lift {α : Type u_1} {X : Type u_2} [] (f : ) :
LocallyConstant (Quotient ().toSetoid) α

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

Instances For
@[simp]
theorem LocallyConstant.lift_comp_proj {α : Type u_1} {X : Type u_2} [] (f : ) :