leanprover-community
diff --git a/‎Mathlib.lean‎
Lines changed: 1 addition & 0 deletions b/‎Mathlib.lean‎
Lines changed: 1 addition & 0 deletions
diff --git a/‎Mathlib/Algebra/GroupWithZero/Range.lean‎
Lines changed: 60 additions & 1 deletion b/‎Mathlib/Algebra/GroupWithZero/Range.lean‎
Lines changed: 60 additions & 1 deletion
diff --git a/‎Mathlib/FieldTheory/RatFunc/AsPolynomial.lean‎
Lines changed: 7 additions & 0 deletions b/‎Mathlib/FieldTheory/RatFunc/AsPolynomial.lean‎
Lines changed: 7 additions & 0 deletions
diff --git a/‎Mathlib/NumberTheory/FunctionField.lean‎
Lines changed: 2 additions & 1 deletion b/‎Mathlib/NumberTheory/FunctionField.lean‎
Lines changed: 2 additions & 1 deletion
diff --git a/‎Mathlib/NumberTheory/LocalField/Basic.lean‎
Lines changed: 15 additions & 4 deletions b/‎Mathlib/NumberTheory/LocalField/Basic.lean‎
Lines changed: 15 additions & 4 deletions
diff --git a/‎Mathlib/NumberTheory/NumberField/FinitePlaces.lean‎
Lines changed: 27 additions & 31 deletions b/‎Mathlib/NumberTheory/NumberField/FinitePlaces.lean‎
Lines changed: 27 additions & 31 deletions
diff --git a/‎Mathlib/NumberTheory/Padics/Complex.lean‎
Lines changed: 13 additions & 8 deletions b/‎Mathlib/NumberTheory/Padics/Complex.lean‎
Lines changed: 13 additions & 8 deletions
diff --git a/‎Mathlib/NumberTheory/Padics/HeightOneSpectrum.lean‎
Lines changed: 0 additions & 4 deletions b/‎Mathlib/NumberTheory/Padics/HeightOneSpectrum.lean‎
Lines changed: 0 additions & 4 deletions
@@ -6656,6 +6656,7 @@ public import Mathlib.RingTheory.Valuation.AlgebraInstances
 public import Mathlib.RingTheory.Valuation.Archimedean
 public import Mathlib.RingTheory.Valuation.Basic
 public import Mathlib.RingTheory.Valuation.Discrete.Basic
+public import Mathlib.RingTheory.Valuation.Discrete.RankOne
 public import Mathlib.RingTheory.Valuation.DiscreteValuativeRel
 public import Mathlib.RingTheory.Valuation.ExtendToLocalization
 public import Mathlib.RingTheory.Valuation.Extension
 
@@ -24,7 +24,7 @@ elements in `range f` and `MonoidWithZeroHom.ValueGroup₀` adds a `0` to the pr
 
 When `B` is commutative, then both `MonoidWithZeroHom.valueGroup f` and
 `MonoidWithZeroHom.ValueGroup₀ f` are also commutative and the former can be described more
-explicitly (see `MonoidWithZeroHom.mem_valueGroup_iff_of_comm`).
+explicitly (see `MonoidWithZeroHom.mem_valueGroup_iff_of_comm` and `mem_valueGroup_iff_of_comm'`).
 
 ## Main declarations
 
@@ -224,6 +224,7 @@ section CommGroupWithZero
 --
 variable [MonoidWithZero A] [CommGroupWithZero B] [MonoidWithZeroHomClass F A B]
 
+/- See also `mem_valueGroup_iff_of_comm'` for a version proving that `f x ≠ 0`. -/
 theorem mem_valueGroup_iff_of_comm {y : Bˣ} :
     y ∈ valueGroup f ↔ ∃ a, f a ≠ 0 ∧ ∃ x, f a * y = f x := by
   refine ⟨fun hy ↦ ?_, fun ⟨a, ha, x, hy⟩ ↦ ?_⟩
@@ -255,6 +256,64 @@ theorem mem_valueGroup_iff_of_comm {y : Bˣ} :
     · apply mem_valueGroup
       use x
 
