Documentation

Mathlib.Topology.Order.LowerUpperTopology

Lower and Upper topology #

This file introduces the lower topology on a preorder as the topology generated by the complements of the left-closed right-infinite intervals.

For completeness we also introduce the dual upper topology, generated by the complements of the right-closed left-infinite intervals.

Main statements #

Implementation notes #

A type synonym WithLower is introduced and for a preorder α, WithLower α is made an instance of TopologicalSpace by the topology generated by the complements of the closed intervals to infinity.

We define a mixin class IsLower for the class of types which are both a preorder and a topology and where the topology is generated by the complements of the closed intervals to infinity. It is shown that WithLower α is an instance of IsLower.

Similarly for the upper topology.

Motivation #

The lower topology is used with the Scott topology to define the Lawson topology. The restriction of the lower topology to the spectrum of a complete lattice coincides with the hull-kernel topology.

References #

Tags #

lower topology, upper topology, preorder

The lower topology is the topology generated by the complements of the left-closed right-infinite intervals.

Equations
Instances For

    The upper topology is the topology generated by the complements of the right-closed left-infinite intervals.

    Equations
    Instances For
      def Topology.WithLower (α : Type u_1) :
      Type u_1

      Type synonym for a preorder equipped with the lower set topology.

      Equations
      Instances For
        @[match_pattern]

        toLower is the identity function to the WithLower of a type.

        Equations
        Instances For
          @[match_pattern]

          ofLower is the identity function from the WithLower of a type.

          Equations
          Instances For
            @[simp]
            theorem Topology.WithLower.to_WithLower_symm_eq {α : Type u_1} :
            Topology.WithLower.toLower.symm = Topology.WithLower.ofLower
            @[simp]
            theorem Topology.WithLower.of_WithLower_symm_eq {α : Type u_1} :
            Topology.WithLower.ofLower.symm = Topology.WithLower.toLower
            @[simp]
            theorem Topology.WithLower.toLower_ofLower {α : Type u_1} (a : Topology.WithLower α) :
            Topology.WithLower.toLower (Topology.WithLower.ofLower a) = a
            @[simp]
            theorem Topology.WithLower.ofLower_toLower {α : Type u_1} (a : α) :
            Topology.WithLower.ofLower (Topology.WithLower.toLower a) = a
            theorem Topology.WithLower.toLower_inj {α : Type u_1} {a : α} {b : α} :
            Topology.WithLower.toLower a = Topology.WithLower.toLower b a = b
            theorem Topology.WithLower.ofLower_inj {α : Type u_1} {a : Topology.WithLower α} {b : Topology.WithLower α} :
            Topology.WithLower.ofLower a = Topology.WithLower.ofLower b a = b
            def Topology.WithLower.rec {α : Type u_2} {β : Topology.WithLower αSort u_1} (h : (a : α) → β (Topology.WithLower.toLower a)) (a : Topology.WithLower α) :
            β a

            A recursor for WithLower. Use as induction x.

            Equations
            Instances For
              Equations
              • = inst
              Equations
              • Topology.WithLower.instInhabited = inst
              Equations
              • Topology.WithLower.instPreorder = inst
              Equations
              theorem Topology.WithLower.isOpen_preimage_ofLower {α : Type u_1} [Preorder α] {s : Set α} :
              IsOpen (Topology.WithLower.ofLower ⁻¹' s) TopologicalSpace.IsOpen s
              theorem Topology.WithLower.isOpen_def {α : Type u_1} [Preorder α] (T : Set (Topology.WithLower α)) :
              IsOpen T TopologicalSpace.IsOpen (Topology.WithLower.toLower ⁻¹' T)
              def Topology.WithUpper (α : Type u_1) :
              Type u_1

              Type synonym for a preorder equipped with the upper topology.

              Equations
              Instances For
                @[match_pattern]

                toUpper is the identity function to the WithUpper of a type.

                Equations
                Instances For
                  @[match_pattern]

                  ofUpper is the identity function from the WithUpper of a type.

                  Equations
                  Instances For
                    @[simp]
                    theorem Topology.WithUpper.to_WithUpper_symm_eq {α : Type u_1} :
                    Topology.WithUpper.toUpper.symm = Topology.WithUpper.ofUpper
                    @[simp]
                    theorem Topology.WithUpper.of_WithUpper_symm_eq {α : Type u_1} :
                    Topology.WithUpper.ofUpper.symm = Topology.WithUpper.toUpper
                    @[simp]
                    theorem Topology.WithUpper.toUpper_ofUpper {α : Type u_1} (a : Topology.WithUpper α) :
                    Topology.WithUpper.toUpper (Topology.WithUpper.ofUpper a) = a
                    @[simp]
                    theorem Topology.WithUpper.ofUpper_toUpper {α : Type u_1} (a : α) :
                    Topology.WithUpper.ofUpper (Topology.WithUpper.toUpper a) = a
                    theorem Topology.WithUpper.toUpper_inj {α : Type u_1} {a : α} {b : α} :
                    Topology.WithUpper.toUpper a = Topology.WithUpper.toUpper b a = b
                    theorem Topology.WithUpper.ofUpper_inj {α : Type u_1} {a : Topology.WithUpper α} {b : Topology.WithUpper α} :
                    Topology.WithUpper.ofUpper a = Topology.WithUpper.ofUpper b a = b
                    def Topology.WithUpper.rec {α : Type u_2} {β : Topology.WithUpper αSort u_1} (h : (a : α) → β (Topology.WithUpper.toUpper a)) (a : Topology.WithUpper α) :
                    β a

                    A recursor for WithUpper. Use as induction x.

                    Equations
                    Instances For
                      Equations
                      • = inst
                      Equations
                      • Topology.WithUpper.instInhabited = inst
                      Equations
                      • Topology.WithUpper.instPreorder = inst
                      Equations
                      theorem Topology.WithUpper.isOpen_preimage_ofUpper {α : Type u_1} [Preorder α] {s : Set α} :
                      IsOpen (Topology.WithUpper.ofUpper ⁻¹' s) TopologicalSpace.IsOpen s
                      theorem Topology.WithUpper.isOpen_def {α : Type u_1} [Preorder α] {s : Set (Topology.WithUpper α)} :
                      IsOpen s TopologicalSpace.IsOpen (Topology.WithUpper.toUpper ⁻¹' s)
                      class Topology.IsLower (α : Type u_1) [t : TopologicalSpace α] [Preorder α] :

                      The lower topology is the topology generated by the complements of the left-closed right-infinite intervals.

                      Instances
                        class Topology.IsUpper (α : Type u_1) [t : TopologicalSpace α] [Preorder α] :

                        The upper topology is the topology generated by the complements of the right-closed left-infinite intervals.

                        Instances

                          The lower topology is homeomorphic to the upper topology on the dual order

                          Equations
                          • Topology.WithLower.toDualHomeomorph = { toFun := OrderDual.toDual, invFun := OrderDual.ofDual, left_inv := , right_inv := , continuous_toFun := , continuous_invFun := }
                          Instances For
                            def Topology.IsLower.lowerBasis (α : Type u_1) [Preorder α] :
                            Set (Set α)

                            The complements of the upper closures of finite sets are a collection of lower sets which form a basis for the lower topology.

                            Equations
                            Instances For

                              If α is equipped with the lower topology, then it is homeomorphic to WithLower α.

                              Equations
                              • Topology.IsLower.withLowerHomeomorph = Topology.WithLower.ofLower.toHomeomorphOfInducing
                              Instances For

                                Left-closed right-infinite intervals [a, ∞) are closed in the lower topology.

                                Equations
                                • =
                                theorem Topology.IsLower.isClosed_upperClosure {α : Type u_1} [Preorder α] [TopologicalSpace α] [Topology.IsLower α] {s : Set α} (h : s.Finite) :

                                The upper closure of a finite set is closed in the lower topology.

                                Every set open in the lower topology is a lower set.

                                @[simp]

                                The closure of a singleton {a} in the lower topology is the left-closed right-infinite interval [a, ∞).

                                theorem Topology.IsLower.continuous_iff_Ici {α : Type u_2} {β : Type u_1} [Preorder α] [TopologicalSpace α] [Topology.IsLower α] [TopologicalSpace β] {f : βα} :
                                Continuous f ∀ (a : α), IsClosed (f ⁻¹' Set.Ici a)

                                A function f : β → α with lower topology in the codomain is continuous if and only if the preimage of every interval Set.Ici a is a closed set.

                                @[deprecated Topology.IsLower.continuous_iff_Ici]
                                theorem Topology.IsLower.continuous_of_Ici {α : Type u_2} {β : Type u_1} [Preorder α] [TopologicalSpace α] [Topology.IsLower α] [TopologicalSpace β] {f : βα} :
                                (∀ (a : α), IsClosed (f ⁻¹' Set.Ici a))Continuous f

                                A function f : β → α with lower topology in the codomain is continuous provided that the preimage of every interval Set.Ici a is a closed set.

                                @[instance 90]

                                The lower topology on a partial order is T₀.

                                Equations
                                • =
                                def Topology.IsUpper.upperBasis (α : Type u_1) [Preorder α] :
                                Set (Set α)

                                The complements of the lower closures of finite sets are a collection of upper sets which form a basis for the upper topology.

                                Equations
                                Instances For

                                  If α is equipped with the upper topology, then it is homeomorphic to WithUpper α.

                                  Equations
                                  • Topology.IsUpper.withUpperHomeomorph = Topology.WithUpper.ofUpper.toHomeomorphOfInducing
                                  Instances For

                                    Left-infinite right-closed intervals (-∞,a] are closed in the upper topology.

                                    Equations
                                    • =
                                    theorem Topology.IsUpper.isClosed_lowerClosure {α : Type u_1} [Preorder α] [TopologicalSpace α] [Topology.IsUpper α] {s : Set α} (h : s.Finite) :

                                    The lower closure of a finite set is closed in the upper topology.

                                    Every set open in the upper topology is a upper set.

                                    @[simp]

                                    The closure of a singleton {a} in the upper topology is the left-infinite right-closed interval (-∞,a].

                                    theorem Topology.IsUpper.continuous_iff_Iic {α : Type u_2} {β : Type u_1} [Preorder α] [TopologicalSpace α] [Topology.IsUpper α] [TopologicalSpace β] {f : βα} :
                                    Continuous f ∀ (a : α), IsClosed (f ⁻¹' Set.Iic a)

                                    A function f : β → α with upper topology in the codomain is continuous if and only if the preimage of every interval Set.Iic a is a closed set.

                                    @[deprecated]
                                    theorem Topology.IsUpper.continuous_of_Iic {α : Type u_2} {β : Type u_1} [Preorder α] [TopologicalSpace α] [Topology.IsUpper α] [TopologicalSpace β] {f : βα} (h : ∀ (a : α), IsClosed (f ⁻¹' Set.Iic a)) :

                                    A function f : β → α with upper topology in the codomain is continuous provided that the preimage of every interval Set.Iic a is a closed set.

                                    @[instance 90]

                                    The upper topology on a partial order is T₀.

                                    Equations
                                    • =
                                    Equations
                                    • =
                                    Equations
                                    • =
                                    @[instance 90]
                                    Equations
                                    • =
                                    @[instance 90]
                                    Equations
                                    • =