# Category of Alexandrov-discrete topological spaces #

This defines AlexDisc, the category of Alexandrov-discrete topological spaces with continuous maps, and proves it's equivalent to the category of preorders.

class AlexandrovDiscreteSpace (α : Type u_1) extends , :
Type u_1

Auxiliary typeclass to define the category of Alexandrov-discrete spaces. Do not use this directly. Use AlexandrovDiscrete instead.

Instances
def AlexDisc :
Type (u_1 + 1)

The category of Alexandrov-discrete spaces.

Equations
Instances For
Equations
Equations
• α.instTopologicalSpace = AlexandrovDiscreteSpace.toTopologicalSpace
Equations
• =
Equations
instance AlexDisc.forgetToTop_faithful :
.Faithful
Equations
@[simp]
theorem AlexDisc.coe_forgetToTop (X : AlexDisc) :
( X) = X
def AlexDisc.of (α : Type u_1) [] :

Construct a bundled AlexDisc from the underlying topological space.

Equations
• = { α := α, str := AlexandrovDiscreteSpace.mk }
Instances For
@[simp]
theorem AlexDisc.coe_of (α : Type u_1) [] :
() = α
@[simp]
theorem AlexDisc.forgetToTop_of (α : Type u_1) [] :
() =
@[simp]
theorem AlexDisc.Iso.mk_inv {α : AlexDisc} {β : AlexDisc} (e : α ≃ₜ β) :
().inv = e.symm.toContinuousMap
@[simp]
theorem AlexDisc.Iso.mk_hom {α : AlexDisc} {β : AlexDisc} (e : α ≃ₜ β) :
().hom = e.toContinuousMap
def AlexDisc.Iso.mk {α : AlexDisc} {β : AlexDisc} (e : α ≃ₜ β) :
α β

Constructs an equivalence between preorders from an order isomorphism between them.

Equations
• = { hom := e.toContinuousMap, inv := e.symm.toContinuousMap, hom_inv_id := , inv_hom_id := }
Instances For
@[simp]
theorem alexDiscEquivPreord_inverse_map :
∀ {X Y : Preord} (f : X →o Y), alexDiscEquivPreord.inverse.map f =

Sends a topological space to its specialisation order.

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