diff --git a/Mathlib/Algebra/Algebra/Equiv.lean b/Mathlib/Algebra/Algebra/Equiv.lean
index e079099d6851dc..ade3aa884f2184 100644
--- a/Mathlib/Algebra/Algebra/Equiv.lean
+++ b/Mathlib/Algebra/Algebra/Equiv.lean
@@ -763,6 +763,11 @@ def algHomUnitsEquiv (R S : Type*) [CommSemiring R] [Semiring S] [Algebra R S] :
 instance _root_.Finite.algEquiv [Finite (A₁ →ₐ[R] A₂)] : Finite (A₁ ≃ₐ[R] A₂) :=
   Finite.of_injective _ AlgEquiv.coe_algHom_injective
 
+-- TODO Morally this is just `isLocalHom_equiv`: can we obviate the need for this instance?
+instance : IsLocalHom e.toAlgHom := by
+  have : IsLocalHom e.toRingEquiv := inferInstance
+  exact ⟨this.map_nonunit⟩
+
 end Semiring
 
 end AlgEquiv
diff --git a/Mathlib/RingTheory/LocalRing/ResidueField/Basic.lean b/Mathlib/RingTheory/LocalRing/ResidueField/Basic.lean
index 92801ec958611a..25ccf5295ce240 100644
--- a/Mathlib/RingTheory/LocalRing/ResidueField/Basic.lean
+++ b/Mathlib/RingTheory/LocalRing/ResidueField/Basic.lean
@@ -113,6 +113,7 @@ theorem map_comp_residue (f : R →+* S) [IsLocalHom f] :
     (ResidueField.map f).comp (residue R) = (residue S).comp f :=
   rfl
 
+@[simp]
 theorem map_residue (f : R →+* S) [IsLocalHom f] (r : R) :
     ResidueField.map f (residue R r) = residue S (f r) :=
   rfl
@@ -206,6 +207,63 @@ lemma finite_of_finite [Module.Finite R S] (hfin : Finite (ResidueField R)) :
 
 end FiniteDimensional
 
+omit [IsLocalRing R]
+
+variable [Algebra R S] [Algebra R T]
+
+/-- A local algebra homomorphism induces an algebra homomorphism on the residue fields.
+
+See `mapAlgHom'` for a variant where the base ring `R` is also quotiented. -/
+noncomputable def mapAlgHom (e : S →ₐ[R] T) [IsLocalHom e] :
+    ResidueField S →ₐ[R] ResidueField T where
+  __ := map e
+  commutes' x := by
+    simp [IsScalarTower.algebraMap_apply R S (ResidueField S),
+      IsScalarTower.algebraMap_apply R T (ResidueField T)]
+
+@[simp]
+theorem mapAlgHom_residue (e : S →ₐ[R] T) [IsLocalHom e] (x : S) :
+    mapAlgHom e (residue S x) = residue T (e x) :=
+  rfl
+
+/-- A local algebra isomorphism induces an algebra isomorphism on the residue fields.
+
+See `mapAlgEquiv'` for a variant where the base ring `R` is also quotiented. -/
+noncomputable def mapAlgEquiv (e : S ≃ₐ[R] T) : ResidueField S ≃ₐ[R] ResidueField T where
+  __ := mapAlgHom e.toAlgHom
+  __ := mapEquiv e.toRingEquiv
+
+@[simp]
+theorem mapAlgEquiv_residue (e : S ≃ₐ[R] T) (x : S) :
+    mapAlgEquiv e (residue S x) = residue T (e x) :=
+  rfl
+
+variable [IsLocalHom (algebraMap R S)] [IsLocalHom (algebraMap R T)]
+
+/-- A local algebra homomorphism induces an algebra homomorphism on the residue fields.
+
+See `mapAlgHom` for a variant where the base ring `R` is not quotiented. -/
+noncomputable def mapAlgHom' (e : S →ₐ[R] T) [IsLocalHom e] :
+    ResidueField S →ₐ[ResidueField R] ResidueField T :=
+  (mapAlgHom e).extendScalarsOfSurjective residue_surjective
+
+@[simp]
+theorem mapAlgHom'_residue [IsLocalRing R] (e : S →ₐ[R] T) [IsLocalHom e] (x : S) :
+    mapAlgHom' e (residue S x) = residue T (e x) :=
+  rfl
+
+/-- A local algebra isomorphism induces an algebra isomorphism on the residue fields.
+
+See `mapAlgEquiv` for a variant where the base ring `R` is not quotiented. -/
+noncomputable def mapAlgEquiv' (e : S ≃ₐ[R] T) :
+    ResidueField S ≃ₐ[ResidueField R] ResidueField T :=
+  (mapAlgEquiv e).extendScalarsOfSurjective residue_surjective
+
+@[simp]
+theorem mapAlgEquiv'_residue [IsLocalRing R] (e : S ≃ₐ[R] T) (x : S) :
+    mapAlgEquiv' e (residue S x) = residue T (e x) :=
+  rfl
+
 end ResidueField
 
 end