feat(RingTheory/LaurentSeries): prove that Laurent Series over a fiel…

…d are complete (#16865)

In this PR we provide a proof that the Laurent series over a field are complete.

Co-authored-by: María Inés de Frutos-Fernández @mariainesdff

Mathlib/Order/Filter/Ultrafilter.lean

@@ -465,4 +465,8 @@ theorem ofComapInfPrincipal_eq_of_map (h : m '' s ∈ g) : (ofComapInfPrincipal
     _ ≤ ↑g ⊓ (𝓟 <| m '' s) := inf_le_inf_right _ map_comap_le
     _ = ↑g := inf_of_le_left (le_principal_iff.mpr h)
 
+theorem eq_of_le_pure {X : Type _} {α : Filter X} (hα : α.NeBot) {x y : X}
+    (hx : α ≤ pure x) (hy : α ≤ pure y) : x = y :=
+  Filter.pure_injective (hα.le_pure_iff.mp hx ▸ hα.le_pure_iff.mp hy)
+
 end Ultrafilter

Mathlib/RingTheory/LaurentSeries.lean

@@ -11,6 +11,7 @@ import Mathlib.RingTheory.HahnSeries.Summable
 import Mathlib.RingTheory.PowerSeries.Inverse
 import Mathlib.FieldTheory.RatFunc.AsPolynomial
 import Mathlib.RingTheory.Localization.FractionRing
+import Mathlib.Topology.UniformSpace.Cauchy
 
 /-!
 # Laurent Series
@@ -26,16 +27,23 @@ import Mathlib.RingTheory.Localization.FractionRing
 * Embedding of rational functions into Laurent series, provided as a coercion, utilizing
 the underlying `RatFunc.coeAlgHom`.
 * Study of the `X`-Adic valuation on the ring of Laurent series over a field
+* In `LaurentSeries.uniformContinuous_coeff` we show that sending a Laurent series to its `d`th
+coefficient is uniformly continuous, ensuring that it sends a Cauchy filter `ℱ` in `LaurentSeries K`
+to a Cauchy filter in `K`: since this latter is given the discrete topology, this provides an
+element `LaurentSeries.Cauchy.coeff ℱ d` in `K` that serves as `d`th coefficient of the Laurent
+series to which the filter `ℱ` converges.
 
 ## Main Results
 * Basic properties of Hasse derivatives
 ### About the `X`-Adic valuation:
 * The (integral) valuation of a power series is the order of the first non-zero coefficient, see
-`intValuation_le_iff_coeff_lt_eq_zero`.
+`LaurentSeries.intValuation_le_iff_coeff_lt_eq_zero`.
 * The valuation of a Laurent series is the order of the first non-zero coefficient, see
-`valuation_le_iff_coeff_lt_eq_zero`.
+`LaurentSeries.valuation_le_iff_coeff_lt_eq_zero`.
 * Every Laurent series of valuation less than `(1 : ℤₘ₀)` comes from a power series, see
-`val_le_one_iff_eq_coe`.
+`LaurentSeries.val_le_one_iff_eq_coe`.
+* The uniform space of `LaurentSeries` over a field is complete, formalized in the instance
+`instLaurentSeriesComplete`.
 
 ## Implementation details
 * Since `LaurentSeries` is just an abbreviation of `HahnSeries ℤ _`, the definition of the
@@ -464,6 +472,7 @@ end RatFunc
 
 namespace LaurentSeries
 
+
 open IsDedekindDomain.HeightOneSpectrum PowerSeries RatFunc
 
 instance : Valued (LaurentSeries K) ℤₘ₀ := Valued.mk' (PowerSeries.idealX K).valuation
@@ -609,3 +618,169 @@ theorem val_le_one_iff_eq_coe (f : LaurentSeries K) : Valued.v f ≤ (1 : ℤₘ
 end LaurentSeries
 
 end AdicValuation
+namespace LaurentSeries
+section Complete
+
+open Filter
+
+open scoped Multiplicative
+
+variable {K : Type*} [Field K]
+
+/- Sending a Laurent series to its `d`-th coefficient is uniformly continuous (independently of the
+ uniformity with which `K` is endowed). -/
+theorem uniformContinuous_coeff {uK : UniformSpace K} (d : ℤ) :
+    UniformContinuous fun f : LaurentSeries K ↦ f.coeff d := by
+  refine uniformContinuous_iff_eventually.mpr fun S hS ↦ eventually_iff_exists_mem.mpr ?_
+  let γ : ℤₘ₀ˣ := Units.mk0 (↑(Multiplicative.ofAdd (-(d + 1)))) WithZero.coe_ne_zero
+  use {P | Valued.v (P.snd - P.fst) < ↑γ}
+  refine ⟨(Valued.hasBasis_uniformity (LaurentSeries K) ℤₘ₀).mem_of_mem (by tauto), fun P hP ↦ ?_⟩
+  rw [eq_coeff_of_valuation_sub_lt K (le_of_lt hP) (lt_add_one _)]
+  exact mem_uniformity_of_eq hS rfl
+
+/-- Since extracting coefficients is uniformly continuous, every Cauchy filter in
+`laurentSeries K` gives rise to a Cauchy filter in `K` for every `d : ℤ`, and such Cauchy filter
+in `K` converges to a principal filter -/
+def Cauchy.coeff {ℱ : Filter (LaurentSeries K)} (hℱ : Cauchy ℱ) : ℤ → K :=
+  let _ : UniformSpace K := ⊥
+  fun d ↦ UniformSpace.DiscreteUnif.cauchyConst rfl <| hℱ.map (uniformContinuous_coeff d)
+
+theorem Cauchy.coeff_tendsto {ℱ : Filter (LaurentSeries K)} (hℱ : Cauchy ℱ) (D : ℤ) :
+    Tendsto (fun f : LaurentSeries K ↦ f.coeff D) ℱ (𝓟 {coeff hℱ D}) :=
+  let _ : UniformSpace K := ⊥
+  le_of_eq <| UniformSpace.DiscreteUnif.eq_const_of_cauchy (by rfl)
+    (hℱ.map (uniformContinuous_coeff D)) ▸ (principal_singleton _).symm
+
+/- For every Cauchy filter of Laurent series, there is a `N` such that the `n`-th coefficient
+vanishes for all `n ≤ N` and almost all series in the filter. This is an auxiliary lemma used
+to construct the limit of the Cauchy filter as a Laurent series, ensuring that the support of the
+limit is `PWO`.
+The result is true also for more general Hahn Series indexed over a partially ordered group `Γ`
+beyond the special case `Γ = ℤ`, that corresponds to Laurent Series: nevertheless the proof below
+does not generalise, as it relies on the study of the `X`-adic valuation attached to the height-one
+prime `X`, and this is peculiar to the one-variable setting. In the future we should prove this
+result in full generality and deduce the case `Γ = ℤ` from that one.-/
+lemma Cauchy.exists_lb_eventual_support {ℱ : Filter (LaurentSeries K)} (hℱ : Cauchy ℱ) :
+    ∃ N, ∀ᶠ f : LaurentSeries K in ℱ, ∀ n < N, f.coeff n = (0 : K) := by
+  let entourage : Set (LaurentSeries K × LaurentSeries K) :=
+    {P : LaurentSeries K × LaurentSeries K |
+      Valued.v (P.snd - P.fst) < ((Multiplicative.ofAdd 0 : Multiplicative ℤ) : ℤₘ₀)}
+  let ζ := Units.mk0 (G₀ := ℤₘ₀) _ (WithZero.coe_ne_zero (a := (Multiplicative.ofAdd 0)))
+  obtain ⟨S, ⟨hS, ⟨T, ⟨hT, H⟩⟩⟩⟩ := mem_prod_iff.mp <| Filter.le_def.mp hℱ.2 entourage
+    <| (Valued.hasBasis_uniformity (LaurentSeries K) ℤₘ₀).mem_of_mem (i := ζ) (by tauto)
+  obtain ⟨f, hf⟩ := forall_mem_nonempty_iff_neBot.mpr hℱ.1 (S ∩ T) (inter_mem_iff.mpr ⟨hS, hT⟩)
+  obtain ⟨N, hN⟩ :  ∃ N : ℤ, ∀ g : LaurentSeries K,
+    Valued.v (g - f) ≤ ↑(Multiplicative.ofAdd (0 : ℤ)) → ∀ n < N, g.coeff n = 0 := by
+    by_cases hf : f = 0
+    · refine ⟨0, fun x hg ↦ ?_⟩
+      rw [hf, sub_zero] at hg
+      exact (valuation_le_iff_coeff_lt_eq_zero K).mp hg
+    · refine ⟨min (f.2.isWF.min (HahnSeries.support_nonempty_iff.mpr hf)) 0 - 1, fun _ hg n hn ↦ ?_⟩
+      rw [eq_coeff_of_valuation_sub_lt K hg (d := 0)]
+      · exact Function.nmem_support.mp fun h ↦
+        f.2.isWF.not_lt_min (HahnSeries.support_nonempty_iff.mpr hf) h
+        <| lt_trans hn <| Int.sub_one_lt_iff.mpr <| min_le_left _ _
+      exact lt_of_lt_of_le hn <| le_of_lt (Int.sub_one_lt_of_le <| min_le_right _ _)
+  use N
+  apply mem_of_superset (inter_mem hS hT)
+  intro g hg
+  have h_prod : (f, g) ∈ entourage := Set.prod_mono (Set.inter_subset_left (t := T))
+    (Set.inter_subset_right (s := S)) |>.trans H <| Set.mem_prod.mpr ⟨hf, hg⟩
+  exact hN g (le_of_lt h_prod)
+
+/- The support of `Cauchy.coeff` has a lower bound. -/
+theorem Cauchy.exists_lb_support {ℱ : Filter (LaurentSeries K)} (hℱ : Cauchy ℱ) :
+    ∃ N, ∀ n, n < N → coeff hℱ n = 0 := by
+  let _ : UniformSpace K := ⊥
+  obtain ⟨N, hN⟩ := exists_lb_eventual_support hℱ
+  refine ⟨N, fun n hn ↦ Ultrafilter.eq_of_le_pure (hℱ.map (uniformContinuous_coeff n)).1
+      ((principal_singleton _).symm ▸ coeff_tendsto _ _) ?_⟩
+  simp only [pure_zero, nonpos_iff]
+  apply Filter.mem_of_superset hN (fun _ ha ↦ ha _ hn)
+
+/- The support of `Cauchy.coeff` is bounded below -/
+theorem Cauchy.coeff_support_bddBelow {ℱ : Filter (LaurentSeries K)} (hℱ : Cauchy ℱ) :
+    BddBelow (coeff hℱ).support := by
+  refine ⟨(exists_lb_support hℱ).choose, fun d hd ↦ ?_⟩
+  by_contra hNd
+  exact hd ((exists_lb_support hℱ).choose_spec d (not_le.mp hNd))
+
+/-- To any Cauchy filter ℱ of `LaurentSeries K`, we can attach a laurent series that is the limit
+of the filter. Its `d`-th coefficient is defined as the limit of `Cauchy.coeff hℱ d`, which is
+again Cauchy but valued in the discrete space `K`. That sufficiently negative coefficients vanish
+follows from `Cauchy.coeff_support_bddBelow` -/
+def Cauchy.limit {ℱ : Filter (LaurentSeries K)} (hℱ : Cauchy ℱ) : LaurentSeries K :=
+  HahnSeries.mk (coeff hℱ) <| Set.IsWF.isPWO (coeff_support_bddBelow _).wellFoundedOn_lt
+
+/- The following lemma shows that for every `d` smaller than the minimum between the integers
+produced in `Cauchy.exists_lb_eventual_support` and `Cauchy.exists_lb_support`, for almost all
+series in `ℱ` the `d`th coefficient coincides with the `d`th coefficient of `Cauchy.coeff hℱ`. -/
+theorem Cauchy.exists_lb_coeff_ne {ℱ : Filter (LaurentSeries K)} (hℱ : Cauchy ℱ) :
+    ∃ N, ∀ᶠ f : LaurentSeries K in ℱ, ∀ d < N, coeff hℱ d = f.coeff d := by
+  obtain ⟨⟨N₁, hN₁⟩, ⟨N₂, hN₂⟩⟩ := exists_lb_eventual_support hℱ, exists_lb_support hℱ
+  refine ⟨min N₁ N₂, ℱ.3 hN₁ fun _ hf d hd ↦ ?_⟩
+  rw [hf d (lt_of_lt_of_le hd (min_le_left _ _)), hN₂ d (lt_of_lt_of_le hd (min_le_right _ _))]
+
+/- Given a Cauchy filter `ℱ` in the Laurent Series and a bound `D`, for almost all series in the
+filter the coefficients below `D` coincide with `Caucy.coeff hℱ`-/
+theorem Cauchy.coeff_eventually_equal {ℱ : Filter (LaurentSeries K)} (hℱ : Cauchy ℱ) {D : ℤ} :
+    ∀ᶠ f : LaurentSeries K in ℱ, ∀ d, d < D → coeff hℱ d = f.coeff d := by
+  -- `φ` sends `d` to the set of Laurent Series having `d`th coefficient equal to `ℱ.coeff`.
+  let φ : ℤ → Set (LaurentSeries K) := fun d ↦ {f | coeff hℱ d = f.coeff d}
+  have intersec₁ :
+    (⋂ n ∈ Set.Iio D, φ n) ⊆ {x : LaurentSeries K | ∀ d : ℤ, d < D → coeff hℱ d = x.coeff d} := by
+    intro _ hf
+    simpa only [Set.mem_iInter] using hf
+  -- The goal is now to show that the intersection of all `φ d` (for `d < D`) is in `ℱ`.
+  let ℓ := (exists_lb_coeff_ne hℱ).choose
+  let N := max ℓ D
+  have intersec₂ : ⋂ n ∈ Set.Iio D, φ n ⊇ (⋂ n ∈ Set.Iio ℓ, φ n) ∩ (⋂ n ∈ Set.Icc ℓ N, φ n) := by
+    simp only [Set.mem_Iio, Set.mem_Icc, Set.subset_iInter_iff]
+    intro i hi x hx
+    simp only [Set.mem_inter_iff, Set.mem_iInter, and_imp] at hx
+    by_cases H : i < ℓ
+    exacts [hx.1 _ H, hx.2 _ (le_of_not_lt H) <| le_of_lt <| lt_max_of_lt_right hi]
+  suffices (⋂ n ∈ Set.Iio ℓ, φ n) ∩ (⋂ n ∈ Set.Icc ℓ N, φ n) ∈ ℱ by
+    exact ℱ.sets_of_superset this <| intersec₂.trans intersec₁
+  /- To show that the intersection we have in sight is in `ℱ`, we use that it contains a double
+  intersection (an infinite and a finite one): by general properties of filters, we are reduced
+  to show that both terms are in `ℱ`, which is easy in light of their definition. -/
+  · simp only [Set.mem_Iio, Set.mem_Ico, inter_mem_iff]
+    constructor
+    · have := (exists_lb_coeff_ne hℱ).choose_spec
+      rw [Filter.eventually_iff] at this
+      convert this
+      ext
+      simp only [Set.mem_iInter, Set.mem_setOf_eq]; rfl
+    · rw [biInter_mem (Set.finite_Icc ℓ N)]
+      intro _ _
+      apply coeff_tendsto hℱ
+      simp only [principal_singleton, mem_pure]; rfl
+
+
+open scoped Topology
+
+/- The main result showing that the Cauchy filter tends to the `Cauchy.limit`-/
+theorem Cauchy.eventually_mem_nhds {ℱ : Filter (LaurentSeries K)} (hℱ : Cauchy ℱ)
+    {U : Set (LaurentSeries K)} (hU : U ∈ 𝓝 (Cauchy.limit hℱ)) : ∀ᶠ f in ℱ, f ∈ U := by
+  obtain ⟨γ, hU₁⟩ := Valued.mem_nhds.mp hU
+  suffices ∀ᶠ f in ℱ, f ∈ {y : LaurentSeries K | Valued.v (y - limit hℱ) < ↑γ} by
+    apply this.mono fun _ hf ↦ hU₁ hf
+  set D := -(Multiplicative.toAdd (WithZero.unzero γ.ne_zero) - 1) with hD₀
+  have hD : ((Multiplicative.ofAdd (-D) : Multiplicative ℤ) : ℤₘ₀) < γ := by
+    rw [← WithZero.coe_unzero γ.ne_zero, WithZero.coe_lt_coe, hD₀, neg_neg, ofAdd_sub,
+      ofAdd_toAdd, div_lt_comm, div_self', ← ofAdd_zero, Multiplicative.ofAdd_lt]
+    exact zero_lt_one
+  apply coeff_eventually_equal hℱ |>.mono
+  intro _ hf
+  apply lt_of_le_of_lt (valuation_le_iff_coeff_lt_eq_zero K |>.mpr _) hD
+  intro n hn
+  rw [HahnSeries.sub_coeff, sub_eq_zero, hf n hn |>.symm]; rfl
+
+/- Laurent Series with coefficients in a field are complete w.r.t. the `X`-adic valuation -/
+instance instLaurentSeriesComplete : CompleteSpace (LaurentSeries K) :=
+  ⟨fun hℱ ↦ ⟨Cauchy.limit hℱ, fun _ hS ↦ Cauchy.eventually_mem_nhds hℱ hS⟩⟩
+
+end Complete
+
+end LaurentSeries

Mathlib/Topology/UniformSpace/Basic.lean

@@ -136,6 +136,31 @@ theorem mem_idRel {a b : α} : (a, b) ∈ @idRel α ↔ a = b :=
 theorem idRel_subset {s : Set (α × α)} : idRel ⊆ s ↔ ∀ a, (a, a) ∈ s := by
   simp [subset_def]
 
+theorem eq_singleton_left_of_prod_subset_idRel {X : Type _} {S T : Set X} (hS : S.Nonempty)
+    (hT : T.Nonempty) (h_diag : S ×ˢ T ⊆ idRel) : ∃ x, S = {x} := by
+  rcases hS, hT with ⟨⟨s, hs⟩, ⟨t, ht⟩⟩
+  refine ⟨s, eq_singleton_iff_nonempty_unique_mem.mpr ⟨⟨s, hs⟩, fun x hx ↦ ?_⟩⟩
+  rw [prod_subset_iff] at h_diag
+  replace hs := h_diag s hs t ht
+  replace hx := h_diag x hx t ht
+  simp only [idRel, mem_setOf_eq] at hx hs
+  rwa [← hs] at hx
+
+theorem eq_singleton_right_prod_subset_idRel {X : Type _} {S T : Set X} (hS : S.Nonempty)
+    (hT : T.Nonempty) (h_diag : S ×ˢ T ⊆ idRel) : ∃ x, T = {x} := by
+  rw [Set.prod_subset_iff] at h_diag
+  replace h_diag := fun x hx y hy => (h_diag y hy x hx).symm
+  exact eq_singleton_left_of_prod_subset_idRel hT hS (prod_subset_iff.mpr h_diag)
+
+theorem eq_singleton_prod_subset_idRel {X : Type _} {S T : Set X} (hS : S.Nonempty)
+    (hT : T.Nonempty) (h_diag : S ×ˢ T ⊆ idRel) : ∃ x, S = {x} ∧ T = {x} := by
+  obtain ⟨⟨x, hx⟩, ⟨y, hy⟩⟩ := eq_singleton_left_of_prod_subset_idRel hS hT h_diag,
+    eq_singleton_right_prod_subset_idRel hS hT h_diag
+  refine ⟨x, ⟨hx, ?_⟩⟩
+  rw [hy, Set.singleton_eq_singleton_iff]
+  exact (Set.prod_subset_iff.mp h_diag x (by simp only [hx, Set.mem_singleton]) y
+    (by simp only [hy, Set.mem_singleton])).symm
+
 /-- The composition of relations -/
 def compRel (r₁ r₂ : Set (α × α)) :=
   { p : α × α | ∃ z : α, (p.1, z) ∈ r₁ ∧ (z, p.2) ∈ r₂ }

Mathlib/Topology/UniformSpace/Cauchy.lean

@@ -787,4 +787,29 @@ theorem secondCountable_of_separable [SeparableSpace α] : SecondCountableTopolo
     refine ⟨_, ⟨y, hys, k, rfl⟩, (hts k).subset hxy, fun z hz => ?_⟩
     exact hUV (ball_subset_of_comp_subset (hk hxy) hUU' (hk hz))
 
+section DiscreteUniformity
+
+open Filter
+
+/-- A Cauchy filter in a discrete uniform space is contained in a principal filter-/
+theorem DiscreteUnif.cauchy_le_pure {X : Type _} {uX : UniformSpace X}
+    (hX : uX = ⊥) {α : Filter X} (hα : Cauchy α) : ∃ x : X, α = pure x := by
+  rcases hα with ⟨α_ne_bot, α_le⟩
+  rw [hX, bot_uniformity, le_principal_iff, mem_prod_iff] at α_le
+  obtain ⟨S, ⟨hS, ⟨T, ⟨hT, H⟩⟩⟩⟩ := α_le
+  obtain ⟨x, rfl⟩ := eq_singleton_left_of_prod_subset_idRel (α_ne_bot.nonempty_of_mem hS)
+    (Filter.nonempty_of_mem hT) H
+  exact ⟨x, α_ne_bot.le_pure_iff.mp <| le_pure_iff.mpr hS⟩
+
+/-- A constant to which a Cauchy filter in a discrete uniform space converges. -/
+noncomputable def DiscreteUnif.cauchyConst {X : Type _} {uX : UniformSpace X}
+    (hX : uX = ⊥) {α : Filter X} (hα : Cauchy α) : X :=
+  (DiscreteUnif.cauchy_le_pure hX hα).choose
+
+theorem DiscreteUnif.eq_const_of_cauchy {X : Type _} {uX : UniformSpace X} (hX : uX = ⊥)
+    {α : Filter X} (hα : Cauchy α) : α = pure (DiscreteUnif.cauchyConst hX hα) :=
+  (DiscreteUnif.cauchy_le_pure hX hα).choose_spec
+
+end DiscreteUniformity
+
 end UniformSpace