feat(ring_theory/valuation/extend_to_localization): Extending valuations to localizations. (#13610)

adamtopaz · alreadydone · adamtopaz · commit 64b3576ff5bb · 2022-04-29T15:58:59.000Z
Co-authored-by: Junyan Xu &lt;junyanxumath@gmail.com&gt;
diff --git a/src/ring_theory/valuation/basic.lean b/src/ring_theory/valuation/basic.lean
@@ -181,6 +181,10 @@ def comap {S : Type*} [ring S] (f : S →+* R) (v : valuation R Γ₀) :
   map_add_le_max' := λ x y, by simp only [comp_app, map_add, f.map_add],
   .. v.to_monoid_with_zero_hom.comp f.to_monoid_with_zero_hom, }
 
+@[simp]
+lemma comap_apply {S : Type*} [ring S] (f : S →+* R) (v : valuation R Γ₀) (s : S) :
+  v.comap f s = v (f s) := rfl
+
 @[simp] lemma comap_id : v.comap (ring_hom.id R) = v := ext $ λ r, rfl
 
 lemma comap_comp {S₁ : Type*} {S₂ : Type*} [ring S₁] [ring S₂] (f : S₁ →+* S₂) (g : S₂ →+* R) :
diff --git a/src/ring_theory/valuation/extend_to_localization.lean b/src/ring_theory/valuation/extend_to_localization.lean
@@ -0,0 +1,49 @@
+/-
+Copyright (c) 2022 Adam Topaz. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Adam Topaz
+-/
+import ring_theory.localization.at_prime
+import ring_theory.valuation.basic
+
+/-!
+
+# Extending valuations to a localization
+
+We show that, given a valuation `v` taking values in a linearly ordered commutative *group*
+with zero `Γ`, and a submonoid `S` of `v.supp.prime_compl`, the valuation `v` can be naturally
+extended to the localization `S⁻¹A`.
+
+-/
+
+variables
+  {A : Type*} [comm_ring A]
+  {Γ : Type*} [linear_ordered_comm_group_with_zero Γ] (v : valuation A Γ)
+  {S : submonoid A} (hS : S ≤ v.supp.prime_compl)
+  (B : Type*) [comm_ring B] [algebra A B] [is_localization S B]
+
+/-- We can extend a valuation `v` on a ring to a localization at a submonoid of
+the complement of `v.supp`. -/
+noncomputable
+def valuation.extend_to_localization : valuation B Γ :=
+let f := is_localization.to_localization_map S B,
+    h : ∀ s : S, is_unit (v.1.to_monoid_hom s) := λ s, is_unit_iff_ne_zero.2 (hS s.2) in
+{ map_zero' := by convert f.lift_eq _ 0; simp,
+  map_add_le_max' := λ x y, begin
+    obtain ⟨a,b,s,rfl,rfl⟩ : ∃ (a b : A) (s : S), f.mk' a s = x ∧ f.mk' b s = y,
+    { obtain ⟨a,s,rfl⟩ := f.mk'_surjective x,
+      obtain ⟨b,t,rfl⟩ := f.mk'_surjective y,
+      use [a * t, b * s, s * t], split;
+      { rw [f.mk'_eq_iff_eq, submonoid.coe_mul], ring_nf } },
+    convert_to f.lift h (f.mk' (a+b) s) ≤ max (f.lift h _) (f.lift h _),
+    { refine congr_arg (f.lift h) (is_localization.eq_mk'_iff_mul_eq.2 _),
+      rw [add_mul, map_add], iterate 2 { erw is_localization.mk'_spec } },
+    iterate 3 { rw f.lift_mk' }, rw max_mul_mul_right,
+    apply mul_le_mul_right' (v.map_add a b),
+  end,
+..f.lift h }
+
+@[simp]
+lemma valuation.extend_to_localization_apply_map_apply (a : A) :
+  v.extend_to_localization hS B (algebra_map A B a) = v a :=
+submonoid.localization_map.lift_eq _ _ a
