From 1fec3c4a56a0a991f7324bb7b1f89ab6a6795d19 Mon Sep 17 00:00:00 2001
From: "Yury G. Kudryashov" <urkud@urkud.name>
Date: Fri, 26 Jan 2024 13:55:43 +0000
Subject: [PATCH] chore(Filter/Ker): move from Filter.Basic to a new file
 (#10023)

Start moving parts of >3K lines long `Filter.Basic` to new files.
---
 Mathlib.lean                    |  1 +
 Mathlib/Order/Filter/Bases.lean |  1 +
 Mathlib/Order/Filter/Basic.lean | 39 ----------------------
 Mathlib/Order/Filter/Ker.lean   | 58 +++++++++++++++++++++++++++++++++
 4 files changed, 60 insertions(+), 39 deletions(-)
 create mode 100644 Mathlib/Order/Filter/Ker.lean

diff --git a/Mathlib.lean b/Mathlib.lean
index 98143c2aa7390..43c654c358a06 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -2938,6 +2938,7 @@ import Mathlib.Order.Filter.FilterProduct
 import Mathlib.Order.Filter.Germ
 import Mathlib.Order.Filter.IndicatorFunction
 import Mathlib.Order.Filter.Interval
+import Mathlib.Order.Filter.Ker
 import Mathlib.Order.Filter.Lift
 import Mathlib.Order.Filter.ModEq
 import Mathlib.Order.Filter.NAry
diff --git a/Mathlib/Order/Filter/Bases.lean b/Mathlib/Order/Filter/Bases.lean
index da61298eac6f2..3cafc3a20d0a5 100644
--- a/Mathlib/Order/Filter/Bases.lean
+++ b/Mathlib/Order/Filter/Bases.lean
@@ -6,6 +6,7 @@ Authors: Yury Kudryashov, Johannes Hölzl, Mario Carneiro, Patrick Massot
 import Mathlib.Data.Prod.PProd
 import Mathlib.Data.Set.Countable
 import Mathlib.Order.Filter.Prod
+import Mathlib.Order.Filter.Ker
 
 #align_import order.filter.bases from "leanprover-community/mathlib"@"996b0ff959da753a555053a480f36e5f264d4207"
 
diff --git a/Mathlib/Order/Filter/Basic.lean b/Mathlib/Order/Filter/Basic.lean
index 4a4fc2d1058cd..b1552a1a3e6f6 100644
--- a/Mathlib/Order/Filter/Basic.lean
+++ b/Mathlib/Order/Filter/Basic.lean
@@ -2982,45 +2982,6 @@ theorem mem_traverse_iff (fs : List β') (t : Set (List α')) :
 
 end ListTraverse
 
-section ker
-variable {ι : Sort*} {α β : Type*} {f g : Filter α} {s : Set α} {a : α}
-open Function Set
-
-/-- The *kernel* of a filter is the intersection of all its sets. -/
-def ker (f : Filter α) : Set α := ⋂₀ f.sets
-
-lemma ker_def (f : Filter α) : f.ker = ⋂ s ∈ f, s := sInter_eq_biInter
-
-@[simp] lemma mem_ker : a ∈ f.ker ↔ ∀ s ∈ f, a ∈ s := mem_sInter
-@[simp] lemma subset_ker : s ⊆ f.ker ↔ ∀ t ∈ f, s ⊆ t := subset_sInter_iff
-
-/-- `Filter.principal` forms a Galois coinsertion with `Filter.ker`. -/
-def gi_principal_ker : GaloisCoinsertion (𝓟 : Set α → Filter α) ker :=
-GaloisConnection.toGaloisCoinsertion (λ s f ↦ by simp [principal_le_iff]) <| by
-  simp only [le_iff_subset, subset_def, mem_ker, mem_principal]; aesop
-
-lemma ker_mono : Monotone (ker : Filter α → Set α) := gi_principal_ker.gc.monotone_u
-lemma ker_surjective : Surjective (ker : Filter α → Set α) := gi_principal_ker.u_surjective
-
-@[simp] lemma ker_bot : ker (⊥ : Filter α) = ∅ := sInter_eq_empty_iff.2 λ _ ↦ ⟨∅, trivial, id⟩
-@[simp] lemma ker_top : ker (⊤ : Filter α) = univ := gi_principal_ker.gc.u_top
-@[simp] lemma ker_eq_univ : ker f = univ ↔ f = ⊤ := gi_principal_ker.gc.u_eq_top.trans <| by simp
-@[simp] lemma ker_inf (f g : Filter α) : ker (f ⊓ g) = ker f ∩ ker g := gi_principal_ker.gc.u_inf
-@[simp] lemma ker_iInf (f : ι → Filter α) : ker (⨅ i, f i) = ⨅ i, ker (f i) :=
-gi_principal_ker.gc.u_iInf
-@[simp] lemma ker_sInf (S : Set (Filter α)) : ker (sInf S) = ⨅ f ∈ S, ker f :=
-gi_principal_ker.gc.u_sInf
-@[simp] lemma ker_principal (s : Set α) : ker (𝓟 s) = s := gi_principal_ker.u_l_eq _
-
-@[simp] lemma ker_pure (a : α) : ker (pure a) = {a} := by rw [← principal_singleton, ker_principal]
-
-@[simp] lemma ker_comap (m : α → β) (f : Filter β) : ker (comap m f) = m ⁻¹' ker f := by
-  ext a
-  simp only [mem_ker, mem_comap, forall_exists_index, and_imp, @forall_swap (Set α), mem_preimage]
-  exact forall₂_congr λ s _ ↦ ⟨λ h ↦ h _ Subset.rfl, λ ha t ht ↦ ht ha⟩
-
-end ker
-
 /-! ### Limits -/
 
 /-- `Filter.Tendsto` is the generic "limit of a function" predicate.
