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.

• IsOpen : Set α → Prop
• isOpen_univ : TopologicalSpace.IsOpen Set.univ
• isOpen_inter (s t : Set α) : TopologicalSpace.IsOpen s → TopologicalSpace.IsOpen t → TopologicalSpace.IsOpen (s ∩ t)
• isOpen_sUnion (s : Set (Set α)) : (∀ t ∈ s, TopologicalSpace.IsOpen t) → TopologicalSpace.IsOpen (⋃₀ s)
• isOpen_sInter (S : Set (Set α)) : (∀ s ∈ S, IsOpen s) → IsOpen (⋂₀ S)

def AlexDisc : Type (u_1 + 1)

The category of Alexandrov-discrete spaces.

Equations

• AlexDisc = CategoryTheory.Bundled AlexandrovDiscreteSpace

instance AlexDisc.instCoeSort : CoeSort AlexDisc (Type u_1)

Equations

• AlexDisc.instCoeSort = CategoryTheory.Bundled.coeSort

instance AlexDisc.instTopologicalSpace (α : AlexDisc) : TopologicalSpace ↑α

Equations

• α.instTopologicalSpace = AlexandrovDiscreteSpace.toTopologicalSpace

instance AlexDisc.instAlexandrovDiscrete (α : AlexDisc) : AlexandrovDiscrete ↑α

instance AlexDisc.instParentProjectionTopologicalSpaceAlexandrovDiscreteSpaceToTopologicalSpace : CategoryTheory.BundledHom.ParentProjection @AlexandrovDiscreteSpace.toTopologicalSpace

instance instAlexDiscLargeCategory : CategoryTheory.LargeCategory AlexDisc

Equations

• instAlexDiscLargeCategory = CategoryTheory.BundledHom.category (CategoryTheory.BundledHom.MapHom ContinuousMap @AlexandrovDiscreteSpace.toTopologicalSpace)

instance AlexDisc.instConcreteCategory : CategoryTheory.ConcreteCategory AlexDisc

Equations

• AlexDisc.instConcreteCategory = CategoryTheory.BundledHom.concreteCategory (CategoryTheory.BundledHom.MapHom ContinuousMap @AlexandrovDiscreteSpace.toTopologicalSpace)

instance AlexDisc.instHasForgetToTop : CategoryTheory.HasForget₂ AlexDisc TopCat

Equations

• AlexDisc.instHasForgetToTop = CategoryTheory.BundledHom.forget₂ ContinuousMap @AlexandrovDiscreteSpace.toTopologicalSpace

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

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

@[simp]

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

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

Construct a bundled AlexDisc from the underlying topological space.

Equations

• AlexDisc.of α = { α := α, str := AlexandrovDiscreteSpace.mk }

@[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 α

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

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

Equations

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

@[simp]

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

@[simp]

theorem AlexDisc.Iso.mk_inv {α β : AlexDisc} (e : ↑α ≃ₜ ↑β) : (AlexDisc.Iso.mk e).inv = ↑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_functor : alexDiscEquivPreord.functor = (CategoryTheory.forget₂ AlexDisc TopCat).comp topToPreord

@[simp]

theorem alexDiscEquivPreord_inverse_obj (X : Preord) : alexDiscEquivPreord.inverse.obj X = AlexDisc.of (Topology.WithUpperSet ↑X)

@[simp]

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

@[simp]

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

@[simp]

theorem alexDiscEquivPreord_inverse_map {X✝ Y✝ : Preord} (f : ↑X✝ →o ↑Y✝) : alexDiscEquivPreord.inverse.map f = Topology.WithUpperSet.map f