feat(ring_theory/ideal/local_ring): Isomorphisms are local (#8850)

Adds the fact that isomorphisms (and ring equivs) are local ring homomorphisms.



Co-authored-by: Johan Commelin <johan@commelin.net>

src/ring_theory/ideal/local_ring.lean

@@ -176,6 +176,14 @@ instance is_local_ring_hom_comp [semiring R] [semiring S] [semiring T]
   is_local_ring_hom (g.comp f) :=
 { map_nonunit := λ a, is_local_ring_hom.map_nonunit a ∘ is_local_ring_hom.map_nonunit (f a) }
 
+instance is_local_ring_hom_equiv [semiring R] [semiring S] (f : R ≃+* S) :
+  is_local_ring_hom f.to_ring_hom :=
+{ map_nonunit := λ a ha,
+  begin
+    convert f.symm.to_ring_hom.is_unit_map ha,
+    rw ring_equiv.symm_to_ring_hom_apply_to_ring_hom_apply,
+  end }
+
 @[simp] lemma is_unit_of_map_unit [semiring R] [semiring S] (f : R →+* S) [is_local_ring_hom f]
   (a) (h : is_unit (f a)) : is_unit a :=
 is_local_ring_hom.map_nonunit a h
@@ -185,6 +193,23 @@ theorem of_irreducible_map [semiring R] [semiring S] (f : R →+* S) [h : is_loc
 ⟨λ h, hfx.not_unit $ is_unit.map f.to_monoid_hom h, λ p q hx, let ⟨H⟩ := h in
 or.imp (H p) (H q) $ hfx.is_unit_or_is_unit $ f.map_mul p q ▸ congr_arg f hx⟩
 
+section
+open category_theory
+
+lemma is_local_ring_hom_of_iso {R S : CommRing} (f : R ≅ S) : is_local_ring_hom f.hom :=
+{ map_nonunit := λ a ha,
+  begin
+    convert f.inv.is_unit_map ha,
+    rw category_theory.coe_hom_inv_id,
+  end }
+
+@[priority 100] -- see Note [lower instance priority]
+instance is_local_ring_hom_of_is_iso {R S : CommRing} (f : R ⟶ S) [is_iso f] :
+  is_local_ring_hom f :=
+is_local_ring_hom_of_iso (as_iso f)
+
+end
+
 section
 open local_ring
 variables [comm_ring R] [local_ring R] [comm_ring S] [local_ring S]