|
| 1 | +/- |
| 2 | +Copyright (c) 2025 María Inés de Frutos-Fernández, Filippo A. E. Nuccio. All rights reserved. |
| 3 | +Released under Apache 2.0 license as described in the file LICENSE. |
| 4 | +Authors: María Inés de Frutos-Fernández, Filippo A. E. Nuccio |
| 5 | +-/ |
| 6 | +import Mathlib.Algebra.Order.Group.Cyclic |
| 7 | +import Mathlib.Algebra.Order.Group.Units |
| 8 | +import Mathlib.RingTheory.Valuation.Basic |
| 9 | + |
| 10 | +/-! |
| 11 | +# Discrete Valuations |
| 12 | +
|
| 13 | +Given a linearly ordered commutative group with zero `Γ` such that `Γˣ` is nontrivial cyclic, a |
| 14 | +valuation `v : A → Γ` on a ring `A` is *discrete*, if `genLTOne Γˣ` belongs to the image, where |
| 15 | +`genLTOne Γˣ` is the generator of `Γˣ` that is `< 1`. When `Γ := ℤₘ₀` (defined in |
| 16 | +`Multiplicative.termℤₘ₀`), `genLTOne Γˣ = ofAdd (-1)` and the condition of being discrete is |
| 17 | +equivalent to asking that `ofAdd (-1 : ℤ)` belongs to the image, in turn equivalent to asking that |
| 18 | +`1 : ℤ` belongs to the image of the corresponding *additive* valuation. |
| 19 | +
|
| 20 | +
|
| 21 | +## Main Definitions |
| 22 | +* `IsDiscrete`: We define a `Γ`-valued valuation `v` to be discrete if `Γˣ` is cyclic and |
| 23 | + `genLTOne Γˣ` belongs to the image of `v`. |
| 24 | +
|
| 25 | +## TODO |
| 26 | +* Define (pre)uniformizers for nontrivial discrete valuations. |
| 27 | +* Relate discrete valuations and discrete valuation rings. |
| 28 | +-/ |
| 29 | + |
| 30 | +namespace Valuation |
| 31 | + |
| 32 | +open Function Set LinearOrderedCommGroup |
| 33 | + |
| 34 | +variable {Γ : Type*} [LinearOrderedCommGroupWithZero Γ] |
| 35 | + |
| 36 | +variable {A : Type*} [Ring A] (v : Valuation A Γ) |
| 37 | + |
| 38 | +/-- Given a linearly ordered commutative group with zero `Γ` such that `Γˣ` is |
| 39 | +nontrivial cyclic, a valuation `v : A → Γ` on a ring `A` is *discrete*, if |
| 40 | +`genLTOne Γˣ` belongs to the image. Note that the latter is equivalent to |
| 41 | +asking that `1 : ℤ` belongs to the image of the corresponding additive valuation. -/ |
| 42 | +class IsDiscrete : Prop where |
| 43 | + exists_generator_lt_one' : ∃ (γ : Γˣ), Subgroup.zpowers γ = ⊤ ∧ γ < 1 ∧ ↑γ ∈ range v |
| 44 | + |
| 45 | +lemma exists_generator_lt_one [IsDiscrete v] : |
| 46 | + ∃ (γ : Γˣ), Subgroup.zpowers γ = ⊤ ∧ γ < 1 ∧ ↑γ ∈ range v := IsDiscrete.exists_generator_lt_one' |
| 47 | + |
| 48 | +/-- Given a discrete valuation `v`, `Valuation.IsDiscrete.generator` is a generator of the value |
| 49 | +group that is `< 1`. -/ |
| 50 | +noncomputable def generator [IsDiscrete v] : Γˣ := v.exists_generator_lt_one.choose |
| 51 | + |
| 52 | +lemma generator_zpowers_eq_top [IsDiscrete v] : |
| 53 | + Subgroup.zpowers (generator v) = (⊤ : Subgroup Γˣ) := v.exists_generator_lt_one.choose_spec.1 |
| 54 | + |
| 55 | +lemma generator_lt_one [IsDiscrete v] : (generator v) < 1 := |
| 56 | + v.exists_generator_lt_one.choose_spec.2.1 |
| 57 | + |
| 58 | +lemma generator_mem_range [IsDiscrete v] : ↑(generator v) ∈ range v := |
| 59 | + v.exists_generator_lt_one.choose_spec.2.2 |
| 60 | + |
| 61 | +lemma IsDiscrete.cyclic_value_group [IsDiscrete v] : IsCyclic Γˣ := by |
| 62 | + rw [isCyclic_iff_exists_zpowers_eq_top] |
| 63 | + exact ⟨_, generator_zpowers_eq_top v⟩ |
| 64 | + |
| 65 | + |
| 66 | +lemma IsDiscrete.nontrivial_value_group [IsDiscrete v] : Nontrivial Γˣ := |
| 67 | + ⟨1, generator v, ne_of_gt <| generator_lt_one v⟩ |
| 68 | + |
| 69 | +variable {K : Type*} [Field K] |
| 70 | + |
| 71 | +/-- A discrete valuation on a field `K` is surjective. -/ |
| 72 | +lemma IsDiscrete.surj (w : Valuation K Γ) [IsDiscrete w] : Surjective w := by |
| 73 | + intro c |
| 74 | + by_cases hc : c = 0 |
| 75 | + · exact ⟨0, by simp [hc]⟩ |
| 76 | + obtain ⟨π, hπ_gen, hπ_lt_one, a, ha⟩ := w.exists_generator_lt_one |
| 77 | + set u : Γˣ := Units.mk0 c hc with hu |
| 78 | + obtain ⟨k, hk⟩ := Subgroup.mem_zpowers_iff.mp (hπ_gen ▸ Subgroup.mem_top u) |
| 79 | + use a^k |
| 80 | + rw [map_zpow₀, ha] |
| 81 | + norm_cast |
| 82 | + rw [hk, hu, Units.val_mk0] |
| 83 | + |
| 84 | +/-- A valuation on a field `K` is discrete if and only if it is surjective. -/ |
| 85 | +lemma isDiscrete_iff_surjective (w : Valuation K Γ) [IsCyclic Γˣ] [Nontrivial Γˣ] : |
| 86 | + IsDiscrete w ↔ Surjective w := by |
| 87 | + refine ⟨fun _ ↦ IsDiscrete.surj w, fun h ↦ ⟨LinearOrderedCommGroup.genLTOne Γˣ, |
| 88 | + by simp, ?_, by apply h⟩⟩ |
| 89 | + simpa using (⊤ : Subgroup Γˣ).genLTOne_lt_one |
| 90 | + |
| 91 | +instance [hv : IsDiscrete v] : IsNontrivial v where |
| 92 | + exists_val_nontrivial := by |
| 93 | + obtain ⟨γ, _, _, x, hx_v⟩ := hv |
| 94 | + exact ⟨x, hx_v ▸ ⟨Units.ne_zero γ, ne_of_lt (by norm_cast)⟩⟩ |
| 95 | + |
| 96 | +end Valuation |
0 commit comments