chore(ring_theory/localization/away): split (#19041)

This breaks off a large initial segment of the [longest chain](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/port.20progress/near/359494005) remaining to port.



Co-authored-by: Scott Morrison <[email protected]>

src/algebra/category/Ring/instances.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Andrew Yang
 -/
 import algebra.category.Ring.basic
-import ring_theory.localization.away
+import ring_theory.localization.away.basic
 import ring_theory.ideal.local_ring
 
 /-!

src/algebraic_geometry/prime_spectrum/basic.lean

@@ -7,7 +7,7 @@ import algebra.punit_instances
 import linear_algebra.finsupp
 import ring_theory.ideal.over
 import ring_theory.ideal.prod
-import ring_theory.localization.away
+import ring_theory.localization.away.basic
 import ring_theory.nilpotent
 import topology.sets.closeds
 import topology.sober

src/ring_theory/jacobson.lean

@@ -3,7 +3,7 @@ Copyright (c) 2020 Devon Tuma. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Devon Tuma
 -/
-import ring_theory.localization.away
+import ring_theory.localization.away.basic
 import ring_theory.ideal.over
 import ring_theory.jacobson_ideal
 

src/ring_theory/local_properties.lean

@@ -5,7 +5,7 @@ Authors: Andrew Yang
 -/
 import ring_theory.finite_type
 import ring_theory.localization.at_prime
-import ring_theory.localization.away
+import ring_theory.localization.away.basic
 import ring_theory.localization.integer
 import ring_theory.localization.submodule
 import ring_theory.nilpotent

src/ring_theory/localization/away/adjoin_root.lean

@@ -0,0 +1,37 @@
+/-
+Copyright (c) 2018 Kenny Lau. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kenny Lau, Mario Carneiro, Johan Commelin, Amelia Livingston, Anne Baanen
+-/
+import ring_theory.adjoin_root
+import ring_theory.localization.away.basic
+
+/-!
+The `R`-`alg_equiv` between the localization of `R` away from `r` and
+`R` with an inverse of `r` adjoined.
+-/
+
+open polynomial adjoin_root localization
+
+variables {R : Type*} [comm_ring R]
+
+local attribute [instance] is_localization.alg_hom_subsingleton adjoin_root.alg_hom_subsingleton
+
+/-- The `R`-`alg_equiv` between the localization of `R` away from `r` and
+    `R` with an inverse of `r` adjoined. -/
+noncomputable def localization.away_equiv_adjoin (r : R) : away r ≃ₐ[R] adjoin_root (C r * X - 1) :=
+alg_equiv.of_alg_hom
+  { commutes' := is_localization.away.away_map.lift_eq r
+      (is_unit_of_mul_eq_one _ _ $ root_is_inv r), .. away_lift _ r _ }
+  (lift_hom _ (is_localization.away.inv_self r) $ by simp only
+    [map_sub, map_mul, aeval_C, aeval_X, is_localization.away.mul_inv_self, aeval_one, sub_self])
+  (subsingleton.elim _ _)
+  (subsingleton.elim _ _)
+
+lemma is_localization.adjoin_inv (r : R) : is_localization.away r (adjoin_root $ C r * X - 1) :=
+is_localization.is_localization_of_alg_equiv _ (localization.away_equiv_adjoin r)
+
+lemma is_localization.away.finite_presentation (r : R) {S} [comm_ring S] [algebra R S]
+  [is_localization.away r S] : algebra.finite_presentation R S :=
+(adjoin_root.finite_presentation _).equiv $ (localization.away_equiv_adjoin r).symm.trans $
+  is_localization.alg_equiv (submonoid.powers r) _ _

src/ring_theory/localization/away.lean → src/ring_theory/localization/away/basic.lean

@@ -3,7 +3,7 @@ Copyright (c) 2018 Kenny Lau. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kenny Lau, Mario Carneiro, Johan Commelin, Amelia Livingston, Anne Baanen
 -/
-import ring_theory.adjoin_root
+import ring_theory.unique_factorization_domain
 import ring_theory.localization.basic
 
 /-!
@@ -172,34 +172,13 @@ end localization
 
 end comm_semiring
 
-open polynomial adjoin_root localization
+open localization
 
 variables {R : Type*} [comm_ring R]
 
-local attribute [instance] is_localization.alg_hom_subsingleton adjoin_root.alg_hom_subsingleton
-
-/-- The `R`-`alg_equiv` between the localization of `R` away from `r` and
-    `R` with an inverse of `r` adjoined. -/
-noncomputable def localization.away_equiv_adjoin (r : R) : away r ≃ₐ[R] adjoin_root (C r * X - 1) :=
-alg_equiv.of_alg_hom
-  { commutes' := is_localization.away.away_map.lift_eq r
-      (is_unit_of_mul_eq_one _ _ $ root_is_inv r), .. away_lift _ r _ }
-  (lift_hom _ (is_localization.away.inv_self r) $ by simp only
-    [map_sub, map_mul, aeval_C, aeval_X, is_localization.away.mul_inv_self, aeval_one, sub_self])
-  (subsingleton.elim _ _)
-  (subsingleton.elim _ _)
-
-lemma is_localization.adjoin_inv (r : R) : is_localization.away r (adjoin_root $ C r * X - 1) :=
-is_localization.is_localization_of_alg_equiv _ (localization.away_equiv_adjoin r)
-
-lemma is_localization.away.finite_presentation (r : R) {S} [comm_ring S] [algebra R S]
-  [is_localization.away r S] : algebra.finite_presentation R S :=
-(adjoin_root.finite_presentation _).equiv $ (localization.away_equiv_adjoin r).symm.trans $
-  is_localization.alg_equiv (submonoid.powers r) _ _
-
 section num_denom
 
-open multiplicity unique_factorization_monoid is_localization
+open unique_factorization_monoid is_localization
 
 variable (x : R)
 

src/ring_theory/ring_hom/integral.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Andrew Yang
 -/
 import ring_theory.ring_hom_properties
+import ring_theory.integral_closure
 
 /-!
 

src/ring_theory/ring_hom_properties.lean

@@ -6,7 +6,7 @@ Authors: Andrew Yang
 import algebra.category.Ring.constructions
 import algebra.category.Ring.colimits
 import category_theory.isomorphism
-import ring_theory.localization.away
+import ring_theory.localization.away.basic
 import ring_theory.is_tensor_product
 
 /-!