feat(topology/order/hom/esakia): Esakia morphisms (#12241)

Define pseudo-epimorphisms and Esakia morphisms following the hom refactor.

src/order/hom/lattice.lean

@@ -102,7 +102,7 @@ class inf_top_hom_class (F : Type*) (α β : out_param $ Type*) [has_inf α]
 
 /-- `lattice_hom_class F α β` states that `F` is a type of lattice morphisms.
 
-You should extend this class when you extend `sup_hom`. -/
+You should extend this class when you extend `lattice_hom`. -/
 class lattice_hom_class (F : Type*) (α β : out_param $ Type*) [lattice α] [lattice β]
   extends sup_hom_class F α β :=
 (map_inf (f : F) (a b : α) : f (a ⊓ b) = f a ⊓ f b)

src/topology/order/hom/esakia.lean

@@ -0,0 +1,236 @@
+/-
+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.hom.bounded
+import order.hom.order
+import topology.order.hom.basic
+
+/-!
+# Esakia morphisms
+
+This file defines pseudo-epimorphisms and Esakia morphisms.
+
+We use the `fun_like` design, so each type of morphisms has a companion typeclass which is meant to
+be satisfied by itself and all stricter types.
+
+## Types of morphisms
+
+* `pseudo_epimorphism`: Pseudo-epimorphisms. Maps `f` such that `f a ≤ b` implies the existence of
+  `a'` such that `a ≤ a'` and `f a' = b`.
+* `esakia_hom`: Esakia morphisms. Continuous pseudo-epimorphisms.
+
+## Typeclasses
+
+* `pseudo_epimorphism_class`
+* `esakia_hom_class`
+
+## References
+
+* [Wikipedia, *Esakia space*](https://en.wikipedia.org/wiki/Esakia_space)
+-/
+
+open function
+
+variables {F α β γ δ : Type*}
+
+/-- The type of pseudo-epimorphisms, aka p-morphisms, aka bounded maps, from `α` to `β`. -/
+structure pseudo_epimorphism (α β : Type*) [preorder α] [preorder β] extends α →o β :=
+(exists_map_eq_of_map_le' ⦃a : α⦄ ⦃b : β⦄ : to_fun a ≤ b → ∃ c, a ≤ c ∧ to_fun c = b)
+
+/-- The type of Esakia morphisms, aka continuous pseudo-epimorphisms, from `α` to `β`. -/
+structure esakia_hom (α β : Type*) [topological_space α] [preorder α] [topological_space β]
+  [preorder β] extends α →Co β :=
+(exists_map_eq_of_map_le' ⦃a : α⦄ ⦃b : β⦄ : to_fun a ≤ b → ∃ c, a ≤ c ∧ to_fun c = b)
+
+/-- `pseudo_epimorphism_class F α β` states that `F` is a type of `⊔`-preserving morphisms.
+
+You should extend this class when you extend `pseudo_epimorphism`. -/
+class pseudo_epimorphism_class (F : Type*) (α β : out_param $ Type*) [preorder α] [preorder β]
+  extends rel_hom_class F ((≤) : α → α → Prop) ((≤) : β → β → Prop) :=
+(exists_map_eq_of_map_le (f : F) ⦃a : α⦄ ⦃b : β⦄ : f a ≤ b → ∃ c, a ≤ c ∧ f c = b)
+
+/-- `esakia_hom_class F α β` states that `F` is a type of lattice morphisms.
+
+You should extend this class when you extend `esakia_hom`. -/
+class esakia_hom_class (F : Type*) (α β : out_param $ Type*) [topological_space α] [preorder α]
+  [topological_space β] [preorder β]
+  extends continuous_order_hom_class F α β :=
+(exists_map_eq_of_map_le (f : F) ⦃a : α⦄ ⦃b : β⦄ : f a ≤ b → ∃ c, a ≤ c ∧ f c = b)
+
+export pseudo_epimorphism_class (exists_map_eq_of_map_le)
+
+@[priority 100] -- See note [lower instance priority]
+instance pseudo_epimorphism_class.to_top_hom_class [partial_order α] [order_top α] [preorder β]
+  [order_top β] [pseudo_epimorphism_class F α β] : top_hom_class F α β :=
+⟨λ f, let ⟨b, h⟩ := exists_map_eq_of_map_le f (@le_top _ _ _ $ f ⊤) in
+  by rw [←top_le_iff.1 h.1, h.2]⟩
+
+@[priority 100] -- See note [lower instance priority]
+instance order_iso_class.to_pseudo_epimorphism_class [preorder α] [preorder β]
+  [order_iso_class F α β] : pseudo_epimorphism_class F α β :=
+⟨λ f a b h, ⟨equiv_like.inv f b, (le_map_inv_iff f).2 h, equiv_like.right_inv _ _⟩⟩
+
+@[priority 100] -- See note [lower instance priority]
+instance esakia_hom_class.to_pseudo_epimorphism_class [topological_space α] [preorder α]
+  [topological_space β] [preorder β] [esakia_hom_class F α β] : pseudo_epimorphism_class F α β :=
+{ .. ‹esakia_hom_class F α β› }
+
+instance [preorder α] [preorder β] [pseudo_epimorphism_class F α β] :
+  has_coe_t F (pseudo_epimorphism α β) :=
+⟨λ f, ⟨f, exists_map_eq_of_map_le f⟩⟩
+
+instance [topological_space α] [preorder α] [topological_space β] [preorder β]
+  [esakia_hom_class F α β] : has_coe_t F (esakia_hom α β) :=
+⟨λ f, ⟨f, exists_map_eq_of_map_le f⟩⟩
+
+/-! ### Pseudo-epimorphisms -/
+
+namespace pseudo_epimorphism
+variables [preorder α] [preorder β] [preorder γ] [preorder δ]
+
+instance : pseudo_epimorphism_class (pseudo_epimorphism α β) α β :=
+{ coe := λ f, f.to_fun,
+  coe_injective' := λ f g h, by { obtain ⟨⟨_, _⟩, _⟩ := f, obtain ⟨⟨_, _⟩, _⟩ := g, congr' },
+  map_rel := λ f, f.monotone',
+  exists_map_eq_of_map_le := pseudo_epimorphism.exists_map_eq_of_map_le' }
+
+/-- Helper instance for when there's too many metavariables to apply `fun_like.has_coe_to_fun`
+directly. -/
+instance : has_coe_to_fun (pseudo_epimorphism α β) (λ _, α → β) := fun_like.has_coe_to_fun
+
+@[simp] lemma to_fun_eq_coe {f : pseudo_epimorphism α β} : f.to_fun = (f : α → β) := rfl
+
+@[ext] lemma ext {f g : pseudo_epimorphism α β} (h : ∀ a, f a = g a) : f = g := fun_like.ext f g h
+
+/-- Copy of a `pseudo_epimorphism` with a new `to_fun` equal to the old one. Useful to fix
+definitional equalities. -/
+protected def copy (f : pseudo_epimorphism α β) (f' : α → β) (h : f' = f) :
+  pseudo_epimorphism α β :=
+⟨f.to_order_hom.copy f' h, by simpa only [h.symm, to_fun_eq_coe] using f.exists_map_eq_of_map_le'⟩
+
+variables (α)
+
+/-- `id` as a `pseudo_epimorphism`. -/
+protected def id : pseudo_epimorphism α α := ⟨order_hom.id, λ a b h, ⟨b, h, rfl⟩⟩
+
+instance : inhabited (pseudo_epimorphism α α) := ⟨pseudo_epimorphism.id α⟩
+
+@[simp] lemma coe_id : ⇑(pseudo_epimorphism.id α) = id := rfl
+@[simp] lemma coe_id_order_hom : (pseudo_epimorphism.id α : α →o α) = order_hom.id := rfl
+
+variables {α}
+
+@[simp] lemma id_apply (a : α) : pseudo_epimorphism.id α a = a := rfl
+
+/-- Composition of `pseudo_epimorphism`s as a `pseudo_epimorphism`. -/
+def comp (g : pseudo_epimorphism β γ) (f : pseudo_epimorphism α β) : pseudo_epimorphism α γ :=
+⟨g.to_order_hom.comp f.to_order_hom, λ a b h₀, begin
+  obtain ⟨b, h₁, rfl⟩ := g.exists_map_eq_of_map_le' h₀,
+  obtain ⟨b, h₂, rfl⟩ := f.exists_map_eq_of_map_le' h₁,
+  exact ⟨b, h₂, rfl⟩,
+end⟩
+
+@[simp] lemma coe_comp (g : pseudo_epimorphism β γ) (f : pseudo_epimorphism α β) :
+  (g.comp f : α → γ) = g ∘ f := rfl
+@[simp] lemma coe_comp_order_hom (g : pseudo_epimorphism β γ) (f : pseudo_epimorphism α β) :
+  (g.comp f : α →o γ) = (g : β →o γ).comp f := rfl
+@[simp] lemma comp_apply (g : pseudo_epimorphism β γ) (f : pseudo_epimorphism α β) (a : α) :
+  (g.comp f) a = g (f a) := rfl
+@[simp] lemma comp_assoc (h : pseudo_epimorphism γ δ) (g : pseudo_epimorphism β γ)
+  (f : pseudo_epimorphism α β) :
+  (h.comp g).comp f = h.comp (g.comp f) := rfl
+@[simp] lemma comp_id (f : pseudo_epimorphism α β) : f.comp (pseudo_epimorphism.id α) = f :=
+ext $ λ a, rfl
+@[simp] lemma id_comp (f : pseudo_epimorphism α β) : (pseudo_epimorphism.id β).comp f = f :=
+ext $ λ a, rfl
+
+lemma cancel_right {g₁ g₂ : pseudo_epimorphism β γ} {f : pseudo_epimorphism α β}
+  (hf : surjective f) :
+  g₁.comp f = g₂.comp f ↔ g₁ = g₂ :=
+⟨λ h, ext $ hf.forall.2 $ fun_like.ext_iff.1 h, congr_arg _⟩
+
+lemma cancel_left {g : pseudo_epimorphism β γ} {f₁ f₂ : pseudo_epimorphism α β} (hg : injective g) :
+  g.comp f₁ = g.comp f₂ ↔ f₁ = f₂ :=
+⟨λ h, ext $ λ a, hg $ by rw [←comp_apply, h, comp_apply], congr_arg _⟩
+
+end pseudo_epimorphism
+
+/-! ### Esakia morphisms -/
+
+namespace esakia_hom
+variables [topological_space α] [preorder α] [topological_space β] [preorder β]
+  [topological_space γ] [preorder γ] [topological_space δ] [preorder δ]
+
+/-- Reinterpret an `esakia_hom` as a `pseudo_epimorphism`. -/
+def to_pseudo_epimorphism (f : esakia_hom α β) : pseudo_epimorphism α β := { ..f }
+
+instance : esakia_hom_class (esakia_hom α β) α β :=
+{ coe := λ f, f.to_fun,
+  coe_injective' := λ f g h,
+    by { obtain ⟨⟨⟨_, _⟩, _⟩, _⟩ := f, obtain ⟨⟨⟨_, _⟩, _⟩, _⟩ := g, congr' },
+  map_rel := λ f, f.monotone',
+  map_continuous := λ f, f.continuous_to_fun,
+  exists_map_eq_of_map_le := λ f, f.exists_map_eq_of_map_le' }
+
+/-- Helper instance for when there's too many metavariables to apply `fun_like.has_coe_to_fun`
+directly. -/
+instance : has_coe_to_fun (esakia_hom α β) (λ _, α → β) := fun_like.has_coe_to_fun
+
+@[simp] lemma to_fun_eq_coe {f : esakia_hom α β} : f.to_fun = (f : α → β) := rfl
+
+@[ext] lemma ext {f g : esakia_hom α β} (h : ∀ a, f a = g a) : f = g := fun_like.ext f g h
+
+/-- Copy of an `esakia_hom` with a new `to_fun` equal to the old one. Useful to fix definitional
+equalities. -/
+protected def copy (f : esakia_hom α β) (f' : α → β) (h : f' = f) : esakia_hom α β :=
+⟨f.to_continuous_order_hom.copy f' h,
+  by simpa only [h.symm, to_fun_eq_coe] using f.exists_map_eq_of_map_le'⟩
+
+variables (α)
+
+/-- `id` as an `esakia_hom`. -/
+protected def id : esakia_hom α α := ⟨continuous_order_hom.id α, λ a b h, ⟨b, h, rfl⟩⟩
+
+instance : inhabited (esakia_hom α α) := ⟨esakia_hom.id α⟩
+
+@[simp] lemma coe_id : ⇑(esakia_hom.id α) = id := rfl
+@[simp] lemma coe_id_continuous_order_hom :
+  (esakia_hom.id α : α →Co α) = continuous_order_hom.id α := rfl
+@[simp] lemma coe_id_pseudo_epimorphism :
+  (esakia_hom.id α : pseudo_epimorphism α α) = pseudo_epimorphism.id α  := rfl
+
+variables {α}
+
+@[simp] lemma id_apply (a : α) : esakia_hom.id α a = a := rfl
+
+/-- Composition of `esakia_hom`s as an `esakia_hom`. -/
+def comp (g : esakia_hom β γ) (f : esakia_hom α β) : esakia_hom α γ :=
+⟨g.to_continuous_order_hom.comp f.to_continuous_order_hom, λ a b h₀, begin
+  obtain ⟨b, h₁, rfl⟩ := g.exists_map_eq_of_map_le' h₀,
+  obtain ⟨b, h₂, rfl⟩ := f.exists_map_eq_of_map_le' h₁,
+  exact ⟨b, h₂, rfl⟩,
+end⟩
+
+@[simp] lemma coe_comp (g : esakia_hom β γ) (f : esakia_hom α β) : (g.comp f : α → γ) = g ∘ f := rfl
+@[simp] lemma comp_apply (g : esakia_hom β γ) (f : esakia_hom α β) (a : α) :
+  (g.comp f) a = g (f a) := rfl
+@[simp] lemma coe_comp_continuous_order_hom (g : esakia_hom β γ) (f : esakia_hom α β) :
+  (g.comp f : α →Co γ) = (g : β →Co γ).comp f := rfl
+@[simp] lemma coe_comp_pseudo_epimorphism (g : esakia_hom β γ) (f : esakia_hom α β) :
+  (g.comp f : pseudo_epimorphism α γ) = (g : pseudo_epimorphism β γ).comp f := rfl
+@[simp] lemma comp_assoc (h : esakia_hom γ δ) (g : esakia_hom β γ) (f : esakia_hom α β) :
+  (h.comp g).comp f = h.comp (g.comp f) := rfl
+@[simp] lemma comp_id (f : esakia_hom α β) : f.comp (esakia_hom.id α) = f := ext $ λ a, rfl
+@[simp] lemma id_comp (f : esakia_hom α β) : (esakia_hom.id β).comp f = f := ext $ λ a, rfl
+
+lemma cancel_right {g₁ g₂ : esakia_hom β γ} {f : esakia_hom α β} (hf : surjective f) :
+  g₁.comp f = g₂.comp f ↔ g₁ = g₂ :=
+⟨λ h, ext $ hf.forall.2 $ fun_like.ext_iff.1 h, congr_arg _⟩
+
+lemma cancel_left {g : esakia_hom β γ} {f₁ f₂ : esakia_hom α β} (hg : injective g) :
+  g.comp f₁ = g.comp f₂ ↔ f₁ = f₂ :=
+⟨λ h, ext $ λ a, hg $ by rw [←comp_apply, h, comp_apply], congr_arg _⟩
+
+end esakia_hom