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
        • α.instTopologicalSpace = AlexandrovDiscreteSpace.toTopologicalSpace
        source
        instance AlexDisc.instAlexandrovDiscrete (α : AlexDisc) :
        AlexandrovDiscrete ↑α
        Equations
        • ⋯ = ⋯
        source
        instance AlexDisc.instParentProjectionTopologicalSpaceAlexandrovDiscreteSpaceToTopologicalSpace :
        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_full :
        (CategoryTheory.forget₂ AlexDisc TopCat).Full
        Equations
        source
        instance AlexDisc.forgetToTop_faithful :
        (CategoryTheory.forget₂ AlexDisc TopCat).Faithful
        Equations
        source
        @[simp]
        theorem AlexDisc.coe_forgetToTop (X : AlexDisc) :
        ↑((CategoryTheory.forget₂ AlexDisc TopCat).obj X) = ↑X
        source
        def AlexDisc.of (α : Type u_1) [TopologicalSpace α] [AlexandrovDiscrete α] :
        AlexDisc

        Construct a bundled AlexDisc from the underlying topological space.

        Equations
        • AlexDisc.of α = { α := α, str := AlexandrovDiscreteSpace.mk }
        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).obj (AlexDisc.of α) = TopCat.of α
          source
          @[simp]
          theorem AlexDisc.Iso.mk_hom {α : AlexDisc} {β : AlexDisc} (e : ↑α ≃ₜ ↑β) :
          (AlexDisc.Iso.mk e).hom = ↑e
          source
          @[simp]
          theorem AlexDisc.Iso.mk_inv {α : AlexDisc} {β : AlexDisc} (e : ↑α ≃ₜ ↑β) :
          (AlexDisc.Iso.mk e).inv = ↑e.symm
          source
          def AlexDisc.Iso.mk {α : AlexDisc} {β : 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 := ⋯ }
          Instances For
            source
            @[simp]
            theorem alexDiscEquivPreord_unitIso :
            alexDiscEquivPreord.unitIso = CategoryTheory.NatIso.ofComponents (fun (X : AlexDisc) => AlexDisc.Iso.mk (id (homeoWithUpperSetTopologyorderIso ↑X))) @alexDiscEquivPreord.proof_4
            source
            @[simp]
            theorem alexDiscEquivPreord_inverse_map :
            ∀ {X Y : Preord} (f : ↑X →o ↑Y), alexDiscEquivPreord.inverse.map f = Topology.WithUpperSet.map f
            source
            @[simp]
            theorem alexDiscEquivPreord_functor :
            alexDiscEquivPreord.functor = (CategoryTheory.forget₂ AlexDisc TopCat).comp topToPreord
            source
            @[simp]
            theorem alexDiscEquivPreord_inverse_obj (X : Preord) :
            alexDiscEquivPreord.inverse.obj X = AlexDisc.of (Topology.WithUpperSet ↑X)
            source
            @[simp]
            theorem alexDiscEquivPreord_counitIso :
            alexDiscEquivPreord.counitIso = CategoryTheory.NatIso.ofComponents (fun (X : Preord) => Preord.Iso.mk (id (orderIsoSpecializationWithUpperSetTopology ↑X).symm)) @alexDiscEquivPreord.proof_5
            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