From 6de40ddd652cd24fc09f146c0a67b8fa242d8341 Mon Sep 17 00:00:00 2001 From: Salvatore Mercuri Date: Wed, 8 Jul 2026 11:42:31 +0100 Subject: [PATCH] make adicCompletionIntegers a type --- .../NumberField/Completion/FinitePlace.lean | 14 ++- .../Padics/HeightOneSpectrum.lean | 20 ++-- .../DedekindDomain/AdicValuation.lean | 100 ++++++++++++++---- .../DedekindDomain/FiniteAdeleRing.lean | 12 +-- Mathlib/RingTheory/LaurentSeries.lean | 18 ++-- 5 files changed, 118 insertions(+), 46 deletions(-) diff --git a/Mathlib/NumberTheory/NumberField/Completion/FinitePlace.lean b/Mathlib/NumberTheory/NumberField/Completion/FinitePlace.lean index 4241695e4ee78e..c903431520fe3e 100644 --- a/Mathlib/NumberTheory/NumberField/Completion/FinitePlace.lean +++ b/Mathlib/NumberTheory/NumberField/Completion/FinitePlace.lean @@ -66,16 +66,20 @@ instance : IsDiscreteValuationRing (v.valuation K).integer := (v.valuation K).valuationSubring_isDiscreteValuationRing instance : IsPrincipalIdealRing (v.adicCompletionIntegers K) := by - unfold HeightOneSpectrum.adicCompletionIntegers - rw [(Valuation.valuationSubring.integers (Valued.v)).isPrincipalIdealRing_iff_not_denselyOrdered, - WithZero.denselyOrdered_set_iff_subsingleton] - simpa using Valued.v.range_nontrivial + have h : IsPrincipalIdealRing (Valued.v (R := v.adicCompletion K)).valuationSubring := by + rw [(Valuation.valuationSubring.integers Valued.v).isPrincipalIdealRing_iff_not_denselyOrdered, + WithZero.denselyOrdered_set_iff_subsingleton] + simpa using Valued.v.range_nontrivial + exact h + +instance : IsLocalRing (v.adicCompletionIntegers K) := + inferInstanceAs (IsLocalRing (adicCompletionIntegers.valuationSubring K v)) -- TODO: make this inferred from `IsRankOneDiscrete`, or -- develop the API for a completion of a base `IsDVR` ring instance : IsDiscreteValuationRing (v.adicCompletionIntegers K) where not_a_field' := by - unfold HeightOneSpectrum.adicCompletionIntegers + change IsLocalRing.maximalIdeal (Valued.v (R := v.adicCompletion K)).valuationSubring ≠ ⊥ simp only [ne_eq, Ideal.ext_iff, Valuation.mem_maximalIdeal_iff, Ideal.mem_bot, Subtype.ext_iff, ZeroMemClass.coe_zero, Subtype.forall, Valuation.mem_valuationSubring_iff, not_forall, exists_prop] diff --git a/Mathlib/NumberTheory/Padics/HeightOneSpectrum.lean b/Mathlib/NumberTheory/Padics/HeightOneSpectrum.lean index 3423a432f69de3..f353e3e9d791d2 100644 --- a/Mathlib/NumberTheory/Padics/HeightOneSpectrum.lean +++ b/Mathlib/NumberTheory/Padics/HeightOneSpectrum.lean @@ -153,15 +153,16 @@ noncomputable def adicCompletion.padicEquiv (v : HeightOneSpectrum R) : /-- The continuous `ℤ`-algebra isomorphism between `v.adicCompletionIntegers ℚ` and `ℤ_[primesEquiv v]`. -/ noncomputable def adicCompletionIntegers.padicIntEquiv (v : HeightOneSpectrum R) : - v.adicCompletionIntegers ℚ ≃A[ℤ] ℤ_[primesEquiv v] where - __ := let e := (mapRingEquiv _ (withValEquiv v).continuous - (withValEquiv v).symm.continuous).restrict _ _ fun _ ↦ by + v.adicCompletionIntegers ℚ ≃A[ℤ] ℤ_[primesEquiv v] := + let g := (((mapRingEquiv _ (withValEquiv v).continuous + (withValEquiv v).symm.continuous).restrict _ _ fun _ ↦ by + simpa using! (valuation_equiv_padicValuation v).valuedCompletion_le_one_iff)).trans + withValIntegersRingEquiv + { __ := g + __ := let e := (mapEquiv (withValEquiv v)).subtype fun _ ↦ by simpa using! (valuation_equiv_padicValuation v).valuedCompletion_le_one_iff - e.trans withValIntegersRingEquiv - __ := let e := (mapEquiv (withValEquiv v)).subtype fun _ ↦ by - simpa using! (valuation_equiv_padicValuation v).valuedCompletion_le_one_iff - (e.trans withValIntegersUniformEquiv).toHomeomorph - commutes' := by simp + (e.trans withValIntegersUniformEquiv).toHomeomorph + commutes' r := map_intCast g r } /-- The diagram ``` @@ -189,7 +190,8 @@ theorem adicCompletionIntegers.coe_padicIntEquiv_symm_apply (v : HeightOneSpectr (adicCompletion.padicEquiv v).symm x := rfl theorem adicCompletion.padicEquiv_bijOn (v : HeightOneSpectrum R) : - Set.BijOn (padicEquiv v) (v.adicCompletionIntegers ℚ) (subring (primesEquiv v)) := by + Set.BijOn (padicEquiv v) (HeightOneSpectrum.adicCompletionIntegers.valuationSubring ℚ v) + (subring (primesEquiv v)) := by refine ⟨fun x hx ↦ ?_, (padicEquiv v).injective.injOn, fun y hy ↦ ?_⟩ · rw [← adicCompletionIntegers.coe_padicIntEquiv_apply v ⟨x, hx⟩] exact norm_le_one ((adicCompletionIntegers.padicIntEquiv v) ⟨x, hx⟩) diff --git a/Mathlib/RingTheory/DedekindDomain/AdicValuation.lean b/Mathlib/RingTheory/DedekindDomain/AdicValuation.lean index f3cb0b5d1c25ae..986f2cf543c8ed 100644 --- a/Mathlib/RingTheory/DedekindDomain/AdicValuation.lean +++ b/Mathlib/RingTheory/DedekindDomain/AdicValuation.lean @@ -622,21 +622,78 @@ lemma adicCompletion_valueGroup_eq : MonoidWithZeroHom.valueGroup (.ofClass (Val refine ⟨b, ?_, y, by simpa [hb, hy] using hx⟩ rwa [← ne_eq, ← (valuation K v).ne_zero_iff, hb, Valuation.ne_zero_iff] -/-- The ring of integers of `adicCompletion`. -/ -def adicCompletionIntegers : ValuationSubring (v.adicCompletion K) := +/-- The ring of integers of `v.adicCompletion K`, as a valuation subring of the completion. -/ +def adicCompletionIntegers.valuationSubring : ValuationSubring (v.adicCompletion K) := Valued.v.valuationSubring +/-- The ring of integers of `v.adicCompletion K`. + +This is defined as its own type, rather than a `ValuationSubring`, for performance reasons +(compare `NumberField.RingOfIntegers`): looking for instances of the form +`SMul (adicCompletionIntegers _ _) (adicCompletionIntegers _ _)` makes much more effective use of +the discrimination tree than instances of the form `SMul (Subtype _) (Subtype _)`. +The drawback is that we have to copy over instances manually. +The underlying valuation subring is `adicCompletionIntegers.valuationSubring`. -/ +def adicCompletionIntegers : Type _ := + adicCompletionIntegers.valuationSubring K v +deriving CommRing, IsDomain, Nontrivial + +namespace adicCompletionIntegers + +instance : TopologicalSpace (adicCompletionIntegers K v) := + inferInstanceAs (TopologicalSpace (adicCompletionIntegers.valuationSubring K v)) + +instance : UniformSpace (adicCompletionIntegers K v) := + inferInstanceAs (UniformSpace (adicCompletionIntegers.valuationSubring K v)) + +instance : Algebra (adicCompletionIntegers K v) (v.adicCompletion K) := + inferInstanceAs (Algebra (adicCompletionIntegers.valuationSubring K v) (v.adicCompletion K)) + +instance : IsFractionRing (adicCompletionIntegers K v) (v.adicCompletion K) := + inferInstanceAs + (IsFractionRing (adicCompletionIntegers.valuationSubring K v) (v.adicCompletion K)) + instance : Inhabited (adicCompletionIntegers K v) := ⟨0⟩ +/-- The canonical inclusion of `adicCompletionIntegers` into the completion. -/ +@[coe] +abbrev val (x : adicCompletionIntegers K v) : v.adicCompletion K := x.1 + +instance : CoeHead (adicCompletionIntegers K v) (v.adicCompletion K) := ⟨val K v⟩ + +@[ext] +theorem ext {x y : adicCompletionIntegers K v} (h : (x : v.adicCompletion K) = y) : x = y := + Subtype.ext h + +@[simp] +theorem coe_mk (x : v.adicCompletion K) (hx) : + ((⟨x, hx⟩ : adicCompletionIntegers K v) : v.adicCompletion K) = x := rfl + +@[simp, norm_cast] +theorem coe_zero : ((0 : adicCompletionIntegers K v) : v.adicCompletion K) = 0 := rfl + +@[simp, norm_cast] +theorem coe_one : ((1 : adicCompletionIntegers K v) : v.adicCompletion K) = 1 := rfl + +@[simp, norm_cast] +theorem coe_add (x y : adicCompletionIntegers K v) : + ((x + y : adicCompletionIntegers K v) : v.adicCompletion K) = ↑x + ↑y := rfl + +@[simp, norm_cast] +theorem coe_mul (x y : adicCompletionIntegers K v) : + ((x * y : adicCompletionIntegers K v) : v.adicCompletion K) = ↑x * ↑y := rfl + +end adicCompletionIntegers + variable (R) theorem mem_adicCompletionIntegers {x : v.adicCompletion K} : - x ∈ v.adicCompletionIntegers K ↔ Valued.v x ≤ 1 := + x ∈ adicCompletionIntegers.valuationSubring K v ↔ Valued.v x ≤ 1 := Iff.rfl theorem notMem_adicCompletionIntegers {x : v.adicCompletion K} : - x ∉ v.adicCompletionIntegers K ↔ 1 < Valued.v x := by + x ∉ adicCompletionIntegers.valuationSubring K v ↔ 1 < Valued.v x := by rw [not_congr <| mem_adicCompletionIntegers R K v] exact not_le @@ -686,11 +743,14 @@ theorem denseRange_algebraMap : DenseRange (algebraMap K (v.adicCompletion K)) : end Algebra -theorem coe_algebraMap_mem (r : R) : ↑((algebraMap R K) r) ∈ adicCompletionIntegers K v := by +theorem coe_algebraMap_mem (r : R) : + ↑((algebraMap R K) r) ∈ adicCompletionIntegers.valuationSubring K v := by rw [mem_adicCompletionIntegers, Valued.valuedCompletion_apply] simpa using v.valuation_le_one _ -instance : Algebra R (v.adicCompletionIntegers K) where +/-- The `R`-algebra structure on the valuation subring of integers. The one on the type +`adicCompletionIntegers` is transported from this. -/ +instance : Algebra R (adicCompletionIntegers.valuationSubring K v) where smul r x := ⟨r • (x : v.adicCompletion K), by rw [Algebra.smul_def] @@ -715,6 +775,9 @@ instance : Algebra R (v.adicCompletionIntegers K) where simp +instances only [Algebra.smul_def] rfl +instance : Algebra R (v.adicCompletionIntegers K) := + inferInstanceAs (Algebra R (adicCompletionIntegers.valuationSubring K v)) + @[simp] lemma algebraMap_adicCompletionIntegers_apply (r : R) : algebraMap R (v.adicCompletionIntegers K) r = (algebraMap R K r : v.adicCompletion K) := by @@ -723,7 +786,7 @@ lemma algebraMap_adicCompletionIntegers_apply (r : R) : instance [FaithfulSMul R K] : FaithfulSMul R (v.adicCompletionIntegers K) := by rw [faithfulSMul_iff_algebraMap_injective] intro x y - rw [Subtype.ext_iff] + rw [adicCompletionIntegers.ext_iff] simp variable {R K} in @@ -744,7 +807,7 @@ 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 + (r : adicCompletion K v) ∈ adicCompletionIntegers.valuationSubring K v := by rw [mem_adicCompletionIntegers, valuedAdicCompletion_eq_valuation] exact valuation_le_one v r @@ -766,8 +829,8 @@ variable {R} open nonZeroDivisors algebraMap in variable {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 + (a : v.adicCompletion K) : ∃ b ∈ R⁰, a * b ∈ adicCompletionIntegers.valuationSubring K v := by + by_cases ha : a ∈ adicCompletionIntegers.valuationSubring K v · use 1 simp [ha] · rw [notMem_adicCompletionIntegers] at ha @@ -783,22 +846,23 @@ lemma adicCompletion.mul_nonZeroDivisor_mem_adicCompletionIntegers (v : HeightOn exact mul_inv_le_one_of_le₀ (le_exp_log.trans (by simp [le_abs_self])) zero_le instance : FaithfulSMul (v.adicCompletionIntegers K) (v.adicCompletion K) := - Subsemiring.faithfulSMul _ + inferInstanceAs (FaithfulSMul (adicCompletionIntegers.valuationSubring K v) (v.adicCompletion K)) theorem adicCompletionIntegers.integers : - (Valued.v : Valuation (v.adicCompletion K) ℤᵐ⁰).Integers ↥(adicCompletionIntegers K v) where + (Valued.v : Valuation (v.adicCompletion K) ℤᵐ⁰).Integers (adicCompletionIntegers K v) where hom_inj := FaithfulSMul.algebraMap_injective _ _ - map_le_one := by simp [mem_adicCompletionIntegers] - exists_of_le_one := by simp [mem_adicCompletionIntegers] + map_le_one x := x.2 + exists_of_le_one {a} h := ⟨⟨a, h⟩, rfl⟩ variable {K v} -theorem adicCompletionIntegers.isUnit_iff_valued_eq_one {a : v.adicCompletionIntegers K} : - IsUnit a ↔ Valued.v a.1 = 1 := by - simp [Valuation.Integers.isUnit_iff_valuation_eq_one (integers K v)] +theorem adicCompletionIntegers.isUnit_iff_valued_eq_one + {a : adicCompletionIntegers.valuationSubring K v} : + IsUnit a ↔ Valued.v a.1 = 1 := + Valuation.Integers.isUnit_iff_valuation_eq_one (integers K v) theorem adicCompletionIntegers.mem_units_iff_valued_eq_one {a : (v.adicCompletion K)ˣ} : - a ∈ (v.adicCompletionIntegers K).units ↔ Valued.v a.1 = 1 := by + a ∈ (adicCompletionIntegers.valuationSubring K v).units ↔ Valued.v a.1 = 1 := by refine ⟨fun h ↦ ?_, fun h ↦ ⟨h.le, by simp [mem_adicCompletionIntegers, inv_le_one_iff₀, h.symm.le]⟩⟩ convert! isUnit_iff_valued_eq_one.1 (Submonoid.unitsEquivIsUnitSubmonoid _ ⟨_, h⟩).2 diff --git a/Mathlib/RingTheory/DedekindDomain/FiniteAdeleRing.lean b/Mathlib/RingTheory/DedekindDomain/FiniteAdeleRing.lean index 7f5ce30facd4e0..e6a8b780998445 100644 --- a/Mathlib/RingTheory/DedekindDomain/FiniteAdeleRing.lean +++ b/Mathlib/RingTheory/DedekindDomain/FiniteAdeleRing.lean @@ -92,13 +92,13 @@ and the restricted product is the subring of `∏_v K_v` consisting of elements are in `R_v` for all but finitely many `v`. -/ def FiniteAdeleRing : Type _ := - Πʳ v : HeightOneSpectrum R, [v.adicCompletion K, v.adicCompletionIntegers K] + Πʳ v : HeightOneSpectrum R, [v.adicCompletion K, adicCompletionIntegers.valuationSubring K v] -instance : CommRing (FiniteAdeleRing R K) := inferInstanceAs <| - CommRing <| Πʳ v : HeightOneSpectrum R, [v.adicCompletion K, v.adicCompletionIntegers K] +instance : CommRing (FiniteAdeleRing R K) := inferInstanceAs <| CommRing <| + Πʳ v : HeightOneSpectrum R, [v.adicCompletion K, adicCompletionIntegers.valuationSubring K v] -instance : TopologicalSpace (FiniteAdeleRing R K) := inferInstanceAs <| - TopologicalSpace <| Πʳ v : HeightOneSpectrum R, [v.adicCompletion K, v.adicCompletionIntegers K] +instance : TopologicalSpace (FiniteAdeleRing R K) := inferInstanceAs <| TopologicalSpace <| + Πʳ v : HeightOneSpectrum R, [v.adicCompletion K, adicCompletionIntegers.valuationSubring K v] instance : DFunLike (FiniteAdeleRing R K) (HeightOneSpectrum R) (adicCompletion K) where coe a := a.1 @@ -142,7 +142,7 @@ section Topology instance : IsTopologicalRing (FiniteAdeleRing R K) := haveI : Fact (∀ v : HeightOneSpectrum R, - IsOpen (v.adicCompletionIntegers K : Set (v.adicCompletion K))) := + IsOpen (adicCompletionIntegers.valuationSubring K v : Set (v.adicCompletion K))) := ⟨fun _ ↦ Valued.isOpen_valuationSubring _⟩ RestrictedProduct.isTopologicalRing (fun (v : HeightOneSpectrum R) ↦ v.adicCompletion K) diff --git a/Mathlib/RingTheory/LaurentSeries.lean b/Mathlib/RingTheory/LaurentSeries.lean index 2de61dbc423458..a09e3038ee4581 100644 --- a/Mathlib/RingTheory/LaurentSeries.lean +++ b/Mathlib/RingTheory/LaurentSeries.lean @@ -1144,7 +1144,7 @@ lemma powerSeriesEquivSubring_coe_apply (f : K⟦X⟧) : /-- Through the isomorphism `LaurentSeriesRingEquiv`, power series land in the unit ball inside the completion of `K⟮X⟯`. -/ theorem mem_integers_of_powerSeries (F : K⟦X⟧) : - (LaurentSeriesRingEquiv K) F ∈ (idealX K).adicCompletionIntegers K⟮X⟯ := by + (LaurentSeriesRingEquiv K) F ∈ adicCompletionIntegers.valuationSubring K⟮X⟯ (idealX K) := by simp only [mem_adicCompletionIntegers, LaurentSeriesRingEquiv_def, valuation_compare, val_le_one_iff_eq_coe] exact ⟨F, rfl⟩ @@ -1152,7 +1152,7 @@ theorem mem_integers_of_powerSeries (F : K⟦X⟧) : /-- Conversely, all elements in the unit ball inside the completion of `K⟮X⟯` come from a power series through the isomorphism `LaurentSeriesRingEquiv`. -/ theorem exists_powerSeries_of_memIntegers {x : RatFuncAdicCompl K} - (hx : x ∈ (idealX K).adicCompletionIntegers K⟮X⟯) : + (hx : x ∈ adicCompletionIntegers.valuationSubring K⟮X⟯ (idealX K)) : ∃ F : K⟦X⟧, (LaurentSeriesRingEquiv K) F = x := by set f := (ratfuncAdicComplRingEquiv K) x with hf have H_x : (LaurentSeriesPkg K).compare ratfuncAdicComplPkg ((ratfuncAdicComplRingEquiv K) x) = @@ -1163,7 +1163,7 @@ theorem exists_powerSeries_of_memIntegers {x : RatFuncAdicCompl K} theorem powerSeries_ext_subring : Subring.map (LaurentSeriesRingEquiv K).toRingHom (powerSeries_as_subring K) = - ((idealX K).adicCompletionIntegers K⟮X⟯).toSubring := by + (adicCompletionIntegers.valuationSubring K⟮X⟯ (idealX K)).toSubring := by ext x refine ⟨fun ⟨f, ⟨F, _, coe_F⟩, hF⟩ ↦ ?_, fun H ↦ ?_⟩ · simp only [ValuationSubring.mem_toSubring, ← hF, ← coe_F] @@ -1190,7 +1190,7 @@ lemma LaurentSeriesRingEquiv_mem_valuationSubring (f : K⟦X⟧) : lemma algebraMap_C_mem_adicCompletionIntegers (x : K) : ((LaurentSeriesRingEquiv K).toRingHom.comp HahnSeries.C) x ∈ - adicCompletionIntegers K⟮X⟯ (idealX K) := by + adicCompletionIntegers.valuationSubring K⟮X⟯ (idealX K) := by have : HahnSeries.C x = ofPowerSeries ℤ K (PowerSeries.C x) := by simp [C_apply, ofPowerSeries_C] simp only [RingHom.comp_apply, RingEquiv.toRingHom_eq_coe, RingHom.coe_coe, this] @@ -1206,10 +1206,12 @@ instance : Algebra K ((idealX K).adicCompletionIntegers K⟮X⟯) := def powerSeriesAlgEquiv : K⟦X⟧ ≃ₐ[K] (idealX K).adicCompletionIntegers K⟮X⟯ := by apply AlgEquiv.ofRingEquiv (f := powerSeriesRingEquiv K) intro a - rw [PowerSeries.algebraMap_eq, RingHom.algebraMap_toAlgebra, ← Subtype.coe_inj, - powerSeriesRingEquiv_coe_apply, - RingHom.codRestrict_apply _ _ (algebraMap_C_mem_adicCompletionIntegers K)] - simp + apply adicCompletionIntegers.ext + -- reduce the right-hand `algebraMap` (defined via `codRestrict`) by `rfl`-level defeq, + -- avoiding a `rw` across the `adicCompletionIntegers`/`valuationSubring` spelling boundary + change ↑(powerSeriesRingEquiv K (algebraMap K K⟦X⟧ a)) = LaurentSeriesRingEquiv K (HahnSeries.C a) + rw [PowerSeries.algebraMap_eq, powerSeriesRingEquiv_coe_apply] + simp [C_apply, ofPowerSeries_C] end PowerSeries