refactor(ring_theory/subring): use bundled homs (#2144)

Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>

Author: urkud

src/field_theory/subfield.lean

@@ -34,12 +34,12 @@ instance preimage.is_subfield {K : Type*} [field K]
 { inv_mem := λ a (ha : f a ∈ s), show f a⁻¹ ∈ s,
     by { rw [f.map_inv],
          exact is_subfield.inv_mem ha },
-  ..is_ring_hom.is_subring_preimage f s }
+  ..f.is_subring_preimage s }
 
 instance image.is_subfield {K : Type*} [field K]
   (f : F →+* K) (s : set F) [is_subfield s] : is_subfield (f '' s) :=
 { inv_mem := λ a ⟨x, xmem, ha⟩, ⟨x⁻¹, is_subfield.inv_mem xmem, ha ▸ f.map_inv⟩,
-  ..is_ring_hom.is_subring_image f s }
+  ..f.is_subring_image s }
 
 instance range.is_subfield {K : Type*} [field K]
   (f : F →+* K) : is_subfield (set.range f) :=

src/ring_theory/integral_closure.lean

@@ -78,10 +78,14 @@ theorem fg_adjoin_of_finite {s : set A} (hfs : s.finite)
   (his : ∀ x ∈ s, is_integral R x) : (algebra.adjoin R s : submodule R A).fg :=
 set.finite.induction_on hfs (λ _, ⟨finset.singleton 1, le_antisymm
   (span_le.2 $ set.singleton_subset_iff.2 $ is_submonoid.one_mem _)
-  (show ring.closure _ ⊆ _, by rw set.union_empty; exact
-    set.subset.trans (ring.closure_subset (set.subset.refl _))
-    (λ y ⟨x, hx⟩, hx ▸ mul_one (algebra_map A x) ▸ algebra.smul_def x (1:A) ▸ (mem_coe _).2
-      (submodule.smul_mem _ x $ subset_span $ or.inl rfl)))⟩)
+  begin
+    change ring.closure _ ⊆ _,
+    simp only [set.union_empty, finset.coe_singleton, span_singleton_eq_range,
+      algebra.smul_def, mul_one],
+    -- TODO drop the next `rw` once `algebra_map` will be a bundled `ring_hom`
+    rw [← ring_hom.coe_of (algebra_map A)]; try { apply_instance },
+    exact ring.closure_subset (set.subset.refl _)
+  end⟩)
 (λ a s has hs ih his, by rw [← set.union_singleton, algebra.adjoin_union_coe_submodule]; exact
   fg_mul _ _ (ih $ λ i hi, his i $ set.mem_insert_of_mem a hi)
     (fg_adjoin_singleton_of_integral _ $ his a $ set.mem_insert a s)) his

src/ring_theory/subring.lean

@@ -26,21 +26,18 @@ instance subset.ring {S : set R} [is_subring S] : ring S :=
 
 instance subtype.ring {S : set R} [is_subring S] : ring (subtype S) := subset.ring
 
-namespace is_ring_hom
-
-instance {S : set R} [is_subring S] : is_ring_hom (@subtype.val R S) :=
-by refine {..} ; intros ; refl
+namespace ring_hom
 
 instance is_subring_preimage {R : Type u} {S : Type v} [ring R] [ring S]
-  (f : R → S) [is_ring_hom f] (s : set S) [is_subring s] : is_subring (f ⁻¹' s) := {}
+  (f : R →+* S) (s : set S) [is_subring s] : is_subring (f ⁻¹' s) := {}
 
 instance is_subring_image {R : Type u} {S : Type v} [ring R] [ring S]
-  (f : R → S) [is_ring_hom f] (s : set R) [is_subring s] : is_subring (f '' s) := {}
+  (f : R →+* S) (s : set R) [is_subring s] : is_subring (f '' s) := {}
 
 instance is_subring_set_range {R : Type u} {S : Type v} [ring R] [ring S]
-  (f : R → S) [is_ring_hom f] : is_subring (set.range f) := {}
+  (f : R →+* S) : is_subring (set.range f) := {}
 
-end is_ring_hom
+end ring_hom
 
 /-- Restrict the codomain of a ring homomorphism to a subring that includes the range. -/
 def ring_hom.cod_restrict {R : Type u} {S : Type v} [ring R] [ring S] (f : R →+* S)
@@ -52,20 +49,12 @@ def ring_hom.cod_restrict {R : Type u} {S : Type v} [ring R] [ring S] (f : R →
   map_mul' := λ x y, subtype.eq $ f.map_mul x y,
   map_one' := subtype.eq f.map_one }
 
-instance subtype_val.is_ring_hom {s : set R} [is_subring s] :
-  is_ring_hom (subtype.val : s → R) :=
-{ ..subtype_val.is_add_group_hom, ..subtype_val.is_monoid_hom }
-
-instance coe.is_ring_hom {s : set R} [is_subring s] : is_ring_hom (coe : s → R) :=
-subtype_val.is_ring_hom
-
-instance subtype_mk.is_ring_hom {γ : Type*} [ring γ] {s : set R} [is_subring s] (f : γ → R)
-  [is_ring_hom f] (h : ∀ x, f x ∈ s) : is_ring_hom (λ x, (⟨f x, h x⟩ : s)) :=
-{ ..subtype_mk.is_add_group_hom f h, ..subtype_mk.is_monoid_hom f h }
+/-- Coersion `S → R` as a ring homormorphism-/
+def is_subring.subtype (S : set R) [is_subring S] : S →+* R :=
+⟨coe, rfl, λ _ _, rfl, rfl, λ _ _, rfl⟩
 
-instance set_inclusion.is_ring_hom {s t : set R} [is_subring s] [is_subring t] (h : s ⊆ t) :
-  is_ring_hom (set.inclusion h) :=
-subtype_mk.is_ring_hom _ _
+@[simp] lemma is_subring.coe_subtype {S : set R} [is_subring S] :
+  ⇑(is_subring.subtype S) = coe := rfl
 
 variables {cR : Type u} [comm_ring cR]
 
@@ -190,18 +179,18 @@ theorem closure_subset_iff (s t : set R) [is_subring t] : closure s ⊆ t ↔ s
 theorem closure_mono {s t : set R} (H : s ⊆ t) : closure s ⊆ closure t :=
 closure_subset $ set.subset.trans H subset_closure
 
-lemma image_closure {S : Type*} [ring S] (f : R → S) [is_ring_hom f] (s : set R) :
+lemma image_closure {S : Type*} [ring S] (f : R →+* S) (s : set R) :
   f '' closure s = closure (f '' s) :=
 le_antisymm
   begin
     rintros _ ⟨x, hx, rfl⟩,
     apply in_closure.rec_on hx; intros,
-    { rw [is_monoid_hom.map_one f], apply is_submonoid.one_mem },
-    { rw [is_ring_hom.map_neg f, is_monoid_hom.map_one f],
+    { rw [f.map_one], apply is_submonoid.one_mem },
+    { rw [f.map_neg, is_monoid_hom.map_one f],
       apply is_add_subgroup.neg_mem, apply is_submonoid.one_mem },
-    { rw [is_monoid_hom.map_mul f],
+    { rw [f.map_mul],
       apply is_submonoid.mul_mem; solve_by_elim [subset_closure, set.mem_image_of_mem] },
-    { rw [is_ring_hom.map_add f], apply is_add_submonoid.add_mem, assumption' },
+    { rw [f.map_add], apply is_add_submonoid.add_mem, assumption' },
   end
   (closure_subset $ set.image_subset _ subset_closure)