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

    Instances
      source
      def AlexDisc :
      Type (u_1 + 1)

      The category of Alexandrov-discrete spaces.

      Equations
      Instances For
        source
        instance AlexDisc.instCoeSort :
        CoeSort AlexDisc (Type u_1)
        Equations
        source
        instance AlexDisc.instTopologicalSpace (α : AlexDisc) :
        TopologicalSpace ↑α
        Equations
        source
        instance AlexDisc.instAlexandrovDiscrete (α : AlexDisc) :
        AlexandrovDiscrete ↑α
        Equations
        source
        instance AlexDisc.instParentProjectionTypeTopologicalSpaceAlexandrovDiscreteSpaceToTopologicalSpace :
        CategoryTheory.BundledHom.ParentProjection @AlexandrovDiscreteSpace.toTopologicalSpace
        Equations
        source
        instance AlexDisc.instConcreteCategory :
        CategoryTheory.ConcreteCategory AlexDisc
        Equations
        source
        instance AlexDisc.instHasForgetToTop :
        CategoryTheory.HasForget₂ AlexDisc TopCat
        Equations
        source
        instance AlexDisc.ForgetToTop.instFull :
        CategoryTheory.Full (CategoryTheory.forget₂ AlexDisc TopCat)
        Equations
        source
        instance AlexDisc.ForgetToTop.instFaithful :
        CategoryTheory.Faithful (CategoryTheory.forget₂ AlexDisc TopCat)
        Equations
        source
        @[simp]
        theorem AlexDisc.coe_forgetToTop (X : AlexDisc) :
        ↑((CategoryTheory.forget₂ AlexDisc TopCat).toPrefunctor.obj X) = ↑X
        source
        def AlexDisc.of (α : Type u_1) [TopologicalSpace α] [AlexandrovDiscrete α] :
        AlexDisc

        Construct a bundled AlexDisc from the underlying topological space.

        Equations
        Instances For
          source
          @[simp]
          theorem AlexDisc.coe_of (α : Type u_1) [TopologicalSpace α] [AlexandrovDiscrete α] :
          ↑(AlexDisc.of α) = α
          source
          @[simp]
          theorem AlexDisc.forgetToTop_of (α : Type u_1) [TopologicalSpace α] [AlexandrovDiscrete α] :
          (CategoryTheory.forget₂ AlexDisc TopCat).toPrefunctor.obj (AlexDisc.of α) = TopCat.of α
          source
          @[simp]
          theorem AlexDisc.Iso.mk_hom {α : AlexDisc} {β : AlexDisc} (e : ↑α ≃ₜ ↑β) :
          (AlexDisc.Iso.mk e).hom = Homeomorph.toContinuousMap e
          source
          @[simp]
          theorem AlexDisc.Iso.mk_inv {α : AlexDisc} {β : AlexDisc} (e : ↑α ≃ₜ ↑β) :
          (AlexDisc.Iso.mk e).inv = Homeomorph.toContinuousMap (Homeomorph.symm e)
          source
          def AlexDisc.Iso.mk {α : AlexDisc} {β : AlexDisc} (e : ↑α ≃ₜ ↑β) :
          α ≅ β

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

          Equations
          Instances For
            source
            @[simp]
            theorem alexDiscEquivPreord_unitIso :
            alexDiscEquivPreord.unitIso = CategoryTheory.NatIso.ofComponents fun (X : AlexDisc) => AlexDisc.Iso.mk (id (homeoWithUpperSetTopologyorderIso ↑X))
            source
            @[simp]
            theorem alexDiscEquivPreord_inverse_map :
            ∀ {X Y : Preord} (f : ↑X →o ↑Y), alexDiscEquivPreord.inverse.toPrefunctor.map f = Topology.WithUpperSet.map f
            source
            @[simp]
            theorem alexDiscEquivPreord_functor :
            alexDiscEquivPreord.functor = CategoryTheory.Functor.comp (CategoryTheory.forget₂ AlexDisc TopCat) topToPreord
            source
            @[simp]
            theorem alexDiscEquivPreord_counitIso :
            alexDiscEquivPreord.counitIso = CategoryTheory.NatIso.ofComponents fun (X : Preord) => Preord.Iso.mk (id (OrderIso.symm (orderIsoSpecializationWithUpperSetTopology ↑X)))
            source
            @[simp]
            theorem alexDiscEquivPreord_inverse_obj (X : Preord) :
            alexDiscEquivPreord.inverse.toPrefunctor.obj X = AlexDisc.of (Topology.WithUpperSet ↑X)
            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