feat(topology/category/Locale): The category of locales (#12580)

Define `Locale`, the category of locales, as the opposite of `Frame`.

src/order/category/Frame.lean

@@ -5,6 +5,8 @@ Authors: Yaël Dillies
 -/
 import order.category.Lattice
 import order.hom.complete_lattice
+import topology.category.CompHaus
+import topology.opens
 
 /-!
 # The category of frames
@@ -18,7 +20,7 @@ This file defines `Frame`, the category of frames.
 
 universes u
 
-open category_theory order
+open category_theory opposite order topological_space
 
 /-- The category of frames. -/
 def Frame := bundled frame
@@ -58,3 +60,13 @@ instance has_forget_to_Lattice : has_forget₂ Frame Lattice :=
   inv_hom_id' := by { ext, exact e.apply_symm_apply _ } }
 
 end Frame
+
+/-- The forgetful functor from `Topᵒᵖ` to `Frame`. -/
+@[simps] def Top_op_to_Frame : Topᵒᵖ ⥤ Frame :=
+{ obj := λ X, Frame.of (opens (unop X : Top)),
+  map := λ X Y f, opens.comap $ quiver.hom.unop f,
+  map_id' := λ X, opens.comap_id }
+
+-- Note, `CompHaus` is too strong. We only need `t0_space`.
+instance CompHaus_op_to_Frame.faithful : faithful (CompHaus_to_Top.op ⋙ Top_op_to_Frame.{u}) :=
+⟨λ X Y f g h, quiver.hom.unop_inj $ opens.comap_injective h⟩

src/topology/category/Locale.lean

@@ -0,0 +1,41 @@
+/-
+Copyright (c) 2022 Yaël Dillies. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yaël Dillies
+-/
+import order.category.Frame
+
+/-!
+# The category of locales
+
+This file defines `Locale`, the category of locales. This is the opposite of the category of frames.
+-/
+
+universes u
+
+open category_theory opposite order topological_space
+
+/-- The category of locales. -/
+@[derive large_category] def Locale := Frameᵒᵖ
+
+namespace Locale
+
+instance : has_coe_to_sort Locale Type* := ⟨λ X, X.unop⟩
+instance (X : Locale) : frame X := X.unop.str
+
+/-- Construct a bundled `Locale` from a `frame`. -/
+def of (α : Type*) [frame α] : Locale := op $ Frame.of α
+
+@[simp] lemma coe_of (α : Type*) [frame α] : ↥(of α) = α := rfl
+
+instance : inhabited Locale := ⟨of punit⟩
+
+end Locale
+
+/-- The forgetful functor from `Top` to `Locale` which forgets that the space has "enough points".
+-/
+@[simps] def Top_to_Locale : Top ⥤ Locale := Top_op_to_Frame.right_op
+
+-- Note, `CompHaus` is too strong. We only need `t0_space`.
+instance CompHaus_to_Locale.faithful : faithful (CompHaus_to_Top ⋙ Top_to_Locale.{u}) :=
+⟨λ X Y f g h, by { dsimp at h, exact opens.comap_injective (quiver.hom.op_inj h) }⟩

src/topology/opens.lean

@@ -21,7 +21,7 @@ We define the subtype of open sets in a topological space.
 - `open_nhds_of x` is the type of open subsets of a topological space `α` containing `x : α`.
 -/
 
-open filter order set
+open filter function order set
 
 variables {α β γ : Type*} [topological_space α] [topological_space β] [topological_space γ]
 
@@ -192,12 +192,19 @@ order_hom_class.mono (comap f) h
 @[simp] lemma comap_val (f : C(α, β)) (U : opens β) : (comap f U).1 = f ⁻¹' U := rfl
 
 protected lemma comap_comp (g : C(β, γ)) (f : C(α, β)) :
-  comap (g.comp f) = (comap f).comp (comap g) :=
-rfl
+  comap (g.comp f) = (comap f).comp (comap g) := rfl
 
 protected lemma comap_comap (g : C(β, γ)) (f : C(α, β)) (U : opens γ) :
   comap f (comap g U) = comap (g.comp f) U := rfl
 
+lemma comap_injective [t0_space β] : injective (comap : C(α, β) → frame_hom (opens β) (opens α)) :=
+λ f g h, continuous_map.ext $ λ a, indistinguishable.eq $ λ s hs, begin
+  simp_rw ←mem_preimage,
+  congr' 2,
+  have := fun_like.congr_fun h ⟨_, hs⟩,
+  exact congr_arg (coe : opens α → set α) this,
+end
+
 /-- A homeomorphism induces an equivalence on open sets, by taking comaps. -/
 @[simp] protected def equiv (f : α ≃ₜ β) : opens α ≃ opens β :=
 { to_fun := opens.comap f.symm.to_continuous_map,