Documentation

Mathlib.Topology.Specialization

Specialization order #

This file defines a type synonym for a topological space considered with its specialisation order.

source
def Specialization (α : Type u_1) :
Type u_1

Type synonym for a topological space considered with its specialisation order.

Equations
Instances For
    source
    @[match_pattern]
    def Specialization.toEquiv {α : Type u_1} :
    α ≃ Specialization α

    toEquiv is the "identity" function to the Specialization of a type.

    Equations
    Instances For
      source
      @[match_pattern]
      def Specialization.ofEquiv {α : Type u_1} :
      Specialization α ≃ α

      ofEquiv is the identity function from the Specialization of a type.

      Equations
      Instances For
        source
        @[simp]
        theorem Specialization.toEquiv_symm {α : Type u_1} :
        Specialization.toEquiv.symm = Specialization.ofEquiv
        source
        @[simp]
        theorem Specialization.ofEquiv_symm {α : Type u_1} :
        Specialization.ofEquiv.symm = Specialization.toEquiv
        source
        @[simp]
        theorem Specialization.toEquiv_ofEquiv {α : Type u_1} (a : Specialization α) :
        Specialization.toEquiv (Specialization.ofEquiv a) = a
        source
        @[simp]
        theorem Specialization.ofEquiv_toEquiv {α : Type u_1} (a : α) :
        Specialization.ofEquiv (Specialization.toEquiv a) = a
        source
        @[simp]
        theorem Specialization.toEquiv_inj {α : Type u_1} {a : α} {b : α} :
        Specialization.toEquiv a = Specialization.toEquiv b ↔ a = b
        source
        @[simp]
        theorem Specialization.ofEquiv_inj {α : Type u_1} {a : Specialization α} {b : Specialization α} :
        Specialization.ofEquiv a = Specialization.ofEquiv b ↔ a = b
        source
        def Specialization.rec {α : Type u_1} {β : Specialization α → Sort u_4} (h : (a : α) → β (Specialization.toEquiv a)) (a : α) :
        β a

        A recursor for Specialization. Use as induction x using Specialization.rec.

        Equations
        Instances For
          source
          instance Specialization.instPreorder {α : Type u_1} [TopologicalSpace α] :
          Preorder (Specialization α)
          Equations
          source
          instance Specialization.instPartialOrder {α : Type u_1} [TopologicalSpace α] [T0Space α] :
          PartialOrder (Specialization α)
          Equations
          source
          @[simp]
          theorem Specialization.toEquiv_le_toEquiv {α : Type u_1} [TopologicalSpace α] {a : α} {b : α} :
          Specialization.toEquiv a ≤ Specialization.toEquiv b ↔ b ⤳ a
          source
          @[simp]
          theorem Specialization.ofEquiv_specializes_ofEquiv {α : Type u_1} [TopologicalSpace α] {a : Specialization α} {b : Specialization α} :
          Specialization.ofEquiv a ⤳ Specialization.ofEquiv b ↔ b ≤ a
          source
          @[simp]
          theorem Specialization.isOpen_toEquiv_preimage {α : Type u_1} [TopologicalSpace α] [AlexandrovDiscrete α] {s : Set (Specialization α)} :
          IsOpen (⇑Specialization.toEquiv ⁻¹' s) ↔ IsUpperSet s
          source
          @[simp]
          theorem Specialization.isUpperSet_ofEquiv_preimage {α : Type u_1} [TopologicalSpace α] [AlexandrovDiscrete α] {s : Set α} :
          IsUpperSet (⇑Specialization.ofEquiv ⁻¹' s) ↔ IsOpen s
          source
          def Specialization.map {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (f : C(α, β)) :
          Specialization α →o Specialization β

          A continuous map between topological spaces induces a monotone map between their specialization orders.

          Equations
          Instances For
            source
            @[simp]
            theorem Specialization.map_id {α : Type u_1} [TopologicalSpace α] :
            Specialization.map (ContinuousMap.id α) = OrderHom.id
            source
            @[simp]
            theorem Specialization.map_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] (g : C(β, γ)) (f : C(α, β)) :
            Specialization.map (ContinuousMap.comp g f) = OrderHom.comp (Specialization.map g) (Specialization.map f)
            source
            def orderIsoSpecializationWithUpperSetTopology (α : Type u_1) [Preorder α] :
            α ≃o Specialization (Topology.WithUpperSet α)

            A preorder is isomorphic to the specialisation order of its upper set topology.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              def homeoWithUpperSetTopologyorderIso (α : Type u_1) [TopologicalSpace α] [AlexandrovDiscrete α] :
              α ≃ₜ Topology.WithUpperSet (Specialization α)

              An Alexandrov-discrete space is isomorphic to the upper set topology of its specialisation order.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                @[simp]
                theorem topToPreord_map :
                ∀ {X Y : TopCat} (f : C(↑X, ↑Y)), topToPreord.toPrefunctor.map f = Specialization.map f
                source
                @[simp]
                theorem topToPreord_obj (X : TopCat) :
                topToPreord.toPrefunctor.obj X = Preord.of (Specialization ↑X)
                source
                def topToPreord :
                CategoryTheory.Functor TopCat Preord

                Sends a topological space to its specialisation order.

                Equations
                Instances For