refactor: make adicCompletionIntegers a type

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]

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⟩)

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

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)
 

Mathlib/RingTheory/LaurentSeries.lean

@@ -1144,15 +1144,15 @@ 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⟩
 
 /-- 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