feat(order/galois_connection): galois_coinsertions (#3656)

Co-authored-by: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com>

src/order/basic.lean

@@ -203,16 +203,18 @@ begin
     apply h _ _ k }
 end
 
-variables [partial_order α] [partial_order β] {f : α → β}
-
-lemma strict_mono_of_monotone_of_injective (h₁ : monotone f) (h₂ : injective f) :
-  strict_mono f :=
+lemma strict_mono_of_monotone_of_injective [partial_order α] [partial_order β] {f : α → β}
+  (h₁ : monotone f) (h₂ : injective f) : strict_mono f :=
 λ a b h,
 begin
   rw lt_iff_le_and_ne at ⊢ h,
   exact ⟨h₁ h.1, λ e, h.2 (h₂ e)⟩
 end
 
+lemma strict_mono_of_le_iff_le [preorder α] [preorder β] {f : α → β}
+  (h : ∀ x y, x ≤ y ↔ f x ≤ f y) : strict_mono f :=
+λ a b, by simp [lt_iff_le_not_le, h] {contextual := tt}
+
 end
 
 /-- Type tag for a set with dual order: `≤` means `≥` and `<` means `>`. -/

src/order/galois_connection.lean

@@ -2,19 +2,55 @@
 Copyright (c) 2017 Johannes Hölzl. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Author: Johannes Hölzl
-
-Galois connections - order theoretic adjoints.
 -/
 import order.complete_lattice
 import order.order_iso
+/-!
+# Galois connections, insertions and coinsertions
+
+Galois connections are order theoretic adjoints, i.e. a pair of functions `u` and `l`,
+  such that `∀a b, l a ≤ b ↔ a ≤ u b`.
+
+## Main definitions
+
+* `galois_connection`: A Galois connection is a pair of functions `l` and `u` satisfying
+  `l a ≤ b ↔ a ≤ u b`. They are special cases of  adjoint functors in category theory,
+  but do not depend on the category theory library in mathlib.
+* `galois_insertion`: A Galois insertion is a Galois connection where `l ∘ u = id`
+* `galois_coinsertion`: A Galois coinsertion is a Galois connection where `u ∘ l = id`
+
+## Implementation details
+
+Galois insertions can be used to lift order structures from one type to another.
+For example if `α` is a complete lattice, and `l : α → β`, and `u : β → α` form
+a Galois insertion, then `β` is also a complete lattice. `l` is the lower adjoint and
+`u` is the upper adjoint.
+
+An example of this is the Galois insertion is in group thery. If `G` is a topological space,
+then there is a Galois insertion between the set of subsets of `G`, `set G`, and the
+set of subgroups of `G`, `subgroup G`. The left adjoint is `subgroup.closure`,
+taking the `subgroup` generated by a `set`, The right adjoint is the coercion from `subgroup G` to
+`set G`, taking the underlying set of an subgroup.
+
+Naively lifting a lattice structure along this Galois insertion would mean that the definition
+of `inf` on subgroups would be `subgroup.closure (↑S ∩ ↑T)`. This is an undesirable definition
+because the intersection of subgroups is already a subgroup, so there is no need to take the
+closure. For this reason a `choice` function is added as a field to the `galois_insertion`
+structure. It has type `Π S : set G, ↑(closure S) ≤ S → subgroup G`. When `↑(closure S) ≤ S`, then
+`S` is already a subgroup, so this function can be defined using `subgroup.mk` and not `closure`.
+This means the infimum of subgroups will be defined to be the intersection of sets, paired
+with a proof that intersection of subgroups is a subgroup, rather than the closure of the
+intersection.
+
+-/
 open function set
 
 universes u v w x
 variables {α : Type u} {β : Type v} {γ : Type w} {ι : Sort x} {a a₁ a₂ : α} {b b₁ b₂ : β}
 
 /-- A Galois connection is a pair of functions `l` and `u` satisfying
