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.

source

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

source

def AlexDisc :

Type (u_1 + 1)

The category of Alexandrov-discrete spaces.

Instances For

source

instance AlexDisc.instCoeSort :

CoeSort AlexDisc (Type u_1)

source

instance AlexDisc.instTopologicalSpace (α : AlexDisc) :

TopologicalSpace ↑α

source

instance AlexDisc.instAlexandrovDiscrete (α : AlexDisc) :

AlexandrovDiscrete ↑α

source

instance AlexDisc.instParentProjectionTypeTopologicalSpaceAlexandrovDiscreteSpaceToTopologicalSpace :

CategoryTheory.BundledHom.ParentProjection @AlexandrovDiscreteSpace.toTopologicalSpace

source

instance AlexDisc.instConcreteCategory :

CategoryTheory.ConcreteCategory AlexDisc

source

instance AlexDisc.instHasForgetToTop :

CategoryTheory.HasForget₂ AlexDisc TopCat

source

instance AlexDisc.ForgetToTop.instFull :

CategoryTheory.Full (CategoryTheory.forget₂ AlexDisc TopCat)

source

instance AlexDisc.ForgetToTop.instFaithful :

CategoryTheory.Faithful (CategoryTheory.forget₂ AlexDisc TopCat)

source

@[simp]

theorem AlexDisc.coe_forgetToTop (X : AlexDisc) :

↑((CategoryTheory.forget₂ AlexDisc TopCat).obj X) = ↑X

source

def AlexDisc.of (α : Type u_1) [TopologicalSpace α] [AlexandrovDiscrete α] :

AlexDisc

Construct a bundled AlexDisc from the underlying topological space.

Instances For

source

@[simp]

theorem AlexDisc.coe_of (α : Type u_1) [TopologicalSpace α] [AlexandrovDiscrete α] :

↑(AlexDisc.of α) = α

source

@[simp]

theorem AlexDisc.forgetToTop_of (α : Type u_1) [TopologicalSpace α] [AlexandrovDiscrete α] :

(CategoryTheory.forget₂ AlexDisc TopCat).obj (AlexDisc.of α) = TopCat.of α

source

@[simp]

theorem AlexDisc.Iso.mk_hom {α : AlexDisc} {β : AlexDisc} (e : ↑α ≃ₜ ↑β) :

(AlexDisc.Iso.mk e).hom = Homeomorph.toContinuousMap e

source

@[simp]

theorem AlexDisc.Iso.mk_inv {α : AlexDisc} {β : AlexDisc} (e : ↑α ≃ₜ ↑β) :

(AlexDisc.Iso.mk e).inv = Homeomorph.toContinuousMap (Homeomorph.symm e)

source

def AlexDisc.Iso.mk {α : AlexDisc} {β : AlexDisc} (e : ↑α ≃ₜ ↑β) :

α ≅ β

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

Instances For

source

@[simp]

theorem alexDiscEquivPreord_unitIso :

alexDiscEquivPreord.unitIso = CategoryTheory.NatIso.ofComponents fun X => AlexDisc.Iso.mk (id (homeoWithUpperSetTopologyorderIso ↑X))

source

@[simp]

theorem alexDiscEquivPreord_inverse_map :

∀ {X Y : Preord} (f : ↑X →o ↑Y), alexDiscEquivPreord.inverse.map f = Topology.WithUpperSet.map f

source

@[simp]

theorem alexDiscEquivPreord_functor :

alexDiscEquivPreord.functor = CategoryTheory.Functor.comp (CategoryTheory.forget₂ AlexDisc TopCat) topToPreord

source

@[simp]

theorem alexDiscEquivPreord_counitIso :

alexDiscEquivPreord.counitIso = CategoryTheory.NatIso.ofComponents fun X => Preord.Iso.mk (id (OrderIso.symm (orderIsoSpecializationWithUpperSetTopology ↑X)))

source

@[simp]

theorem alexDiscEquivPreord_inverse_obj (X : Preord) :

alexDiscEquivPreord.inverse.obj X = AlexDisc.of (Topology.WithUpperSet ↑X)

source

def alexDiscEquivPreord :

AlexDisc ≌ Preord

Sends a topological space to its specialisation order.

Instances For