diff --git a/Mathlib/RingTheory/Spectrum/Maximal/Localization.lean b/Mathlib/RingTheory/Spectrum/Maximal/Localization.lean
index c50deed3b78a6a..bd4d0585ad626b 100644
--- a/Mathlib/RingTheory/Spectrum/Maximal/Localization.lean
+++ b/Mathlib/RingTheory/Spectrum/Maximal/Localization.lean
@@ -71,7 +71,7 @@ abbrev PiLocalization : Type _ := Π I : MaximalSpectrum R, Localization.AtPrime
 
 /-- The canonical ring homomorphism from a commutative semiring to the product of its
 localizations at all maximal ideals. It is always injective. -/
-def toPiLocalization : R →+* PiLocalization R := algebraMap R _
+def toPiLocalization : R →ₐ[R] PiLocalization R := Algebra.ofId R (PiLocalization R)
 
 theorem toPiLocalization_injective : Function.Injective (toPiLocalization R) := fun r r' eq ↦ by
   rw [← one_mul r, ← one_mul r']
@@ -92,7 +92,7 @@ noncomputable def mapPiLocalization : PiLocalization R →+* PiLocalization S :=
 
 theorem mapPiLocalization_naturality :
     (mapPiLocalization f hf).comp (toPiLocalization R) =
-      (toPiLocalization S).comp f := by
+      (toPiLocalization S).toRingHom.comp f := by
   ext r I
   change Localization.localRingHom _ _ _ rfl (algebraMap _ _ r) = algebraMap _ _ (f r)
   simp_rw [← IsLocalization.mk'_one (M := (I.1.comap f).primeCompl), Localization.localRingHom_mk',
@@ -152,7 +152,8 @@ theorem finite_of_toPiLocalization_surjective
     Finite (MaximalSpectrum R) := by
   replace surj := mapPiLocalization_bijective _ ⟨toPiLocalization_injective R, surj⟩
     |>.2.comp surj
-  rw [← RingHom.coe_comp, mapPiLocalization_naturality, RingHom.coe_comp] at surj
+  rw [← AlgHom.coe_toRingHom,
+    ← RingHom.coe_comp, mapPiLocalization_naturality, RingHom.coe_comp] at surj
   exact finite_of_toPiLocalization_pi_surjective surj.of_comp
 
 end MaximalSpectrum
@@ -164,7 +165,7 @@ abbrev PiLocalization : Type _ := Π p : PrimeSpectrum R, Localization p.asIdeal
 
 /-- The canonical ring homomorphism from a commutative semiring to the product of its
 localizations at all prime ideals. It is always injective. -/
-def toPiLocalization : R →+* PiLocalization R := algebraMap R _
+def toPiLocalization : R →ₐ[R] PiLocalization R := Algebra.ofId R (PiLocalization R)
 
 theorem toPiLocalization_injective : Function.Injective (toPiLocalization R) :=
   fun _ _ eq ↦ MaximalSpectrum.toPiLocalization_injective R <|
@@ -172,8 +173,8 @@ theorem toPiLocalization_injective : Function.Injective (toPiLocalization R) :=
 
 /-- The projection from the product of localizations at primes to the product of
 localizations at maximal ideals. -/
-def piLocalizationToMaximal : PiLocalization R →+* MaximalSpectrum.PiLocalization R :=
-  Pi.ringHom fun I ↦ Pi.evalRingHom _ I.toPrimeSpectrum
+def piLocalizationToMaximal : PiLocalization R →ₐ[R] MaximalSpectrum.PiLocalization R :=
+  Pi.algHom _ _  fun I ↦ Pi.evalAlgHom _ _ I.toPrimeSpectrum
 
 open scoped Classical in
 theorem piLocalizationToMaximal_surjective : Function.Surjective (piLocalizationToMaximal R) :=
@@ -218,7 +219,7 @@ noncomputable def mapPiLocalization : PiLocalization R →+* PiLocalization S :=
   Pi.ringHom fun I ↦ (Localization.localRingHom _ I.1 f rfl).comp (Pi.evalRingHom _ (comap f I))
 
 theorem mapPiLocalization_naturality :
-    (mapPiLocalization f).comp (toPiLocalization R) = (toPiLocalization S).comp f := by
+    (mapPiLocalization f).comp (toPiLocalization R) = (toPiLocalization S).toRingHom.comp f := by
   ext r I
   change Localization.localRingHom _ _ _ rfl (algebraMap _ _ r) = algebraMap _ _ (f r)
   simp_rw [← IsLocalization.mk'_one (M := (I.1.comap f).primeCompl), Localization.localRingHom_mk',
@@ -247,7 +248,7 @@ variable {ι} (R : ι → Type*) [∀ i, CommSemiring (R i)] [∀ i, Nontrivial
 theorem toPiLocalization_not_surjective_of_infinite [Infinite ι] :
     ¬ Function.Surjective (toPiLocalization (Π i, R i)) :=
   fun surj ↦ MaximalSpectrum.toPiLocalization_not_surjective_of_infinite R <| by
-    rw [← piLocalizationToMaximal_comp_toPiLocalization]
+    rw [← AlgHom.coe_toRingHom, ← piLocalizationToMaximal_comp_toPiLocalization]
     exact (piLocalizationToMaximal_surjective _).comp surj
 
 variable {R}
@@ -264,7 +265,8 @@ theorem finite_of_toPiLocalization_surjective
     (surj : Function.Surjective (toPiLocalization R)) :
     Finite (PrimeSpectrum R) := by
   replace surj := (mapPiLocalization_bijective _ ⟨toPiLocalization_injective R, surj⟩).2.comp surj
-  rw [← RingHom.coe_comp, mapPiLocalization_naturality, RingHom.coe_comp] at surj
+  rw [← AlgHom.coe_toRingHom,
+    ← RingHom.coe_comp, mapPiLocalization_naturality, RingHom.coe_comp] at surj
   exact finite_of_toPiLocalization_pi_surjective surj.of_comp
 
 end PrimeSpectrum
diff --git a/Mathlib/RingTheory/Spectrum/Prime/Topology.lean b/Mathlib/RingTheory/Spectrum/Prime/Topology.lean
index 8654ec4f0b46da..0cc80faeddaa6e 100644
--- a/Mathlib/RingTheory/Spectrum/Prime/Topology.lean
+++ b/Mathlib/RingTheory/Spectrum/Prime/Topology.lean
@@ -718,10 +718,20 @@ canonically isomorphic to the product of its localizations at the (finitely many
 @[stacks 00JA
 "See also `PrimeSpectrum.discreteTopology_iff_finite_isMaximal_and_sInf_le_nilradical`."]
 def _root_.MaximalSpectrum.toPiLocalizationEquiv :
-    R ≃+* MaximalSpectrum.PiLocalization R :=
+    R ≃ₐ[R] MaximalSpectrum.PiLocalization R :=
   .ofBijective _ ⟨MaximalSpectrum.toPiLocalization_injective R,
     maximalSpectrumToPiLocalization_surjective_of_discreteTopology R⟩
 
+@[simp]
+theorem _root_.MaximalSpectrum.toPiLocalizationEquiv_apply (x : R) :
+    MaximalSpectrum.toPiLocalizationEquiv R x = algebraMap R _ x :=
+  rfl
+
+@[simp]
+theorem _root_.MaximalSpectrum.toPiLocalizationEquiv_apply_apply (x : R) (I : MaximalSpectrum R) :
+    MaximalSpectrum.toPiLocalizationEquiv R x I = algebraMap R _ x :=
+  rfl
+
 theorem discreteTopology_iff_toPiLocalization_surjective {R} [CommSemiring R] :
     DiscreteTopology (PrimeSpectrum R) ↔ Function.Surjective (toPiLocalization R) :=
   ⟨fun _ ↦ toPiLocalization_surjective_of_discreteTopology _,
@@ -732,10 +742,24 @@ theorem discreteTopology_iff_toPiLocalization_bijective {R} [CommSemiring R] :
   discreteTopology_iff_toPiLocalization_surjective.trans
     (and_iff_right <| toPiLocalization_injective _).symm
 
-lemma toPiLocalization_bijective {R : Type*} [CommRing R]
-    [DiscreteTopology (PrimeSpectrum R)] : Function.Bijective (toPiLocalization R) :=
+variable {R} in
+lemma toPiLocalization_bijective : Function.Bijective (toPiLocalization R) :=
   discreteTopology_iff_toPiLocalization_bijective.mp inferInstance
 
+/-- If the prime spectrum of a commutative semiring R has discrete Zariski topology, then R is
+canonically isomorphic to the product of its localizations at the (finitely many) prime ideals. -/
+def toPiLocalizationEquiv : R ≃ₐ[R] PiLocalization R :=
+  .ofBijective _ toPiLocalization_bijective
+
+@[simp]
+theorem toPiLocalizationEquiv_apply (x : R) : toPiLocalizationEquiv R x = algebraMap R _ x :=
+  rfl
+
+@[simp]
+theorem toPiLocalizationEquiv_apply_apply (x : R) (I : PrimeSpectrum R) :
+    toPiLocalizationEquiv R x I = algebraMap R _ x :=
+  rfl
+
 end DiscreteTopology
 
 section Order