feat: port Topology.Order.LowerTopology (#2163)

Co-authored-by: Johan Commelin <johan@commelin.net>

Mathlib.lean

@@ -1064,6 +1064,7 @@ import Mathlib.Topology.Order
 import Mathlib.Topology.Order.Basic
 import Mathlib.Topology.Order.Hom.Basic
 import Mathlib.Topology.Order.Lattice
+import Mathlib.Topology.Order.LowerTopology
 import Mathlib.Topology.Order.Priestley
 import Mathlib.Topology.Paracompact
 import Mathlib.Topology.Partial

Mathlib/Topology/Order/LowerTopology.lean

@@ -0,0 +1,290 @@
+/-
+Copyright (c) 2023 Christopher Hoskin. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Christopher Hoskin
+
+! This file was ported from Lean 3 source module topology.order.lower_topology
+! leanprover-community/mathlib commit 98e83c3d541c77cdb7da20d79611a780ff8e7d90
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
+-/
+import Mathlib.Topology.Homeomorph
+import Mathlib.Topology.Order.Lattice
+import Mathlib.Order.Hom.CompleteLattice
+
+/-!
+# Lower topology
+
+This file introduces the lower topology on a preorder as the topology generated by the complements
+of the closed intervals to infinity.
+
+## Main statements
+
+- `LowerTopology.t0Space` - the lower topology on a partial order is T₀
+- `LowerTopology.isTopologicalBasis` - the complements of the upper closures of finite
+  subsets form a basis for the lower topology
+- `LowerTopology.continuousInf` - the inf map is continuous with respect to the lower topology
+
+## Implementation notes
+
+A type synonym `WithLowerTopology` is introduced and for a preorder `α`, `WithLowerTopology α`
+is made an instance of `TopologicalSpace` by the topology generated by the complements of the
+closed intervals to infinity.
+
+We define a mixin class `LowerTopology` 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 `WithLowerTopology α` is an instance of `LowerTopology`.
+
+## 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
+
+* [Gierz et al, *A Compendium of Continuous Lattices*][GierzEtAl1980]
+
+## Tags
+
+lower topology, preorder
+-/
+
+
+variable (α β : Type _)
+
+open Set TopologicalSpace
+
+/-- Type synonym for a preorder equipped with the lower topology. -/
+def WithLowerTopology := α
+#align with_lower_topology WithLowerTopology
+
+variable {α β}
+
+namespace WithLowerTopology
+
+/-- `toLower` is the identity function to the `WithLowerTopology` of a type.  -/
+@[match_pattern]
+def toLower : α ≃ WithLowerTopology α := Equiv.refl _
+#align with_lower_topology.to_lower WithLowerTopology.toLower
+
+/-- `ofLower` is the identity function from the `WithLowerTopology` of a type.  -/
+@[match_pattern]
+def ofLower : WithLowerTopology α ≃ α := Equiv.refl _
+#align with_lower_topology.of_lower WithLowerTopology.ofLower
+
+@[simp]
+theorem to_withLowerTopology_symm_eq : (@toLower α).symm = ofLower :=
+  rfl
+#align with_lower_topology.to_with_lower_topology_symm_eq WithLowerTopology.to_withLowerTopology_symm_eq
+
+@[simp]
+theorem of_withLowerTopology_symm_eq : (@ofLower α).symm = toLower :=
+  rfl
+#align with_lower_topology.of_with_lower_topology_symm_eq WithLowerTopology.of_withLowerTopology_symm_eq
+
+@[simp]
+theorem toLower_ofLower (a : WithLowerTopology α) : toLower (ofLower a) = a :=
+  rfl
+#align with_lower_topology.to_lower_of_lower WithLowerTopology.toLower_ofLower
+
+@[simp]
+theorem ofLower_toLower (a : α) : ofLower (toLower a) = a :=
+  rfl
+#align with_lower_topology.of_lower_to_lower WithLowerTopology.ofLower_toLower
+
+-- porting note: removed @[simp] to make linter happy
+theorem toLower_inj {a b : α} : toLower a = toLower b ↔ a = b :=
+  Iff.rfl
+#align with_lower_topology.to_lower_inj WithLowerTopology.toLower_inj
+
+-- porting note: removed @[simp] to make linter happy
+theorem ofLower_inj {a b : WithLowerTopology α} : ofLower a = ofLower b ↔ a = b :=
+  Iff.rfl
+#align with_lower_topology.of_lower_inj WithLowerTopology.ofLower_inj
+
+/-- A recursor for `WithLowerTopology`. Use as `induction x using WithLowerTopology.rec`. -/
+protected def rec {β : WithLowerTopology α → Sort _} (h : ∀ a, β (toLower a)) : ∀ a, β a := fun a =>
+  h (ofLower a)
+#align with_lower_topology.rec WithLowerTopology.rec
+
+instance [Nonempty α] : Nonempty (WithLowerTopology α) :=
+  ‹Nonempty α›
+
+instance [Inhabited α] : Inhabited (WithLowerTopology α) :=
+  ‹Inhabited α›
+
+variable [Preorder α]
+
+instance : Preorder (WithLowerTopology α) :=
+  ‹Preorder α›
+
+instance : TopologicalSpace (WithLowerTopology α) :=
+  generateFrom { s | ∃ a, Ici aᶜ = s }
+
+theorem isOpen_preimage_ofLower (S : Set α) :
+    IsOpen (WithLowerTopology.ofLower ⁻¹' S) ↔
+      (generateFrom { s : Set α | ∃ a : α, Ici aᶜ = s }).IsOpen S :=
+  Iff.rfl
+#align with_lower_topology.is_open_preimage_of_lower WithLowerTopology.isOpen_preimage_ofLower
+
+theorem isOpen_def (T : Set (WithLowerTopology α)) :
+    IsOpen T ↔
+      (generateFrom { s : Set α | ∃ a : α, Ici aᶜ = s }).IsOpen (WithLowerTopology.toLower ⁻¹' T) :=
+  Iff.rfl
+#align with_lower_topology.is_open_def WithLowerTopology.isOpen_def
+
+end WithLowerTopology
+
+/--
+The lower topology is the topology generated by the complements of the closed intervals to infinity.
+-/
+class LowerTopology (α : Type _) [t : TopologicalSpace α] [Preorder α] : Prop where
+  topology_eq_lowerTopology : t = generateFrom { s | ∃ a, Ici aᶜ = s }
+#align lower_topology LowerTopology
+
+instance [Preorder α] : LowerTopology (WithLowerTopology α) :=
+  ⟨rfl⟩
+
+namespace LowerTopology
+
+/-- The complements of the upper closures of finite sets are a collection of lower sets
+which form a basis for the lower topology. -/
+def lowerBasis (α : Type _) [Preorder α] :=
+  { s : Set α | ∃ t : Set α, t.Finite ∧ (upperClosure t : Set α)ᶜ = s }
+#align lower_topology.lower_basis LowerTopology.lowerBasis
+
+section Preorder
+
+variable (α)
+variable [Preorder α] [TopologicalSpace α] [LowerTopology α] {s : Set α}
+
+lemma topology_eq : ‹_› = generateFrom { s | ∃ a : α, (Ici a)ᶜ = s } := topology_eq_lowerTopology
+
+variable {α}
+
+/-- If `α` is equipped with the lower topology, then it is homeomorphic to `WithLowerTopology α`.
+-/
+def withLowerTopologyHomeomorph : WithLowerTopology α ≃ₜ α :=
+  WithLowerTopology.ofLower.toHomeomorphOfInducing ⟨by erw [topology_eq α, induced_id]; rfl⟩
+#align lower_topology.with_lower_topology_homeomorph LowerTopology.withLowerTopologyHomeomorph
+
+theorem isOpen_iff_generate_Ici_compl : IsOpen s ↔ GenerateOpen { t | ∃ a, Ici aᶜ = t } s := by
+  rw [topology_eq α]; rfl
+#align lower_topology.is_open_iff_generate_Ici_compl LowerTopology.isOpen_iff_generate_Ici_compl
+
+/-- Left-closed right-infinite intervals [a, ∞) are closed in the lower topology. -/
+theorem isClosed_Ici (a : α) : IsClosed (Ici a) :=
+  isOpen_compl_iff.1 <| isOpen_iff_generate_Ici_compl.2 <| GenerateOpen.basic _ ⟨a, rfl⟩
+#align lower_topology.is_closed_Ici LowerTopology.isClosed_Ici
+
+/-- The upper closure of a finite set is closed in the lower topology. -/
+theorem isClosed_upperClosure (h : s.Finite) : IsClosed (upperClosure s : Set α) := by
+  simp only [← UpperSet.infᵢ_Ici, UpperSet.coe_infᵢ]
+  exact isClosed_bunionᵢ h fun a _ => isClosed_Ici a
+#align lower_topology.is_closed_upper_closure LowerTopology.isClosed_upperClosure
+
+/-- Every set open in the lower topology is a lower set. -/
+theorem isLowerSet_of_isOpen (h : IsOpen s) : IsLowerSet s := by
+  -- porting note: `rw` leaves a shadowed assumption
+  replace h := isOpen_iff_generate_Ici_compl.1 h
+  induction h
+  case basic u h' => obtain ⟨a, rfl⟩ := h'; exact (isUpperSet_Ici a).compl
+  case univ => exact isLowerSet_univ
+  case inter u v _ _ hu2 hv2 => exact hu2.inter hv2
+  case unionₛ _ _ ih => exact isLowerSet_unionₛ ih
+#align lower_topology.is_lower_set_of_is_open LowerTopology.isLowerSet_of_isOpen
+
+theorem isUpperSet_of_isClosed (h : IsClosed s) : IsUpperSet s :=
+  isLowerSet_compl.1 <| isLowerSet_of_isOpen h.isOpen_compl
+#align lower_topology.is_upper_set_of_is_closed LowerTopology.isUpperSet_of_isClosed
+
+/--
+The closure of a singleton `{a}` in the lower topology is the left-closed right-infinite interval
+[a, ∞).
+-/
+@[simp]
+theorem closure_singleton (a : α) : closure {a} = Ici a :=
+  Subset.antisymm ((closure_minimal fun _ h => h.ge) <| isClosed_Ici a) <|
+    (isUpperSet_of_isClosed isClosed_closure).Ici_subset <| subset_closure rfl
+#align lower_topology.closure_singleton LowerTopology.closure_singleton
+
+protected theorem isTopologicalBasis : IsTopologicalBasis (lowerBasis α) := by
+  convert isTopologicalBasis_of_subbasis (topology_eq α)
+  simp_rw [lowerBasis, coe_upperClosure, compl_unionᵢ]
+  ext s
+  constructor
+  · rintro ⟨F, hF, rfl⟩
+    refine' ⟨(fun a => Ici aᶜ) '' F, ⟨hF.image _, image_subset_iff.2 fun _ _ => ⟨_, rfl⟩⟩, _⟩
+    simp only [interₛ_image]
+  · rintro ⟨F, ⟨hF, hs⟩, rfl⟩
+    haveI := hF.to_subtype
+    rw [subset_def, Subtype.forall'] at hs
+    choose f hf using hs
+    exact ⟨_, finite_range f, by simp_rw [binterᵢ_range, hf, interₛ_eq_interᵢ]⟩
+#align lower_topology.is_topological_basis LowerTopology.isTopologicalBasis
+
+/-- 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.
+
+TODO: upgrade to an `iff`. -/
+lemma continuous_of_Ici [TopologicalSpace β] {f : β → α} (h : ∀ a, IsClosed (f ⁻¹' (Ici a))) :
+    Continuous f := by
+  obtain rfl := LowerTopology.topology_eq α
+  refine continuous_generateFrom ?_
+  rintro _ ⟨a, rfl⟩
+  exact (h a).isOpen_compl
+
+end Preorder
+
+section PartialOrder
+
+variable [PartialOrder α] [TopologicalSpace α] [LowerTopology α]
+
+-- see Note [lower instance priority]
+/-- The lower topology on a partial order is T₀. -/
+instance (priority := 90) t0Space : T0Space α :=
+  (t0Space_iff_inseparable α).2 fun x y h =>
+    Ici_injective <| by simpa only [inseparable_iff_closure_eq, closure_singleton] using h
+
+end PartialOrder
+
+end LowerTopology
+
+instance [Preorder α] [TopologicalSpace α] [LowerTopology α] [OrderBot α] [Preorder β]
+    [TopologicalSpace β] [LowerTopology β] [OrderBot β] : LowerTopology (α × β) where
+  topology_eq_lowerTopology := by
+    refine' le_antisymm (le_generateFrom _) _
+    · rintro _ ⟨x, rfl⟩
+      exact ((LowerTopology.isClosed_Ici _).prod <| LowerTopology.isClosed_Ici _).isOpen_compl
+    rw [(LowerTopology.isTopologicalBasis.prod LowerTopology.isTopologicalBasis).eq_generateFrom,
+      le_generateFrom_iff_subset_isOpen, image2_subset_iff]
+    rintro _ ⟨s, hs, rfl⟩ _ ⟨t, ht, rfl⟩
+    dsimp
+    simp_rw [coe_upperClosure, compl_unionᵢ, prod_eq, preimage_interᵢ, preimage_compl]
+    -- without `let`, `refine` tries to use the product topology and fails
+    let _ : TopologicalSpace (α × β) := generateFrom { s | ∃ a, Ici aᶜ = s }
+    refine (isOpen_binterᵢ hs fun a _ => ?_).inter (isOpen_binterᵢ ht fun b _ => ?_)
+    · exact GenerateOpen.basic _ ⟨(a, ⊥), by simp [Ici_prod_eq, prod_univ]⟩
+    · exact GenerateOpen.basic _ ⟨(⊥, b), by simp [Ici_prod_eq, univ_prod]⟩
+
+section CompleteLattice
+
+variable [CompleteLattice α] [CompleteLattice β] [TopologicalSpace α] [LowerTopology α]
+  [TopologicalSpace β] [LowerTopology β]
+
+protected theorem InfₛHom.continuous (f : InfₛHom α β) : Continuous f := by
+  refine LowerTopology.continuous_of_Ici fun b => ?_
+  convert LowerTopology.isClosed_Ici (infₛ <| f ⁻¹' Ici b)
+  refine' Subset.antisymm (fun a => infₛ_le) fun a ha => le_trans _ <|
+    OrderHomClass.mono (f : α →o β) ha
+  refine' LE.le.trans _ (map_infₛ f _).ge
+  simp
+#align Inf_hom.continuous InfₛHom.continuous
+
+-- see Note [lower instance priority]
+instance (priority := 90) LowerTopology.continuousInf : ContinuousInf α :=
+  ⟨(infInfₛHom : InfₛHom (α × α) α).continuous⟩
+#align lower_topology.to_has_continuous_inf LowerTopology.continuousInf
+
+end CompleteLattice
+