+theorem mem_valueGroup_iff_of_comm' {y : Bˣ} :
+    y ∈ valueGroup f ↔ ∃ a, f a ≠ 0 ∧ ∃ x, f x ≠ 0 ∧ f a * y = f x := by
+  rw [mem_valueGroup_iff_of_comm]
+  exact ⟨fun ⟨a, ha, x, hax⟩ ↦ ⟨a, ha, x, by aesop, hax⟩, fun ⟨a, ha, x, hx, hax⟩ ↦ ⟨a, ha, x, hax⟩⟩
+
+namespace valueGroup
+
+variable {r₁ s₁ r₂ s₂ : A}
+
+/-- The map sending a pair of nonzero `r s : A` to the element `(v r)⁻¹ * (v s)`
+of `ValueGroup₀ v`. -/
+def mk (r s : A) (hr : f r ≠ 0) (hs : f s ≠ 0) : valueGroup f :=
+    (⟨(.mk0 _ hr)⁻¹ * (.mk0 _ hs), mul_mem (inv_mem (mem_valueGroup _ (by simp)))
+    (mem_valueGroup _ (by simp))⟩ : valueGroup f)
+
+@[simp] theorem mk_inj {hr₁ : f r₁ ≠ 0} {hs₁ : f s₁ ≠ 0} {hr₂ : f r₂ ≠ 0} {hs₂ : f s₂ ≠ 0} :
+    mk f r₁ s₁ hr₁ hs₁ = mk f r₂ s₂ hr₂ hs₂ ↔ f (r₁ * s₂) = f (r₂ * s₁) := by
+  simp only [mk, Subtype.mk.injEq, map_mul]
+  rw [inv_mul_eq_inv_mul_iff_mul_eq_mul, eq_comm]
+  simp [Units.ext_iff, mul_comm (f r₂), mul_comm (f s₂)]
+
+@[simp] theorem mk_mul {hr₁ : f r₁ ≠ 0} {hs₁ : f s₁ ≠ 0} {hr₂ : f r₂ ≠ 0} {hs₂ : f s₂ ≠ 0} :
+    mk f r₁ s₁ hr₁ hs₁ * mk f r₂ s₂ hr₂ hs₂ =
+      mk f (r₁ * r₂) (s₁ * s₂) (by simp_all) (by simp_all) := by
+  simp only [mk, map_mul, MulMemClass.mk_mul_mk, Units.mk0_mul, Subtype.mk.injEq]
+  rw [mul_mul_mul_comm, mul_inv]
+
+end valueGroup
+namespace ValueGroup₀
+
+/-- The map sending a pair of nonzero `r s : A` to the element `(v r)⁻¹ * (v s)`
+of `ValueGroup₀ v`. -/
+def mk [DecidablePred fun b : B ↦ b = 0] (r s : A) : ValueGroup₀ f :=
+    if h : f r = 0 ∨ f s = 0 then 0 else
+    valueGroup.mk f r s ((not_or.mp h).1) ((not_or.mp h).2)
+
+lemma mk_eq_of_ne_zero [DecidablePred fun b : B ↦ b = 0] (r s : A) (hr : f r ≠ 0) (hs : f s ≠ 0) :
+    ValueGroup₀.mk f r s = valueGroup.mk f r s hr hs := by
+  simp [ValueGroup₀.mk, hr, hs]
+
+theorem zero_or_exists_mk (x : ValueGroup₀ f) :
+    x = 0 ∨ ∃ r s hr hs, x = valueGroup.mk f r s hr hs := by
+  obtain _ | ⟨x, hx⟩ := x
+  · left; rfl
+  · rw [mem_valueGroup_iff_of_comm'] at hx
+    obtain ⟨r, hr, s, hs, hrs⟩ := hx
+    refine .inr ⟨r, s, hr, hs, Option.some_inj.mpr <| by
+      simp only [valueGroup.mk, Subtype.mk.injEq]
+      rw [eq_inv_mul_iff_mul_eq]
+      simp [← hrs, mul_comm]⟩
+
+theorem zero_or_exists_mk' (x : ValueGroup₀ f) :
+    x = 0 ∨ ∃ d : {xy : A × A // f xy.1 ≠ 0 ∧ f xy.2 ≠ 0}, x =
+      valueGroup.mk f d.1.1 d.1.2 d.2.1 d.2.2 :=
+  x.zero_or_exists_mk.imp _root_.id fun ⟨r, s, hr, hs, hx⟩ ↦ ⟨⟨(r, s), ⟨hr, hs⟩⟩, hx⟩
+
+end ValueGroup₀
+
 instance : CommGroupWithZero (ValueGroup₀ f) where
 
 end CommGroupWithZero
 
@@ -401,6 +401,13 @@ instance : Valued K⟮X⟯ ℤᵐ⁰ := Valued.mk' ((idealX K).valuation _)
 theorem v_def {x : K⟮X⟯} :
     Valued.v x = (idealX K).valuation _ x := rfl
 
+lemma valuation_surjective : Function.Surjective (Valued.v (R := RatFunc K)) := by
+  intro n
+  by_cases hn0 : n = 0
+  · use 0; simp [hn0]
+  · use (RatFunc.X ^ (-WithZero.log n))
+    simp [WithZero.exp_log hn0]
+
 end RatFunc
 
 end AdicValuation
@@ -253,7 +253,8 @@ instance : Inhabited (FqtInfty Fq) :=
 /-- The valuation at infinity on `k(t)` extends to a valuation on `FqtInfty`. -/
 instance valuedFqtInfty : Valued (FqtInfty Fq) ℤᵐ⁰ := (inftyValuedFqt Fq).valuedCompletion
 
-theorem valuedFqtInfty.def {x : FqtInfty Fq} : Valued.v x = (inftyValuedFqt Fq).extension x := rfl
+theorem valuedFqtInfty.def {x : FqtInfty Fq} :
+  Valued.v x = (inftyValuedFqt Fq).extensionValuation x := rfl
 
 end InftyValuation
 
 
@@ -86,11 +86,16 @@ lemma isCompact_closedBall (γ : ValueGroupWithZero K) : IsCompact { x | valuati
       intro x hx
       dsimp at hx ⊢
       exact hx.trans_lt (hr.trans_le hr1)
+  simp_rw [← (valuation K).restrict_le_iff] at H ⊢
   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 _ _).symm
   ext x
-  simp [div_mul_eq_mul_div, div_le_iff₀, IsValuativeTopology.v_eq_valuation, hγ, hr]
+  simp only [Set.mem_setOf_eq, Homeomorph.coe_symm_toEquiv, Homeomorph.mulLeft₀_symm_apply, inv_div,
+    Set.preimage_setOf_eq, map_mul, map_div₀, Valuation.restrict_le_iff]
+  rw [div_mul_eq_mul_div, div_le_iff₀ (by simp [hγ])]
+  simp only [IsValuativeTopology.v_eq_valuation, ← map_mul, Valuation.restrict_le_iff]
+  simp [hr]
 
 instance : CompactSpace 𝒪[K] := isCompact_iff_compactSpace.mp (isCompact_closedBall K 1)
 
@@ -132,7 +137,9 @@ instance : Finite 𝓀[K] :=
   letI := IsTopologicalAddGroup.rightUniformSpace K
   haveI := isUniformAddGroup_of_addCommGroup (G := K)
   letI : (Valued.v (R := K)).RankOne :=
-    ⟨IsRankLeOne.nonempty.some.emb, IsRankLeOne.nonempty.some.strictMono⟩
+  { hom' := IsRankLeOne.nonempty.some.emb (R := K).comp MonoidWithZeroHom.ValueGroup₀.embedding
+    strictMono' := IsRankLeOne.nonempty.some.strictMono.comp
+        MonoidWithZeroHom.ValueGroup₀.embedding_strictMono }
   (compactSpace_iff_completeSpace_and_isDiscreteValuationRing_and_finite_residueField.mp
     (inferInstanceAs (CompactSpace 𝒪[K]))).2.2
 
@@ -147,15 +154,19 @@ variable (K : Type*) [Field K] [ValuativeRel K]
 
 instance : CompleteSpace K :=
   letI : (Valued.v (R := K)).RankOne :=
-    ⟨IsRankLeOne.nonempty.some.emb, IsRankLeOne.nonempty.some.strictMono⟩
+  { hom' := IsRankLeOne.nonempty.some.emb (R := K).comp MonoidWithZeroHom.ValueGroup₀.embedding
+    strictMono' := IsRankLeOne.nonempty.some.strictMono.comp
+        MonoidWithZeroHom.ValueGroup₀.embedding_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⟩
+  { hom' := IsRankLeOne.nonempty.some.emb (R := K).comp MonoidWithZeroHom.ValueGroup₀.embedding
+    strictMono' := IsRankLeOne.nonempty.some.strictMono.comp
+        MonoidWithZeroHom.ValueGroup₀.embedding_strictMono }
   (compactSpace_iff_completeSpace_and_isDiscreteValuationRing_and_finite_residueField.mp
     (inferInstanceAs (CompactSpace 𝒪[K]))).1
 
 
@@ -15,6 +15,7 @@ public import Mathlib.RingTheory.Ideal.Norm.AbsNorm
 public import Mathlib.RingTheory.Valuation.Archimedean
 public import Mathlib.Topology.Algebra.Valued.NormedValued
 public import Mathlib.LinearAlgebra.FreeModule.IdealQuotient
+public import Mathlib.RingTheory.Valuation.Discrete.RankOne
 
 import Mathlib.Algebra.FiniteSupport.Basic
 
@@ -58,15 +59,8 @@ instance : IsPrincipalIdealRing (v.valuation K).integer := by
     WithZero.denselyOrdered_set_iff_subsingleton]
   simpa using (v.valuation K).toMonoidWithZeroHom.range_nontrivial
 
--- TODO: make this inferred from `IsRankOneDiscrete`
-instance : IsDiscreteValuationRing (v.valuation K).integer where
-  not_a_field' := by
-    simp only [ne_eq, Ideal.ext_iff, IsLocalRing.mem_maximalIdeal, mem_nonunits_iff,
-      Valuation.Integer.not_isUnit_iff_valuation_lt_one, Ideal.mem_bot, Subtype.forall, not_forall]
-    obtain ⟨π, hπ⟩ := v.valuation_exists_uniformizer K
-    use π
-    simp [Valuation.mem_integer_iff, ← exp_zero, Subtype.ext_iff, -exp_neg,
-      ← (v.valuation K).map_eq_zero_iff, hπ]
+instance : IsDiscreteValuationRing (v.valuation K).integer :=
+  (v.valuation K).valuationSubring_isDiscreteValuationRing
 
 instance : IsPrincipalIdealRing (v.adicCompletionIntegers K) := by
   unfold HeightOneSpectrum.adicCompletionIntegers
@@ -137,24 +131,24 @@ noncomputable def FinitePlace.embedding : K →+* adicCompletion K v :=
 
 theorem FinitePlace.embedding_apply (x : K) : embedding v x = ↑x := rfl
 
-noncomputable instance : (v.valuation K).RankOne where
-  hom := toNNReal (absNorm_ne_zero v)
-  strictMono' := toNNReal_strictMono (one_lt_absNorm_nnreal v)
-  exists_val_nontrivial := by
-    rcases Submodule.exists_mem_ne_zero_of_ne_bot v.ne_bot with ⟨x, hx1, hx2⟩
-    use x
-    rw [valuation_of_algebraMap]
-    exact ⟨v.intValuation_ne_zero _ hx2, ((intValuation_lt_one_iff_mem _ _).2 hx1).ne⟩
-
-noncomputable instance instRankOneValuedAdicCompletion :
-    Valuation.RankOne (Valued.v : Valuation (v.adicCompletion K) ℤᵐ⁰) where
-  hom := toNNReal (absNorm_ne_zero v)
-  strictMono' := toNNReal_strictMono (one_lt_absNorm_nnreal v)
-  exists_val_nontrivial := by
-    rcases Submodule.exists_mem_ne_zero_of_ne_bot v.ne_bot with ⟨x, hx1, hx2⟩
-    use x
-    rw [valuedAdicCompletion_eq_valuation' v (x : K)]
-    simpa [valuation_of_algebraMap] using ⟨v.intValuation_ne_zero _ hx2, hx1⟩
+noncomputable instance : ((Valued.v : Valuation (v.adicCompletion K) ℤᵐ⁰)).IsRankOneDiscrete where
+  exists_generator_lt_one' := by
+    have h : (v.valuation K).IsRankOneDiscrete := Valuation.IsRankOneDiscrete.mk' (valuation K v)
+    exact ⟨h.generator, by rw [h.generator_zpowers_eq_valueGroup, adicCompletion_valueGroup_eq],
+      h.generator_lt_one⟩
+
+open Valuation.IsRankOneDiscrete
+
+noncomputable instance : (v.valuation K).RankOne :=
+  rankOne (v.valuation K) (one_lt_absNorm_nnreal v)
+
+noncomputable instance instRankOneAdicCompletion :
+    (Valued.v : Valuation (v.adicCompletion K) ℤᵐ⁰).RankOne :=
+  rankOne (Valued.v : Valuation (v.adicCompletion K) ℤᵐ⁰) (one_lt_absNorm_nnreal v)
+
+lemma rankOne_hom'_def :
+    (instRankOneAdicCompletion v).hom' = (toNNReal (absNorm_ne_zero v)).comp
+      (valueGroup₀_equiv_withZeroMulInt Valued.v).toMonoidWithZeroHom := rfl
 
 /-- The `v`-adic completion of `K` is a normed field. -/
 noncomputable instance instNormedFieldValuedAdicCompletion : NormedField (adicCompletion K v) :=
@@ -185,10 +179,12 @@ lemma isFinitePlace_iff (v : AbsoluteValue K ℝ) :
 
 /-- The norm of the image after the embedding associated to `v` is equal to the `v`-adic absolute
 value. -/
-theorem FinitePlace.norm_def (x : K) :
-    ‖embedding v x‖ = adicAbv v x := by
-  simp +instances [NormedField.toNorm, instNormedFieldValuedAdicCompletion, Valued.toNormedField,
-    Valued.norm, Valuation.RankOne.hom, embedding_apply, adicAbv_def]
+theorem FinitePlace.norm_def (x : K) : ‖embedding v x‖ = adicAbv v x := by
+  simp +instances [NormedField.toNorm, instNormedFieldValuedAdicCompletion,
+    Valued.toNormedField, Valued.norm, Valuation.RankOne.hom,
+    embedding_apply, adicAbv_def, rankOne_hom'_def,
+    valueGroup₀_equiv_withZeroMulInt_restrict_apply_of_surjective
+      (valuedAdicCompletion_surjective K v)]
 
 /-- The norm of the image after the embedding associated to `v` is equal to the norm of `v` raised
 to the power of the `v`-adic valuation. -/
 
@@ -102,12 +102,14 @@ theorem valuation_p (p : ℕ) [Fact p.Prime] : Valued.v (p : PadicAlgCl p) = 1 /
   rw [valuation_coe, norm_extends, Padic.norm_p, one_div, NNReal.coe_inv,
     NNReal.coe_natCast]
 
+open MonoidWithZeroHom.ValueGroup₀
+
 set_option backward.isDefEq.respectTransparency false in
 set_option linter.style.whitespace false in -- manual alignment is not recognised
 /-- The valuation on `PadicAlgCl p` has rank one. -/
 instance : RankOne (PadicAlgCl.valued p).v where
-  hom         := MonoidWithZeroHom.id ℝ≥0
-  strictMono' := strictMono_id
+  hom'        := embedding
+  strictMono' := embedding_strictMono
   exists_val_nontrivial := by
     use p
     have hp : Nat.Prime p := hp.1
@@ -148,7 +150,7 @@ instance valued : Valued ℂ_[p] ℝ≥0 := Valued.valuedCompletion
 set_option backward.isDefEq.respectTransparency false in
 /-- The valuation on `ℂ_[p]` extends the valuation on `PadicAlgCl p`. -/
 theorem valuation_extends (x : PadicAlgCl p) : Valued.v (x : ℂ_[p]) = Valued.v x :=
-  Valued.extension_extends _
+  Valued.extensionValuation_apply_coe _
 
 set_option backward.isDefEq.respectTransparency false in
 theorem coe_eq (x : PadicAlgCl p) : (x : ℂ_[p]) = algebraMap (PadicAlgCl p) ℂ_[p] x := rfl
@@ -169,21 +171,23 @@ theorem valuation_p : Valued.v (p : ℂ_[p]) = 1 / (p : ℝ≥0) := by
   rw [← map_natCast (algebraMap (PadicAlgCl p) ℂ_[p]), ← coe_eq, valuation_extends,
     PadicAlgCl.valuation_p]
 
+open MonoidWithZeroHom.ValueGroup₀
+
 set_option backward.isDefEq.respectTransparency false in
 set_option linter.style.whitespace false in -- manual alignment is not recognised
 /-- The valuation on `ℂ_[p]` has rank one. -/
 instance : RankOne (PadicComplex.valued p).v where
-  hom         := MonoidWithZeroHom.id ℝ≥0
-  strictMono' := strictMono_id
+  hom'        := embedding
+  strictMono' := embedding_strictMono
   exists_val_nontrivial := by
     use p
     have hp : Nat.Prime p := hp.1
     simp only [valuation_p, one_div, ne_eq, inv_eq_zero, Nat.cast_eq_zero, inv_eq_one,
       Nat.cast_eq_one]
     exact ⟨hp.ne_zero, hp.ne_one⟩
 
-lemma rankOne_hom_eq :
-    RankOne.hom (PadicComplex.valued p).v = RankOne.hom (PadicAlgCl.valued p).v := rfl
+@[simp]
+theorem RankOne.hom_eq_embedding : RankOne.hom (PadicComplex.valued p).v = embedding := rfl
 
 /-- `ℂ_[p]` is a normed field, where the norm extends from `PadicAlgCl` along completion. -/
 instance normedField : NormedField ℂ_[p] := inferInstance
@@ -215,7 +219,8 @@ theorem norm_eq_norm' : (‖·‖ : ℂ_[p] → ℝ) = Valued.norm := by
     letI := S.toNonUnitalSeminormedRing.toSeminormedAddCommGroup.toSeminormedAddGroup
     exact @uniformContinuous_norm ℂ_[p] this
   · intro x
-    simp only [Valued.norm_def, valuation_extends]
+    simp only [Valued.norm_def, RankOne.hom_eq_embedding]
+    erw [embedding_restrict (PadicComplex.valued p).v x, valuation_extends]
     exact (PadicAlgCl.valuation_coe p x).symm
 
 /-- The norm on `ℂ_[p]` is compatible with the valuation. -/
 
@@ -141,8 +141,6 @@ open Valuation
 noncomputable def withValEquiv (v : HeightOneSpectrum R) :
     WithVal (v.valuation ℚ) ≃ᵤ WithVal (padicValuation (primesEquiv v)) :=
   (valuation_equiv_padicValuation v).uniformEquiv
-    (exists_div_eq_of_surjective (v.valuation_surjective ℚ))
-    (exists_div_eq_of_surjective (surjective_padicValuation (primesEquiv v)))
 
 /-- The continuous `ℚ`-algebra isomorphism between `v.adicCompletion ℚ` and `ℚ_[primesEquiv v]`. -/
 noncomputable def adicCompletion.padicEquiv (v : HeightOneSpectrum R) :
@@ -159,11 +157,9 @@ noncomputable def adicCompletionIntegers.padicIntEquiv (v : HeightOneSpectrum R)
   __ := let e := (mapRingEquiv _ (withValEquiv v).continuous
           (withValEquiv v).symm.continuous).restrict _ _ fun _ ↦ by
             simpa using (valuation_equiv_padicValuation v).valuedCompletion_le_one_iff
-              (v.valuation_surjective ℚ) (surjective_padicValuation _)
         e.trans withValIntegersRingEquiv
   __ := let e := (mapEquiv (withValEquiv v)).subtype fun _ ↦ by
           simpa using (valuation_equiv_padicValuation v).valuedCompletion_le_one_iff
-            (v.valuation_surjective ℚ) (surjective_padicValuation _)
         (e.trans withValIntegersUniformEquiv).toHomeomorph
   commutes' := by simp