diff --git a/Mathlib/Order/Filter/Ker.lean b/Mathlib/Order/Filter/Ker.lean
new file mode 100644
index 0000000000000..f0cce2ee42c8c
--- /dev/null
+++ b/Mathlib/Order/Filter/Ker.lean
@@ -0,0 +1,58 @@
+/-
+Copyright (c) 2023 Yaël Dillies. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yaël Dillies
+-/
+import Mathlib.Order.Filter.Basic
+
+/-!
+# Kernel of a filter
+
+In this file we define the *kernel* `Filter.ker f` of a filter `f`
+to be the intersection of all its sets.
+
+We also prove that `Filter.principal` and `Filter.ker` form a Galois coinsertion
+and prove other basic theorems about `Filter.ker`.
+-/
+
+open Function Set
+
+namespace Filter
+
+variable {ι : Sort*} {α β : Type*} {f g : Filter α} {s : Set α} {a : α}
+
+/-- The *kernel* of a filter is the intersection of all its sets. -/
+def ker (f : Filter α) : Set α := ⋂₀ f.sets
+
+lemma ker_def (f : Filter α) : f.ker = ⋂ s ∈ f, s := sInter_eq_biInter
+
+@[simp] lemma mem_ker : a ∈ f.ker ↔ ∀ s ∈ f, a ∈ s := mem_sInter
+@[simp] lemma subset_ker : s ⊆ f.ker ↔ ∀ t ∈ f, s ⊆ t := subset_sInter_iff
+
+/-- `Filter.principal` forms a Galois coinsertion with `Filter.ker`. -/
+def gi_principal_ker : GaloisCoinsertion (𝓟 : Set α → Filter α) ker :=
+  GaloisConnection.toGaloisCoinsertion (fun s f ↦ by simp [principal_le_iff]) <| by
+    simp only [le_iff_subset, subset_def, mem_ker, mem_principal]; aesop
+
+lemma ker_mono : Monotone (ker : Filter α → Set α) := gi_principal_ker.gc.monotone_u
+lemma ker_surjective : Surjective (ker : Filter α → Set α) := gi_principal_ker.u_surjective
+
+@[simp] lemma ker_bot : ker (⊥ : Filter α) = ∅ := sInter_eq_empty_iff.2 fun _ ↦ ⟨∅, trivial, id⟩
+@[simp] lemma ker_top : ker (⊤ : Filter α) = univ := gi_principal_ker.gc.u_top
+@[simp] lemma ker_eq_univ : ker f = univ ↔ f = ⊤ := gi_principal_ker.gc.u_eq_top.trans <| by simp
+@[simp] lemma ker_inf (f g : Filter α) : ker (f ⊓ g) = ker f ∩ ker g := gi_principal_ker.gc.u_inf
+@[simp] lemma ker_iInf (f : ι → Filter α) : ker (⨅ i, f i) = ⨅ i, ker (f i) :=
+  gi_principal_ker.gc.u_iInf
+@[simp] lemma ker_sInf (S : Set (Filter α)) : ker (sInf S) = ⨅ f ∈ S, ker f :=
+  gi_principal_ker.gc.u_sInf
+@[simp] lemma ker_principal (s : Set α) : ker (𝓟 s) = s := gi_principal_ker.u_l_eq _
+
+@[simp] lemma ker_pure (a : α) : ker (pure a) = {a} := by rw [← principal_singleton, ker_principal]
+
+@[simp] lemma ker_comap (m : α → β) (f : Filter β) : ker (comap m f) = m ⁻¹' ker f := by
+  ext a
+  simp only [mem_ker, mem_comap, forall_exists_index, and_imp, @forall_swap (Set α), mem_preimage]
+  exact forall₂_congr fun s _ ↦ ⟨fun h ↦ h _ Subset.rfl, fun ha t ht ↦ ht ha⟩
+
+end Filter
+