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 : TopologicalSpace X} (x y : DiscreteQuotient X), x = y ↔ Setoid.r = Setoid.r

theorem DiscreteQuotient.ext {X : Type u_5} : ∀ {inst : TopologicalSpace X} (x y : DiscreteQuotient X), Setoid.r = Setoid.r → x = y

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

The type of discrete quotients of a topological space.

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

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

theorem DiscreteQuotient.toSetoid_injective {X : Type u_2} [TopologicalSpace X] : Function.Injective DiscreteQuotient.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 = { toSetoid := { 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) : Setoid.Rel S.toSetoid x x

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

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

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

Equations

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

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

Equations

• DiscreteQuotient.instTopologicalSpaceQuotientToSetoid S = 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

• DiscreteQuotient.proj S = Quotient.mk''

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

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

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

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

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

Equations

• ⋯ = ⋯

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

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

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

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

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

instance DiscreteQuotient.instInfDiscreteQuotient {X : Type u_2} [TopologicalSpace X] : Inf (DiscreteQuotient X)

Equations

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

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

Equations

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

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

Equations

• DiscreteQuotient.instOrderTopDiscreteQuotientToLEToPreorderToPartialOrderInstSemilatticeInfDiscreteQuotient = OrderTop.mk ⋯

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

Equations

• DiscreteQuotient.instInhabitedDiscreteQuotient = { default := ⊤ }

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

Equations

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

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

Equations

• ⋯ = ⋯

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

The quotient by ⊤ : DiscreteQuotient X is a Subsingleton.

Equations

• ⋯ = ⋯

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) : DiscreteQuotient.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) : DiscreteQuotient.comap (ContinuousMap.comp g f) S = DiscreteQuotient.comap f (DiscreteQuotient.comap g S)

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

def DiscreteQuotient.ofLE {X : Type u_2} [TopologicalSpace X] {A : DiscreteQuotient X} {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' (fun (x : X) => x) h

@[simp]

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

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

@[simp]

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

@[simp]

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

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

@[simp]

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

@[simp]

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

instance DiscreteQuotient.instOrderBotDiscreteQuotientToLEToPreorderToPartialOrderInstSemilatticeInfDiscreteQuotient {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.instOrderBotDiscreteQuotientToLEToPreorderToPartialOrderInstSemilatticeInfDiscreteQuotient = OrderBot.mk ⋯

@[simp]

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

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

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

theorem DiscreteQuotient.proj_bot_bijective {X : Type u_2} [TopologicalSpace X] [DiscreteTopology X] : Function.Bijective (DiscreteQuotient.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) : DiscreteQuotient.LEComap (ContinuousMap.id X) A A

@[simp]

theorem DiscreteQuotient.leComap_id_iff {X : Type u_2} [TopologicalSpace X] {A : DiscreteQuotient X} {A' : DiscreteQuotient X} : DiscreteQuotient.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} : DiscreteQuotient.LEComap g B C → DiscreteQuotient.LEComap f A B → DiscreteQuotient.LEComap (ContinuousMap.comp g f) A C

theorem DiscreteQuotient.LEComap.mono {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {f : C(X, Y)} {A : DiscreteQuotient X} {A' : DiscreteQuotient X} {B : DiscreteQuotient Y} {B' : DiscreteQuotient Y} (h : DiscreteQuotient.LEComap f A B) (hA : A' ≤ A) (hB : B ≤ B') : DiscreteQuotient.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 : DiscreteQuotient.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 : DiscreteQuotient.LEComap f A B) : Continuous (DiscreteQuotient.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 : DiscreteQuotient.LEComap f A B) : DiscreteQuotient.map f cond ∘ DiscreteQuotient.proj A = DiscreteQuotient.proj B ∘ ⇑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 : DiscreteQuotient.LEComap f A B) (x : X) : DiscreteQuotient.map f cond (DiscreteQuotient.proj A x) = DiscreteQuotient.proj B (f x)

@[simp]

theorem DiscreteQuotient.map_id {X : Type u_2} [TopologicalSpace X] {A : DiscreteQuotient X} : DiscreteQuotient.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 : DiscreteQuotient.LEComap g B C) (h2 : DiscreteQuotient.LEComap f A B) : DiscreteQuotient.map (ContinuousMap.comp g f) ⋯ = DiscreteQuotient.map g h1 ∘ DiscreteQuotient.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 : DiscreteQuotient Y} {B' : DiscreteQuotient Y} (cond : DiscreteQuotient.LEComap f A B) (h : B ≤ B') (a : Quotient A.toSetoid) : DiscreteQuotient.ofLE h (DiscreteQuotient.map f cond a) = DiscreteQuotient.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 : DiscreteQuotient Y} {B' : DiscreteQuotient Y} (cond : DiscreteQuotient.LEComap f A B) (h : B ≤ B') : DiscreteQuotient.ofLE h ∘ DiscreteQuotient.map f cond = DiscreteQuotient.map f ⋯

@[simp]

theorem DiscreteQuotient.map_ofLE {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {f : C(X, Y)} {A : DiscreteQuotient X} {A' : DiscreteQuotient X} {B : DiscreteQuotient Y} (cond : DiscreteQuotient.LEComap f A B) (h : A' ≤ A) (c : Quotient A'.toSetoid) : DiscreteQuotient.map f cond (DiscreteQuotient.ofLE h c) = DiscreteQuotient.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 : DiscreteQuotient X} {A' : DiscreteQuotient X} {B : DiscreteQuotient Y} (cond : DiscreteQuotient.LEComap f A B) (h : A' ≤ A) : DiscreteQuotient.map f cond ∘ DiscreteQuotient.ofLE h = DiscreteQuotient.map f ⋯

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

theorem DiscreteQuotient.fiber_subset_ofLE {X : Type u_2} [TopologicalSpace X] {A : DiscreteQuotient X} {B : DiscreteQuotient X} (h : A ≤ B) (a : Quotient A.toSetoid) : DiscreteQuotient.proj A ⁻¹' {a} ⊆ DiscreteQuotient.proj B ⁻¹' {DiscreteQuotient.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), DiscreteQuotient.ofLE h (Qs A) = Qs B) : ∃ (x : X), ∀ (Q : DiscreteQuotient X), DiscreteQuotient.proj Q x = Qs Q

instance DiscreteQuotient.instFiniteQuotientToSetoid {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.

Equations

• ⋯ = ⋯

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

• One or more equations did not get rendered due to their size.

theorem DiscreteQuotient.comp_finsetClopens (X : Type u_2) [TopologicalSpace X] [CompactSpace X] : ((Set.image fun (t : TopologicalSpace.Clopens X) => t.carrier) ∘ Finset.toSet) ∘ DiscreteQuotient.finsetClopens X = fun (x : DiscreteQuotient X) => match x with | { toSetoid := f, isOpen_setOf_rel := isOpen_setOf_rel } => Setoid.classes f

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 (DiscreteQuotient.finsetClopens X)

finsetClopens X is injective.

noncomputable def DiscreteQuotient.equivFinsetClopens (X : Type u_2) [TopologicalSpace X] [CompactSpace X] : DiscreteQuotient X ≃ ↑(Set.range (DiscreteQuotient.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

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

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

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

Equations

• LocallyConstant.lift f = { toFun := fun (a : Quotient (LocallyConstant.discreteQuotient f).toSetoid) => Quotient.liftOn' a ⇑f ⋯, isLocallyConstant := ⋯ }

@[simp]

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