feat: the definition of nonarchimedean local fields (#27465)

Co-authored-by: Yakov Pechersky <pechersky@users.noreply.github.com>
Co-authored-by: pre-commit-ci-lite[bot] <117423508+pre-commit-ci-lite[bot]@users.noreply.github.com>

Author: 3 people

Mathlib.lean

@@ -4879,6 +4879,7 @@ import Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic
 import Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum
 import Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity
 import Mathlib.NumberTheory.LegendreSymbol.ZModChar
+import Mathlib.NumberTheory.LocalField.Basic
 import Mathlib.NumberTheory.LucasLehmer
 import Mathlib.NumberTheory.LucasPrimality
 import Mathlib.NumberTheory.MaricaSchoenheim

Mathlib/NumberTheory/LocalField/Basic.lean

@@ -0,0 +1,159 @@
+/-
+Copyright (c) 2025 Andrew Yang. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Andrew Yang
+-/
+import Mathlib.RingTheory.Valuation.DiscreteValuativeRel
+import Mathlib.Topology.Algebra.Valued.LocallyCompact
+import Mathlib.Topology.Algebra.Valued.ValuativeRel
+
+/-!
+
+# Definition of (Non-archimedean) local fields
+
+Given a topological field `K` equipped with an equivalence class of valuations (a `ValuativeRel`),
+we say that it is a non-archimedean local field if the topology comes from the given valuation,
+and it is locally compact and non-discrete.
+
+-/
+
+/--
+Given a topological field `K` equipped with an equivalence class of valuations (a `ValuativeRel`),
+we say that it is a non-archimedean local field if the topology comes from the given valuation,
+and it is locally compact and non-discrete.
+
+This implies the following typeclasses via `inferInstance`
+- `IsValuativeTopology K`
+- `LocallyCompactSpace K`
+- `IsTopologicalDivisionRing K`
+- `ValuativeRel.IsNontrivial K`
+- `ValuativeRel.IsRankLeOne K`
+- `ValuativeRel.IsDiscrete K`
+- `IsDiscreteValuationRing 𝒪[K]`
+- `Finite 𝓀[K]`
+
+Assuming we have a compatible `UniformSpace K` instance
+(e.g. via `IsTopologicalAddGroup.toUniformSpace` and `isUniformAddGroup_of_addCommGroup`) then
+- `CompleteSpace K`
+- `CompleteSpace 𝒪[K]`
+-/
+class IsNonarchimedeanLocalField
+    (K : Type*) [Field K] [ValuativeRel K] [TopologicalSpace K] : Prop extends
+  IsValuativeTopology K,
+  LocallyCompactSpace K,
+  ValuativeRel.IsNontrivial K
+
+open ValuativeRel Valued.integer
+
+open scoped WithZero
+
+namespace IsNonarchimedeanLocalField
+
+section TopologicalSpace
+
+variable (K : Type*) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K]
+
+attribute [local simp] zero_lt_iff
+
+instance : IsTopologicalDivisionRing K := by
+  letI := IsTopologicalAddGroup.toUniformSpace K
+  haveI := isUniformAddGroup_of_addCommGroup (G := K)
+  infer_instance
+
+lemma isCompact_closedBall (γ : ValueGroupWithZero K) : IsCompact { x | valuation K x ≤ γ } := by
+  obtain ⟨γ, rfl⟩ := ValuativeRel.valuation_surjective γ
+  by_cases hγ : γ = 0
+  · simp [hγ]
+  letI := IsTopologicalAddGroup.toUniformSpace K
+  letI := isUniformAddGroup_of_addCommGroup (G := K)
+  obtain ⟨s, hs, -, hs'⟩ := LocallyCompactSpace.local_compact_nhds (0 : K) .univ Filter.univ_mem
+  obtain ⟨r, hr, hr1, H⟩ :
+      ∃ r', r' ≠ 0 ∧ valuation K r' < 1 ∧ { x | valuation K x ≤ valuation K r' } ⊆ s := by
+    obtain ⟨r, hr, hrs⟩ := (IsValuativeTopology.hasBasis_nhds_zero' K).mem_iff.mp hs
+    obtain ⟨r', hr', hr⟩ := Valuation.IsNontrivial.exists_lt_one (v := valuation K)
+    simp only [ne_eq, map_eq_zero] at hr'
+    obtain hr1 | hr1 := lt_or_ge r 1
+    · obtain ⟨r, rfl⟩ := ValuativeRel.valuation_surjective r
+      simp only [ne_eq, map_eq_zero] at hr
+      refine ⟨r ^ 2, by simpa using hr, by simpa [pow_two], fun x hx ↦ hrs ?_⟩
+      simp only [map_pow, Set.mem_setOf_eq] at hx ⊢
+      exact hx.trans_lt (by simpa [pow_two, hr])
+    · refine ⟨r', hr', hr, .trans ?_ hrs⟩
+      intro x hx
+      dsimp at hx ⊢
+      exact hx.trans_lt (hr.trans_le hr1)
+  convert (hs'.of_isClosed_subset (Valued.isClosed_closedBall K _) H).image
+    (Homeomorph.mulLeft₀ (γ / r) (by simp [hr, div_eq_zero_iff, hγ])).continuous using 1
+  refine .trans ?_ (Equiv.image_eq_preimage _ _).symm
+  ext x
+  simp [div_mul_eq_mul_div, div_le_iff₀, IsValuativeTopology.v_eq_valuation, hγ, hr]
+
+instance : CompactSpace 𝒪[K] := isCompact_iff_compactSpace.mp (isCompact_closedBall K 1)
+
+instance (K : Type*) [Field K] [ValuativeRel K] [UniformSpace K] [IsUniformAddGroup K]
+    [IsValuativeTopology K] : (Valued.v (R := K) (Γ₀ := ValueGroupWithZero K)).Compatible :=
+  inferInstanceAs (valuation K).Compatible
+
+instance : IsDiscreteValuationRing 𝒪[K] :=
+  letI := IsTopologicalAddGroup.toUniformSpace K
+  haveI := isUniformAddGroup_of_addCommGroup (G := K)
+  haveI : CompactSpace (Valued.integer K) := inferInstanceAs (CompactSpace 𝒪[K])
+  Valued.integer.isDiscreteValuationRing_of_compactSpace
+
+/-- The value group of a local field is (uniquely) isomorphic to `ℤᵐ⁰`. -/
+noncomputable
+def valueGroupWithZeroIsoInt : ValueGroupWithZero K ≃*o ℤᵐ⁰ := by
+  apply Nonempty.some
+  letI := IsTopologicalAddGroup.toUniformSpace K
+  haveI := isUniformAddGroup_of_addCommGroup (G := K)
+  obtain ⟨_⟩ := Valued.integer.locallyFiniteOrder_units_mrange_of_isCompact_integer
+    (isCompact_iff_compactSpace.mpr (inferInstanceAs (CompactSpace 𝒪[K])))
+  let e : (MonoidHom.mrange (valuation K)) ≃*o ValueGroupWithZero K :=
+    ⟨.ofBijective (MonoidHom.mrange (valuation K)).subtype ⟨Subtype.val_injective, fun x ↦
+      ⟨⟨x, ValuativeRel.valuation_surjective x⟩, rfl⟩⟩, .rfl⟩
+  have : Nontrivial (ValueGroupWithZero K)ˣ := isNontrivial_iff_nontrivial_units.mp inferInstance
+  have : Nontrivial (↥(MonoidHom.mrange (valuation K)))ˣ :=
+    (Units.map_injective (f := e.symm.toMonoidHom) e.symm.injective).nontrivial
+  exact ⟨e.symm.trans (LocallyFiniteOrder.orderMonoidWithZeroEquiv _)⟩
+
+instance : ValuativeRel.IsDiscrete K :=
+  (ValuativeRel.nonempty_orderIso_withZeroMul_int_iff.mp ⟨valueGroupWithZeroIsoInt K⟩).1
+
+instance : ValuativeRel.IsRankLeOne K :=
+  ValuativeRel.isRankLeOne_iff_mulArchimedean.mpr
+    (.comap (valueGroupWithZeroIsoInt K).toMonoidHom (valueGroupWithZeroIsoInt K).strictMono)
+
+instance : Finite 𝓀[K] :=
+  letI := IsTopologicalAddGroup.toUniformSpace K
+  haveI := isUniformAddGroup_of_addCommGroup (G := K)
+  letI : (Valued.v (R := K)).RankOne :=
+    ⟨IsRankLeOne.nonempty.some.emb, IsRankLeOne.nonempty.some.strictMono⟩
+  (compactSpace_iff_completeSpace_and_isDiscreteValuationRing_and_finite_residueField.mp
+    (inferInstanceAs (CompactSpace 𝒪[K]))).2.2
+
+proof_wanted isAdicComplete : IsAdicComplete 𝓂[K] 𝒪[K]
+
+end TopologicalSpace
+
+section UniformSpace
+
+variable (K : Type*) [Field K] [ValuativeRel K]
+  [UniformSpace K] [IsUniformAddGroup K] [IsNonarchimedeanLocalField K]
+
+instance : CompleteSpace K :=
+  letI : (Valued.v (R := K)).RankOne :=
+    ⟨IsRankLeOne.nonempty.some.emb, IsRankLeOne.nonempty.some.strictMono⟩
+  open scoped Valued in
+  have : ProperSpace K := .of_nontriviallyNormedField_of_weaklyLocallyCompactSpace K
+  (properSpace_iff_completeSpace_and_isDiscreteValuationRing_integer_and_finite_residueField.mp
+    inferInstance).1
+
+instance : CompleteSpace 𝒪[K] :=
+  letI : (Valued.v (R := K)).RankOne :=
+    ⟨IsRankLeOne.nonempty.some.emb, IsRankLeOne.nonempty.some.strictMono⟩
+  (compactSpace_iff_completeSpace_and_isDiscreteValuationRing_and_finite_residueField.mp
+    (inferInstanceAs (CompactSpace 𝒪[K]))).1
+
+end UniformSpace
+
+end IsNonarchimedeanLocalField

Mathlib/RingTheory/Valuation/RankOne.lean

@@ -121,7 +121,6 @@ variable {R : Type*} [CommRing R] [ValuativeRel R]
 and the rank is at most one. -/
 def Valuation.RankOne.ofRankLeOneStruct [ValuativeRel.IsNontrivial R] (e : RankLeOneStruct R) :
     Valuation.RankOne (valuation R) where
-  __ : Valuation.IsNontrivial (valuation R) := isNontrivial_iff_isNontrivial.mp inferInstance
   hom := e.emb
   strictMono' := e.strictMono
 
@@ -141,7 +140,7 @@ lemma ValuativeRel.isRankLeOne_of_rankOne [h : (valuation R).RankOne] :
 
 lemma ValuativeRel.isNontrivial_of_rankOne [h : (valuation R).RankOne] :
     ValuativeRel.IsNontrivial R :=
-  isNontrivial_iff_isNontrivial.mpr h.toIsNontrivial
+  (isNontrivial_iff_isNontrivial _).mpr h.toIsNontrivial
 
 open WithZero
 
@@ -152,7 +151,7 @@ lemma ValuativeRel.isRankLeOne_iff_mulArchimedean :
     exact .comap f.toMonoidHom hf
   · intro h
     by_cases H : IsNontrivial R
-    · rw [isNontrivial_iff_isNontrivial] at H
+    · rw [isNontrivial_iff_isNontrivial (valuation R)] at H
       rw [← (valuation R).nonempty_rankOne_iff_mulArchimedean] at h
       obtain ⟨f⟩ := h
       exact isRankLeOne_of_rankOne

Mathlib/RingTheory/Valuation/ValuativeRel/Basic.lean

@@ -654,45 +654,58 @@ lemma isNontrivial_iff_nontrivial_units :
     · exact ⟨s.val, by simp, by simpa using h.symm⟩
     · exact ⟨r.val, by simp, by simpa using hr⟩
 
-lemma isNontrivial_iff_isNontrivial :
-    IsNontrivial R ↔ (valuation R).IsNontrivial := by
+lemma isNontrivial_iff_isNontrivial
+    {Γ₀ : Type*} [LinearOrderedCommMonoidWithZero Γ₀] (v : Valuation R Γ₀) [v.Compatible] :
+    IsNontrivial R ↔ v.IsNontrivial := by
   constructor
   · rintro ⟨r, hr, hr'⟩
     induction r using ValueGroupWithZero.ind with | mk r s
-    by_cases hs : valuation R s = 1
-    · refine ⟨r, ?_, ?_⟩
-      · simpa [valuation] using hr
-      · simp only [ne_eq, ValueGroupWithZero.mk_eq_one, not_and, valuation, Valuation.coe_mk,
-          MonoidWithZeroHom.coe_mk, ZeroHom.coe_mk, OneMemClass.coe_one] at hr' hs ⊢
-        contrapose! hr'
-        exact hr'.imp hs.right.trans' hs.left.trans
-    · refine ⟨s, ?_, hs⟩
-      simp [valuation, ← posSubmonoid_def]
+    have hγ : v r ≠ 0 := by simpa [Valuation.Compatible.rel_iff_le (v := v)] using hr
+    have hγ' : v r ≤ v s → v r < v s := by
+      simpa [Valuation.Compatible.rel_iff_le (v := v)] using hr'
+    by_cases hr : v r = 1
+    · exact ⟨s, by simp, fun h ↦ by simp [h, hr] at hγ'⟩
+    · exact ⟨r, by simpa using hγ, hr⟩
   · rintro ⟨r, hr, hr'⟩
-    exact ⟨valuation R r, hr, hr'⟩
+    exact ⟨valuation R r, (isEquiv v (valuation R)).ne_zero.mp hr,
+      by simpa [(isEquiv v (valuation R)).eq_one_iff_eq_one] using hr'⟩
 
-variable (R) in
-/-- A ring with a valuative relation is discrete if its value group-with-zero
-has a maximal element `< 1`. -/
-class IsDiscrete where
-  has_maximal_element :
-    ∃ γ : ValueGroupWithZero R, γ < 1 ∧ (∀ δ : ValueGroupWithZero R, δ < 1 → δ ≤ γ)
+instance {Γ₀ : Type*} [LinearOrderedCommMonoidWithZero Γ₀]
+    [IsNontrivial R] (v : Valuation R Γ₀) [v.Compatible] :
+    v.IsNontrivial := by rwa [← isNontrivial_iff_isNontrivial]
 
-lemma valuation_surjective (γ : ValueGroupWithZero R) :
+lemma ValueGroupWithZero.mk_eq_valuation {K : Type*} [Field K] [ValuativeRel K]
+    (x : K) (y : posSubmonoid K) :
+    ValueGroupWithZero.mk x y = valuation K (x / y) := by
+  rw [Valuation.map_div, ValueGroupWithZero.mk_eq_div]
+
+lemma exists_valuation_div_valuation_eq (γ : ValueGroupWithZero R) :
     ∃ (a : R) (b : posSubmonoid R), valuation _ a / valuation _ (b : R) = γ := by
   induction γ using ValueGroupWithZero.ind with | mk a b
   use a, b
   simp [valuation, div_eq_mul_inv, ValueGroupWithZero.inv_mk (b : R) 1 b.prop]
 
 lemma exists_valuation_posSubmonoid_div_valuation_posSubmonoid_eq (γ : (ValueGroupWithZero R)ˣ) :
     ∃ (a b : posSubmonoid R), valuation R a / valuation _ (b : R) = γ := by
-  obtain ⟨a, b, hab⟩ := valuation_surjective γ.val
+  obtain ⟨a, b, hab⟩ := exists_valuation_div_valuation_eq γ.val
   lift a to posSubmonoid R using by
     rw [posSubmonoid_def, ← valuation_eq_zero_iff]
     intro H
     simp [H, eq_comm] at hab
   use a, b
 
+-- See `exists_valuation_div_valuation_eq` for the version that works for all rings.
+theorem valuation_surjective {K : Type*} [Field K] [ValuativeRel K] :
+    Function.Surjective (valuation K) :=
+  ValueGroupWithZero.ind (ValueGroupWithZero.mk_eq_valuation · · ▸ ⟨_, rfl⟩)
+
+variable (R) in
+/-- A ring with a valuative relation is discrete if its value group-with-zero
+has a maximal element `< 1`. -/
+class IsDiscrete where
+  has_maximal_element :
+    ∃ γ : ValueGroupWithZero R, γ < 1 ∧ (∀ δ : ValueGroupWithZero R, δ < 1 → δ ≤ γ)
+
 end ValuativeRel
 
 open Topology ValuativeRel in
@@ -736,8 +749,8 @@ lemma ValueGroupWithZero.embed_valuation (γ : ValueGroupWithZero R) :
 
 lemma ValueGroupWithZero.embed_strictMono [v.Compatible] : StrictMono (embed v) := by
   intro a b h
-  obtain ⟨a, r, rfl⟩ := valuation_surjective a
-  obtain ⟨b, s, rfl⟩ := valuation_surjective b
+  obtain ⟨a, r, rfl⟩ := exists_valuation_div_valuation_eq a
+  obtain ⟨b, s, rfl⟩ := exists_valuation_div_valuation_eq b
   simp only [map_div₀]
   rw [div_lt_div_iff₀] at h ⊢
   any_goals simp [zero_lt_iff]

Mathlib/Topology/Algebra/Valued/ValuativeRel.lean

@@ -74,17 +74,34 @@ instance (priority := low) {R : Type*} [CommRing R] [ValuativeRel R] [UniformSpa
   «v» := valuation R
   is_topological_valuation := mem_nhds_zero_iff
 
+lemma v_eq_valuation {R : Type*} [CommRing R] [ValuativeRel R] [UniformSpace R]
+    [IsUniformAddGroup R] [IsValuativeTopology R] :
+    Valued.v = valuation R := rfl
+
 theorem hasBasis_nhds (x : R) :
     (𝓝 x).HasBasis (fun _ => True)
       fun γ : (ValueGroupWithZero R)ˣ => { z | v (z - x) < γ } := by
   simp [Filter.hasBasis_iff, mem_nhds_iff']
 
+/-- A variant of `hasBasis_nhds` where `· ≠ 0` is unbundled. -/
+lemma hasBasis_nhds' (x : R) :
+    (𝓝 x).HasBasis (· ≠ 0) ({ y | v (y - x) < · }) :=
+  (hasBasis_nhds x).to_hasBasis (fun γ _ ↦ ⟨γ, by simp⟩)
+    fun γ hγ ↦ ⟨.mk0 γ hγ, by simp⟩
+
 variable (R) in
 theorem hasBasis_nhds_zero :
     (𝓝 (0 : R)).HasBasis (fun _ => True)
       fun γ : (ValueGroupWithZero R)ˣ => { x | v x < γ } := by
   convert hasBasis_nhds (0 : R); rw [sub_zero]
 
+variable (R) in
+/-- A variant of `hasBasis_nhds_zero` where `· ≠ 0` is unbundled. -/
+lemma hasBasis_nhds_zero' :
+    (𝓝 0).HasBasis (· ≠ 0) ({ x | v x < · }) :=
+  (hasBasis_nhds_zero R).to_hasBasis (fun γ _ ↦ ⟨γ, by simp⟩)
+    fun γ hγ ↦ ⟨.mk0 γ hγ, by simp⟩
+
 @[deprecated (since := "2025-08-01")]
 alias _root_.ValuativeTopology.hasBasis_nhds_zero := hasBasis_nhds_zero