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
                      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