-  `l a ≤ b ↔ a ≤ u b`. They are closely connected to adjoint functors
-  in category theory. -/
+  `l a ≤ b ↔ a ≤ u b`. They are special cases of  adjoint functors in category theory,
+    but do not depend on the category theory library in mathlib. -/
 def galois_connection [preorder α] [preorder β] (l : α → β) (u : β → α) := ∀a b, l a ≤ b ↔ a ≤ u b
 
 /-- Makes a Galois connection from an order-preserving bijection. -/
@@ -186,7 +222,9 @@ assume x y, (le_div_iff_mul_le x y h).symm
 end nat
 
 /-- A Galois insertion is a Galois connection where `l ∘ u = id`. It also contains a constructive
-choice function, to give better definitional equalities when lifting order structures. -/
+choice function, to give better definitional equalities when lifting order structures. Dual
+to `galois_coinsertion` -/
+@[nolint has_inhabited_instance]
 structure galois_insertion {α β : Type*} [preorder α] [preorder β] (l : α → β) (u : β → α) :=
 (choice : Πx:α, u (l x) ≤ x → β)
 (gc : galois_connection l u)
@@ -210,6 +248,15 @@ protected def order_iso.to_galois_insertion [preorder α] [preorder β] (oi : @o
   le_l_u := λ g, le_of_eq (oi.right_inv g).symm,
   choice_eq := λ b h, rfl }
 
+/-- Make a `galois_insertion l u` from a `galois_connection l u` such that `∀ b, b ≤ l (u b)` -/
+def galois_connection.to_galois_insertion {α β : Type*} [preorder α] [preorder β]
+  {l : α → β} {u : β → α} (gc : galois_connection l u) (h : ∀ b, b ≤ l (u b)) :
+  galois_insertion l u :=
+{ choice := λ x _, l x,
+  gc := gc,
+  le_l_u := h,
+  choice_eq := λ _ _, rfl }
+
 /-- Lift the bottom along a Galois connection -/
 def galois_connection.lift_order_bot {α β : Type*} [order_bot α] [partial_order β]
   {l : α → β} {u : β → α} (gc : galois_connection l u) :
