From f3ff68d6d7985ebd78ef406cae97c3acbc7addfc Mon Sep 17 00:00:00 2001 From: Fabrizio Barroero Date: Sun, 1 Dec 2024 20:32:47 +0100 Subject: [PATCH 01/32] feat(NumberTheory/NumberField/FinitePlaces): the finite places of a number field --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) --- Mathlib.lean | 1 + .../NumberField/FinitePlaces.lean | 244 ++++++++++++++++++ 2 files changed, 245 insertions(+) create mode 100644 Mathlib/NumberTheory/NumberField/FinitePlaces.lean diff --git a/Mathlib.lean b/Mathlib.lean index 99e0381f97d9a..89daf47588dbe 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -3871,6 +3871,7 @@ import Mathlib.NumberTheory.NumberField.Discriminant.Basic import Mathlib.NumberTheory.NumberField.Discriminant.Defs import Mathlib.NumberTheory.NumberField.Embeddings import Mathlib.NumberTheory.NumberField.EquivReindex +import Mathlib.NumberTheory.NumberField.FinitePlaces import Mathlib.NumberTheory.NumberField.FractionalIdeal import Mathlib.NumberTheory.NumberField.House import Mathlib.NumberTheory.NumberField.Norm diff --git a/Mathlib/NumberTheory/NumberField/FinitePlaces.lean b/Mathlib/NumberTheory/NumberField/FinitePlaces.lean new file mode 100644 index 0000000000000..910787fe41bfe --- /dev/null +++ b/Mathlib/NumberTheory/NumberField/FinitePlaces.lean @@ -0,0 +1,244 @@ +/- +Copyright (c) 2024 Fabrizio Barroero. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Author: Fabrizio Barroero +-/ +import Mathlib.Data.Int.WithZero +import Mathlib.NumberTheory.NumberField.Embeddings +import Mathlib.RingTheory.DedekindDomain.AdicValuation +import Mathlib.RingTheory.DedekindDomain.Factorization +import Mathlib.RingTheory.Ideal.Norm.absNorm +import Mathlib.Topology.Algebra.Valued.NormedValued + +/-! +# Finite places of number fields +This file defines finite places of a number field `K` as absolute values coming from an embedding +into a completion of `K` associated to a non-zero prime ideal of `𝓞 K`. + +## Main Definitions and Results +* `NumberField.vadic_abv`: a `v`-adic absolute value on `K`. +* `NumberField.FinitePlace`: the type of finite places of a number field `K`. +* `NumberField.FinitePlace.mulSupport_Finite`: the `v`-adic absolute value of a non-zero element of +`K` is different from 1 for at most finitely many `v`. + +## Tags +number field, places, finite places +-/ + +open Ideal IsDedekindDomain HeightOneSpectrum NumberField WithZeroMulInt + +namespace NumberField + +section absoluteValue + +variable {K : Type*} [Field K] [NumberField K] (v : HeightOneSpectrum (𝓞 K)) + +/-- The norm of a maximal ideal as an element of `ℝ≥0` is `> 1` -/ +lemma one_lt_norm : 1 < (absNorm v.asIdeal : NNReal) := by + norm_cast + by_contra! h + apply IsPrime.ne_top v.isPrime + rw [← absNorm_eq_one_iff] + have : 0 < absNorm v.asIdeal := by + rw [Nat.pos_iff_ne_zero, absNorm_ne_zero_iff] + set k := 𝓞 K ⧸ v.asIdeal + have : Field k := Ideal.Quotient.field v.asIdeal + have : Fintype k := Ideal.fintypeQuotientOfFreeOfNeBot v.asIdeal v.ne_bot + exact Fintype.finite this + omega + +private lemma norm_ne_zero : (absNorm v.asIdeal : NNReal) ≠ 0 := ne_zero_of_lt (one_lt_norm v) + +/-- The `v`-adic absolute value on `K` defined as the norm of `v` raised to negative `v`-adic +valuation.-/ +noncomputable def vadic_abv : AbsoluteValue K ℝ where + toFun := fun x ↦ toNNReal (norm_ne_zero v) (v.valuation x) + map_mul' := fun _ _ ↦ by simp only [_root_.map_mul, NNReal.coe_mul] + nonneg' := fun _ ↦ NNReal.zero_le_coe + eq_zero' := fun _ ↦ by simp only [NNReal.coe_eq_zero, map_eq_zero] + add_le' := by + intro x y + simp only + norm_cast + -- the triangular inequality is implied by the ultrametric one + apply le_trans _ <| max_le_add_of_nonneg (zero_le ((toNNReal (norm_ne_zero v)) (v.valuation x))) + (zero_le ((toNNReal (norm_ne_zero v)) (v.valuation y))) + have h_mono := StrictMono.monotone (toNNReal_strictMono (one_lt_norm v)) + rw [← Monotone.map_max h_mono] --max goes inside withZeroMultIntToNNReal + exact h_mono (Valuation.map_add v.valuation x y) + +theorem vadic_abv_def {x : K} : vadic_abv v x = toNNReal (norm_ne_zero v) (v.valuation x) := rfl + +end absoluteValue + +section FinitePlace +variable {K : Type*} [Field K] [NumberField K] (v : HeightOneSpectrum (𝓞 K)) + +/-- The embedding of a NumberField inside its completion with respect to `v`. -/ +def embedding : K →+* adicCompletion K v := + @UniformSpace.Completion.coeRingHom K _ v.adicValued.toUniformSpace _ _ + +noncomputable instance instRankOneValuedAdicCompletion : + Valuation.RankOne (valuedAdicCompletion K v).v where + hom := { + toFun := toNNReal (norm_ne_zero v) + map_zero' := rfl + map_one' := rfl + map_mul' := MonoidWithZeroHom.map_mul (toNNReal (norm_ne_zero v)) + } + strictMono' := toNNReal_strictMono (one_lt_norm v) + nontrivial' := by + rcases Submodule.exists_mem_ne_zero_of_ne_bot v.ne_bot with ⟨x, hx1, hx2⟩ + use (x : K) + rw [valuedAdicCompletion_eq_valuation' v (x : K)] + constructor + · simpa only [ne_eq, map_eq_zero, NoZeroSMulDivisors.algebraMap_eq_zero_iff] + · apply ne_of_lt + rw [valuation_eq_intValuationDef, intValuation_lt_one_iff_dvd] + exact dvd_span_singleton.mpr hx1 + +/-- The `v`-adic completion of `K` is a normed field. -/ +noncomputable instance instNormedFieldValuedAdicCompletion : NormedField (adicCompletion K v) := + Valued.toNormedField (adicCompletion K v) (WithZero (Multiplicative ℤ)) + +/-- A finite place of a number field `K` is a place associated to an embedding into a completion +with respect to a maximal ideal. -/ +def FinitePlace (K : Type*) [Field K] [NumberField K] := {w : AbsoluteValue K ℝ // + ∃ v : IsDedekindDomain.HeightOneSpectrum (𝓞 K), place (embedding v) = w} + +/-- Return the finite place defined by a maximal ideal `v`. -/ +noncomputable def FinitePlace.mk (v : HeightOneSpectrum (𝓞 K)) : FinitePlace K := + ⟨place (embedding v), ⟨v, rfl⟩⟩ + +/-- 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‖ = vadic_abv v x := by + simp only [NormedField.toNorm, instNormedFieldValuedAdicCompletion, Valued.toNormedField, + instFieldAdicCompletion, Valued.norm, Valuation.RankOne.hom, MonoidWithZeroHom.coe_mk, + ZeroHom.coe_mk, embedding, UniformSpace.Completion.coeRingHom, RingHom.coe_mk, + MonoidHom.coe_mk, OneHom.coe_mk, Valued.valuedCompletion_apply, NNReal.coe_inj] + rfl + +open FinitePlace + +/-- The `v`-adic norm of an integer is at most 1. -/ +theorem norm_le_one (x : 𝓞 K) : ‖embedding v x‖ ≤ 1 := by + rw [norm_def, vadic_abv_def, NNReal.coe_le_one, toNNReal_le_one_iff (one_lt_norm v)] + exact valuation_le_one v x + +/-- The `v`-adic norm of an integer is 1 if and only if it is not in the ideal. -/ +theorem norm_eq_one_iff_not_mem (x : 𝓞 K) : ‖(embedding v) x‖ = 1 ↔ x ∉ v.asIdeal := by + rw [norm_def, vadic_abv_def, NNReal.coe_eq_one, toNNReal_eq_one_iff (v.valuation (x : K)) + (norm_ne_zero v) (Ne.symm (ne_of_lt (one_lt_norm v))), valuation_eq_intValuationDef, + ← dvd_span_singleton, ← intValuation_lt_one_iff_dvd, not_lt] + exact Iff.symm (LE.le.ge_iff_eq (intValuation_le_one v x)) + +/-- The `v`-adic norm of an integer is less than 1 if and only if it is in the ideal. -/ +theorem norm_lt_one_iff_mem (x : 𝓞 K) : ‖embedding v x‖ < 1 ↔ x ∈ v.asIdeal := by + rw [norm_def, vadic_abv_def, NNReal.coe_lt_one, toNNReal_lt_one_iff (one_lt_norm v), + valuation_eq_intValuationDef, intValuation_lt_one_iff_dvd] + exact dvd_span_singleton + +end FinitePlace + +namespace FinitePlace +variable {K : Type*} [Field K] [NumberField K] + +instance : FunLike (FinitePlace K) K ℝ where + coe w x := w.1 x + coe_injective' _ _ h := Subtype.eq (AbsoluteValue.ext fun x => congr_fun h x) + +instance : MonoidWithZeroHomClass (FinitePlace K) K ℝ where + map_mul w _ _ := w.1.map_mul _ _ + map_one w := w.1.map_one + map_zero w := w.1.map_zero + +instance : NonnegHomClass (FinitePlace K) K ℝ where + apply_nonneg w _ := w.1.nonneg _ + +@[simp] +theorem apply (v : HeightOneSpectrum (𝓞 K)) (x : K) : mk v x = ‖embedding v x‖ := rfl + +/-- For a finite place `w`, return a maximal ideal `v` such that `w = finite_place v` . -/ +noncomputable def maximal_ideal (w : FinitePlace K) : HeightOneSpectrum (𝓞 K) := w.2.choose + +@[simp] +theorem mk_max_ideal (w : FinitePlace K) : mk (maximal_ideal w) = w := Subtype.ext w.2.choose_spec + +@[simp] +theorem norm_embedding_eq (w : FinitePlace K) (x : K) : + ‖embedding (maximal_ideal w) x‖ = w x := by + have h : w x = (mk (maximal_ideal w)) x := by simp only [mk_max_ideal] + rw [h] + rfl + +theorem eq_iff_eq (x : K) (r : ℝ) : (∀ w : FinitePlace K, w x = r) ↔ + ∀ v : HeightOneSpectrum (𝓞 K), ‖embedding v x‖ = r := Set.forall_subtype_range_iff + +theorem le_iff_le (x : K) (r : ℝ) : (∀ w : FinitePlace K, w x ≤ r) ↔ + ∀ v : HeightOneSpectrum (𝓞 K), ‖embedding v x‖ ≤ r := Set.forall_subtype_range_iff + +theorem pos_iff {w : FinitePlace K} {x : K} : 0 < w x ↔ x ≠ 0 := AbsoluteValue.pos_iff w.1 + +@[simp] +theorem mk_eq_iff {v₁ v₂ : HeightOneSpectrum (𝓞 K)} : mk v₁ = mk v₂ ↔ v₁ = v₂ := by + refine ⟨?_, fun a ↦ by rw [a]⟩ + contrapose! + intro h + rw [DFunLike.ne_iff] + have : ∃ x : 𝓞 K, x ∈ v₁.asIdeal ∧ x ∉ v₂.asIdeal := by + by_contra! + apply h + exact HeightOneSpectrum.ext_iff.mpr (IsMaximal.eq_of_le (isMaximal v₁) IsPrime.ne_top' this) + rcases this with ⟨x, hx1, hx2⟩ + use x + simp only [apply] + rw [← norm_lt_one_iff_mem ] at hx1 + rw [← norm_eq_one_iff_not_mem] at hx2 + linarith + +theorem max_ideal_mk (v : HeightOneSpectrum (𝓞 K)) : maximal_ideal (mk v) = v := by + rw [← mk_eq_iff, mk_max_ideal] + +theorem mulSupport_Finite_int {x : 𝓞 K} (h_x_nezero : x ≠ 0) : + (Function.mulSupport fun w : FinitePlace K => w x).Finite := by + have (w : FinitePlace K) : w x ≠ 1 ↔ w x < 1 := by + have := norm_le_one w.maximal_ideal x + rw [norm_embedding_eq] at this + exact Decidable.ne_iff_lt_iff_le.mpr this + simp_rw [Function.mulSupport, this, ← norm_embedding_eq, norm_lt_one_iff_mem, + ← Ideal.dvd_span_singleton] + have h : {v : HeightOneSpectrum (𝓞 K) | v.asIdeal ∣ span {x}}.Finite := by + apply Ideal.finite_factors + simp only [Submodule.zero_eq_bot, ne_eq, span_singleton_eq_bot, h_x_nezero, not_false_eq_true] + have h_inj : Set.InjOn (fun w : FinitePlace K ↦ maximal_ideal w) + {x_1 | x_1.maximal_ideal.asIdeal ∣ span {x}} := by + apply Function.Injective.injOn + intro w₁ w₂ h + rw [← mk_max_ideal w₁, ← mk_max_ideal w₂] + exact congrArg mk h + apply Set.Finite.of_finite_image _ h_inj + have h_subs : ((fun w : FinitePlace K ↦ w.maximal_ideal) '' + {x_1 : FinitePlace K | x_1.maximal_ideal.asIdeal ∣ span {x}}) ⊆ + {v : HeightOneSpectrum (𝓞 K) | v.asIdeal ∣ span {x}} := by + simp only [dvd_span_singleton, Set.image_subset_iff, Set.preimage_setOf_eq, subset_refl] + exact Set.Finite.subset h h_subs + +theorem mulSupport_Finite {x : K} (h_x_nezero : x ≠ 0) : + (Function.mulSupport fun w : FinitePlace K => w x).Finite := by + rcases @IsFractionRing.div_surjective (𝓞 K) _ K _ _ _ x with ⟨a, b, hb, hfrac⟩ + subst hfrac + simp_all only [ne_eq, div_eq_zero_iff, NoZeroSMulDivisors.algebraMap_eq_zero_iff, not_or, + map_div₀] + obtain ⟨ha, hb⟩ := h_x_nezero + rw [← RingOfIntegers.coe_eq_algebraMap, ← RingOfIntegers.coe_eq_algebraMap] + apply Set.Finite.subset (Set.Finite.union (mulSupport_Finite_int ha) (mulSupport_Finite_int hb)) + intro w + contrapose! + intro a_1 + simp_all only [Set.mem_union, Function.mem_mulSupport, ne_eq, not_or, Decidable.not_not, + one_ne_zero, not_false_eq_true, div_self, not_true_eq_false] + +end FinitePlace + +end NumberField From bb54b6d4c1be4ddf4b213df2bcae750ca64315bc Mon Sep 17 00:00:00 2001 From: Fabrizio Barroero Date: Sun, 1 Dec 2024 20:40:21 +0100 Subject: [PATCH 02/32] Fix --- Mathlib/NumberTheory/NumberField/FinitePlaces.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Mathlib/NumberTheory/NumberField/FinitePlaces.lean b/Mathlib/NumberTheory/NumberField/FinitePlaces.lean index 910787fe41bfe..81299a47cc1c2 100644 --- a/Mathlib/NumberTheory/NumberField/FinitePlaces.lean +++ b/Mathlib/NumberTheory/NumberField/FinitePlaces.lean @@ -1,13 +1,13 @@ /- Copyright (c) 2024 Fabrizio Barroero. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Author: Fabrizio Barroero +Authors: Fabrizio Barroero -/ import Mathlib.Data.Int.WithZero import Mathlib.NumberTheory.NumberField.Embeddings import Mathlib.RingTheory.DedekindDomain.AdicValuation import Mathlib.RingTheory.DedekindDomain.Factorization -import Mathlib.RingTheory.Ideal.Norm.absNorm +import Mathlib.RingTheory.Ideal.Norm.AbsNorm import Mathlib.Topology.Algebra.Valued.NormedValued /-! From d549a0d93e39b090a1bff246a32749af185a0897 Mon Sep 17 00:00:00 2001 From: Fabrizio Barroero Date: Sun, 1 Dec 2024 20:53:01 +0100 Subject: [PATCH 03/32] fix2 --- Mathlib/NumberTheory/NumberField/FinitePlaces.lean | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/Mathlib/NumberTheory/NumberField/FinitePlaces.lean b/Mathlib/NumberTheory/NumberField/FinitePlaces.lean index 81299a47cc1c2..4be3b2f379742 100644 --- a/Mathlib/NumberTheory/NumberField/FinitePlaces.lean +++ b/Mathlib/NumberTheory/NumberField/FinitePlaces.lean @@ -41,9 +41,7 @@ lemma one_lt_norm : 1 < (absNorm v.asIdeal : NNReal) := by rw [← absNorm_eq_one_iff] have : 0 < absNorm v.asIdeal := by rw [Nat.pos_iff_ne_zero, absNorm_ne_zero_iff] - set k := 𝓞 K ⧸ v.asIdeal - have : Field k := Ideal.Quotient.field v.asIdeal - have : Fintype k := Ideal.fintypeQuotientOfFreeOfNeBot v.asIdeal v.ne_bot + have : Fintype (𝓞 K ⧸ v.asIdeal) := Ideal.fintypeQuotientOfFreeOfNeBot v.asIdeal v.ne_bot exact Fintype.finite this omega From 32ec1378b37903b45cbdee70ba7cbf428aa665b0 Mon Sep 17 00:00:00 2001 From: Fabrizio Barroero Date: Tue, 3 Dec 2024 22:23:08 +0100 Subject: [PATCH 04/32] Update Mathlib/NumberTheory/NumberField/FinitePlaces.lean Co-authored-by: Michael Stoll <99838730+MichaelStollBayreuth@users.noreply.github.com> --- Mathlib/NumberTheory/NumberField/FinitePlaces.lean | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/Mathlib/NumberTheory/NumberField/FinitePlaces.lean b/Mathlib/NumberTheory/NumberField/FinitePlaces.lean index 4be3b2f379742..6915cb73a8458 100644 --- a/Mathlib/NumberTheory/NumberField/FinitePlaces.lean +++ b/Mathlib/NumberTheory/NumberField/FinitePlaces.lean @@ -41,8 +41,7 @@ lemma one_lt_norm : 1 < (absNorm v.asIdeal : NNReal) := by rw [← absNorm_eq_one_iff] have : 0 < absNorm v.asIdeal := by rw [Nat.pos_iff_ne_zero, absNorm_ne_zero_iff] - have : Fintype (𝓞 K ⧸ v.asIdeal) := Ideal.fintypeQuotientOfFreeOfNeBot v.asIdeal v.ne_bot - exact Fintype.finite this + exact (v.asIdeal.fintypeQuotientOfFreeOfNeBot v.ne_bot).finite omega private lemma norm_ne_zero : (absNorm v.asIdeal : NNReal) ≠ 0 := ne_zero_of_lt (one_lt_norm v) From e577dd59e2c20d6c330eec1417ce1ceb79c08a13 Mon Sep 17 00:00:00 2001 From: Fabrizio Barroero Date: Tue, 3 Dec 2024 22:23:46 +0100 Subject: [PATCH 05/32] Update Mathlib/NumberTheory/NumberField/FinitePlaces.lean Co-authored-by: Michael Stoll <99838730+MichaelStollBayreuth@users.noreply.github.com> --- Mathlib/NumberTheory/NumberField/FinitePlaces.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/NumberTheory/NumberField/FinitePlaces.lean b/Mathlib/NumberTheory/NumberField/FinitePlaces.lean index 6915cb73a8458..da2815243ef25 100644 --- a/Mathlib/NumberTheory/NumberField/FinitePlaces.lean +++ b/Mathlib/NumberTheory/NumberField/FinitePlaces.lean @@ -57,7 +57,7 @@ noncomputable def vadic_abv : AbsoluteValue K ℝ where intro x y simp only norm_cast - -- the triangular inequality is implied by the ultrametric one + -- the triangle inequality is implied by the ultrametric one apply le_trans _ <| max_le_add_of_nonneg (zero_le ((toNNReal (norm_ne_zero v)) (v.valuation x))) (zero_le ((toNNReal (norm_ne_zero v)) (v.valuation y))) have h_mono := StrictMono.monotone (toNNReal_strictMono (one_lt_norm v)) From a06dbdc5d0a76b62eeb8ded3d9498934fa5cce2c Mon Sep 17 00:00:00 2001 From: Fabrizio Barroero Date: Tue, 3 Dec 2024 22:24:27 +0100 Subject: [PATCH 06/32] Update Mathlib/NumberTheory/NumberField/FinitePlaces.lean Co-authored-by: Michael Stoll <99838730+MichaelStollBayreuth@users.noreply.github.com> --- Mathlib/NumberTheory/NumberField/FinitePlaces.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/Mathlib/NumberTheory/NumberField/FinitePlaces.lean b/Mathlib/NumberTheory/NumberField/FinitePlaces.lean index da2815243ef25..38420bc3f949d 100644 --- a/Mathlib/NumberTheory/NumberField/FinitePlaces.lean +++ b/Mathlib/NumberTheory/NumberField/FinitePlaces.lean @@ -60,9 +60,9 @@ noncomputable def vadic_abv : AbsoluteValue K ℝ where -- the triangle inequality is implied by the ultrametric one apply le_trans _ <| max_le_add_of_nonneg (zero_le ((toNNReal (norm_ne_zero v)) (v.valuation x))) (zero_le ((toNNReal (norm_ne_zero v)) (v.valuation y))) - have h_mono := StrictMono.monotone (toNNReal_strictMono (one_lt_norm v)) - rw [← Monotone.map_max h_mono] --max goes inside withZeroMultIntToNNReal - exact h_mono (Valuation.map_add v.valuation x y) + have h_mono := (toNNReal_strictMono (one_lt_norm v)).monotone + rw [← h_mono.map_max] --max goes inside withZeroMultIntToNNReal + exact h_mono (v.valuation.map_add x y) theorem vadic_abv_def {x : K} : vadic_abv v x = toNNReal (norm_ne_zero v) (v.valuation x) := rfl From 7e00a638773db7ce6a7c670adc52d00c09a78afa Mon Sep 17 00:00:00 2001 From: Fabrizio Barroero Date: Tue, 3 Dec 2024 22:25:20 +0100 Subject: [PATCH 07/32] Update Mathlib/NumberTheory/NumberField/FinitePlaces.lean Co-authored-by: Michael Stoll <99838730+MichaelStollBayreuth@users.noreply.github.com> --- Mathlib/NumberTheory/NumberField/FinitePlaces.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/NumberTheory/NumberField/FinitePlaces.lean b/Mathlib/NumberTheory/NumberField/FinitePlaces.lean index 38420bc3f949d..b3889d8aeb480 100644 --- a/Mathlib/NumberTheory/NumberField/FinitePlaces.lean +++ b/Mathlib/NumberTheory/NumberField/FinitePlaces.lean @@ -71,7 +71,7 @@ end absoluteValue section FinitePlace variable {K : Type*} [Field K] [NumberField K] (v : HeightOneSpectrum (𝓞 K)) -/-- The embedding of a NumberField inside its completion with respect to `v`. -/ +/-- The embedding of a number field inside its completion with respect to `v`. -/ def embedding : K →+* adicCompletion K v := @UniformSpace.Completion.coeRingHom K _ v.adicValued.toUniformSpace _ _ From ded4a4ea7fab53b0d904437cc201f8dd76d218ff Mon Sep 17 00:00:00 2001 From: Fabrizio Barroero Date: Tue, 3 Dec 2024 22:25:39 +0100 Subject: [PATCH 08/32] Update Mathlib/NumberTheory/NumberField/FinitePlaces.lean Co-authored-by: Michael Stoll <99838730+MichaelStollBayreuth@users.noreply.github.com> --- Mathlib/NumberTheory/NumberField/FinitePlaces.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/NumberTheory/NumberField/FinitePlaces.lean b/Mathlib/NumberTheory/NumberField/FinitePlaces.lean index b3889d8aeb480..0b422784867e3 100644 --- a/Mathlib/NumberTheory/NumberField/FinitePlaces.lean +++ b/Mathlib/NumberTheory/NumberField/FinitePlaces.lean @@ -73,7 +73,7 @@ variable {K : Type*} [Field K] [NumberField K] (v : HeightOneSpectrum (𝓞 K)) /-- The embedding of a number field inside its completion with respect to `v`. -/ def embedding : K →+* adicCompletion K v := - @UniformSpace.Completion.coeRingHom K _ v.adicValued.toUniformSpace _ _ + @UniformSpace.Completion.coeRingHom K _ v.adicValued.toUniformSpace _ _ noncomputable instance instRankOneValuedAdicCompletion : Valuation.RankOne (valuedAdicCompletion K v).v where From 8acbcc6f7f8a26ce15636995a683263da38596d9 Mon Sep 17 00:00:00 2001 From: Fabrizio Barroero Date: Tue, 3 Dec 2024 22:26:03 +0100 Subject: [PATCH 09/32] Update Mathlib/NumberTheory/NumberField/FinitePlaces.lean Co-authored-by: Michael Stoll <99838730+MichaelStollBayreuth@users.noreply.github.com> --- Mathlib/NumberTheory/NumberField/FinitePlaces.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/NumberTheory/NumberField/FinitePlaces.lean b/Mathlib/NumberTheory/NumberField/FinitePlaces.lean index 0b422784867e3..39fd86f743263 100644 --- a/Mathlib/NumberTheory/NumberField/FinitePlaces.lean +++ b/Mathlib/NumberTheory/NumberField/FinitePlaces.lean @@ -96,7 +96,7 @@ noncomputable instance instRankOneValuedAdicCompletion : /-- The `v`-adic completion of `K` is a normed field. -/ noncomputable instance instNormedFieldValuedAdicCompletion : NormedField (adicCompletion K v) := - Valued.toNormedField (adicCompletion K v) (WithZero (Multiplicative ℤ)) + Valued.toNormedField (adicCompletion K v) (WithZero (Multiplicative ℤ)) /-- A finite place of a number field `K` is a place associated to an embedding into a completion with respect to a maximal ideal. -/ From 733dc84ca827e99e56613409806c6d88db5dc861 Mon Sep 17 00:00:00 2001 From: Fabrizio Barroero Date: Tue, 3 Dec 2024 22:26:31 +0100 Subject: [PATCH 10/32] Update Mathlib/NumberTheory/NumberField/FinitePlaces.lean Co-authored-by: Michael Stoll <99838730+MichaelStollBayreuth@users.noreply.github.com> --- Mathlib/NumberTheory/NumberField/FinitePlaces.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/NumberTheory/NumberField/FinitePlaces.lean b/Mathlib/NumberTheory/NumberField/FinitePlaces.lean index 39fd86f743263..03716c99ab50e 100644 --- a/Mathlib/NumberTheory/NumberField/FinitePlaces.lean +++ b/Mathlib/NumberTheory/NumberField/FinitePlaces.lean @@ -105,7 +105,7 @@ def FinitePlace (K : Type*) [Field K] [NumberField K] := {w : AbsoluteValue K /-- Return the finite place defined by a maximal ideal `v`. -/ noncomputable def FinitePlace.mk (v : HeightOneSpectrum (𝓞 K)) : FinitePlace K := - ⟨place (embedding v), ⟨v, rfl⟩⟩ + ⟨place (embedding v), ⟨v, rfl⟩⟩ /-- The norm of the image after the embedding associated to `v` is equal to the `v`-adic absolute value. -/ From 26ecee8cca734255799ca06e4995d4912197a22f Mon Sep 17 00:00:00 2001 From: Fabrizio Barroero Date: Tue, 3 Dec 2024 22:26:53 +0100 Subject: [PATCH 11/32] Update Mathlib/NumberTheory/NumberField/FinitePlaces.lean Co-authored-by: Michael Stoll <99838730+MichaelStollBayreuth@users.noreply.github.com> --- Mathlib/NumberTheory/NumberField/FinitePlaces.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/NumberTheory/NumberField/FinitePlaces.lean b/Mathlib/NumberTheory/NumberField/FinitePlaces.lean index 03716c99ab50e..cebca07f59096 100644 --- a/Mathlib/NumberTheory/NumberField/FinitePlaces.lean +++ b/Mathlib/NumberTheory/NumberField/FinitePlaces.lean @@ -126,7 +126,7 @@ theorem norm_le_one (x : 𝓞 K) : ‖embedding v x‖ ≤ 1 := by /-- The `v`-adic norm of an integer is 1 if and only if it is not in the ideal. -/ theorem norm_eq_one_iff_not_mem (x : 𝓞 K) : ‖(embedding v) x‖ = 1 ↔ x ∉ v.asIdeal := by rw [norm_def, vadic_abv_def, NNReal.coe_eq_one, toNNReal_eq_one_iff (v.valuation (x : K)) - (norm_ne_zero v) (Ne.symm (ne_of_lt (one_lt_norm v))), valuation_eq_intValuationDef, + (norm_ne_zero v) (one_lt_norm v).ne', valuation_eq_intValuationDef, ← dvd_span_singleton, ← intValuation_lt_one_iff_dvd, not_lt] exact Iff.symm (LE.le.ge_iff_eq (intValuation_le_one v x)) From fb8a89cd12db32893382ef667418ba7f5d6ddbe1 Mon Sep 17 00:00:00 2001 From: Fabrizio Barroero Date: Tue, 3 Dec 2024 22:28:15 +0100 Subject: [PATCH 12/32] Update Mathlib/NumberTheory/NumberField/FinitePlaces.lean Co-authored-by: Michael Stoll <99838730+MichaelStollBayreuth@users.noreply.github.com> --- Mathlib/NumberTheory/NumberField/FinitePlaces.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/NumberTheory/NumberField/FinitePlaces.lean b/Mathlib/NumberTheory/NumberField/FinitePlaces.lean index cebca07f59096..ec190cddfa224 100644 --- a/Mathlib/NumberTheory/NumberField/FinitePlaces.lean +++ b/Mathlib/NumberTheory/NumberField/FinitePlaces.lean @@ -128,7 +128,7 @@ theorem norm_eq_one_iff_not_mem (x : 𝓞 K) : ‖(embedding v) x‖ = 1 ↔ x rw [norm_def, vadic_abv_def, NNReal.coe_eq_one, toNNReal_eq_one_iff (v.valuation (x : K)) (norm_ne_zero v) (one_lt_norm v).ne', valuation_eq_intValuationDef, ← dvd_span_singleton, ← intValuation_lt_one_iff_dvd, not_lt] - exact Iff.symm (LE.le.ge_iff_eq (intValuation_le_one v x)) + exact (intValuation_le_one v x).ge_iff_eq.symm /-- The `v`-adic norm of an integer is less than 1 if and only if it is in the ideal. -/ theorem norm_lt_one_iff_mem (x : 𝓞 K) : ‖embedding v x‖ < 1 ↔ x ∈ v.asIdeal := by From e7d3c018e849e5ac426ab732c2792d5ec52ffbd9 Mon Sep 17 00:00:00 2001 From: Fabrizio Barroero Date: Tue, 3 Dec 2024 22:28:50 +0100 Subject: [PATCH 13/32] Update Mathlib/NumberTheory/NumberField/FinitePlaces.lean Co-authored-by: Michael Stoll <99838730+MichaelStollBayreuth@users.noreply.github.com> --- Mathlib/NumberTheory/NumberField/FinitePlaces.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/NumberTheory/NumberField/FinitePlaces.lean b/Mathlib/NumberTheory/NumberField/FinitePlaces.lean index ec190cddfa224..52ff847f83cc0 100644 --- a/Mathlib/NumberTheory/NumberField/FinitePlaces.lean +++ b/Mathlib/NumberTheory/NumberField/FinitePlaces.lean @@ -143,7 +143,7 @@ variable {K : Type*} [Field K] [NumberField K] instance : FunLike (FinitePlace K) K ℝ where coe w x := w.1 x - coe_injective' _ _ h := Subtype.eq (AbsoluteValue.ext fun x => congr_fun h x) + coe_injective' _ _ h := Subtype.eq (AbsoluteValue.ext <| congr_fun h) instance : MonoidWithZeroHomClass (FinitePlace K) K ℝ where map_mul w _ _ := w.1.map_mul _ _ From bea3cb850c94460c7784001f96825a0f2d3bb73c Mon Sep 17 00:00:00 2001 From: Fabrizio Barroero Date: Tue, 3 Dec 2024 22:29:16 +0100 Subject: [PATCH 14/32] Update Mathlib/NumberTheory/NumberField/FinitePlaces.lean Co-authored-by: Michael Stoll <99838730+MichaelStollBayreuth@users.noreply.github.com> --- Mathlib/NumberTheory/NumberField/FinitePlaces.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/NumberTheory/NumberField/FinitePlaces.lean b/Mathlib/NumberTheory/NumberField/FinitePlaces.lean index 52ff847f83cc0..ed4a302e2820c 100644 --- a/Mathlib/NumberTheory/NumberField/FinitePlaces.lean +++ b/Mathlib/NumberTheory/NumberField/FinitePlaces.lean @@ -146,7 +146,7 @@ instance : FunLike (FinitePlace K) K ℝ where coe_injective' _ _ h := Subtype.eq (AbsoluteValue.ext <| congr_fun h) instance : MonoidWithZeroHomClass (FinitePlace K) K ℝ where - map_mul w _ _ := w.1.map_mul _ _ + map_mul w := w.1.map_mul map_one w := w.1.map_one map_zero w := w.1.map_zero From 5b8d18a80eb48f5d1a37ee79a92872fe98896860 Mon Sep 17 00:00:00 2001 From: Fabrizio Barroero Date: Tue, 3 Dec 2024 22:29:26 +0100 Subject: [PATCH 15/32] Update Mathlib/NumberTheory/NumberField/FinitePlaces.lean Co-authored-by: Michael Stoll <99838730+MichaelStollBayreuth@users.noreply.github.com> --- Mathlib/NumberTheory/NumberField/FinitePlaces.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/NumberTheory/NumberField/FinitePlaces.lean b/Mathlib/NumberTheory/NumberField/FinitePlaces.lean index ed4a302e2820c..00607d5ddd2af 100644 --- a/Mathlib/NumberTheory/NumberField/FinitePlaces.lean +++ b/Mathlib/NumberTheory/NumberField/FinitePlaces.lean @@ -151,7 +151,7 @@ instance : MonoidWithZeroHomClass (FinitePlace K) K ℝ where map_zero w := w.1.map_zero instance : NonnegHomClass (FinitePlace K) K ℝ where - apply_nonneg w _ := w.1.nonneg _ + apply_nonneg w := w.1.nonneg @[simp] theorem apply (v : HeightOneSpectrum (𝓞 K)) (x : K) : mk v x = ‖embedding v x‖ := rfl From dd6469ef832132e54953cdcbcd4e4415333daffd Mon Sep 17 00:00:00 2001 From: Fabrizio Barroero Date: Tue, 3 Dec 2024 22:34:41 +0100 Subject: [PATCH 16/32] Update Mathlib/NumberTheory/NumberField/FinitePlaces.lean Co-authored-by: Michael Stoll <99838730+MichaelStollBayreuth@users.noreply.github.com> --- Mathlib/NumberTheory/NumberField/FinitePlaces.lean | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/Mathlib/NumberTheory/NumberField/FinitePlaces.lean b/Mathlib/NumberTheory/NumberField/FinitePlaces.lean index 00607d5ddd2af..3c8def4528c60 100644 --- a/Mathlib/NumberTheory/NumberField/FinitePlaces.lean +++ b/Mathlib/NumberTheory/NumberField/FinitePlaces.lean @@ -170,7 +170,8 @@ theorem norm_embedding_eq (w : FinitePlace K) (x : K) : rfl theorem eq_iff_eq (x : K) (r : ℝ) : (∀ w : FinitePlace K, w x = r) ↔ - ∀ v : HeightOneSpectrum (𝓞 K), ‖embedding v x‖ = r := Set.forall_subtype_range_iff + ∀ v : HeightOneSpectrum (𝓞 K), ‖embedding v x‖ = r := + Set.forall_subtype_range_iff theorem le_iff_le (x : K) (r : ℝ) : (∀ w : FinitePlace K, w x ≤ r) ↔ ∀ v : HeightOneSpectrum (𝓞 K), ‖embedding v x‖ ≤ r := Set.forall_subtype_range_iff From bbb64c7d0f911b40ae58b589af9e53014eef3785 Mon Sep 17 00:00:00 2001 From: Fabrizio Barroero Date: Tue, 3 Dec 2024 22:34:52 +0100 Subject: [PATCH 17/32] Update Mathlib/NumberTheory/NumberField/FinitePlaces.lean Co-authored-by: Michael Stoll <99838730+MichaelStollBayreuth@users.noreply.github.com> --- Mathlib/NumberTheory/NumberField/FinitePlaces.lean | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/Mathlib/NumberTheory/NumberField/FinitePlaces.lean b/Mathlib/NumberTheory/NumberField/FinitePlaces.lean index 3c8def4528c60..43672101d9e6a 100644 --- a/Mathlib/NumberTheory/NumberField/FinitePlaces.lean +++ b/Mathlib/NumberTheory/NumberField/FinitePlaces.lean @@ -174,7 +174,8 @@ theorem eq_iff_eq (x : K) (r : ℝ) : (∀ w : FinitePlace K, w x = r) ↔ Set.forall_subtype_range_iff theorem le_iff_le (x : K) (r : ℝ) : (∀ w : FinitePlace K, w x ≤ r) ↔ - ∀ v : HeightOneSpectrum (𝓞 K), ‖embedding v x‖ ≤ r := Set.forall_subtype_range_iff + ∀ v : HeightOneSpectrum (𝓞 K), ‖embedding v x‖ ≤ r := + Set.forall_subtype_range_iff theorem pos_iff {w : FinitePlace K} {x : K} : 0 < w x ↔ x ≠ 0 := AbsoluteValue.pos_iff w.1 From b04d7460ab088194c0fc2fbcf8a1a65119e707a9 Mon Sep 17 00:00:00 2001 From: Fabrizio Barroero Date: Tue, 3 Dec 2024 22:36:05 +0100 Subject: [PATCH 18/32] Update Mathlib/NumberTheory/NumberField/FinitePlaces.lean Co-authored-by: Michael Stoll <99838730+MichaelStollBayreuth@users.noreply.github.com> --- Mathlib/NumberTheory/NumberField/FinitePlaces.lean | 8 +++----- 1 file changed, 3 insertions(+), 5 deletions(-) diff --git a/Mathlib/NumberTheory/NumberField/FinitePlaces.lean b/Mathlib/NumberTheory/NumberField/FinitePlaces.lean index 43672101d9e6a..689823485838a 100644 --- a/Mathlib/NumberTheory/NumberField/FinitePlaces.lean +++ b/Mathlib/NumberTheory/NumberField/FinitePlaces.lean @@ -185,11 +185,9 @@ theorem mk_eq_iff {v₁ v₂ : HeightOneSpectrum (𝓞 K)} : mk v₁ = mk v₂ contrapose! intro h rw [DFunLike.ne_iff] - have : ∃ x : 𝓞 K, x ∈ v₁.asIdeal ∧ x ∉ v₂.asIdeal := by - by_contra! - apply h - exact HeightOneSpectrum.ext_iff.mpr (IsMaximal.eq_of_le (isMaximal v₁) IsPrime.ne_top' this) - rcases this with ⟨x, hx1, hx2⟩ + have ⟨x, hx1, hx2⟩ : ∃ x : 𝓞 K, x ∈ v₁.asIdeal ∧ x ∉ v₂.asIdeal := by + by_contra! H + exact h <| HeightOneSpectrum.ext_iff.mpr (IsMaximal.eq_of_le (isMaximal v₁) IsPrime.ne_top' H) use x simp only [apply] rw [← norm_lt_one_iff_mem ] at hx1 From 636edbf53b666b47d9c7c5ef93f740566ef074e8 Mon Sep 17 00:00:00 2001 From: Fabrizio Barroero Date: Tue, 3 Dec 2024 22:36:54 +0100 Subject: [PATCH 19/32] Update Mathlib/NumberTheory/NumberField/FinitePlaces.lean Co-authored-by: Michael Stoll <99838730+MichaelStollBayreuth@users.noreply.github.com> --- Mathlib/NumberTheory/NumberField/FinitePlaces.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/NumberTheory/NumberField/FinitePlaces.lean b/Mathlib/NumberTheory/NumberField/FinitePlaces.lean index 689823485838a..48aae4277a576 100644 --- a/Mathlib/NumberTheory/NumberField/FinitePlaces.lean +++ b/Mathlib/NumberTheory/NumberField/FinitePlaces.lean @@ -198,7 +198,7 @@ theorem max_ideal_mk (v : HeightOneSpectrum (𝓞 K)) : maximal_ideal (mk v) = v rw [← mk_eq_iff, mk_max_ideal] theorem mulSupport_Finite_int {x : 𝓞 K} (h_x_nezero : x ≠ 0) : - (Function.mulSupport fun w : FinitePlace K => w x).Finite := by + (Function.mulSupport fun w : FinitePlace K ↦ w x).Finite := by have (w : FinitePlace K) : w x ≠ 1 ↔ w x < 1 := by have := norm_le_one w.maximal_ideal x rw [norm_embedding_eq] at this From c655b3b9c18900bbc16ee980868f7c6b3d7ec9d4 Mon Sep 17 00:00:00 2001 From: Fabrizio Barroero Date: Tue, 3 Dec 2024 22:37:21 +0100 Subject: [PATCH 20/32] Update Mathlib/NumberTheory/NumberField/FinitePlaces.lean Co-authored-by: Michael Stoll <99838730+MichaelStollBayreuth@users.noreply.github.com> --- Mathlib/NumberTheory/NumberField/FinitePlaces.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/NumberTheory/NumberField/FinitePlaces.lean b/Mathlib/NumberTheory/NumberField/FinitePlaces.lean index 48aae4277a576..c8a002f7f9291 100644 --- a/Mathlib/NumberTheory/NumberField/FinitePlaces.lean +++ b/Mathlib/NumberTheory/NumberField/FinitePlaces.lean @@ -202,7 +202,7 @@ theorem mulSupport_Finite_int {x : 𝓞 K} (h_x_nezero : x ≠ 0) : have (w : FinitePlace K) : w x ≠ 1 ↔ w x < 1 := by have := norm_le_one w.maximal_ideal x rw [norm_embedding_eq] at this - exact Decidable.ne_iff_lt_iff_le.mpr this + exact ne_iff_lt_iff_le.mpr this simp_rw [Function.mulSupport, this, ← norm_embedding_eq, norm_lt_one_iff_mem, ← Ideal.dvd_span_singleton] have h : {v : HeightOneSpectrum (𝓞 K) | v.asIdeal ∣ span {x}}.Finite := by From 74c83857aadd69ed710374c84642c1462e5f73ed Mon Sep 17 00:00:00 2001 From: Fabrizio Barroero Date: Tue, 3 Dec 2024 22:37:59 +0100 Subject: [PATCH 21/32] Update Mathlib/NumberTheory/NumberField/FinitePlaces.lean Co-authored-by: Michael Stoll <99838730+MichaelStollBayreuth@users.noreply.github.com> --- Mathlib/NumberTheory/NumberField/FinitePlaces.lean | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/Mathlib/NumberTheory/NumberField/FinitePlaces.lean b/Mathlib/NumberTheory/NumberField/FinitePlaces.lean index c8a002f7f9291..e3861df21920f 100644 --- a/Mathlib/NumberTheory/NumberField/FinitePlaces.lean +++ b/Mathlib/NumberTheory/NumberField/FinitePlaces.lean @@ -208,8 +208,7 @@ theorem mulSupport_Finite_int {x : 𝓞 K} (h_x_nezero : x ≠ 0) : have h : {v : HeightOneSpectrum (𝓞 K) | v.asIdeal ∣ span {x}}.Finite := by apply Ideal.finite_factors simp only [Submodule.zero_eq_bot, ne_eq, span_singleton_eq_bot, h_x_nezero, not_false_eq_true] - have h_inj : Set.InjOn (fun w : FinitePlace K ↦ maximal_ideal w) - {x_1 | x_1.maximal_ideal.asIdeal ∣ span {x}} := by + have h_inj : Set.InjOn FinitePlace.maximal_ideal {w | w.maximal_ideal.asIdeal ∣ span {x}} := by apply Function.Injective.injOn intro w₁ w₂ h rw [← mk_max_ideal w₁, ← mk_max_ideal w₂] From bb4e382ed315f4cc572941226c0161fa455ba595 Mon Sep 17 00:00:00 2001 From: Fabrizio Barroero Date: Tue, 3 Dec 2024 22:38:33 +0100 Subject: [PATCH 22/32] Update Mathlib/NumberTheory/NumberField/FinitePlaces.lean Co-authored-by: Michael Stoll <99838730+MichaelStollBayreuth@users.noreply.github.com> --- Mathlib/NumberTheory/NumberField/FinitePlaces.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/NumberTheory/NumberField/FinitePlaces.lean b/Mathlib/NumberTheory/NumberField/FinitePlaces.lean index e3861df21920f..bd9d6c84597c9 100644 --- a/Mathlib/NumberTheory/NumberField/FinitePlaces.lean +++ b/Mathlib/NumberTheory/NumberField/FinitePlaces.lean @@ -221,7 +221,7 @@ theorem mulSupport_Finite_int {x : 𝓞 K} (h_x_nezero : x ≠ 0) : exact Set.Finite.subset h h_subs theorem mulSupport_Finite {x : K} (h_x_nezero : x ≠ 0) : - (Function.mulSupport fun w : FinitePlace K => w x).Finite := by + (Function.mulSupport fun w : FinitePlace K ↦ w x).Finite := by rcases @IsFractionRing.div_surjective (𝓞 K) _ K _ _ _ x with ⟨a, b, hb, hfrac⟩ subst hfrac simp_all only [ne_eq, div_eq_zero_iff, NoZeroSMulDivisors.algebraMap_eq_zero_iff, not_or, From 59b3808617e5be0fd9f726ab9f32b4bca3a20e43 Mon Sep 17 00:00:00 2001 From: Fabrizio Barroero Date: Tue, 3 Dec 2024 22:39:06 +0100 Subject: [PATCH 23/32] Update Mathlib/NumberTheory/NumberField/FinitePlaces.lean Co-authored-by: Michael Stoll <99838730+MichaelStollBayreuth@users.noreply.github.com> --- Mathlib/NumberTheory/NumberField/FinitePlaces.lean | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/Mathlib/NumberTheory/NumberField/FinitePlaces.lean b/Mathlib/NumberTheory/NumberField/FinitePlaces.lean index bd9d6c84597c9..645e7295e9a98 100644 --- a/Mathlib/NumberTheory/NumberField/FinitePlaces.lean +++ b/Mathlib/NumberTheory/NumberField/FinitePlaces.lean @@ -222,8 +222,7 @@ theorem mulSupport_Finite_int {x : 𝓞 K} (h_x_nezero : x ≠ 0) : theorem mulSupport_Finite {x : K} (h_x_nezero : x ≠ 0) : (Function.mulSupport fun w : FinitePlace K ↦ w x).Finite := by - rcases @IsFractionRing.div_surjective (𝓞 K) _ K _ _ _ x with ⟨a, b, hb, hfrac⟩ - subst hfrac + rcases IsFractionRing.div_surjective (A := 𝓞 K) x with ⟨a, b, hb, rfl⟩ simp_all only [ne_eq, div_eq_zero_iff, NoZeroSMulDivisors.algebraMap_eq_zero_iff, not_or, map_div₀] obtain ⟨ha, hb⟩ := h_x_nezero From 9b470522ff96daf424cef273b8ef940aa6211bb5 Mon Sep 17 00:00:00 2001 From: Fabrizio Barroero Date: Tue, 3 Dec 2024 22:39:25 +0100 Subject: [PATCH 24/32] Update Mathlib/NumberTheory/NumberField/FinitePlaces.lean Co-authored-by: Michael Stoll <99838730+MichaelStollBayreuth@users.noreply.github.com> --- Mathlib/NumberTheory/NumberField/FinitePlaces.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/NumberTheory/NumberField/FinitePlaces.lean b/Mathlib/NumberTheory/NumberField/FinitePlaces.lean index 645e7295e9a98..c618f4243d20d 100644 --- a/Mathlib/NumberTheory/NumberField/FinitePlaces.lean +++ b/Mathlib/NumberTheory/NumberField/FinitePlaces.lean @@ -226,7 +226,7 @@ theorem mulSupport_Finite {x : K} (h_x_nezero : x ≠ 0) : simp_all only [ne_eq, div_eq_zero_iff, NoZeroSMulDivisors.algebraMap_eq_zero_iff, not_or, map_div₀] obtain ⟨ha, hb⟩ := h_x_nezero - rw [← RingOfIntegers.coe_eq_algebraMap, ← RingOfIntegers.coe_eq_algebraMap] + simp_rw [← RingOfIntegers.coe_eq_algebraMap] apply Set.Finite.subset (Set.Finite.union (mulSupport_Finite_int ha) (mulSupport_Finite_int hb)) intro w contrapose! From 4a31859e2ea46127a8d7f01b1c7a61004b2c1f7e Mon Sep 17 00:00:00 2001 From: Fabrizio Barroero Date: Tue, 3 Dec 2024 22:39:44 +0100 Subject: [PATCH 25/32] Update Mathlib/NumberTheory/NumberField/FinitePlaces.lean Co-authored-by: Michael Stoll <99838730+MichaelStollBayreuth@users.noreply.github.com> --- Mathlib/NumberTheory/NumberField/FinitePlaces.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/NumberTheory/NumberField/FinitePlaces.lean b/Mathlib/NumberTheory/NumberField/FinitePlaces.lean index c618f4243d20d..b28df607336b4 100644 --- a/Mathlib/NumberTheory/NumberField/FinitePlaces.lean +++ b/Mathlib/NumberTheory/NumberField/FinitePlaces.lean @@ -227,7 +227,7 @@ theorem mulSupport_Finite {x : K} (h_x_nezero : x ≠ 0) : map_div₀] obtain ⟨ha, hb⟩ := h_x_nezero simp_rw [← RingOfIntegers.coe_eq_algebraMap] - apply Set.Finite.subset (Set.Finite.union (mulSupport_Finite_int ha) (mulSupport_Finite_int hb)) + apply ((mulSupport_Finite_int ha).union (mulSupport_Finite_int hb)).subset intro w contrapose! intro a_1 From 6995e9ccb4fce64ea61316690a17f3325348bc80 Mon Sep 17 00:00:00 2001 From: Fabrizio Barroero Date: Wed, 4 Dec 2024 00:06:17 +0100 Subject: [PATCH 26/32] implement suggestions --- .../NumberField/FinitePlaces.lean | 119 +++++++++--------- 1 file changed, 60 insertions(+), 59 deletions(-) diff --git a/Mathlib/NumberTheory/NumberField/FinitePlaces.lean b/Mathlib/NumberTheory/NumberField/FinitePlaces.lean index b28df607336b4..93ac3267f11fd 100644 --- a/Mathlib/NumberTheory/NumberField/FinitePlaces.lean +++ b/Mathlib/NumberTheory/NumberField/FinitePlaces.lean @@ -16,7 +16,7 @@ This file defines finite places of a number field `K` as absolute values coming into a completion of `K` associated to a non-zero prime ideal of `𝓞 K`. ## Main Definitions and Results -* `NumberField.vadic_abv`: a `v`-adic absolute value on `K`. +* `NumberField.vadicAbv`: a `v`-adic absolute value on `K`. * `NumberField.FinitePlace`: the type of finite places of a number field `K`. * `NumberField.FinitePlace.mulSupport_Finite`: the `v`-adic absolute value of a non-zero element of `K` is different from 1 for at most finitely many `v`. @@ -48,15 +48,12 @@ private lemma norm_ne_zero : (absNorm v.asIdeal : NNReal) ≠ 0 := ne_zero_of_lt /-- The `v`-adic absolute value on `K` defined as the norm of `v` raised to negative `v`-adic valuation.-/ -noncomputable def vadic_abv : AbsoluteValue K ℝ where - toFun := fun x ↦ toNNReal (norm_ne_zero v) (v.valuation x) - map_mul' := fun _ _ ↦ by simp only [_root_.map_mul, NNReal.coe_mul] - nonneg' := fun _ ↦ NNReal.zero_le_coe - eq_zero' := fun _ ↦ by simp only [NNReal.coe_eq_zero, map_eq_zero] - add_le' := by - intro x y - simp only - norm_cast +noncomputable def vadicAbv : AbsoluteValue K ℝ where + toFun x := toNNReal (norm_ne_zero v) (v.valuation x) + map_mul' _ _ := by simp only [_root_.map_mul, NNReal.coe_mul] + nonneg' _ := NNReal.zero_le_coe + eq_zero' _ := by simp only [NNReal.coe_eq_zero, map_eq_zero] + add_le' x y := by -- the triangle inequality is implied by the ultrametric one apply le_trans _ <| max_le_add_of_nonneg (zero_le ((toNNReal (norm_ne_zero v)) (v.valuation x))) (zero_le ((toNNReal (norm_ne_zero v)) (v.valuation y))) @@ -64,7 +61,7 @@ noncomputable def vadic_abv : AbsoluteValue K ℝ where rw [← h_mono.map_max] --max goes inside withZeroMultIntToNNReal exact h_mono (v.valuation.map_add x y) -theorem vadic_abv_def {x : K} : vadic_abv v x = toNNReal (norm_ne_zero v) (v.valuation x) := rfl +theorem vadicAbv_def {x : K} : vadicAbv v x = toNNReal (norm_ne_zero v) (v.valuation x) := rfl end absoluteValue @@ -100,40 +97,54 @@ noncomputable instance instNormedFieldValuedAdicCompletion : NormedField (adicCo /-- A finite place of a number field `K` is a place associated to an embedding into a completion with respect to a maximal ideal. -/ -def FinitePlace (K : Type*) [Field K] [NumberField K] := {w : AbsoluteValue K ℝ // - ∃ v : IsDedekindDomain.HeightOneSpectrum (𝓞 K), place (embedding v) = w} +def FinitePlace (K : Type*) [Field K] [NumberField K] := + {w : AbsoluteValue K ℝ // ∃ v : HeightOneSpectrum (𝓞 K), place (embedding v) = w} /-- Return the finite place defined by a maximal ideal `v`. -/ noncomputable def FinitePlace.mk (v : HeightOneSpectrum (𝓞 K)) : FinitePlace K := ⟨place (embedding v), ⟨v, rfl⟩⟩ +lemma toNNReal_Valued_eq_vadicAbv (x : K) : + toNNReal (norm_ne_zero v) (Valued.v (self:=v.adicValued) x) = vadicAbv v x := rfl + /-- 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‖ = vadic_abv v x := by +theorem FinitePlace.norm_def (x : K) : ‖embedding v x‖ = vadicAbv v x := by simp only [NormedField.toNorm, instNormedFieldValuedAdicCompletion, Valued.toNormedField, instFieldAdicCompletion, Valued.norm, Valuation.RankOne.hom, MonoidWithZeroHom.coe_mk, - ZeroHom.coe_mk, embedding, UniformSpace.Completion.coeRingHom, RingHom.coe_mk, - MonoidHom.coe_mk, OneHom.coe_mk, Valued.valuedCompletion_apply, NNReal.coe_inj] - rfl + ZeroHom.coe_mk, embedding, UniformSpace.Completion.coeRingHom, RingHom.coe_mk, MonoidHom.coe_mk, + OneHom.coe_mk, Valued.valuedCompletion_apply, toNNReal_Valued_eq_vadicAbv] + +/-- 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. -/ +theorem FinitePlace.norm_def' (x : K) : ‖embedding v x‖ = toNNReal (norm_ne_zero v) + (v.valuation x) := by + rw [norm_def, vadicAbv_def] + +/-- 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 for integers. -/ +theorem FinitePlace.norm_def'' (x : 𝓞 K) : ‖embedding v x‖ = toNNReal (norm_ne_zero v) + (v.intValuationDef x) := by + rw [norm_def, vadicAbv_def, valuation_eq_intValuationDef] open FinitePlace /-- The `v`-adic norm of an integer is at most 1. -/ theorem norm_le_one (x : 𝓞 K) : ‖embedding v x‖ ≤ 1 := by - rw [norm_def, vadic_abv_def, NNReal.coe_le_one, toNNReal_le_one_iff (one_lt_norm v)] + rw [norm_def', NNReal.coe_le_one, toNNReal_le_one_iff (one_lt_norm v)] exact valuation_le_one v x /-- The `v`-adic norm of an integer is 1 if and only if it is not in the ideal. -/ theorem norm_eq_one_iff_not_mem (x : 𝓞 K) : ‖(embedding v) x‖ = 1 ↔ x ∉ v.asIdeal := by - rw [norm_def, vadic_abv_def, NNReal.coe_eq_one, toNNReal_eq_one_iff (v.valuation (x : K)) - (norm_ne_zero v) (one_lt_norm v).ne', valuation_eq_intValuationDef, - ← dvd_span_singleton, ← intValuation_lt_one_iff_dvd, not_lt] + rw [norm_def'', NNReal.coe_eq_one, toNNReal_eq_one_iff (v.intValuationDef x) + (norm_ne_zero v) (one_lt_norm v).ne', ← dvd_span_singleton, + ← intValuation_lt_one_iff_dvd, not_lt] exact (intValuation_le_one v x).ge_iff_eq.symm /-- The `v`-adic norm of an integer is less than 1 if and only if it is in the ideal. -/ theorem norm_lt_one_iff_mem (x : 𝓞 K) : ‖embedding v x‖ < 1 ↔ x ∈ v.asIdeal := by - rw [norm_def, vadic_abv_def, NNReal.coe_lt_one, toNNReal_lt_one_iff (one_lt_norm v), - valuation_eq_intValuationDef, intValuation_lt_one_iff_dvd] + rw [norm_def'', NNReal.coe_lt_one, toNNReal_lt_one_iff (one_lt_norm v), + intValuation_lt_one_iff_dvd] exact dvd_span_singleton end FinitePlace @@ -157,25 +168,15 @@ instance : NonnegHomClass (FinitePlace K) K ℝ where theorem apply (v : HeightOneSpectrum (𝓞 K)) (x : K) : mk v x = ‖embedding v x‖ := rfl /-- For a finite place `w`, return a maximal ideal `v` such that `w = finite_place v` . -/ -noncomputable def maximal_ideal (w : FinitePlace K) : HeightOneSpectrum (𝓞 K) := w.2.choose +noncomputable def maximalIdeal (w : FinitePlace K) : HeightOneSpectrum (𝓞 K) := w.2.choose @[simp] -theorem mk_max_ideal (w : FinitePlace K) : mk (maximal_ideal w) = w := Subtype.ext w.2.choose_spec +theorem mk_maximalIdeal (w : FinitePlace K) : mk (maximalIdeal w) = w := Subtype.ext w.2.choose_spec @[simp] theorem norm_embedding_eq (w : FinitePlace K) (x : K) : - ‖embedding (maximal_ideal w) x‖ = w x := by - have h : w x = (mk (maximal_ideal w)) x := by simp only [mk_max_ideal] - rw [h] - rfl - -theorem eq_iff_eq (x : K) (r : ℝ) : (∀ w : FinitePlace K, w x = r) ↔ - ∀ v : HeightOneSpectrum (𝓞 K), ‖embedding v x‖ = r := - Set.forall_subtype_range_iff - -theorem le_iff_le (x : K) (r : ℝ) : (∀ w : FinitePlace K, w x ≤ r) ↔ - ∀ v : HeightOneSpectrum (𝓞 K), ‖embedding v x‖ ≤ r := - Set.forall_subtype_range_iff + ‖embedding (maximalIdeal w) x‖ = w x := by + rw [show w x = (mk (maximalIdeal w)) x by simp only [mk_maximalIdeal], apply] theorem pos_iff {w : FinitePlace K} {x : K} : 0 < w x ↔ x ≠ 0 := AbsoluteValue.pos_iff w.1 @@ -187,20 +188,28 @@ theorem mk_eq_iff {v₁ v₂ : HeightOneSpectrum (𝓞 K)} : mk v₁ = mk v₂ rw [DFunLike.ne_iff] have ⟨x, hx1, hx2⟩ : ∃ x : 𝓞 K, x ∈ v₁.asIdeal ∧ x ∉ v₂.asIdeal := by by_contra! H - exact h <| HeightOneSpectrum.ext_iff.mpr (IsMaximal.eq_of_le (isMaximal v₁) IsPrime.ne_top' H) + exact h <| HeightOneSpectrum.ext_iff.mpr <| IsMaximal.eq_of_le (isMaximal v₁) IsPrime.ne_top' H use x simp only [apply] rw [← norm_lt_one_iff_mem ] at hx1 rw [← norm_eq_one_iff_not_mem] at hx2 linarith -theorem max_ideal_mk (v : HeightOneSpectrum (𝓞 K)) : maximal_ideal (mk v) = v := by - rw [← mk_eq_iff, mk_max_ideal] +theorem maximalIdeal_mk (v : HeightOneSpectrum (𝓞 K)) : maximalIdeal (mk v) = v := by + rw [← mk_eq_iff, mk_maximalIdeal] + +lemma maximalIdeal_injective : (fun w : FinitePlace K ↦ maximalIdeal w).Injective := by + intro w₁ w₂ h + rw [← mk_maximalIdeal w₁, ← mk_maximalIdeal w₂] + exact congrArg mk h -theorem mulSupport_Finite_int {x : 𝓞 K} (h_x_nezero : x ≠ 0) : +lemma maximalIdeal_inj (w₁ w₂ : FinitePlace K) : maximalIdeal w₁ = maximalIdeal w₂ ↔ w₁ = w₂ := + maximalIdeal_injective.eq_iff + +theorem mulSupport_finite_int {x : 𝓞 K} (h_x_nezero : x ≠ 0) : (Function.mulSupport fun w : FinitePlace K ↦ w x).Finite := by have (w : FinitePlace K) : w x ≠ 1 ↔ w x < 1 := by - have := norm_le_one w.maximal_ideal x + have := norm_le_one w.maximalIdeal x rw [norm_embedding_eq] at this exact ne_iff_lt_iff_le.mpr this simp_rw [Function.mulSupport, this, ← norm_embedding_eq, norm_lt_one_iff_mem, @@ -208,31 +217,23 @@ theorem mulSupport_Finite_int {x : 𝓞 K} (h_x_nezero : x ≠ 0) : have h : {v : HeightOneSpectrum (𝓞 K) | v.asIdeal ∣ span {x}}.Finite := by apply Ideal.finite_factors simp only [Submodule.zero_eq_bot, ne_eq, span_singleton_eq_bot, h_x_nezero, not_false_eq_true] - have h_inj : Set.InjOn FinitePlace.maximal_ideal {w | w.maximal_ideal.asIdeal ∣ span {x}} := by - apply Function.Injective.injOn - intro w₁ w₂ h - rw [← mk_max_ideal w₁, ← mk_max_ideal w₂] - exact congrArg mk h - apply Set.Finite.of_finite_image _ h_inj - have h_subs : ((fun w : FinitePlace K ↦ w.maximal_ideal) '' - {x_1 : FinitePlace K | x_1.maximal_ideal.asIdeal ∣ span {x}}) ⊆ - {v : HeightOneSpectrum (𝓞 K) | v.asIdeal ∣ span {x}} := by - simp only [dvd_span_singleton, Set.image_subset_iff, Set.preimage_setOf_eq, subset_refl] - exact Set.Finite.subset h h_subs - -theorem mulSupport_Finite {x : K} (h_x_nezero : x ≠ 0) : + have h_inj : Set.InjOn FinitePlace.maximalIdeal {w | w.maximalIdeal.asIdeal ∣ span {x}} := + Function.Injective.injOn maximalIdeal_injective + refine Set.Finite.of_finite_image (Set.Finite.subset h ?_) h_inj + simp only [dvd_span_singleton, Set.image_subset_iff, Set.preimage_setOf_eq, subset_refl] + +theorem mulSupport_finite {x : K} (h_x_nezero : x ≠ 0) : (Function.mulSupport fun w : FinitePlace K ↦ w x).Finite := by rcases IsFractionRing.div_surjective (A := 𝓞 K) x with ⟨a, b, hb, rfl⟩ simp_all only [ne_eq, div_eq_zero_iff, NoZeroSMulDivisors.algebraMap_eq_zero_iff, not_or, map_div₀] obtain ⟨ha, hb⟩ := h_x_nezero simp_rw [← RingOfIntegers.coe_eq_algebraMap] - apply ((mulSupport_Finite_int ha).union (mulSupport_Finite_int hb)).subset + apply ((mulSupport_finite_int ha).union (mulSupport_finite_int hb)).subset intro w + simp only [Function.mem_mulSupport, ne_eq, Set.mem_union] contrapose! - intro a_1 - simp_all only [Set.mem_union, Function.mem_mulSupport, ne_eq, not_or, Decidable.not_not, - one_ne_zero, not_false_eq_true, div_self, not_true_eq_false] + simp +contextual only [ne_eq, one_ne_zero, not_false_eq_true, div_self, implies_true] end FinitePlace From 3490051391c18f1c2a06e3484513614a2917a4f1 Mon Sep 17 00:00:00 2001 From: Fabrizio Barroero Date: Thu, 5 Dec 2024 21:19:02 +0100 Subject: [PATCH 27/32] Update Mathlib/NumberTheory/NumberField/FinitePlaces.lean Co-authored-by: Michael Stoll <99838730+MichaelStollBayreuth@users.noreply.github.com> --- Mathlib/NumberTheory/NumberField/FinitePlaces.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/NumberTheory/NumberField/FinitePlaces.lean b/Mathlib/NumberTheory/NumberField/FinitePlaces.lean index 93ac3267f11fd..465f2237b4421 100644 --- a/Mathlib/NumberTheory/NumberField/FinitePlaces.lean +++ b/Mathlib/NumberTheory/NumberField/FinitePlaces.lean @@ -18,7 +18,7 @@ into a completion of `K` associated to a non-zero prime ideal of `𝓞 K`. ## Main Definitions and Results * `NumberField.vadicAbv`: a `v`-adic absolute value on `K`. * `NumberField.FinitePlace`: the type of finite places of a number field `K`. -* `NumberField.FinitePlace.mulSupport_Finite`: the `v`-adic absolute value of a non-zero element of +* `NumberField.FinitePlace.mulSupport_finite`: the `v`-adic absolute value of a non-zero element of `K` is different from 1 for at most finitely many `v`. ## Tags From df5bc8b0e32f8da03c343fb8f59443347e4eb998 Mon Sep 17 00:00:00 2001 From: Fabrizio Barroero Date: Thu, 5 Dec 2024 22:24:47 +0100 Subject: [PATCH 28/32] Update Mathlib/NumberTheory/NumberField/FinitePlaces.lean Co-authored-by: Michael Stoll <99838730+MichaelStollBayreuth@users.noreply.github.com> --- Mathlib/NumberTheory/NumberField/FinitePlaces.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/NumberTheory/NumberField/FinitePlaces.lean b/Mathlib/NumberTheory/NumberField/FinitePlaces.lean index 465f2237b4421..376d546f228eb 100644 --- a/Mathlib/NumberTheory/NumberField/FinitePlaces.lean +++ b/Mathlib/NumberTheory/NumberField/FinitePlaces.lean @@ -176,7 +176,7 @@ theorem mk_maximalIdeal (w : FinitePlace K) : mk (maximalIdeal w) = w := Subtype @[simp] theorem norm_embedding_eq (w : FinitePlace K) (x : K) : ‖embedding (maximalIdeal w) x‖ = w x := by - rw [show w x = (mk (maximalIdeal w)) x by simp only [mk_maximalIdeal], apply] + conv_rhs => rw [← mk_maximalIdeal w, apply] theorem pos_iff {w : FinitePlace K} {x : K} : 0 < w x ↔ x ≠ 0 := AbsoluteValue.pos_iff w.1 From 2a0b28f076ca7cf598538de7db963c6da7a9947f Mon Sep 17 00:00:00 2001 From: Fabrizio Barroero Date: Thu, 5 Dec 2024 23:08:32 +0100 Subject: [PATCH 29/32] Update Mathlib/NumberTheory/NumberField/FinitePlaces.lean Co-authored-by: Michael Stoll <99838730+MichaelStollBayreuth@users.noreply.github.com> --- Mathlib/NumberTheory/NumberField/FinitePlaces.lean | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/Mathlib/NumberTheory/NumberField/FinitePlaces.lean b/Mathlib/NumberTheory/NumberField/FinitePlaces.lean index 376d546f228eb..07fe99316e6b4 100644 --- a/Mathlib/NumberTheory/NumberField/FinitePlaces.lean +++ b/Mathlib/NumberTheory/NumberField/FinitePlaces.lean @@ -198,10 +198,8 @@ theorem mk_eq_iff {v₁ v₂ : HeightOneSpectrum (𝓞 K)} : mk v₁ = mk v₂ theorem maximalIdeal_mk (v : HeightOneSpectrum (𝓞 K)) : maximalIdeal (mk v) = v := by rw [← mk_eq_iff, mk_maximalIdeal] -lemma maximalIdeal_injective : (fun w : FinitePlace K ↦ maximalIdeal w).Injective := by - intro w₁ w₂ h - rw [← mk_maximalIdeal w₁, ← mk_maximalIdeal w₂] - exact congrArg mk h +lemma maximalIdeal_injective : (fun w : FinitePlace K ↦ maximalIdeal w).Injective := + Function.HasLeftInverse.injective ⟨mk, mk_maximalIdeal⟩ lemma maximalIdeal_inj (w₁ w₂ : FinitePlace K) : maximalIdeal w₁ = maximalIdeal w₂ ↔ w₁ = w₂ := maximalIdeal_injective.eq_iff From e69676f5db9ae6138ad8a41200b53c94fcda4020 Mon Sep 17 00:00:00 2001 From: Fabrizio Barroero Date: Thu, 5 Dec 2024 23:08:45 +0100 Subject: [PATCH 30/32] Update Mathlib/NumberTheory/NumberField/FinitePlaces.lean Co-authored-by: Michael Stoll <99838730+MichaelStollBayreuth@users.noreply.github.com> --- Mathlib/NumberTheory/NumberField/FinitePlaces.lean | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/Mathlib/NumberTheory/NumberField/FinitePlaces.lean b/Mathlib/NumberTheory/NumberField/FinitePlaces.lean index 07fe99316e6b4..682cd95713c26 100644 --- a/Mathlib/NumberTheory/NumberField/FinitePlaces.lean +++ b/Mathlib/NumberTheory/NumberField/FinitePlaces.lean @@ -206,10 +206,8 @@ lemma maximalIdeal_inj (w₁ w₂ : FinitePlace K) : maximalIdeal w₁ = maximal theorem mulSupport_finite_int {x : 𝓞 K} (h_x_nezero : x ≠ 0) : (Function.mulSupport fun w : FinitePlace K ↦ w x).Finite := by - have (w : FinitePlace K) : w x ≠ 1 ↔ w x < 1 := by - have := norm_le_one w.maximalIdeal x - rw [norm_embedding_eq] at this - exact ne_iff_lt_iff_le.mpr this + have (w : FinitePlace K) : w x ≠ 1 ↔ w x < 1 := + ne_iff_lt_iff_le.mpr <| norm_embedding_eq w x ▸ norm_le_one w.maximalIdeal x simp_rw [Function.mulSupport, this, ← norm_embedding_eq, norm_lt_one_iff_mem, ← Ideal.dvd_span_singleton] have h : {v : HeightOneSpectrum (𝓞 K) | v.asIdeal ∣ span {x}}.Finite := by From 8b4671c7e49cdcf5f85c5a3dcb83bade9d645cc2 Mon Sep 17 00:00:00 2001 From: Fabrizio Barroero Date: Thu, 5 Dec 2024 23:27:50 +0100 Subject: [PATCH 31/32] Update Mathlib/NumberTheory/NumberField/FinitePlaces.lean Co-authored-by: Michael Stoll <99838730+MichaelStollBayreuth@users.noreply.github.com> --- Mathlib/NumberTheory/NumberField/FinitePlaces.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/NumberTheory/NumberField/FinitePlaces.lean b/Mathlib/NumberTheory/NumberField/FinitePlaces.lean index 682cd95713c26..e8628180455b4 100644 --- a/Mathlib/NumberTheory/NumberField/FinitePlaces.lean +++ b/Mathlib/NumberTheory/NumberField/FinitePlaces.lean @@ -215,7 +215,7 @@ theorem mulSupport_finite_int {x : 𝓞 K} (h_x_nezero : x ≠ 0) : simp only [Submodule.zero_eq_bot, ne_eq, span_singleton_eq_bot, h_x_nezero, not_false_eq_true] have h_inj : Set.InjOn FinitePlace.maximalIdeal {w | w.maximalIdeal.asIdeal ∣ span {x}} := Function.Injective.injOn maximalIdeal_injective - refine Set.Finite.of_finite_image (Set.Finite.subset h ?_) h_inj + refine (h.subset ?_).of_finite_image h_inj simp only [dvd_span_singleton, Set.image_subset_iff, Set.preimage_setOf_eq, subset_refl] theorem mulSupport_finite {x : K} (h_x_nezero : x ≠ 0) : From 4e978f3c0087c352130fad24f7862cacb218ec48 Mon Sep 17 00:00:00 2001 From: Fabrizio Barroero Date: Thu, 5 Dec 2024 23:29:07 +0100 Subject: [PATCH 32/32] norm_def_int --- Mathlib/NumberTheory/NumberField/FinitePlaces.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/Mathlib/NumberTheory/NumberField/FinitePlaces.lean b/Mathlib/NumberTheory/NumberField/FinitePlaces.lean index e8628180455b4..834648c1e128e 100644 --- a/Mathlib/NumberTheory/NumberField/FinitePlaces.lean +++ b/Mathlib/NumberTheory/NumberField/FinitePlaces.lean @@ -123,7 +123,7 @@ theorem FinitePlace.norm_def' (x : K) : ‖embedding v x‖ = toNNReal (norm_ne_ /-- 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 for integers. -/ -theorem FinitePlace.norm_def'' (x : 𝓞 K) : ‖embedding v x‖ = toNNReal (norm_ne_zero v) +theorem FinitePlace.norm_def_int (x : 𝓞 K) : ‖embedding v x‖ = toNNReal (norm_ne_zero v) (v.intValuationDef x) := by rw [norm_def, vadicAbv_def, valuation_eq_intValuationDef] @@ -136,14 +136,14 @@ theorem norm_le_one (x : 𝓞 K) : ‖embedding v x‖ ≤ 1 := by /-- The `v`-adic norm of an integer is 1 if and only if it is not in the ideal. -/ theorem norm_eq_one_iff_not_mem (x : 𝓞 K) : ‖(embedding v) x‖ = 1 ↔ x ∉ v.asIdeal := by - rw [norm_def'', NNReal.coe_eq_one, toNNReal_eq_one_iff (v.intValuationDef x) + rw [norm_def_int, NNReal.coe_eq_one, toNNReal_eq_one_iff (v.intValuationDef x) (norm_ne_zero v) (one_lt_norm v).ne', ← dvd_span_singleton, ← intValuation_lt_one_iff_dvd, not_lt] exact (intValuation_le_one v x).ge_iff_eq.symm /-- The `v`-adic norm of an integer is less than 1 if and only if it is in the ideal. -/ theorem norm_lt_one_iff_mem (x : 𝓞 K) : ‖embedding v x‖ < 1 ↔ x ∈ v.asIdeal := by - rw [norm_def'', NNReal.coe_lt_one, toNNReal_lt_one_iff (one_lt_norm v), + rw [norm_def_int, NNReal.coe_lt_one, toNNReal_lt_one_iff (one_lt_norm v), intValuation_lt_one_iff_dvd] exact dvd_span_singleton