Documentation

Mathlib.Topology.Order.Category.AlexDisc

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
structure AlexDiscextends TopCat :
Type (u_1 + 1)

The category of Alexandrov-discrete spaces.

Instances For
    source
    instance AlexDisc.instCoeSortType :
    CoeSort AlexDisc (Type u_1)
    Equations
    source
    instance AlexDisc.category :
    CategoryTheory.Category.{u_1, u_1 + 1} AlexDisc
    Equations
    source
    instance AlexDisc.concreteCategory :
    CategoryTheory.ConcreteCategory AlexDisc fun (x1 x2 : AlexDisc) => C(↑x1.toTopCat, ↑x2.toTopCat)
    Equations
    source
    instance AlexDisc.instHasForgetToTop :
    CategoryTheory.HasForget₂ AlexDisc TopCat
    Equations
    source
    instance AlexDisc.forgetToTop_full :
    (CategoryTheory.forget₂ AlexDisc TopCat).Full
    source
    instance AlexDisc.forgetToTop_faithful :
    (CategoryTheory.forget₂ AlexDisc TopCat).Faithful
    source
    @[reducible, inline]
    abbrev AlexDisc.of (X : Type u_1) [TopologicalSpace X] [AlexandrovDiscrete X] :
    AlexDisc

    Construct a bundled AlexDisc from the underlying topological space.

    Equations
    Instances For
      source
      theorem AlexDisc.coe_of (α : Type u_1) [TopologicalSpace α] [AlexandrovDiscrete α] :
      ↑(of α).toTopCat = α
      source
      @[simp]
      theorem AlexDisc.forgetToTop_of (α : Type u_1) [TopologicalSpace α] [AlexandrovDiscrete α] :
      (CategoryTheory.forget₂ AlexDisc TopCat).obj (of α) = TopCat.of α
      source
      @[simp]
      theorem AlexDisc.coe_forgetToTop (X : AlexDisc) :
      ↑((CategoryTheory.forget₂ AlexDisc TopCat).obj X) = ↑X.toTopCat
      source
      def AlexDisc.Iso.mk {α β : AlexDisc} (e : ↑α.toTopCat ≃ₜ ↑β.toTopCat) :
      α ≅ β

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

      Equations
      Instances For
        source
        @[simp]
        theorem AlexDisc.Iso.mk_hom {α β : AlexDisc} (e : ↑α.toTopCat ≃ₜ ↑β.toTopCat) :
        (mk e).hom = TopCat.ofHom ↑e
        source
        @[simp]
        theorem AlexDisc.Iso.mk_inv {α β : AlexDisc} (e : ↑α.toTopCat ≃ₜ ↑β.toTopCat) :
        (mk e).inv = TopCat.ofHom ↑e.symm
        source
        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.
        Instances For
          source
          @[simp]
          theorem alexDiscEquivPreord_inverse_obj_str (X : Preord) :
          (alexDiscEquivPreord.inverse.obj X).str = Topology.WithUpperSet.instTopologicalSpace
          source
          @[simp]
          theorem alexDiscEquivPreord_inverse_obj_carrier (X : Preord) :
          ↑(alexDiscEquivPreord.inverse.obj X).toTopCat = Topology.WithUpperSet ↑X
          source
          @[simp]
          theorem alexDiscEquivPreord_functor :
          alexDiscEquivPreord.functor = (CategoryTheory.forget₂ AlexDisc TopCat).comp topToPreord
          source
          @[simp]
          theorem alexDiscEquivPreord_unitIso :
          alexDiscEquivPreord.unitIso = CategoryTheory.NatIso.ofComponents (fun (X : AlexDisc) => AlexDisc.Iso.mk (id (homeoWithUpperSetTopologyorderIso ↑X.toTopCat))) @alexDiscEquivPreord.proof_4
          source
          @[simp]
          theorem alexDiscEquivPreord_inverse_map {X✝ Y✝ : Preord} (f : X✝ ⟶ Y✝) :
          alexDiscEquivPreord.inverse.map f = TopCat.ofHom (Topology.WithUpperSet.map (Preord.Hom.hom f))
          source
          @[simp]
          theorem alexDiscEquivPreord_counitIso :
          alexDiscEquivPreord.counitIso = CategoryTheory.NatIso.ofComponents (fun (X : Preord) => Preord.Iso.mk (id (orderIsoSpecializationWithUpperSetTopology ↑X).symm)) @alexDiscEquivPreord.proof_5