feat: port RingTheory.Localization.Away.AdjoinRoot (#4725)

Author: joneugster

Mathlib.lean

@@ -2279,6 +2279,7 @@ import Mathlib.RingTheory.JacobsonIdeal
 import Mathlib.RingTheory.LaurentSeries
 import Mathlib.RingTheory.Localization.AsSubring
 import Mathlib.RingTheory.Localization.AtPrime
+import Mathlib.RingTheory.Localization.Away.AdjoinRoot
 import Mathlib.RingTheory.Localization.Away.Basic
 import Mathlib.RingTheory.Localization.Basic
 import Mathlib.RingTheory.Localization.Cardinality

Mathlib/RingTheory/AdjoinRoot.lean

@@ -350,18 +350,18 @@ theorem liftHom_of {x : R} : liftHom f a hfx (of f x) = algebraMap _ _ x :=
 section AdjoinInv
 
 @[simp]
-theorem root_is_inv (r : R) : of _ r * root (C r * X - 1) = 1 := by
+theorem root_isInv (r : R) : of _ r * root (C r * X - 1) = 1 := by
   convert sub_eq_zero.1 ((eval₂_sub _).symm.trans <| eval₂_root <| C r * X - 1) <;>
     simp only [eval₂_mul, eval₂_C, eval₂_X, eval₂_one]
-#align adjoin_root.root_is_inv AdjoinRoot.root_is_inv
+#align adjoin_root.root_is_inv AdjoinRoot.root_isInv
 
 theorem algHom_subsingleton {S : Type _} [CommRing S] [Algebra R S] {r : R} :
     Subsingleton (AdjoinRoot (C r * X - 1) →ₐ[R] S) :=
   ⟨fun f g =>
     algHom_ext
       (@inv_unique _ _ (algebraMap R S r) _ _
-        (by rw [← f.commutes, ← f.map_mul, algebraMap_eq, root_is_inv, map_one])
-        (by rw [← g.commutes, ← g.map_mul, algebraMap_eq, root_is_inv, map_one]))⟩
+        (by rw [← f.commutes, ← f.map_mul, algebraMap_eq, root_isInv, map_one])
+        (by rw [← g.commutes, ← g.map_mul, algebraMap_eq, root_isInv, map_one]))⟩
 #align adjoin_root.alg_hom_subsingleton AdjoinRoot.algHom_subsingleton
 
 end AdjoinInv

Mathlib/RingTheory/Localization/Away/AdjoinRoot.lean

@@ -0,0 +1,53 @@
+/-
+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
+
+! This file was ported from Lean 3 source module ring_theory.localization.away.adjoin_root
+! leanprover-community/mathlib commit a7c017d750512a352b623b1824d75da5998457d0
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
+-/
+import Mathlib.RingTheory.AdjoinRoot
+import Mathlib.RingTheory.Localization.Away.Basic
+
+/-!
+The `R`-`AlgEquiv` between the localization of `R` away from `r` and
+`R` with an inverse of `r` adjoined.
+-/
+
+open Polynomial AdjoinRoot Localization
+
+variable {R : Type _} [CommRing R]
+
+-- Porting note: removed `IsLocalization.algHom_subsingleton` due to
+-- `cannot find synthesization order for instance`
+attribute [local instance] AdjoinRoot.algHom_subsingleton
+
+/-- The `R`-`AlgEquiv` between the localization of `R` away from `r` and
+    `R` with an inverse of `r` adjoined. -/
+noncomputable def Localization.awayEquivAdjoin (r : R) : Away r ≃ₐ[R] AdjoinRoot (C r * X - 1) :=
+  AlgEquiv.ofAlgHom
+    { awayLift _ r
+      -- Porting note: This argument used to be found automatically, i.e. `_`
+      (isUnit_of_mul_eq_one ((algebraMap R (AdjoinRoot (C r * X - 1))) r) (root (C r * X - 1))
+        (root_isInv r)) with
+      commutes' :=
+        IsLocalization.Away.AwayMap.lift_eq r (isUnit_of_mul_eq_one _ _ <| root_isInv r) }
+    (liftHom _ (IsLocalization.Away.invSelf r) <| by
+      simp only [map_sub, map_mul, aeval_C, aeval_X, IsLocalization.Away.mul_invSelf, aeval_one,
+        sub_self])
+    (Subsingleton.elim _ _)
+    -- Porting note: fix since `IsLocalization.algHom_subsingleton` is no local instance anymore
+    (Subsingleton.elim (h := IsLocalization.algHom_subsingleton (Submonoid.powers r)) _ _)
+#align localization.away_equiv_adjoin Localization.awayEquivAdjoin
+
+theorem IsLocalization.adjoin_inv (r : R) : IsLocalization.Away r (AdjoinRoot <| C r * X - 1) :=
+  IsLocalization.isLocalization_of_algEquiv _ (Localization.awayEquivAdjoin r)
+#align is_localization.adjoin_inv IsLocalization.adjoin_inv
+
+theorem IsLocalization.Away.finitePresentation (r : R) {S} [CommRing S] [Algebra R S]
+    [IsLocalization.Away r S] : Algebra.FinitePresentation R S :=
+  (AdjoinRoot.finitePresentation _).equiv <|
+    (Localization.awayEquivAdjoin r).symm.trans <| IsLocalization.algEquiv (Submonoid.powers r) _ _
+#align is_localization.away.finite_presentation IsLocalization.Away.finitePresentation