[Merged by Bors] - feat(RingTheory/Localization/AtPrime/Basic): add variants of localAlgHom and localAlgEquiv

Mathlib/RingTheory/Localization/AtPrime/Basic.lean

@@ -296,8 +296,10 @@ noncomputable def localRingEquiv (J : Ideal P) [J.IsPrime] (f : R ≃+* P) (hIJ
   right_inv x := by simp [localRingHom, map_map]
 
 variable {S} in
-/-- For an algebra hom `f : S →ₐ[R] P` and a prime ideal `J` in `P`, the induced ring hom from the
-localization of `R` at `J ∩ S` to the localization of `P` at `J`. -/
+/-- For an `R`-algebra homomorphism `f : S →ₐ[R] P` and prime ideals `I = f⁻¹(J)`, the induced
+`R`-algebra homomorphism from the localization of `S` at `I` to the localization of `P` at `J`.
+
+See `localAlgHom'` for a variant where the base ring `R` is also localized. -/
 noncomputable def localAlgHom [Algebra R P] (I : Ideal S) [I.IsPrime] (J : Ideal P) [J.IsPrime]
     (f : S →ₐ[R] P) (hIJ : I = J.comap f) :
     Localization.AtPrime I →ₐ[R] Localization.AtPrime J where
@@ -312,7 +314,9 @@ variable {S} in
     localAlgHom I J f hIJ x = localRingHom I J f.toRingHom hIJ x := rfl
 
 variable {S} in
-/-- Isomorphic algebras have isomorphic localizations. -/
+/-- Isomorphic algebras have isomorphic localizations.
+
+See `localAlgEquiv'` for a variant where the base ring is also localized. -/
 @[simps]
 noncomputable def localAlgEquiv [Algebra R P] (I : Ideal S) [I.IsPrime] (J : Ideal P) [J.IsPrime]
     (f : S ≃ₐ[R] P) (hIJ : I = J.comap f) :
@@ -349,8 +353,8 @@ namespace AtPrime
 
 section
 
-variable {A B C : Type*} [CommRing A] [CommRing B] [CommRing C] [Algebra A B] [Algebra A C]
-  [Algebra R A] [Algebra R B] [IsScalarTower R A B] [Algebra B C] [IsScalarTower A B C]
+variable {A B C : Type*} [CommSemiring A] [CommSemiring B] [Algebra R A] [Algebra R B] [Algebra A B]
+  [IsScalarTower R A B] [CommSemiring C] [Algebra A C] [Algebra B C] [IsScalarTower A B C]
 
 /-- If `P` lies over `p`, then `Localization.AtPrime P` is an algebra over `Localization.AtPrime p`.
 This is not an instance for performance reasons and to avoid diamonds in the situation where the top
@@ -414,6 +418,34 @@ theorem mapPiEvalRingHom_algebraMap_apply {r : Π i, R i} :
 
 end AtPrime
 
+section localAlg
+
+open AtPrime
+
+variable {S} [Algebra R P] (J : Ideal S) (K : Ideal P) [J.IsPrime] [K.IsPrime]
+  [J.LiesOver I] [Algebra (Localization.AtPrime I) (Localization.AtPrime J)] [IsLiesOverAlgebra I J]
+  [K.LiesOver I] [Algebra (Localization.AtPrime I) (Localization.AtPrime K)] [IsLiesOverAlgebra I K]
+
+/-- For an `R`-algebra homomorphism `f : S →ₐ[R] P` and prime ideals `J = f⁻¹(K)` lying over `I`,
+the induced algebra homomorphism from the localization of `S` at `J` to the localization of `P` at
+`K` over the localization of `R` at `I`.
+
+See `localAlgHom` for a variant where the base ring `R` is not localized. -/
+@[simps!]
+noncomputable def localAlgHom' (f : S →ₐ[R] P) (h : J = K.comap f) :
+    Localization.AtPrime J →ₐ[Localization.AtPrime I] Localization.AtPrime K :=
+  (localAlgHom J K f h).extendScalarsOfIsLocalization (Localization.AtPrime I) I.primeCompl
+
+/-- Isomorphic algebras have isomorphic localizations.
+
+See `localAlgEquiv` for a variant where the base ring is not localized. -/
+@[simps!]
+noncomputable def localAlgEquiv' (f : S ≃ₐ[R] P) (h : J = K.comap f) :
+    Localization.AtPrime J ≃ₐ[Localization.AtPrime I] Localization.AtPrime K :=
+  (localAlgEquiv J K f h).extendScalarsOfIsLocalization (Localization.AtPrime I) I.primeCompl
+
+end localAlg
+
 end Localization
 
 section

Mathlib/RingTheory/Localization/Basic.lean

@@ -687,8 +687,8 @@ theorem IsLocalization.algHom_ext {R A L B : Type*}
 
 section extend
 
-variable {R A B : Type*} [CommRing R] [CommRing A] [CommRing B]
-  (S : Type*) [CommRing S] [Algebra R S] (M : Submonoid R) [IsLocalization M S]
+variable {R A B : Type*} [CommSemiring R] [Semiring A] [Semiring B]
+  (S : Type*) [CommSemiring S] [Algebra R S] (M : Submonoid R) [IsLocalization M S]
   [Algebra R A] [Algebra S A] [IsScalarTower R S A]
   [Algebra R B] [Algebra S B] [IsScalarTower R S B]