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

The category of Alexandrov-discrete spaces.

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

    Construct a bundled AlexDisc from the underlying topological space.

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

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

      Instances For
        source
        📐 coverage
        @[simp]
        theorem AlexDisc.Iso.mk_inv {α β : AlexDisc} (e : ↑α.toTopCat ≃ₜ ↑β.toTopCat) :
        (mk e).inv = CategoryTheory.ConcreteCategory.ofHom ↑e.symm
        source
        📐 coverage
        @[simp]
        theorem AlexDisc.Iso.mk_hom {α β : AlexDisc} (e : ↑α.toTopCat ≃ₜ ↑β.toTopCat) :
        (mk e).hom = CategoryTheory.ConcreteCategory.ofHom ↑e
        source
        🔸 coverage
        def alexDiscEquivPreord :
        AlexDisc ≌ Preord

        Sends a topological space to its specialisation order.

        Instances For
          source
          📐 coverage
          @[simp]
          theorem alexDiscEquivPreord_counitIso :
          alexDiscEquivPreord.counitIso = CategoryTheory.NatIso.ofComponents (fun (X : Preord) => Preord.Iso.mk (id (orderIsoSpecializationWithUpperSetTopology ↑X).symm)) @alexDiscEquivPreord._proof_4
          source
          📐 coverage
          @[simp]
          theorem alexDiscEquivPreord_inverse_obj_str (X : Preord) :
          (alexDiscEquivPreord.inverse.obj X).str = Topology.WithUpperSet.instTopologicalSpace
          source
          📐 coverage
          @[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))
          source
          📐 coverage
          @[simp]
          theorem alexDiscEquivPreord_functor :
          alexDiscEquivPreord.functor = (CategoryTheory.forget₂ AlexDisc TopCat).comp topToPreord
          source
          📐 coverage
          @[simp]
          theorem alexDiscEquivPreord_unitIso :
          alexDiscEquivPreord.unitIso = CategoryTheory.NatIso.ofComponents (fun (X : AlexDisc) => AlexDisc.Iso.mk (id (homeoWithUpperSetTopologyorderIso ↑X.toTopCat))) @alexDiscEquivPreord._proof_3
          source
          📐 coverage
          @[simp]
          theorem alexDiscEquivPreord_inverse_obj_carrier (X : Preord) :
          ↑(alexDiscEquivPreord.inverse.obj X).toTopCat = Topology.WithUpperSet ↑X