chore(topology/algebra/valuation): add universe (#11962)

Co-authored-by: Oliver Nash <github@olivernash.org>

src/topology/algebra/valuation.lean

@@ -13,29 +13,34 @@ import ring_theory.valuation.basic
 
 In this file, we define the non archimedean topology induced by a valuation on a ring.
 The main definition is a `valued` type class which equips a ring with a valuation taking
-values in a group with zero (living in the same universe). Other instances are then deduced from
-this.
+values in a group with zero. Other instances are then deduced from this.
 -/
 
 open_locale classical topological_space
 open set valuation
 noncomputable theory
 
-universe u
+universes v u
 
-/-- A valued ring is a ring that comes equipped with a distinguished valuation.-/
-class valued (R : Type u) [ring R] :=
-(Γ₀ : Type u)
-[grp : linear_ordered_comm_group_with_zero Γ₀]
-(v : valuation R Γ₀)
+/-- A valued ring is a ring that comes equipped with a distinguished valuation. The class `valued`
+is designed for the situation that there is a canonical valuation on the ring. It allows such a
+valuation to be registered as a typeclass; this is used for instance by `valued.topological_space`.
 
-attribute [instance] valued.grp
+TODO: show that there always exists an equivalent valuation taking values in a type belonging to
+the same universe as the ring. -/
+class valued (R : Type u) [ring R] (Γ₀ : out_param (Type v))
+  [linear_ordered_comm_group_with_zero Γ₀] :=
+(v : valuation R Γ₀)
 
 namespace valued
-variables {R : Type*} [ring R] [valued R]
+variables {R : Type u} [ring R] (Γ₀ : Type v) [linear_ordered_comm_group_with_zero Γ₀]
+  [hv : valued R Γ₀]
+
+include hv
 
 /-- The basis of open subgroups for the topology on a valued ring.-/
-lemma subgroups_basis : ring_subgroups_basis (λ γ : (Γ₀ R)ˣ, valued.v.lt_add_subgroup γ) :=
+lemma subgroups_basis :
+  ring_subgroups_basis (λ γ : Γ₀ˣ, (valued.v.lt_add_subgroup γ : add_subgroup R)) :=
 { inter := begin
     rintros γ₀ γ₁,
     use min γ₀ γ₁,
@@ -46,22 +51,22 @@ lemma subgroups_basis : ring_subgroups_basis (λ γ : (Γ₀ R)ˣ, valued.v.lt_a
     cases exists_square_le γ with γ₀ h,
     use γ₀,
     rintro - ⟨r, s, r_in, s_in, rfl⟩,
-    calc v (r*s) = v r * v s : valuation.map_mul _ _ _
+    calc (v (r*s) : Γ₀) = v r * v s : valuation.map_mul _ _ _
              ... < γ₀*γ₀ : mul_lt_mul₀ r_in s_in
              ... ≤ γ : by exact_mod_cast h
   end,
   left_mul := begin
     rintros x γ,
     rcases group_with_zero.eq_zero_or_unit (v x) with Hx | ⟨γx, Hx⟩,
-    { use 1,
-      rintros y (y_in : v y < 1),
+    { use (1 : Γ₀ˣ),
+      rintros y (y_in : (v y : Γ₀) < 1),
       change v (x * y) < _,
       rw [valuation.map_mul, Hx, zero_mul],
       exact units.zero_lt γ },
     { simp only [image_subset_iff, set_of_subset_set_of, preimage_set_of_eq, valuation.map_mul],
       use γx⁻¹*γ,
       rintros y (vy_lt : v y < ↑(γx⁻¹ * γ)),
-      change v (x * y) < γ,
+      change (v (x * y) : Γ₀) < γ,
       rw [valuation.map_mul, Hx, mul_comm],
       rw [units.coe_mul, mul_comm] at vy_lt,
       simpa using mul_inv_lt_of_lt_mul₀ vy_lt }
@@ -70,30 +75,36 @@ lemma subgroups_basis : ring_subgroups_basis (λ γ : (Γ₀ R)ˣ, valued.v.lt_a
     rintros x γ,
     rcases group_with_zero.eq_zero_or_unit (v x) with Hx | ⟨γx, Hx⟩,
     { use 1,
-      rintros y (y_in : v y < 1),
+      rintros y (y_in : (v y : Γ₀) < 1),
       change v (y * x) < _,
       rw [valuation.map_mul, Hx, mul_zero],
       exact units.zero_lt γ },
     { use γx⁻¹*γ,
       rintros y (vy_lt : v y < ↑(γx⁻¹ * γ)),
-      change v (y * x) < γ,
+      change (v (y * x) : Γ₀) < γ,
       rw [valuation.map_mul, Hx],
       rw [units.coe_mul, mul_comm] at vy_lt,
       simpa using mul_inv_lt_of_lt_mul₀ vy_lt }
   end }
 
-@[priority 100]
-instance : topological_space R := subgroups_basis.topology
+/-- The topological space structure on a valued ring.
+
+NOTE: The `dangerous_instance` linter does not check whether the metavariables only occur in
+arguments marked with `out_param`, so in this instance it gives a false positive. -/
+@[nolint dangerous_instance, priority 100]
+instance : topological_space R := (subgroups_basis Γ₀).topology
+
+variable {Γ₀}
 
 lemma mem_nhds {s : set R} {x : R} :
-  (s ∈ 𝓝 x) ↔ ∃ γ : (valued.Γ₀ R)ˣ, {y | v (y - x) < γ } ⊆ s :=
-by simpa [(subgroups_basis.has_basis_nhds x).mem_iff]
+  (s ∈ 𝓝 x) ↔ ∃ (γ : Γ₀ˣ), {y | (v (y - x) : Γ₀) < γ } ⊆ s :=
+by simpa [((subgroups_basis Γ₀).has_basis_nhds x).mem_iff]
 
 lemma mem_nhds_zero {s : set R} :
-  (s ∈ 𝓝 (0 : R)) ↔ ∃ γ : (Γ₀ R)ˣ, {x | v x < (γ : Γ₀ R) } ⊆ s :=
+  (s ∈ 𝓝 (0 : R)) ↔ ∃ γ : Γ₀ˣ, {x | v x < (γ : Γ₀) } ⊆ s :=
 by simp [valued.mem_nhds, sub_zero]
 
-lemma loc_const {x : R} (h : v x ≠ 0) : {y : R | v y = v x} ∈ 𝓝 x :=
+lemma loc_const {x : R} (h : (v x : Γ₀) ≠ 0) : {y : R | v y = v x} ∈ 𝓝 x :=
 begin
   rw valued.mem_nhds,
   rcases units.exists_iff_ne_zero.mpr h with ⟨γ, hx⟩,
@@ -103,23 +114,26 @@ begin
   exact valuation.map_eq_of_sub_lt _ y_in
 end
 
-/-- The uniform structure on a valued ring.-/
-@[priority 100]
+/-- The uniform structure on a valued ring.
+
+NOTE: The `dangerous_instance` linter does not check whether the metavariables only occur in
+arguments marked with `out_param`, so in this instance it gives a false positive.-/
+@[nolint dangerous_instance, priority 100]
 instance uniform_space : uniform_space R := topological_add_group.to_uniform_space R
 
 /-- A valued ring is a uniform additive group.-/
 @[priority 100]
 instance uniform_add_group : uniform_add_group R := topological_add_group_is_uniform
 
 lemma cauchy_iff {F : filter R} :
-  cauchy F ↔ F.ne_bot ∧ ∀ γ : (Γ₀ R)ˣ, ∃ M ∈ F, ∀ x y ∈ M, v (y - x) < γ :=
+  cauchy F ↔ F.ne_bot ∧ ∀ γ : Γ₀ˣ, ∃ M ∈ F, ∀ x y ∈ M, (v (y - x) : Γ₀) < γ :=
 begin
   rw add_group_filter_basis.cauchy_iff,
   apply and_congr iff.rfl,
-  simp_rw subgroups_basis.mem_add_group_filter_basis_iff,
+  simp_rw (subgroups_basis Γ₀).mem_add_group_filter_basis_iff,
   split,
   { intros h γ,
-    exact h _ (subgroups_basis.mem_add_group_filter_basis _) },
+    exact h _ ((subgroups_basis Γ₀).mem_add_group_filter_basis _) },
   { rintros h - ⟨γ, rfl⟩,
     exact h γ }
 end

src/topology/algebra/valued_field.lean

@@ -34,12 +34,12 @@ open_locale topological_space
 
 section division_ring
 
-variables {K : Type*} [division_ring K]
+variables {K : Type*} [division_ring K] {Γ₀ : Type*} [linear_ordered_comm_group_with_zero Γ₀]
 
 section valuation_topological_division_ring
 
 section inversion_estimate
-variables {Γ₀ : Type*} [linear_ordered_comm_group_with_zero Γ₀] (v : valuation K Γ₀)
+variables (v : valuation K Γ₀)
 
 -- The following is the main technical lemma ensuring that inversion is continuous
 -- in the topology induced by a valuation on a division ring (ie the next instance)
@@ -82,13 +82,13 @@ open valued
 /-- The topology coming from a valuation on a division ring makes it a topological division ring
     [BouAC, VI.5.1 middle of Proposition 1] -/
 @[priority 100]
-instance valued.topological_division_ring [valued K] : topological_division_ring K :=
+instance valued.topological_division_ring [valued K Γ₀] : topological_division_ring K :=
 { continuous_inv :=
     begin
       intros x x_ne s s_in,
       cases valued.mem_nhds.mp s_in with γ hs, clear s_in,
       rw [mem_map, valued.mem_nhds],
-      change ∃ (γ : (valued.Γ₀ K)ˣ), {y : K | v (y - x) < γ} ⊆ {x : K | x⁻¹ ∈ s},
+      change ∃ (γ : Γ₀ˣ), {y : K | (v (y - x) : Γ₀) < γ} ⊆ {x : K | x⁻¹ ∈ s},
       have vx_ne := (valuation.ne_zero_iff $ v).mpr x_ne,
       let γ' := units.mk0 _ vx_ne,
       use min (γ * (γ'*γ')) γ',
@@ -102,7 +102,7 @@ instance valued.topological_division_ring [valued K] : topological_division_ring
 
 /-- A valued division ring is separated. -/
 @[priority 100]
-instance valued_ring.separated [valued K] : separated_space K :=
+instance valued_ring.separated [valued K Γ₀] : separated_space K :=
 begin
   apply topological_add_group.separated_of_zero_sep,
   intros x x_ne,
@@ -113,13 +113,12 @@ begin
   exact ⟨γ', λ y hy, by simpa using hy⟩,
 end
 
-
 section
 local attribute [instance] linear_ordered_comm_group_with_zero.topological_space
 
 open valued
 
-lemma valued.continuous_valuation [valued K] : continuous (v : K → Γ₀ K) :=
+lemma valued.continuous_valuation [valued K Γ₀] : continuous (v : K → Γ₀) :=
 begin
   rw continuous_iff_continuous_at,
   intro x,
@@ -133,7 +132,7 @@ begin
     rw valued.mem_nhds_zero,
     use [γ, set.subset.refl _] },
   { change tendsto _ _ _,
-    have v_ne : v x ≠ 0, from (valuation.ne_zero_iff _).mpr h,
+    have v_ne : (v x : Γ₀) ≠ 0, from (valuation.ne_zero_iff _).mpr h,
     rw linear_ordered_comm_group_with_zero.tendsto_of_ne_zero v_ne,
     apply valued.loc_const v_ne },
 end
@@ -146,7 +145,10 @@ end division_ring
 section valuation_on_valued_field_completion
 open uniform_space
 
-variables {K : Type*} [field K] [valued K]
+variables {K : Type*} [field K] {Γ₀ : Type*} [linear_ordered_comm_group_with_zero Γ₀]
+  [hv: valued K Γ₀]
+
+include hv
 
 open valued uniform_space
 
@@ -157,7 +159,7 @@ local notation `hat ` := completion
 instance valued.completable : completable_top_field K :=
 { nice := begin
     rintros F hF h0,
-    have : ∃ (γ₀ : (Γ₀ K)ˣ) (M ∈ F), ∀ x ∈ M, (γ₀ : Γ₀ K) ≤ v x,
+    have : ∃ (γ₀ : Γ₀ˣ) (M ∈ F), ∀ x ∈ M, (γ₀ : Γ₀) ≤ v x,
     { rcases filter.inf_eq_bot_iff.mp h0 with ⟨U, U_in, M, M_in, H⟩,
       rcases valued.mem_nhds_zero.mp U_in with ⟨γ₀, hU⟩,
       existsi [γ₀, M, M_in],
@@ -183,14 +185,14 @@ instance valued.completable : completable_top_field K :=
       replace x_in₀ := H₀ x x_in₀,
       replace y_in₀ := H₀ y y_in₀, clear H₀,
       apply valuation.inversion_estimate,
-      { have : v x ≠ 0,
+      { have : (v x : Γ₀) ≠ 0,
         { intro h, rw h at x_in₀, simpa using x_in₀, },
         exact (valuation.ne_zero_iff _).mp this },
       { refine lt_of_lt_of_le H₁ _,
         rw units.min_coe,
         apply min_le_min _ x_in₀,
         rw mul_assoc,
-        have : ((γ₀ * γ₀ : (Γ₀ K)ˣ) : Γ₀ K) ≤ v x * v x,
+        have : ((γ₀ * γ₀ : Γ₀ˣ) : Γ₀) ≤ v x * v x,
           from calc ↑γ₀ * ↑γ₀ ≤ ↑γ₀ * v x : mul_le_mul_left' x_in₀ ↑γ₀
                           ... ≤ _ : mul_le_mul_right' x_in₀ (v x),
         rw units.coe_mul,
@@ -201,10 +203,10 @@ instance valued.completable : completable_top_field K :=
 local attribute [instance] linear_ordered_comm_group_with_zero.topological_space
 
 /-- The extension of the valuation of a valued field to the completion of the field. -/
-noncomputable def valued.extension : hat K → Γ₀ K :=
-completion.dense_inducing_coe.extend (v : K → Γ₀ K)
+noncomputable def valued.extension : hat K → Γ₀ :=
+completion.dense_inducing_coe.extend (v : K → Γ₀)
 
-lemma valued.continuous_extension : continuous (valued.extension : hat K → Γ₀ K) :=
+lemma valued.continuous_extension : continuous (valued.extension : hat K → Γ₀) :=
  begin
   refine completion.dense_inducing_coe.continuous_extend _,
   intro x₀,
@@ -215,12 +217,12 @@ lemma valued.continuous_extension : continuous (valued.extension : hat K → Γ
     intro γ₀,
     rw valued.mem_nhds,
     exact ⟨γ₀, by simp⟩ },
-  { have preimage_one : v ⁻¹' {(1 : Γ₀ K)} ∈ 𝓝 (1 : K),
-    { have : v (1 : K) ≠ 0, { rw valuation.map_one, exact zero_ne_one.symm },
+  { have preimage_one : v ⁻¹' {(1 : Γ₀)} ∈ 𝓝 (1 : K),
+    { have : (v (1 : K) : Γ₀) ≠ 0, { rw valuation.map_one, exact zero_ne_one.symm },
       convert valued.loc_const this,
       ext x,
       rw [valuation.map_one, mem_preimage, mem_singleton_iff, mem_set_of_eq] },
-    obtain ⟨V, V_in, hV⟩ : ∃ V ∈ 𝓝 (1 : hat K), ∀ x : K, (x : hat K) ∈ V → v x = 1,
+    obtain ⟨V, V_in, hV⟩ : ∃ V ∈ 𝓝 (1 : hat K), ∀ x : K, (x : hat K) ∈ V → (v x : Γ₀) = 1,
     { rwa [completion.dense_inducing_coe.nhds_eq_comap, mem_comap] at preimage_one },
 
     have : ∃ V' ∈ (𝓝 (1 : hat K)), (0 : hat K) ∉ V' ∧ ∀ x y ∈ V', x*y⁻¹ ∈ V,
@@ -261,14 +263,14 @@ lemma valued.continuous_extension : continuous (valued.extension : hat K → Γ
       rintro rfl,
       exact mul_ne_zero (ne_of_mem_of_not_mem y₀_in zeroV') h H },
     rcases this with ⟨z₀, y₀, y₀_in, hz₀, z₀_ne⟩,
-    have vz₀_ne: v z₀ ≠ 0 := by rwa valuation.ne_zero_iff,
+    have vz₀_ne: (v z₀ : Γ₀) ≠ 0 := by rwa valuation.ne_zero_iff,
     refine ⟨v z₀, _⟩,
     rw [linear_ordered_comm_group_with_zero.tendsto_of_ne_zero vz₀_ne, mem_comap],
     use [(λ x, x*x₀) '' V', nhds_right],
     intros x x_in,
     rcases mem_preimage.1 x_in with ⟨y, y_in, hy⟩, clear x_in,
     change y*x₀ = coe x at hy,
-    have : v (x*z₀⁻¹) = 1,
+    have : (v (x*z₀⁻¹) : Γ₀) = 1,
     { apply hV,
       have : ((z₀⁻¹ : K) : hat K) = z₀⁻¹,
       from ring_hom.map_inv (completion.coe_ring_hom : K →+* hat K) z₀,
@@ -281,19 +283,19 @@ lemma valued.continuous_extension : continuous (valued.extension : hat K → Γ
 end
 
 @[norm_cast]
-lemma valued.extension_extends (x : K) : valued.extension (x : hat K) = v x :=
+lemma valued.extension_extends (x : K) : (valued.extension (x : hat K) : Γ₀) = v x :=
 begin
-  haveI : t2_space (valued.Γ₀ K) := regular_space.t2_space _,
+  haveI : t2_space Γ₀ := regular_space.t2_space _,
   refine completion.dense_inducing_coe.extend_eq_of_tendsto _,
   rw ← completion.dense_inducing_coe.nhds_eq_comap,
   exact valued.continuous_valuation.continuous_at,
 end
 
 /-- the extension of a valuation on a division ring to its completion. -/
 noncomputable def valued.extension_valuation :
-  valuation (hat K) (Γ₀ K) :=
+  valuation (hat K) Γ₀ :=
 { to_fun := valued.extension,
-  map_zero' := by { simpa [← v.map_zero, ← valued.extension_extends (0 : K)] },
+  map_zero' := by { rw [← v.map_zero, ← valued.extension_extends (0 : K)], refl, },
   map_one' := by { rw [← completion.coe_one, valued.extension_extends (1 : K)],
                    exact valuation.map_one _ },
   map_mul' := λ x y, begin
@@ -312,7 +314,7 @@ noncomputable def valued.extension_valuation :
   map_add_le_max' := λ x y, begin
     rw le_max_iff,
     apply completion.induction_on₂ x y,
-    { have cont : continuous (valued.extension : hat K → Γ₀ K) := valued.continuous_extension,
+    { have cont : continuous (valued.extension : hat K → Γ₀) := valued.continuous_extension,
       exact  (is_closed_le (cont.comp continuous_add) $ cont.comp continuous_fst).union
         (is_closed_le (cont.comp continuous_add) $ cont.comp continuous_snd) },
     { intros x y,