Documentation

Mathlib.Topology.Specialization

Specialization order #

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

source
def Specialization (α : Type u_1) :
Type u_1

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

Equations
source
@[match_pattern]
def Specialization.toEquiv {α : Type u_1} :
α ≃ Specialization α

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

Equations
source
@[match_pattern]
def Specialization.ofEquiv {α : Type u_1} :
Specialization α ≃ α

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

Equations
source
@[simp]
theorem Specialization.toEquiv_symm {α : Type u_1} :
toEquiv.symm = ofEquiv
source
@[simp]
theorem Specialization.ofEquiv_symm {α : Type u_1} :
ofEquiv.symm = toEquiv
source
@[simp]
theorem Specialization.toEquiv_ofEquiv {α : Type u_1} (a : Specialization α) :
toEquiv (ofEquiv a) = a
source
@[simp]
theorem Specialization.ofEquiv_toEquiv {α : Type u_1} (a : α) :
ofEquiv (toEquiv a) = a
source
@[simp]
theorem Specialization.toEquiv_inj {α : Type u_1} {a b : α} :
toEquiv a = toEquiv b ↔ a = b
source
@[simp]
theorem Specialization.ofEquiv_inj {α : Type u_1} {a b : Specialization α} :
ofEquiv a = ofEquiv b ↔ a = b
source
def Specialization.rec {α : Type u_1} {β : Specialization α → Sort u_4} (h : (a : α) → β (toEquiv a)) (a : Specialization α) :
β a

A recursor for Specialization. Use as induction x.

Equations
source
instance Specialization.instPreorder {α : Type u_1} [TopologicalSpace α] :
Preorder (Specialization α)
Equations
source
instance Specialization.instPartialOrder {α : Type u_1} [TopologicalSpace α] [T0Space α] :
PartialOrder (Specialization α)
Equations
source
@[simp]
theorem Specialization.toEquiv_le_toEquiv {α : Type u_1} [TopologicalSpace α] {a b : α} :
toEquiv a ≤ toEquiv b ↔ b ⤳ a
source
@[simp]
theorem Specialization.ofEquiv_specializes_ofEquiv {α : Type u_1} [TopologicalSpace α] {a b : Specialization α} :
ofEquiv a ⤳ ofEquiv b ↔ b ≤ a
source
@[simp]
theorem Specialization.isOpen_toEquiv_preimage {α : Type u_1} [TopologicalSpace α] [AlexandrovDiscrete α] {s : Set (Specialization α)} :
IsOpen (⇑toEquiv ⁻¹' s) ↔ IsUpperSet s
source
@[simp]
theorem Specialization.isUpperSet_ofEquiv_preimage {α : Type u_1} [TopologicalSpace α] [AlexandrovDiscrete α] {s : Set α} :
IsUpperSet (⇑ofEquiv ⁻¹' s) ↔ IsOpen s
source
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
source
@[simp]
theorem Specialization.map_id {α : Type u_1} [TopologicalSpace α] :
map (ContinuousMap.id α) = OrderHom.id
source
@[simp]
theorem Specialization.map_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] (g : C(β, γ)) (f : C(α, β)) :
map (g.comp f) = (map g).comp (map f)
source
def orderIsoSpecializationWithUpperSetTopology (α : Type u_1) [Preorder α] :
α ≃o Specialization (Topology.WithUpperSet α)

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

Equations
source
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
source
def topToPreord :
CategoryTheory.Functor TopCat Preord

Sends a topological space to its specialisation order.

Equations
  • One or more equations did not get rendered due to their size.
source
@[simp]
theorem topToPreord_obj (X : TopCat) :
topToPreord.obj X = Preord.of (Specialization ↑X)
source
@[simp]
theorem topToPreord_map {X Y : TopCat} (f : X ⟶ Y) :
topToPreord.map f = Specialization.map (TopCat.Hom.hom f)