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
TopologicalSpace
,
AlexandrovDiscrete
:
Type u_1
Auxiliary typeclass to define the category of Alexandrov-discrete spaces. Do not use this
directly. Use AlexandrovDiscrete
instead.
Instances
@[simp]
theorem
AlexDisc.coe_forgetToTop
(X : AlexDisc)
:
↑((CategoryTheory.forget₂ AlexDisc TopCat).obj X) = ↑X
Construct a bundled AlexDisc
from the underlying topological space.
Instances For
@[simp]
theorem
AlexDisc.coe_of
(α : Type u_1)
[TopologicalSpace α]
[AlexandrovDiscrete α]
:
↑(AlexDisc.of α) = α
@[simp]
theorem
AlexDisc.forgetToTop_of
(α : Type u_1)
[TopologicalSpace α]
[AlexandrovDiscrete α]
:
(CategoryTheory.forget₂ AlexDisc TopCat).obj (AlexDisc.of α) = TopCat.of α
@[simp]
theorem
AlexDisc.Iso.mk_hom
{α : AlexDisc}
{β : AlexDisc}
(e : ↑α ≃ₜ ↑β)
:
(AlexDisc.Iso.mk e).hom = Homeomorph.toContinuousMap e
@[simp]
theorem
AlexDisc.Iso.mk_inv
{α : AlexDisc}
{β : AlexDisc}
(e : ↑α ≃ₜ ↑β)
:
(AlexDisc.Iso.mk e).inv = Homeomorph.toContinuousMap (Homeomorph.symm e)
@[simp]
theorem
alexDiscEquivPreord_unitIso :
alexDiscEquivPreord.unitIso = CategoryTheory.NatIso.ofComponents fun X => AlexDisc.Iso.mk (id (homeoWithUpperSetTopologyorderIso ↑X))
@[simp]
theorem
alexDiscEquivPreord_inverse_map :
∀ {X Y : Preord} (f : ↑X →o ↑Y), alexDiscEquivPreord.inverse.map f = Topology.WithUpperSet.map f
@[simp]
@[simp]
theorem
alexDiscEquivPreord_counitIso :
alexDiscEquivPreord.counitIso = CategoryTheory.NatIso.ofComponents fun X =>
Preord.Iso.mk (id (OrderIso.symm (orderIsoSpecializationWithUpperSetTopology ↑X)))
@[simp]
theorem
alexDiscEquivPreord_inverse_obj
(X : Preord)
:
alexDiscEquivPreord.inverse.obj X = AlexDisc.of (Topology.WithUpperSet ↑X)
Sends a topological space to its specialisation order.