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.

Auxiliary typeclass to define the category of Alexandrov-discrete spaces. Do not use this directly. Use AlexandrovDiscrete instead.

    Instances
      def AlexDisc :
      Type (u_1 + 1)

      The category of Alexandrov-discrete spaces.

      Equations
      Instances For
        Equations
        Equations
        • α.instTopologicalSpace = AlexandrovDiscreteSpace.toTopologicalSpace

        Construct a bundled AlexDisc from the underlying topological space.

        Equations
        • AlexDisc.of α = { α := α, str := AlexandrovDiscreteSpace.mk }
        Instances For
          @[simp]
          theorem AlexDisc.coe_of (α : Type u_1) [TopologicalSpace α] [AlexandrovDiscrete α] :
          (AlexDisc.of α) = α
          @[simp]
          theorem AlexDisc.Iso.mk_hom {α : AlexDisc} {β : AlexDisc} (e : α ≃ₜ β) :
          (AlexDisc.Iso.mk e).hom = e
          @[simp]
          theorem AlexDisc.Iso.mk_inv {α : AlexDisc} {β : AlexDisc} (e : α ≃ₜ β) :
          (AlexDisc.Iso.mk e).inv = e.symm
          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
            @[simp]
            theorem alexDiscEquivPreord_inverse_map :
            ∀ {X Y : Preord} (f : X →o Y), alexDiscEquivPreord.inverse.map f = Topology.WithUpperSet.map f

            Sends a topological space to its specialisation order.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For