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.

structure AlexDiscextends TopCat : Type (u_1 + 1)

The category of Alexandrov-discrete spaces.

• carrier : Type u_1
• str : TopologicalSpace ↑self.toTopCat
• is_alexandrovDiscrete : AlexandrovDiscrete ↑self.toTopCat

instance AlexDisc.instCoeSortType : CoeSort AlexDisc (Type u_1)

Equations

• AlexDisc.instCoeSortType = { coe := fun (X : AlexDisc) => ↑X.toTopCat }

instance AlexDisc.category : CategoryTheory.Category.{u_1, u_1 + 1} AlexDisc

Equations

• AlexDisc.category = inferInstanceAs (CategoryTheory.Category.{?u.2, ?u.2 + 1} (CategoryTheory.InducedCategory TopCat AlexDisc.toTopCat))

instance AlexDisc.concreteCategory : CategoryTheory.ConcreteCategory AlexDisc fun (x1 x2 : AlexDisc) => C(↑x1.toTopCat, ↑x2.toTopCat)

Equations

• AlexDisc.concreteCategory = CategoryTheory.InducedCategory.concreteCategory AlexDisc.toTopCat

instance AlexDisc.instHasForgetToTop : CategoryTheory.HasForget₂ AlexDisc TopCat

Equations

• AlexDisc.instHasForgetToTop = CategoryTheory.InducedCategory.hasForget₂ AlexDisc.toTopCat

instance AlexDisc.forgetToTop_full : (CategoryTheory.forget₂ AlexDisc TopCat).Full

instance AlexDisc.forgetToTop_faithful : (CategoryTheory.forget₂ AlexDisc TopCat).Faithful

@[reducible, inline]

abbrev AlexDisc.of (X : Type u_1) [TopologicalSpace X] [AlexandrovDiscrete X] : AlexDisc

Construct a bundled AlexDisc from the underlying topological space.

Equations

• AlexDisc.of X = { carrier := X, str := inst✝¹, is_alexandrovDiscrete := inst✝ }

theorem AlexDisc.coe_of (α : Type u_1) [TopologicalSpace α] [AlexandrovDiscrete α] : ↑(of α).toTopCat = α

@[simp]

theorem AlexDisc.forgetToTop_of (α : Type u_1) [TopologicalSpace α] [AlexandrovDiscrete α] : (CategoryTheory.forget₂ AlexDisc TopCat).obj (of α) = { carrier := α, str := inst✝ }

@[simp]

theorem AlexDisc.coe_forgetToTop (X : AlexDisc) : ↑((CategoryTheory.forget₂ AlexDisc TopCat).obj X) = ↑X.toTopCat

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

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

Equations

• AlexDisc.Iso.mk e = { hom := CategoryTheory.ConcreteCategory.ofHom ↑e, inv := CategoryTheory.ConcreteCategory.ofHom ↑e.symm, hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[simp]

theorem AlexDisc.Iso.mk_hom {α β : AlexDisc} (e : ↑α.toTopCat ≃ₜ ↑β.toTopCat) : (mk e).hom = CategoryTheory.ConcreteCategory.ofHom ↑e

@[simp]

theorem AlexDisc.Iso.mk_inv {α β : AlexDisc} (e : ↑α.toTopCat ≃ₜ ↑β.toTopCat) : (mk e).inv = CategoryTheory.ConcreteCategory.ofHom ↑e.symm

def alexDiscEquivPreord : AlexDisc ≌ Preord

Sends a topological space to its specialisation order.

Equations

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

@[simp]

theorem alexDiscEquivPreord_inverse_obj_str (X : Preord) : (alexDiscEquivPreord.inverse.obj X).str = Topology.WithUpperSet.instTopologicalSpace

@[simp]

theorem alexDiscEquivPreord_inverse_obj_carrier (X : Preord) : ↑(alexDiscEquivPreord.inverse.obj X).toTopCat = Topology.WithUpperSet ↑X

@[simp]

theorem alexDiscEquivPreord_functor : alexDiscEquivPreord.functor = (CategoryTheory.forget₂ AlexDisc TopCat).comp topToPreord

@[simp]

theorem alexDiscEquivPreord_unitIso : alexDiscEquivPreord.unitIso = CategoryTheory.NatIso.ofComponents (fun (X : AlexDisc) => AlexDisc.Iso.mk (id (homeoWithUpperSetTopologyorderIso ↑X.toTopCat))) @alexDiscEquivPreord._proof_3

@[simp]

theorem alexDiscEquivPreord_inverse_map {X✝ Y✝ : Preord} (f : X✝ ⟶ Y✝) : alexDiscEquivPreord.inverse.map f = CategoryTheory.ConcreteCategory.ofHom (Topology.WithUpperSet.map (Preord.Hom.hom f))

@[simp]

theorem alexDiscEquivPreord_counitIso : alexDiscEquivPreord.counitIso = CategoryTheory.NatIso.ofComponents (fun (X : Preord) => Preord.Iso.mk (id (orderIsoSpecializationWithUpperSetTopology ↑X).symm)) @alexDiscEquivPreord._proof_4