@@ -248,7 +295,7 @@ lemma l_supr_u [complete_lattice α] [complete_lattice β] (gi : galois_insertio
 calc l (⨆ (i : ι), u (f i)) = ⨆ (i : ι), l (u (f i)) : gi.gc.l_supr
                         ... = ⨆ (i : ι), f i : congr_arg _ $ funext $ λ i, gi.l_u_eq (f i)
 
-lemma l_supr_of_ul [complete_lattice α] [complete_lattice β] (gi : galois_insertion l u)
+lemma l_supr_of_ul_eq_self [complete_lattice α] [complete_lattice β] (gi : galois_insertion l u)
   {ι : Sort x} (f : ι → α) (hf : ∀ i, u (l (f i)) = f i) :
   l (⨆ i, (f i)) = ⨆ i, l (f i) :=
 calc l (⨆ (i : ι), (f i)) = l ⨆ (i : ι), (u (l (f i))) : by simp [hf]
@@ -265,12 +312,20 @@ lemma l_infi_u [complete_lattice α] [complete_lattice β] (gi : galois_insertio
 calc l (⨅ (i : ι), u (f i)) = l (u (⨅ (i : ι), (f i))) : congr_arg l gi.gc.u_infi.symm
                         ... = ⨅ (i : ι), f i : gi.l_u_eq _
 
-lemma l_infi_of_ul [complete_lattice α] [complete_lattice β] (gi : galois_insertion l u)
+lemma l_infi_of_ul_eq_self [complete_lattice α] [complete_lattice β] (gi : galois_insertion l u)
   {ι : Sort x} (f : ι → α) (hf : ∀ i, u (l (f i)) = f i) :
   l (⨅ i, (f i)) = ⨅ i, l (f i) :=
 calc l (⨅ i, (f i)) =  l ⨅ (i : ι), (u (l (f i))) : by simp [hf]
                 ... = ⨅ i, l (f i) : gi.l_infi_u _
 
+lemma u_le_u_iff [preorder α] [preorder β] (gi : galois_insertion l u) {a b} :
+  u a ≤ u b ↔ a ≤ b :=
+⟨λ h, le_trans (gi.le_l_u _) (gi.gc.l_le h),
+    λ h, gi.gc.monotone_u h⟩
+
+lemma strict_mono_u [preorder α] [partial_order β] (gi : galois_insertion l u) : strict_mono u :=
+strict_mono_of_le_iff_le $ λ _ _, gi.u_le_u_iff.symm
+
 section lift
 
 variables [partial_order β]
@@ -324,3 +379,171 @@ def lift_complete_lattice [complete_lattice α] (gi : galois_insertion l u) : co
 end lift
 
 end galois_insertion
+
+/-- A Galois coinsertion is a Galois connection where `u ∘ l = id`. It also contains a constructive
+choice function, to give better definitional equalities when lifting order structures. Dual to
+`galois_insertion` -/
+@[nolint has_inhabited_instance]
+structure galois_coinsertion {α β : Type*} [preorder α] [preorder β] (l : α → β) (u : β → α) :=
+(choice : Πx:β, x ≤ l (u x) → α)
+(gc : galois_connection l u)
+(u_l_le : ∀x, u (l x) ≤ x)
+(choice_eq : ∀a h, choice a h = u a)
+
+/-- Make a `galois_insertion u l` in the `order_dual`, from a `galois_coinsertion l u` -/
+def galois_coinsertion.dual {α β : Type*} [preorder α] [preorder β] {l : α → β} {u : β → α} :
+  galois_coinsertion l u → @galois_insertion (order_dual β) (order_dual α) _ _ u l :=
+λ x, ⟨x.1, x.2.dual, x.3, x.4⟩
+
+/-- Make a `galois_coinsertion u l` in the `order_dual`, from a `galois_insertion l u` -/
+def galois_insertion.dual {α β : Type*} [preorder α] [preorder β] {l : α → β} {u : β → α} :
+  galois_insertion l u → @galois_coinsertion (order_dual β) (order_dual α) _ _ u l :=
+λ x, ⟨x.1, x.2.dual, x.3, x.4⟩
+
+/-- Make a `galois_coinsertion l u` from a `galois_insertion l u` in the `order_dual` -/
+def galois_coinsertion.of_dual {α β : Type*} [preorder α] [preorder β] {l : α → β} {u : β → α} :
+  @galois_insertion (order_dual β) (order_dual α) _ _ u l → galois_coinsertion l u :=
+λ x, ⟨x.1, x.2.dual, x.3, x.4⟩
+
+/-- Make a `galois_insertion l u` from a `galois_coinsertion l u` in the `order_dual` -/
+def galois_insertion.of_dual {α β : Type*} [preorder α] [preorder β] {l : α → β} {u : β → α} :
+  @galois_coinsertion (order_dual β) (order_dual α) _ _ u l → galois_insertion l u :=
+λ x, ⟨x.1, x.2.dual, x.3, x.4⟩
+
+/-- Makes a Galois coinsertion from an order-preserving bijection. -/
+protected def order_iso.to_galois_coinsertion [preorder α] [preorder β] (oi : @order_iso α β (≤) (≤)) :
+@galois_coinsertion α β _ _ (oi) (oi.symm) :=
+{ choice := λ b h, oi.symm b,
+  gc := oi.to_galois_connection,
+  u_l_le := λ g, le_of_eq (oi.left_inv g),
+  choice_eq := λ b h, rfl }
+
+/-- A constructor for a Galois coinsertion with the trivial `choice` function. -/
+def galois_coinsertion.monotone_intro {α β : Type*} [preorder α] [preorder β] {l : α → β} {u : β → α}
+  (hu : monotone u) (hl : monotone l) (hlu : ∀ b, l (u b) ≤ b) (hul : ∀ a, u (l a) = a) :
+  galois_coinsertion l u :=
+galois_coinsertion.of_dual (galois_insertion.monotone_intro hl.order_dual hu.order_dual hlu hul)
+
+/-- Make a `galois_coinsertion l u` from a `galois_connection l u` such that `∀ b, b ≤ l (u b)` -/
+def galois_connection.to_galois_coinsertion {α β : Type*} [preorder α] [preorder β]
+  {l : α → β} {u : β → α} (gc : galois_connection l u) (h : ∀ a, u (l a) ≤ a) :
+  galois_coinsertion l u :=
+{ choice := λ x _, u x,
+  gc := gc,
+  u_l_le := h,
+  choice_eq := λ _ _, rfl }
+
+/-- Lift the top along a Galois connection -/
+def galois_connection.lift_order_top {α β : Type*} [partial_order α] [order_top β]
+  {l : α → β} {u : β → α} (gc : galois_connection l u) :
+  order_top α :=
+{ top    := u ⊤,
+  le_top := assume b, gc.le_u $ le_top,
+  .. ‹partial_order α› }
+
+namespace galois_coinsertion
+
+variables {l : α → β} {u : β → α}
+
+lemma u_l_eq [partial_order α] [preorder β] (gi : galois_coinsertion l u) (a : α) :
+  u (l a) = a :=
+gi.dual.l_u_eq a
+
+lemma u_surjective [partial_order α] [preorder β] (gi : galois_coinsertion l u) :
+  surjective u :=
+gi.dual.l_surjective
+
+lemma l_injective [partial_order α] [preorder β] (gi : galois_coinsertion l u) :
+  injective l :=
+gi.dual.u_injective
+
+lemma u_inf_l [semilattice_inf α] [semilattice_inf β] (gi : galois_coinsertion l u) (a b : α) :
+  u (l a ⊓ l b) = a ⊓ b :=
+gi.dual.l_sup_u a b
+
+lemma u_infi_l [complete_lattice α] [complete_lattice β] (gi : galois_coinsertion l u)
+  {ι : Sort x} (f : ι → α) :
+  u (⨅ i, l (f i)) = ⨅ i, (f i) :=
+gi.dual.l_supr_u _
+
+lemma u_infi_of_lu_eq_self [complete_lattice α] [complete_lattice β] (gi : galois_coinsertion l u)
+  {ι : Sort x} (f : ι → β) (hf : ∀ i, l (u (f i)) = f i) :
+  u (⨅ i, (f i)) = ⨅ i, u (f i) :=
+gi.dual.l_supr_of_ul_eq_self _ hf
+
+lemma u_sup_l [semilattice_sup α] [semilattice_sup β] (gi : galois_coinsertion l u) (a b : α) :
+  u (l a ⊔ l b) = a ⊔ b :=
+gi.dual.l_inf_u _ _
+
+lemma u_supr_l [complete_lattice α] [complete_lattice β] (gi : galois_coinsertion l u)
+  {ι : Sort x} (f : ι → α) :
+  u (⨆ i, l (f i)) = ⨆ i, (f i) :=
+gi.dual.l_infi_u _
+
+lemma u_supr_of_lu_eq_self [complete_lattice α] [complete_lattice β] (gi : galois_coinsertion l u)
+  {ι : Sort x} (f : ι → β) (hf : ∀ i, l (u (f i)) = f i) :
+  u (⨆ i, (f i)) = ⨆ i, u (f i) :=
+gi.dual.l_infi_of_ul_eq_self _ hf
+
+lemma l_le_l_iff [preorder α] [preorder β] (gi : galois_coinsertion l u) {a b} :
+  l a ≤ l b ↔ a ≤ b :=
+gi.dual.u_le_u_iff
+
+lemma strict_mono_l [partial_order α] [preorder β] (gi : galois_coinsertion l u) : strict_mono l :=
+λ a b h, gi.dual.strict_mono_u h
+
+section lift
+
+variables [partial_order α]
+
+/-- Lift the infima along a Galois coinsertion -/
+def lift_semilattice_inf [semilattice_inf β] (gi : galois_coinsertion l u) : semilattice_inf α :=
+{ inf := λa b, u (l a ⊓ l b),
+  inf_le_left  := assume a b, le_trans (gi.gc.monotone_u $ inf_le_left) (gi.u_l_le a),
+  inf_le_right := assume a b, le_trans (gi.gc.monotone_u $ inf_le_right) (gi.u_l_le b),
+  le_inf       := assume a b c hac hbc, gi.gc.le_u $ le_inf (gi.gc.monotone_l hac) (gi.gc.monotone_l hbc),
+  .. ‹partial_order α› }
+
+/-- Lift the suprema along a Galois coinsertion -/
+def lift_semilattice_sup [semilattice_sup β] (gi : galois_coinsertion l u) : semilattice_sup α :=
+{ sup := λa b, gi.choice (l a ⊔ l b) $
+    (sup_le (gi.gc.monotone_l $ gi.gc.le_u $ le_sup_left) (gi.gc.monotone_l $ gi.gc.le_u $ le_sup_right)),
+  le_sup_left  := by simp only [gi.choice_eq]; exact assume a b, gi.gc.le_u le_sup_left,
+  le_sup_right := by simp only [gi.choice_eq]; exact assume a b, gi.gc.le_u le_sup_right,
+  sup_le       := by simp only [gi.choice_eq]; exact assume a b c hac hbc,
+    le_trans (gi.gc.monotone_u $ sup_le (gi.gc.monotone_l hac) (gi.gc.monotone_l hbc)) (gi.u_l_le c),
+  .. ‹partial_order α› }
+
+/-- Lift the suprema and infima along a Galois coinsertion -/
+def lift_lattice [lattice β] (gi : galois_coinsertion l u) : lattice α :=
+{ .. gi.lift_semilattice_sup, .. gi.lift_semilattice_inf }
+
+/-- Lift the bot along a Galois coinsertion -/
+def lift_order_bot [order_bot β] (gi : galois_coinsertion l u) : order_bot α :=
+{ bot    := gi.choice ⊥ $ bot_le,
+  bot_le := by simp only [gi.choice_eq]; exact assume b, le_trans (gi.gc.monotone_u bot_le) (gi.u_l_le b),
+  .. ‹partial_order α› }
+
+/-- Lift the top, bottom, suprema, and infima along a Galois coinsertion -/
+def lift_bounded_lattice [bounded_lattice β] (gi : galois_coinsertion l u) : bounded_lattice α :=
+{ .. gi.lift_lattice, .. gi.lift_order_bot, .. gi.gc.lift_order_top }
+
+/-- Lift all suprema and infima along a Galois coinsertion -/
+def lift_complete_lattice [complete_lattice β] (gi : galois_coinsertion l u) : complete_lattice α :=
+{ Inf := λs, u (⨅ a∈s, l a),
+  le_Inf := assume s a hs, gi.gc.le_u $ le_infi $ assume b, le_infi $ assume hb, gi.gc.monotone_l $ hs _ hb,
+  Inf_le := assume s a ha, le_trans (gi.gc.monotone_u $ infi_le_of_le a $
+    infi_le_of_le ha $ le_refl _) (gi.u_l_le a),
+  Sup := λs, gi.choice (⨆ a∈s, l a) $ supr_le $ assume b, supr_le $ assume hb,
+    gi.gc.monotone_l $ gi.gc.le_u $ le_supr_of_le b $ le_supr_of_le hb $ le_refl _,
+  le_Sup := by simp only [gi.choice_eq]; exact
+    assume s a ha, gi.gc.le_u $ le_supr_of_le a $ le_supr_of_le ha $ le_refl _,
+  Sup_le := by simp only [gi.choice_eq]; exact
+    assume s a hs, le_trans (gi.gc.monotone_u $ supr_le $ assume b,
+        show (⨆ (hb : b ∈ s), l b) ≤ l a, from supr_le $ assume hb, gi.gc.monotone_l $ hs b hb)
+      (gi.u_l_le a),
+  .. gi.lift_bounded_lattice }
+
+end lift
+
+end galois_coinsertion