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.

structure DiscreteQuotient (X : Type u_5) [TopologicalSpace X] extends Setoid X : Type u_5

The type of discrete quotients of a topological space.

• r : X → X → Prop
• iseqv : Equivalence ⇑self.toSetoid
• isOpen_setOf_rel (x : X) : IsOpen (setOf (self.toSetoid x))

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

theorem DiscreteQuotient.ext {X : Type u_5} {inst✝ : TopologicalSpace X} {x y : DiscreteQuotient X} (r : ⇑x.toSetoid = ⇑y.toSetoid) : x = y

theorem DiscreteQuotient.ext_iff {X : Type u_5} {inst✝ : TopologicalSpace X} {x y : DiscreteQuotient X} : x = y ↔ ⇑x.toSetoid = ⇑y.toSetoid

theorem DiscreteQuotient.toSetoid_injective {X : Type u_2} [TopologicalSpace X] : Function.Injective toSetoid

def DiscreteQuotient.ofIsClopen {X : Type u_2} [TopologicalSpace X] {A : Set X} (h : IsClopen A) : DiscreteQuotient X

Construct a discrete quotient from a clopen set.

Equations

• DiscreteQuotient.ofIsClopen h = { r := fun (x y : X) => x ∈ A ↔ y ∈ A, iseqv := ⋯, isOpen_setOf_rel := ⋯ }

theorem DiscreteQuotient.refl {X : Type u_2} [TopologicalSpace X] (S : DiscreteQuotient X) (x : X) : S.toSetoid x x

theorem DiscreteQuotient.symm {X : Type u_2} [TopologicalSpace X] (S : DiscreteQuotient X) (x y : X) : S.toSetoid x y → S.toSetoid y x

theorem DiscreteQuotient.trans {X : Type u_2} [TopologicalSpace X] (S : DiscreteQuotient X) (x y z : X) : S.toSetoid x y → S.toSetoid y z → S.toSetoid x z

instance DiscreteQuotient.instCoeSortType {X : Type u_2} [TopologicalSpace X] : CoeSort (DiscreteQuotient X) (Type u_2)

Equations

• DiscreteQuotient.instCoeSortType = { coe := fun (S : DiscreteQuotient X) => Quotient S.toSetoid }

instance DiscreteQuotient.instTopologicalSpaceQuotient {X : Type u_2} [TopologicalSpace X] (S : DiscreteQuotient X) : TopologicalSpace (Quotient S.toSetoid)

Equations

• S.instTopologicalSpaceQuotient = inferInstanceAs (TopologicalSpace (Quotient S.toSetoid))

def DiscreteQuotient.proj {X : Type u_2} [TopologicalSpace X] (S : DiscreteQuotient X) : X → Quotient S.toSetoid

The projection from X to the given discrete quotient.

Equations

• S.proj = Quotient.mk''

theorem DiscreteQuotient.fiber_eq {X : Type u_2} [TopologicalSpace X] (S : DiscreteQuotient X) (x : X) : S.proj ⁻¹' {S.proj x} = setOf (S.toSetoid x)

theorem DiscreteQuotient.proj_surjective {X : Type u_2} [TopologicalSpace X] (S : DiscreteQuotient X) : Function.Surjective S.proj

theorem DiscreteQuotient.proj_isQuotientMap {X : Type u_2} [TopologicalSpace X] (S : DiscreteQuotient X) : Topology.IsQuotientMap S.proj

theorem DiscreteQuotient.proj_continuous {X : Type u_2} [TopologicalSpace X] (S : DiscreteQuotient X) : Continuous S.proj

instance DiscreteQuotient.instDiscreteTopologyQuotient {X : Type u_2} [TopologicalSpace X] (S : DiscreteQuotient X) : DiscreteTopology (Quotient S.toSetoid)

theorem DiscreteQuotient.proj_isLocallyConstant {X : Type u_2} [TopologicalSpace X] (S : DiscreteQuotient X) : IsLocallyConstant S.proj

