# 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

The type of discrete quotients of a topological space.

• r : XXProp
• iseqv : Equivalence Setoid.r
• isOpen_setOf_rel : ∀ (x : X), IsOpen (setOf (self.Rel x))

For every point x, the set { y | Rel x y } is an open set.

Instances For
theorem DiscreteQuotient.isOpen_setOf_rel {X : Type u_5} [] (self : ) (x : X) :
IsOpen (setOf (self.Rel x))

For every point x, the set { y | Rel x y } is an open set.

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

Construct a discrete quotient from a clopen set.

Equations
• = { r := fun (x y : X) => x A y A, iseqv := , isOpen_setOf_rel := }
Instances For
theorem DiscreteQuotient.refl {X : Type u_2} [] (S : ) (x : X) :
S.Rel x x
theorem DiscreteQuotient.symm {X : Type u_2} [] (S : ) (x : X) (y : X) :
S.Rel x yS.Rel y x
theorem DiscreteQuotient.trans {X : Type u_2} [] (S : ) (x : X) (y : X) (z : X) :
S.Rel x yS.Rel y zS.Rel x z
instance DiscreteQuotient.instCoeSortType {X : Type u_2} [] :
CoeSort () (Type u_2)
Equations
• DiscreteQuotient.instCoeSortType = { coe := fun (S : ) => Quotient S.toSetoid }
Equations
def DiscreteQuotient.proj {X : Type u_2} [] (S : ) :
XQuotient S.toSetoid

The projection from X to the given discrete quotient.

Equations
• S.proj = Quotient.mk''
Instances For
theorem DiscreteQuotient.fiber_eq {X : Type u_2} [] (S : ) (x : X) :
S.proj ⁻¹' {S.proj x} = setOf (S.Rel x)
theorem DiscreteQuotient.proj_quotientMap {X : Type u_2} [] (S : ) :
theorem DiscreteQuotient.proj_continuous {X : Type u_2} [] (S : ) :
Continuous S.proj
Equations
• =
theorem DiscreteQuotient.isClopen_preimage {X : Type u_2} [] (S : ) (A : Set (Quotient S.toSetoid)) :
IsClopen (S.proj ⁻¹' A)
theorem DiscreteQuotient.isOpen_preimage {X : Type u_2} [] (S : ) (A : Set (Quotient S.toSetoid)) :
IsOpen (S.proj ⁻¹' A)
theorem DiscreteQuotient.isClosed_preimage {X : Type u_2} [] (S : ) (A : Set (Quotient S.toSetoid)) :
IsClosed (S.proj ⁻¹' A)
theorem DiscreteQuotient.isClopen_setOf_rel {X : Type u_2} [] (S : ) (x : X) :
IsClopen (setOf (S.Rel x))
instance DiscreteQuotient.instInf {X : Type u_2} [] :
Equations
• DiscreteQuotient.instInf = { inf := fun (S₁ S₂ : ) => { toSetoid := S₁.toSetoid S₂.toSetoid, isOpen_setOf_rel := } }
Equations
instance DiscreteQuotient.instOrderTop {X : Type u_2} [] :
Equations
• DiscreteQuotient.instOrderTop =
instance DiscreteQuotient.instInhabited {X : Type u_2} [] :
Equations
• DiscreteQuotient.instInhabited = { default := }
instance DiscreteQuotient.inhabitedQuotient {X : Type u_2} [] (S : ) [] :
Inhabited (Quotient S.toSetoid)
Equations
• S.inhabitedQuotient = { default := S.proj default }
instance DiscreteQuotient.instNonemptyQuotient {X : Type u_2} [] (S : ) [] :
Nonempty (Quotient S.toSetoid)
Equations
• =

The quotient by ⊤ : DiscreteQuotient X is a Subsingleton.

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

Comap a discrete quotient along a continuous map.

Equations
• = { toSetoid := Setoid.comap (f) S.toSetoid, isOpen_setOf_rel := }
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.

Equations
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) :
DiscreteQuotient.ofLE h (A.proj x) = B.proj x
@[simp]
theorem DiscreteQuotient.ofLE_comp_proj {X : Type u_2} [] {A : } {B : } (h : A B) :
A.proj = B.proj

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

Equations
• DiscreteQuotient.instOrderBotOfLocallyConnectedSpace =
@[simp]
theorem DiscreteQuotient.proj_bot_eq {X : Type u_2} [] {x : X} {y : X} :
.proj x = .proj y
theorem DiscreteQuotient.proj_bot_inj {X : Type u_2} [] [] {x : X} {y : X} :
.proj x = .proj y 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.

Equations
• = ()
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 : } :
DiscreteQuotient.LEComap (g.comp f) A 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.

Equations
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 : ) :
DiscreteQuotient.map f cond A.proj = B.proj f
@[simp]
theorem DiscreteQuotient.map_proj {X : Type u_2} {Y : Type u_3} [] [] {f : C(X, Y)} {A : } {B : } (cond : ) (x : X) :
DiscreteQuotient.map f cond (A.proj x) = B.proj (f x)
@[simp]
theorem DiscreteQuotient.map_id {X : Type u_2} [] {A : } :
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 : ) :
DiscreteQuotient.map (g.comp f) =
@[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 : ), Q.proj x = Q.proj y) :
x = y
theorem DiscreteQuotient.fiber_subset_ofLE {X : Type u_2} [] {A : } {B : } (h : A B) (a : Quotient A.toSetoid) :
A.proj ⁻¹' {a} B.proj ⁻¹' {}
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 : X), ∀ (Q : ), Q.proj x = Qs Q
instance DiscreteQuotient.instFiniteQuotientOfCompactSpace {X : Type u_2} [] (S : ) [] :
Finite (Quotient S.toSetoid)

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

Equations
• =
noncomputable def DiscreteQuotient.finsetClopens (X : Type u_2) [] [] (d : ) :

If X is a compact space, then we associate to any discrete quotient on X a finite set of clopen subsets of X, given by the fibers of proj.

TODO: prove that these form a partition of X

Equations
Instances For
theorem DiscreteQuotient.comp_finsetClopens (X : Type u_2) [] [] :
((Set.image fun (t : ) => t.carrier) Finset.toSet) = fun (x : ) => match x with | { toSetoid := f, isOpen_setOf_rel := isOpen_setOf_rel } => f.classes

A helper lemma to prove that finsetClopens X is injective, see finsetClopens_inj.

theorem DiscreteQuotient.finsetClopens_inj (X : Type u_2) [] [] :

finsetClopens X is injective.

noncomputable def DiscreteQuotient.equivFinsetClopens (X : Type u_2) [] [] :

The discrete quotients of a compact space are in bijection with a subtype of the type of Finset (Clopens X).

TODO: show that this is precisely those finsets of clopens which form a partition of X.

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

Any locally constant function induces a discrete quotient.

Equations
• f.discreteQuotient = { toSetoid := , isOpen_setOf_rel := }
Instances For
def LocallyConstant.lift {α : Type u_1} {X : Type u_2} [] (f : ) :
LocallyConstant (Quotient f.discreteQuotient.toSetoid) α

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

Equations
• f.lift = { toFun := fun (a : Quotient f.discreteQuotient.toSetoid) => a.liftOn' f , isLocallyConstant := }
Instances For
@[simp]
theorem LocallyConstant.lift_comp_proj {α : Type u_1} {X : Type u_2} [] (f : ) :
f.lift f.discreteQuotient.proj = f