From caac5b13fb72ba0c5d0b35a0067de108db65e964 Mon Sep 17 00:00:00 2001 From: Kevin Buzzard Date: Sun, 28 Jul 2024 16:59:53 +0000 Subject: [PATCH] feat: topology on ring of finite adeles. (#14176) Use `SubmodulesRingBasis` to put a topology on the finite adeles. --- .../DedekindDomain/AdicValuation.lean | 63 ++++++++++++++ .../DedekindDomain/FiniteAdeleRing.lean | 86 +++++++++++++++++++ 2 files changed, 149 insertions(+) diff --git a/Mathlib/RingTheory/DedekindDomain/AdicValuation.lean b/Mathlib/RingTheory/DedekindDomain/AdicValuation.lean index 4385401a68139..9659b2099784c 100644 --- a/Mathlib/RingTheory/DedekindDomain/AdicValuation.lean +++ b/Mathlib/RingTheory/DedekindDomain/AdicValuation.lean @@ -83,6 +83,10 @@ def intValuationDef (r : R) : ℤₘ₀ := theorem intValuationDef_if_pos {r : R} (hr : r = 0) : v.intValuationDef r = 0 := if_pos hr +@[simp] +theorem intValuationDef_zero : v.intValuationDef 0 = 0 := + if_pos rfl + theorem intValuationDef_if_neg {r : R} (hr : r ≠ 0) : v.intValuationDef r = Multiplicative.ofAdd @@ -312,6 +316,10 @@ theorem valuation_of_mk' {r : R} {s : nonZeroDivisors R} : theorem valuation_of_algebraMap (r : R) : v.valuation (algebraMap R K r) = v.intValuation r := by rw [valuation_def, Valuation.extendToLocalization_apply_map_apply] +open scoped algebraMap in +lemma valuation_eq_intValuationDef (r : R) : v.valuation (r : K) = v.intValuationDef r := + Valuation.extendToLocalization_apply_map_apply .. + /-- The `v`-adic valuation on `R` is bounded above by 1. -/ theorem valuation_le_one (r : R) : v.valuation (algebraMap R K r) ≤ 1 := by rw [valuation_of_algebraMap]; exact v.intValuation_le_one r @@ -394,6 +402,11 @@ theorem mem_adicCompletionIntegers {x : v.adicCompletion K} : x ∈ v.adicCompletionIntegers K ↔ (Valued.v x : ℤₘ₀) ≤ 1 := Iff.rfl +theorem not_mem_adicCompletionIntegers {x : v.adicCompletion K} : + x ∉ v.adicCompletionIntegers K ↔ 1 < (Valued.v x : ℤₘ₀) := by + rw [not_congr <| mem_adicCompletionIntegers R K v] + exact not_le + section AlgebraInstances instance (priority := 100) adicValued.has_uniform_continuous_const_smul' : @@ -457,6 +470,28 @@ instance : Algebra R (v.adicCompletionIntegers K) where simp only [Subring.coe_mul, Algebra.smul_def] rfl +variable {R K} in +open scoped algebraMap in -- to make the coercions from `R` fire +/-- The valuation on the completion agrees with the global valuation on elements of the +integer ring. -/ +theorem valuedAdicCompletion_eq_valuation (r : R) : + Valued.v (r : v.adicCompletion K) = v.valuation (r : K) := by + convert Valued.valuedCompletion_apply (r : K) + +variable {R K} in +/-- The valuation on the completion agrees with the global valuation on elements of the field. -/ +theorem valuedAdicCompletion_eq_valuation' (k : K) : + Valued.v (k : v.adicCompletion K) = v.valuation k := by + convert Valued.valuedCompletion_apply k + +variable {R K} in +open scoped algebraMap in -- to make the coercion from `R` fire +/-- A global integer is in the local integers. -/ +lemma coe_mem_adicCompletionIntegers (r : R) : + (r : adicCompletion K v) ∈ adicCompletionIntegers K v := by + rw [mem_adicCompletionIntegers, valuedAdicCompletion_eq_valuation, valuation_eq_intValuationDef] + exact intValuation_le_one v r + @[simp] theorem coe_smul_adicCompletionIntegers (r : R) (x : v.adicCompletionIntegers K) : (↑(r • x) : v.adicCompletion K) = r • (x : v.adicCompletion K) := @@ -477,4 +512,32 @@ instance adicCompletion.instIsScalarTower' : end AlgebraInstances +open nonZeroDivisors algebraMap in +variable {R K} in +lemma adicCompletion.mul_nonZeroDivisor_mem_adicCompletionIntegers (v : HeightOneSpectrum R) + (a : v.adicCompletion K) : ∃ b ∈ R⁰, a * b ∈ v.adicCompletionIntegers K := by + by_cases ha : a ∈ v.adicCompletionIntegers K + · use 1 + simp [ha, Submonoid.one_mem] + · rw [not_mem_adicCompletionIntegers] at ha + -- Let the additive valuation of a be -d with d>0 + obtain ⟨d, hd⟩ : ∃ d : ℤ, Valued.v a = ofAdd d := + Option.ne_none_iff_exists'.mp <| (lt_trans zero_lt_one ha).ne' + rw [hd, WithZero.one_lt_coe, ← ofAdd_zero, ofAdd_lt] at ha + -- let ϖ be a uniformiser + obtain ⟨ϖ, hϖ⟩ := intValuation_exists_uniformizer v + have hϖ0 : ϖ ≠ 0 := by rintro rfl; simp at hϖ + -- use ϖ^d + refine ⟨ϖ^d.natAbs, pow_mem (mem_nonZeroDivisors_of_ne_zero hϖ0) _, ?_⟩ + -- now manually translate the goal (an inequality in ℤₘ₀) to an inequality in ℤ + rw [mem_adicCompletionIntegers, algebraMap.coe_pow, map_mul, hd, map_pow, + valuedAdicCompletion_eq_valuation, valuation_eq_intValuationDef, hϖ, ← WithZero.coe_pow, + ← WithZero.coe_mul, WithZero.coe_le_one, ← toAdd_le, toAdd_mul, toAdd_ofAdd, toAdd_pow, + toAdd_ofAdd, toAdd_one, + show d.natAbs • (-1) = (d.natAbs : ℤ) • (-1) by simp only [nsmul_eq_mul, + Int.natCast_natAbs, smul_eq_mul], + ← Int.eq_natAbs_of_zero_le ha.le, smul_eq_mul] + -- and now it's easy + linarith + end IsDedekindDomain.HeightOneSpectrum diff --git a/Mathlib/RingTheory/DedekindDomain/FiniteAdeleRing.lean b/Mathlib/RingTheory/DedekindDomain/FiniteAdeleRing.lean index ec3da1af1cae9..7b7ad16bb8ddd 100644 --- a/Mathlib/RingTheory/DedekindDomain/FiniteAdeleRing.lean +++ b/Mathlib/RingTheory/DedekindDomain/FiniteAdeleRing.lean @@ -327,6 +327,12 @@ instance : CommRing (FiniteAdeleRing R K) := instance : Algebra K (FiniteAdeleRing R K) := Subalgebra.algebra (subalgebra R K) +instance : Algebra R (FiniteAdeleRing R K) := + ((algebraMap K (FiniteAdeleRing R K)).comp (algebraMap R K)).toAlgebra + +instance : IsScalarTower R K (FiniteAdeleRing R K) := + IsScalarTower.of_algebraMap_eq' rfl + instance : Coe (FiniteAdeleRing R K) (K_hat R K) where coe := fun x ↦ x.1 @@ -348,6 +354,86 @@ instance : Algebra (R_hat R K) (FiniteAdeleRing R K) where commutes' _ _ := mul_comm _ _ smul_def' r x := rfl +instance : CoeFun (FiniteAdeleRing R K) + (fun _ ↦ ∀ (v : HeightOneSpectrum R), adicCompletion K v) where + coe a v := a.1 v + +open scoped algebraMap in +variable {R K} in +lemma exists_finiteIntegralAdele_iff (a : FiniteAdeleRing R K) : (∃ c : R_hat R K, + a = c) ↔ ∀ (v : HeightOneSpectrum R), a v ∈ adicCompletionIntegers K v := + ⟨by rintro ⟨c, rfl⟩ v; exact (c v).2, fun h ↦ ⟨fun v ↦ ⟨a v, h v⟩, rfl⟩⟩ + +section Topology + +open Classical nonZeroDivisors Multiplicative Additive IsDedekindDomain.HeightOneSpectrum + +open scoped algebraMap -- coercion from R to FiniteAdeleRing R K +open scoped DiscreteValuation + +variable {R K} in +lemma mul_nonZeroDivisor_mem_finiteIntegralAdeles (a : FiniteAdeleRing R K) : + ∃ (b : R⁰) (c : R_hat R K), a * ((b : R) : FiniteAdeleRing R K) = c := by + let S := {v | a v ∉ adicCompletionIntegers K v} + choose b hb h using adicCompletion.mul_nonZeroDivisor_mem_adicCompletionIntegers (R := R) (K := K) + let p := ∏ᶠ v ∈ S, b v (a v) + have hp : p ∈ R⁰ := finprod_mem_induction (· ∈ R⁰) (one_mem _) (fun _ _ => mul_mem) <| + fun _ _ ↦ hb _ _ + use ⟨p, hp⟩ + rw [exists_finiteIntegralAdele_iff] + intro v + by_cases hv : a v ∈ adicCompletionIntegers K v + · exact mul_mem hv <| coe_mem_adicCompletionIntegers _ _ + · dsimp only + have pprod : p = b v (a v) * ∏ᶠ w ∈ S \ {v}, b w (a w) := by + rw [← finprod_mem_singleton (a := v) (f := fun v ↦ b v (a v)), + finprod_mem_mul_diff (singleton_subset_iff.2 ‹v ∈ S›) a.2] + rw [pprod] + push_cast + rw [← mul_assoc] + exact mul_mem (h v (a v)) <| coe_mem_adicCompletionIntegers _ _ + +open scoped Pointwise + +theorem submodulesRingBasis : SubmodulesRingBasis + (fun (r : R⁰) ↦ Submodule.span (R_hat R K) {((r : R) : FiniteAdeleRing R K)}) where + inter i j := ⟨i * j, by + push_cast + simp only [le_inf_iff, Submodule.span_singleton_le_iff_mem, Submodule.mem_span_singleton] + exact ⟨⟨((j : R) : R_hat R K), by rw [mul_comm]; rfl⟩, ⟨((i : R) : R_hat R K), rfl⟩⟩⟩ + leftMul a r := by + rcases mul_nonZeroDivisor_mem_finiteIntegralAdeles a with ⟨b, c, h⟩ + use r * b + rintro x ⟨m, hm, rfl⟩ + simp only [Submonoid.coe_mul, SetLike.mem_coe] at hm + rw [Submodule.mem_span_singleton] at hm ⊢ + rcases hm with ⟨n, rfl⟩ + simp only [LinearMapClass.map_smul, DistribMulAction.toLinearMap_apply, smul_eq_mul] + use n * c + push_cast + rw [mul_left_comm, h, mul_comm _ (c : FiniteAdeleRing R K), + Algebra.smul_def', Algebra.smul_def', ← mul_assoc] + rfl + mul r := ⟨r, by + intro x hx + rw [mem_mul] at hx + rcases hx with ⟨a, ha, b, hb, rfl⟩ + simp only [SetLike.mem_coe, Submodule.mem_span_singleton] at ha hb ⊢ + rcases ha with ⟨m, rfl⟩ + rcases hb with ⟨n, rfl⟩ + use m * n * (r : R) + simp only [Algebra.smul_def', map_mul] + rw [mul_mul_mul_comm, mul_assoc] + rfl⟩ + +instance : TopologicalSpace (FiniteAdeleRing R K) := + SubmodulesRingBasis.topology (submodulesRingBasis R K) + +-- the point of the above: this now works +example : TopologicalRing (FiniteAdeleRing R K) := inferInstance + +end Topology + end FiniteAdeleRing end DedekindDomain