theorem DiscreteQuotient.isClopen_preimage {X : Type u_2} [TopologicalSpace X] (S : DiscreteQuotient X) (A : Set (Quotient S.toSetoid)) : IsClopen (S.proj ⁻¹' A)

theorem DiscreteQuotient.isOpen_preimage {X : Type u_2} [TopologicalSpace X] (S : DiscreteQuotient X) (A : Set (Quotient S.toSetoid)) : IsOpen (S.proj ⁻¹' A)

theorem DiscreteQuotient.isClosed_preimage {X : Type u_2} [TopologicalSpace X] (S : DiscreteQuotient X) (A : Set (Quotient S.toSetoid)) : IsClosed (S.proj ⁻¹' A)

theorem DiscreteQuotient.isClopen_setOf_rel {X : Type u_2} [TopologicalSpace X] (S : DiscreteQuotient X) (x : X) : IsClopen (setOf (S.toSetoid x))

instance DiscreteQuotient.instMin {X : Type u_2} [TopologicalSpace X] : Min (DiscreteQuotient X)

Equations

• DiscreteQuotient.instMin = { min := fun (S₁ S₂ : DiscreteQuotient X) => { toSetoid := S₁.toSetoid ⊓ S₂.toSetoid, isOpen_setOf_rel := ⋯ } }

instance DiscreteQuotient.instSemilatticeInf {X : Type u_2} [TopologicalSpace X] : SemilatticeInf (DiscreteQuotient X)

Equations

• DiscreteQuotient.instSemilatticeInf = Function.Injective.semilatticeInf DiscreteQuotient.toSetoid ⋯ ⋯

instance DiscreteQuotient.instOrderTop {X : Type u_2} [TopologicalSpace X] : OrderTop (DiscreteQuotient X)

Equations

• DiscreteQuotient.instOrderTop = { top := { toSetoid := ⊤, isOpen_setOf_rel := ⋯ }, le_top := ⋯ }

instance DiscreteQuotient.instInhabited {X : Type u_2} [TopologicalSpace X] : Inhabited (DiscreteQuotient X)

Equations

• DiscreteQuotient.instInhabited = { default := ⊤ }

instance DiscreteQuotient.inhabitedQuotient {X : Type u_2} [TopologicalSpace X] (S : DiscreteQuotient X) [Inhabited X] : Inhabited (Quotient S.toSetoid)

Equations

• S.inhabitedQuotient = { default := S.proj default }

instance DiscreteQuotient.instNonemptyQuotient {X : Type u_2} [TopologicalSpace X] (S : DiscreteQuotient X) [Nonempty X] : Nonempty (Quotient S.toSetoid)

instance DiscreteQuotient.instSubsingletonQuotientTop {X : Type u_2} [TopologicalSpace X] : Subsingleton (Quotient ⊤.toSetoid)

The quotient by ⊤ : DiscreteQuotient X is a Subsingleton.

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

Comap a discrete quotient along a continuous map.

Equations

• DiscreteQuotient.comap f S = { toSetoid := Setoid.comap (⇑f) S.toSetoid, isOpen_setOf_rel := ⋯ }

@[simp]

theorem DiscreteQuotient.comap_id {X : Type u_2} [TopologicalSpace X] (S : DiscreteQuotient X) : comap (ContinuousMap.id X) S = S

@[simp]

theorem DiscreteQuotient.comap_comp {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (g : C(Y, Z)) (f : C(X, Y)) (S : DiscreteQuotient Z) : comap (g.comp f) S = comap f (comap g S)

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

def DiscreteQuotient.ofLE {X : Type u_2} [TopologicalSpace X] {A B : DiscreteQuotient X} (h : A ≤ B) : Quotient A.toSetoid → Quotient B.toSetoid

The map induced by a refinement of a discrete quotient.

Equations

• DiscreteQuotient.ofLE h = Quotient.map' id h

@[simp]

theorem DiscreteQuotient.ofLE_refl {X : Type u_2} [TopologicalSpace X] {A : DiscreteQuotient X} : ofLE ⋯ = id

theorem DiscreteQuotient.ofLE_refl_apply {X : Type u_2} [TopologicalSpace X] {A : DiscreteQuotient X} (a : Quotient A.toSetoid) : ofLE ⋯ a = a

@[simp]

theorem DiscreteQuotient.ofLE_ofLE {X : Type u_2} [TopologicalSpace X] {A B C : DiscreteQuotient X} (h₁ : A ≤ B) (h₂ : B ≤ C) (x : Quotient A.toSetoid) : ofLE h₂ (ofLE h₁ x) = ofLE ⋯ x

@[simp]

theorem DiscreteQuotient.ofLE_comp_ofLE {X : Type u_2} [TopologicalSpace X] {A B C : DiscreteQuotient X} (h₁ : A ≤ B) (h₂ : B ≤ C) : ofLE h₂ ∘ ofLE h₁ = ofLE ⋯

theorem DiscreteQuotient.ofLE_continuous {X : Type u_2} [TopologicalSpace X] {A B : DiscreteQuotient X} (h : A ≤ B) : Continuous (ofLE h)

@[simp]

theorem DiscreteQuotient.ofLE_proj {X : Type u_2} [TopologicalSpace X] {A B : DiscreteQuotient X} (h : A ≤ B) (x : X) : ofLE h (A.proj x) = B.proj x

@[simp]

theorem DiscreteQuotient.ofLE_comp_proj {X : Type u_2} [TopologicalSpace X] {A B : DiscreteQuotient X} (h : A ≤ B) : ofLE h ∘ A.proj = B.proj

instance DiscreteQuotient.instOrderBotOfLocallyConnectedSpace {X : Type u_2} [TopologicalSpace X] [LocallyConnectedSpace X] : OrderBot (DiscreteQuotient X)

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 = { bot := let __Setoid := connectedComponentSetoid X; { toSetoid := __Setoid, isOpen_setOf_rel := ⋯ }, bot_le := ⋯ }

@[simp]

theorem DiscreteQuotient.proj_bot_eq {X : Type u_2} [TopologicalSpace X] [LocallyConnectedSpace X] {x y : X} : ⊥.proj x = ⊥.proj y ↔ connectedComponent x = connectedComponent y

theorem DiscreteQuotient.proj_bot_inj {X : Type u_2} [TopologicalSpace X] [DiscreteTopology X] {x y : X} : ⊥.proj x = ⊥.proj y ↔ x = y

theorem DiscreteQuotient.proj_bot_injective {X : Type u_2} [TopologicalSpace X] [DiscreteTopology X] : Function.Injective ⊥.proj

theorem DiscreteQuotient.proj_bot_bijective {X : Type u_2} [TopologicalSpace X] [DiscreteTopology X] : Function.Bijective ⊥.proj

def DiscreteQuotient.LEComap {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (f : C(X, Y)) (A : DiscreteQuotient X) (B : DiscreteQuotient Y) : Prop

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

• DiscreteQuotient.LEComap f A B = (A ≤ DiscreteQuotient.comap f B)

theorem DiscreteQuotient.leComap_id {X : Type u_2} [TopologicalSpace X] (A : DiscreteQuotient X) : LEComap (ContinuousMap.id X) A A

@[simp]

theorem DiscreteQuotient.leComap_id_iff {X : Type u_2} [TopologicalSpace X] {A A' : DiscreteQuotient X} : LEComap (ContinuousMap.id X) A A' ↔ A ≤ A'

theorem DiscreteQuotient.LEComap.comp {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {f : C(X, Y)} {A : DiscreteQuotient X} {B : DiscreteQuotient Y} {g : C(Y, Z)} {C : DiscreteQuotient Z} : LEComap g B C → LEComap f A B → LEComap (g.comp f) A C

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

def DiscreteQuotient.map {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {A : DiscreteQuotient X} {B : DiscreteQuotient Y} (f : C(X, Y)) (cond : LEComap f A B) : Quotient A.toSetoid → Quotient B.toSetoid

Map a discrete quotient along a continuous map.

Equations

• DiscreteQuotient.map f cond = Quotient.map' (⇑f) cond

theorem DiscreteQuotient.map_continuous {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {f : C(X, Y)} {A : DiscreteQuotient X} {B : DiscreteQuotient Y} (cond : LEComap f A B) : Continuous (map f cond)

@[simp]

theorem DiscreteQuotient.map_comp_proj {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {f : C(X, Y)} {A : DiscreteQuotient X} {B : DiscreteQuotient Y} (cond : LEComap f A B) : map f cond ∘ A.proj = B.proj ∘ ⇑f

@[simp]

theorem DiscreteQuotient.map_proj {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {f : C(X, Y)} {A : DiscreteQuotient X} {B : DiscreteQuotient Y} (cond : LEComap f A B) (x : X) : map f cond (A.proj x) = B.proj (f x)

@[simp]

theorem DiscreteQuotient.map_id {X : Type u_2} [TopologicalSpace X] {A : DiscreteQuotient X} : map (ContinuousMap.id X) ⋯ = id

theorem DiscreteQuotient.map_comp {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {f : C(X, Y)} {A : DiscreteQuotient X} {B : DiscreteQuotient Y} {g : C(Y, Z)} {C : DiscreteQuotient Z} (h1 : LEComap g B C) (h2 : LEComap f A B) : map (g.comp f) ⋯ = map g h1 ∘ map f h2

@[simp]

theorem DiscreteQuotient.ofLE_map {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {f : C(X, Y)} {A : DiscreteQuotient X} {B B' : DiscreteQuotient Y} (cond : LEComap f A B) (h : B ≤ B') (a : Quotient A.toSetoid) : ofLE h (map f cond a) = map f ⋯ a

@[simp]

theorem DiscreteQuotient.ofLE_comp_map {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {f : C(X, Y)} {A : DiscreteQuotient X} {B B' : DiscreteQuotient Y} (cond : LEComap f A B) (h : B ≤ B') : ofLE h ∘ map f cond = map f ⋯

@[simp]

theorem DiscreteQuotient.map_ofLE {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {f : C(X, Y)} {A A' : DiscreteQuotient X} {B : DiscreteQuotient Y} (cond : LEComap f A B) (h : A' ≤ A) (c : Quotient A'.toSetoid) : map f cond (ofLE h c) = map f ⋯ c

@[simp]

theorem DiscreteQuotient.map_comp_ofLE {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {f : C(X, Y)} {A A' : DiscreteQuotient X} {B : DiscreteQuotient Y} (cond : LEComap f A B) (h : A' ≤ A) : map f cond ∘ ofLE h = map f ⋯

theorem DiscreteQuotient.eq_of_forall_proj_eq {X : Type u_2} [TopologicalSpace X] [T2Space X] [CompactSpace X] [disc : TotallyDisconnectedSpace X] {x y : X} (h : ∀ (Q : DiscreteQuotient X), Q.proj x = Q.proj y) : x = y

theorem DiscreteQuotient.fiber_subset_ofLE {X : Type u_2} [TopologicalSpace X] {A B : DiscreteQuotient X} (h : A ≤ B) (a : Quotient A.toSetoid) : A.proj ⁻¹' {a} ⊆ B.proj ⁻¹' {ofLE h a}

theorem DiscreteQuotient.exists_of_compat {X : Type u_2} [TopologicalSpace X] [CompactSpace X] (Qs : (Q : DiscreteQuotient X) → Quotient Q.toSetoid) (compat : ∀ (A B : DiscreteQuotient X) (h : A ≤ B), ofLE h (Qs A) = Qs B) : ∃ (x : X), ∀ (Q : DiscreteQuotient X), Q.proj x = Qs Q

instance DiscreteQuotient.instFiniteQuotientOfCompactSpace {X : Type u_2} [TopologicalSpace X] (S : DiscreteQuotient X) [CompactSpace X] : Finite (Quotient S.toSetoid)

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

noncomputable def DiscreteQuotient.finsetClopens (X : Type u_2) [TopologicalSpace X] [CompactSpace X] (d : DiscreteQuotient X) : Finset (TopologicalSpace.Clopens X)

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

• DiscreteQuotient.finsetClopens X d = (Set.range fun (x : Quotient d.toSetoid) => { carrier := d.proj ⁻¹' {x}, isClopen' := ⋯ }).toFinset

theorem DiscreteQuotient.comp_finsetClopens (X : Type u_2) [TopologicalSpace X] [CompactSpace X] : ((Set.image fun (t : TopologicalSpace.Clopens X) => t.carrier) ∘ Finset.toSet) ∘ finsetClopens X = fun (x : DiscreteQuotient 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) [TopologicalSpace X] [CompactSpace X] : Function.Injective (finsetClopens X)

finsetClopens X is injective.

noncomputable def DiscreteQuotient.equivFinsetClopens (X : Type u_2) [TopologicalSpace X] [CompactSpace X] : DiscreteQuotient X ≃ ↑(Set.range (finsetClopens X))

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

• DiscreteQuotient.equivFinsetClopens X = Equiv.ofInjective (DiscreteQuotient.finsetClopens X) ⋯

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

Any locally constant function induces a discrete quotient.

Equations

• f.discreteQuotient = { toSetoid := Setoid.comap ⇑f ⊥, isOpen_setOf_rel := ⋯ }

def LocallyConstant.lift {α : Type u_1} {X : Type u_2} [TopologicalSpace X] (f : LocallyConstant X α) : 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 := ⋯ }

@[simp]

theorem LocallyConstant.lift_comp_proj {α : Type u_1} {X : Type u_2} [TopologicalSpace X] (f : LocallyConstant X α) : ⇑f.lift ∘ f.discreteQuotient.proj = ⇑f