Specialization order

This file defines a type synonym for a topological space considered with its specialisation order.

def Specialization (α : Type u_1) : Type u_1

Type synonym for a topological space considered with its specialisation order.

Equations

• Specialization α = α

@[match_pattern]

def Specialization.toEquiv {α : Type u_1} : α ≃ Specialization α

toEquiv is the "identity" function to the Specialization of a type.

Equations

• Specialization.toEquiv = Equiv.refl α

@[match_pattern]

def Specialization.ofEquiv {α : Type u_1} : Specialization α ≃ α

ofEquiv is the identity function from the Specialization of a type.

Equations

• Specialization.ofEquiv = Equiv.refl (Specialization α)

@[simp]

theorem Specialization.toEquiv_symm {α : Type u_1} : Specialization.toEquiv.symm = Specialization.ofEquiv

@[simp]

theorem Specialization.ofEquiv_symm {α : Type u_1} : Specialization.ofEquiv.symm = Specialization.toEquiv

@[simp]

theorem Specialization.toEquiv_ofEquiv {α : Type u_1} (a : Specialization α) : Specialization.toEquiv (Specialization.ofEquiv a) = a

@[simp]

theorem Specialization.ofEquiv_toEquiv {α : Type u_1} (a : α) : Specialization.ofEquiv (Specialization.toEquiv a) = a

@[simp]

theorem Specialization.toEquiv_inj {α : Type u_1} {a : α} {b : α} : Specialization.toEquiv a = Specialization.toEquiv b ↔ a = b

@[simp]

theorem Specialization.ofEquiv_inj {α : Type u_1} {a : Specialization α} {b : Specialization α} : Specialization.ofEquiv a = Specialization.ofEquiv b ↔ a = b

def Specialization.rec {α : Type u_1} {β : Specialization α → Sort u_4} (h : (a : α) → β (Specialization.toEquiv a)) (a : Specialization α) : β a

A recursor for Specialization. Use as induction x.

Equations

• Specialization.rec h a = h (Specialization.ofEquiv a)

instance Specialization.instPreorder {α : Type u_1} [TopologicalSpace α] : Preorder (Specialization α)

Equations

• Specialization.instPreorder = specializationPreorder α

instance Specialization.instPartialOrder {α : Type u_1} [TopologicalSpace α] [T0Space α] : PartialOrder (Specialization α)

Equations

• Specialization.instPartialOrder = specializationOrder α

@[simp]

theorem Specialization.toEquiv_le_toEquiv {α : Type u_1} [TopologicalSpace α] {a : α} {b : α} : Specialization.toEquiv a ≤ Specialization.toEquiv b ↔ b ⤳ a

@[simp]

theorem Specialization.ofEquiv_specializes_ofEquiv {α : Type u_1} [TopologicalSpace α] {a : Specialization α} {b : Specialization α} : Specialization.ofEquiv a ⤳ Specialization.ofEquiv b ↔ b ≤ a

@[simp]

theorem Specialization.isOpen_toEquiv_preimage {α : Type u_1} [TopologicalSpace α] [AlexandrovDiscrete α] {s : Set (Specialization α)} : IsOpen (⇑Specialization.toEquiv ⁻¹' s) ↔ IsUpperSet s

@[simp]

theorem Specialization.isUpperSet_ofEquiv_preimage {α : Type u_1} [TopologicalSpace α] [AlexandrovDiscrete α] {s : Set α} : IsUpperSet (⇑Specialization.ofEquiv ⁻¹' s) ↔ IsOpen s

def Specialization.map {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (f : C(α, β)) : Specialization α →o Specialization β

A continuous map between topological spaces induces a monotone map between their specialization orders.

Equations

• Specialization.map f = { toFun := ⇑Specialization.toEquiv ∘ ⇑f ∘ ⇑Specialization.ofEquiv, monotone' := ⋯ }

@[simp]

theorem Specialization.map_id {α : Type u_1} [TopologicalSpace α] : Specialization.map (ContinuousMap.id α) = OrderHom.id

@[simp]

theorem Specialization.map_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] (g : C(β, γ)) (f : C(α, β)) : Specialization.map (g.comp f) = (Specialization.map g).comp (Specialization.map f)

def orderIsoSpecializationWithUpperSetTopology (α : Type u_1) [Preorder α] : α ≃o Specialization (Topology.WithUpperSet α)

A preorder is isomorphic to the specialisation order of its upper set topology.

Equations

• orderIsoSpecializationWithUpperSetTopology α = { toEquiv := Topology.WithUpperSet.toUpperSet.trans Specialization.toEquiv, map_rel_iff' := ⋯ }

def homeoWithUpperSetTopologyorderIso (α : Type u_1) [TopologicalSpace α] [AlexandrovDiscrete α] : α ≃ₜ Topology.WithUpperSet (Specialization α)

An Alexandrov-discrete space is isomorphic to the upper set topology of its specialisation order.

Equations

• homeoWithUpperSetTopologyorderIso α = (Specialization.toEquiv.trans Topology.WithUpperSet.toUpperSet).toHomeomorph ⋯

def topToPreord : CategoryTheory.Functor TopCat Preord

Sends a topological space to its specialisation order.

Equations

• topToPreord = { obj := fun (X : TopCat) => Preord.of (Specialization ↑X), map := fun {X Y : TopCat} => Specialization.map, map_id := topToPreord.proof_1, map_comp := @topToPreord.proof_2 }

@[simp]

theorem topToPreord_obj (X : TopCat) : topToPreord.obj X = Preord.of (Specialization ↑X)

@[simp]

theorem topToPreord_map : ∀ {X Y : TopCat} (f : C(↑X, ↑Y)), topToPreord.map f = Specialization.map f