feat(Data/Set/Lattice, Order/Filter/Basic): more lemmas about `kernIm…

…age` and filter analog (#5744)

Co-authored-by: Junyan Xu <junyanxumath@gmail.com> @alreadydone

This was originally discussed on Zulip, and Junyan made most of the work in [this message](https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/congruence.20of.20filters.20for.20tendsto/near/294976522). I just changed some proofs to use a bit more Galois connections.

This is a bit of a gadget but it does simplify the proof of `comap_iSup`, and it will also be convenient to define the space of functions with support a compact subset of a fixed set. See [this message](https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/congruence.20of.20filters.20for.20tendsto/near/302238889) for more details.

Mathlib/Data/Set/Lattice.lean

@@ -26,7 +26,7 @@ for `Set α`, and some more set constructions.
 * `Set.completeAtomicBooleanAlgebra`: `Set α` is a `CompleteAtomicBooleanAlgebra` with `≤ = ⊆`,
   `< = ⊂`, `⊓ = ∩`, `⊔ = ∪`, `⨅ = ⋂`, `⨆ = ⋃` and `\` as the set difference.
   See `Set.BooleanAlgebra`.
-* `Set.kern_image`: For a function `f : α → β`, `s.kern_image f` is the set of `y` such that
+* `Set.kernImage`: For a function `f : α → β`, `s.kernImage f` is the set of `y` such that
   `f ⁻¹ y ⊆ s`.
 * `Set.seq`: Union of the image of a set under a **seq**uence of functions. `seq s t` is the union
   of `f '' t` over all `f ∈ s`, where `t : Set α` and `s : Set (α → β)`.
@@ -182,6 +182,14 @@ instance Set.completeAtomicBooleanAlgebra : CompleteAtomicBooleanAlgebra (Set α
     sInf_le := fun s t t_in a h => h _ t_in
     iInf_iSup_eq := by intros; ext; simp [Classical.skolem] }
 
+/-- `kernImage f s` is the set of `y` such that `f ⁻¹ y ⊆ s`. -/
+def kernImage (f : α → β) (s : Set α) : Set β :=
+  { y | ∀ ⦃x⦄, f x = y → x ∈ s }
+#align set.kern_image Set.kernImage
+
+lemma subset_kernImage_iff {f : α → β} : s ⊆ kernImage f t ↔ f ⁻¹' s ⊆ t :=
+  ⟨fun h _ hx ↦ h hx rfl,
+    fun h _ hx y hy ↦ h (show f y ∈ s from hy.symm ▸ hx)⟩
 section GaloisConnection
 
 variable {f : α → β}
@@ -190,20 +198,48 @@ protected theorem image_preimage : GaloisConnection (image f) (preimage f) := fu
   image_subset_iff
 #align set.image_preimage Set.image_preimage
 
-/-- `kernImage f s` is the set of `y` such that `f ⁻¹ y ⊆ s`. -/
-def kernImage (f : α → β) (s : Set α) : Set β :=
-  { y | ∀ ⦃x⦄, f x = y → x ∈ s }
-#align set.kern_image Set.kernImage
-
-protected theorem preimage_kernImage : GaloisConnection (preimage f) (kernImage f) := fun a _ =>
-  ⟨fun h _ hx y hy =>
-    have : f y ∈ a := hy.symm ▸ hx
-    h this,
-    fun h x (hx : f x ∈ a) => h hx rfl⟩
+protected theorem preimage_kernImage : GaloisConnection (preimage f) (kernImage f) := fun _ _ =>
+  subset_kernImage_iff.symm
 #align set.preimage_kern_image Set.preimage_kernImage
 
 end GaloisConnection
 
+section kernImage
+
+variable {f : α → β}
+
+lemma kernImage_mono : Monotone (kernImage f) :=
+  Set.preimage_kernImage.monotone_u
+
+lemma kernImage_eq_compl {s : Set α} : kernImage f s = (f '' sᶜ)ᶜ :=
+  Set.preimage_kernImage.u_unique (Set.image_preimage.compl)
+    (fun t ↦ compl_compl (f ⁻¹' t) ▸ Set.preimage_compl)
+
+lemma kernImage_compl {s : Set α} : kernImage f (sᶜ) = (f '' s)ᶜ := by
+  rw [kernImage_eq_compl, compl_compl]
+
+lemma kernImage_empty : kernImage f ∅ = (range f)ᶜ := by
+  rw [kernImage_eq_compl, compl_empty, image_univ]
+
+lemma kernImage_preimage_eq_iff {s : Set β} : kernImage f (f ⁻¹' s) = s ↔ (range f)ᶜ ⊆ s := by
+  rw [kernImage_eq_compl, ← preimage_compl, compl_eq_comm, eq_comm, image_preimage_eq_iff,
+      compl_subset_comm]
+
+lemma compl_range_subset_kernImage {s : Set α} : (range f)ᶜ ⊆ kernImage f s := by
+  rw [← kernImage_empty]
+  exact kernImage_mono (empty_subset _)
+
+lemma kernImage_union_preimage {s : Set α} {t : Set β} :
+    kernImage f (s ∪ f ⁻¹' t) = kernImage f s ∪ t := by
+  rw [kernImage_eq_compl, kernImage_eq_compl, compl_union, ← preimage_compl, image_inter_preimage,
+      compl_inter, compl_compl]
+
+lemma kernImage_preimage_union {s : Set α} {t : Set β} :
+    kernImage f (f ⁻¹' t ∪ s) = t ∪ kernImage f s := by
+  rw [union_comm, kernImage_union_preimage, union_comm]
+
+end kernImage
+
 /-! ### Union and intersection over an indexed family of sets -/
 
 

Mathlib/Order/Filter/Basic.lean

@@ -1903,7 +1903,7 @@ section Comap
 equivalent conditions hold.
 
 1. There exists a set `t ∈ f` such that `m ⁻¹' t ⊆ s`. This is used as a definition.
-2. The set `{y | ∀ x, m x = y → x ∈ s}` belongs to `f`, see `Filter.mem_comap'`.
+2. The set `kernImage m s = {y | ∀ x, m x = y → x ∈ s}` belongs to `f`, see `Filter.mem_comap'`.
 3. The set `(m '' sᶜ)ᶜ` belongs to `f`, see `Filter.mem_comap_iff_compl` and
 `Filter.compl_mem_comap`. -/
 def comap (m : α → β) (f : Filter β) : Filter α
@@ -1922,6 +1922,11 @@ theorem mem_comap' : s ∈ comap f l ↔ { y | ∀ ⦃x⦄, f x = y → x ∈ s
     fun h => ⟨_, h, fun x hx => hx rfl⟩⟩
 #align filter.mem_comap' Filter.mem_comap'
 
+-- TODO: it would be nice to use `kernImage` much more to take advantage of common name and API,
+-- and then this would become `mem_comap'`
+theorem mem_comap'' : s ∈ comap f l ↔ kernImage f s ∈ l :=
+  mem_comap'
+
 /-- RHS form is used, e.g., in the definition of `UniformSpace`. -/
 lemma mem_comap_prod_mk {x : α} {s : Set β} {F : Filter (α × β)} :
   s ∈ comap (Prod.mk x) F ↔ {p : α × β | p.fst = x → p.snd ∈ s} ∈ F :=
@@ -1939,14 +1944,53 @@ theorem frequently_comap : (∃ᶠ a in comap f l, p a) ↔ ∃ᶠ b in l, ∃ a
 #align filter.frequently_comap Filter.frequently_comap
 
 theorem mem_comap_iff_compl : s ∈ comap f l ↔ (f '' sᶜ)ᶜ ∈ l := by
-  simp only [mem_comap', compl_def, mem_image, mem_setOf_eq, not_exists, not_and', not_not]
+  simp only [mem_comap'', kernImage_eq_compl]
 #align filter.mem_comap_iff_compl Filter.mem_comap_iff_compl
 
 theorem compl_mem_comap : sᶜ ∈ comap f l ↔ (f '' s)ᶜ ∈ l := by rw [mem_comap_iff_compl, compl_compl]
 #align filter.compl_mem_comap Filter.compl_mem_comap
 
 end Comap
 
+section KernMap
+
+/-- The analog of `kernImage` for filters. A set `s` belongs to `Filter.kernMap m f` if either of
+the following equivalent conditions hold.
+
+1. There exists a set `t ∈ f` such that `s = kernImage m t`. This is used as a definition.
+2. There exists a set `t` such that `tᶜ ∈ f` and `sᶜ = m '' t`, see `Filter.mem_kernMap_iff_compl`
+and `Filter.compl_mem_kernMap`.
+
+This definition because it gives a right adjoint to `Filter.comap`, and because it has a nice
+interpretation when working with `co-` filters (`Filter.cocompact`, `Filter.cofinite`, ...).
+For example, `kernMap m (cocompact α)` is the filter generated by the complements of the sets
+`m '' K` where `K` is a compact subset of `α`. -/
+def kernMap (m : α → β) (f : Filter α) : Filter β where
+  sets := (kernImage m) '' f.sets
+  univ_sets := ⟨univ, f.univ_sets, by simp [kernImage_eq_compl]⟩
+  sets_of_superset := by
+    rintro _ t ⟨s, hs, rfl⟩ hst
+    refine ⟨s ∪ m ⁻¹' t, mem_of_superset hs (subset_union_left s _), ?_⟩
+    rw [kernImage_union_preimage, union_eq_right_iff_subset.mpr hst]
+  inter_sets := by
+    rintro _ _ ⟨s₁, h₁, rfl⟩ ⟨s₂, h₂, rfl⟩
+    exact ⟨s₁ ∩ s₂, f.inter_sets h₁ h₂, Set.preimage_kernImage.u_inf⟩
+
+variable {m : α → β} {f : Filter α}
+
+theorem mem_kernMap {s : Set β} : s ∈ kernMap m f ↔ ∃ t ∈ f, kernImage m t = s :=
+  Iff.rfl
+
+theorem mem_kernMap_iff_compl {s : Set β} : s ∈ kernMap m f ↔ ∃ t, tᶜ ∈ f ∧ m '' t = sᶜ := by
+  rw [mem_kernMap, compl_surjective.exists]
+  refine exists_congr (fun x ↦ and_congr_right fun _ ↦ ?_)
+  rw [kernImage_compl, compl_eq_comm, eq_comm]
+
+theorem compl_mem_kernMap {s : Set β} : sᶜ ∈ kernMap m f ↔ ∃ t, tᶜ ∈ f ∧ m '' t = s := by
+  simp_rw [mem_kernMap_iff_compl, compl_compl]
+
+end KernMap
+
 /-- The monadic bind operation on filter is defined the usual way in terms of `map` and `join`.
 
 Unfortunately, this `bind` does not result in the expected applicative. See `Filter.seq` for the
@@ -2169,6 +2213,16 @@ theorem gc_map_comap (m : α → β) : GaloisConnection (map m) (comap m) :=
   fun _ _ => map_le_iff_le_comap
 #align filter.gc_map_comap Filter.gc_map_comap
 
+theorem comap_le_iff_le_kernMap : comap m g ≤ f ↔ g ≤ kernMap m f := by
+  simp [Filter.le_def, mem_comap'', mem_kernMap, -mem_comap]
+
+theorem gc_comap_kernMap (m : α → β) : GaloisConnection (comap m) (kernMap m) :=
+  fun _ _ ↦ comap_le_iff_le_kernMap
+
+theorem kernMap_principal {s : Set α} : kernMap m (𝓟 s) = 𝓟 (kernImage m s) := by
+  refine eq_of_forall_le_iff (fun g ↦ ?_)
+  rw [← comap_le_iff_le_kernMap, le_principal_iff, le_principal_iff, mem_comap'']
+
 @[mono]
 theorem map_mono : Monotone (map m) :=
   (gc_map_comap m).monotone_l
@@ -2242,15 +2296,7 @@ theorem disjoint_comap (h : Disjoint g₁ g₂) : Disjoint (comap m g₁) (comap
 #align filter.disjoint_comap Filter.disjoint_comap
 
 theorem comap_iSup {ι} {f : ι → Filter β} {m : α → β} : comap m (iSup f) = ⨆ i, comap m (f i) :=
-  le_antisymm
-    (fun s hs =>
-      have : ∀ i, ∃ t, t ∈ f i ∧ m ⁻¹' t ⊆ s := by
-        simpa only [mem_comap, exists_prop, mem_iSup] using mem_iSup.1 hs
-      let ⟨t, ht⟩ := Classical.axiom_of_choice this
-      ⟨⋃ i, t i, mem_iSup.2 fun i => (f i).sets_of_superset (ht i).1 (subset_iUnion _ _), by
-        rw [preimage_iUnion, iUnion_subset_iff]
-        exact fun i => (ht i).2⟩)
-    (iSup_le fun i => comap_mono <| le_iSup _ _)
+  (gc_comap_kernMap m).l_iSup
 #align filter.comap_supr Filter.comap_iSup
 
 theorem comap_sSup {s : Set (Filter β)} {m : α → β} : comap m (sSup s) = ⨆ f ∈ s, comap m f := by

Mathlib/Order/GaloisConnection.lean

@@ -339,6 +339,13 @@ protected theorem dfun {ι : Type u} {α : ι → Type v} {β : ι → Type w} [
   forall_congr' fun i => gc i (a i) (b i)
 #align galois_connection.dfun GaloisConnection.dfun
 
+protected theorem compl [BooleanAlgebra α] [BooleanAlgebra β] {l : α → β} {u : β → α}
+    (gc : GaloisConnection l u) :
+    GaloisConnection (compl ∘ u ∘ compl) (compl ∘ l ∘ compl) := by
+  intro a b
+  dsimp
+  rw [le_compl_iff_le_compl, gc, compl_le_iff_compl_le]
+
 end Constructions
 
 theorem l_comm_of_u_comm {X : Type _} [Preorder X] {Y : Type _} [Preorder Y] {Z : Type _}