feat(algebra/group/units_hom): make is_unit.map work on `monoid_hom…

…_class` (#12577)

`ring_hom.is_unit_map` and `mv_power_series.is_unit_constant_coeff` are now redundant, but to keep this diff small I've left them around.

src/algebra/group/units_hom.lean

@@ -98,9 +98,9 @@ end monoid_hom
 section is_unit
 variables {M : Type*} {N : Type*}
 
-@[to_additive] lemma is_unit.map [monoid M] [monoid N]
-  (f : M →* N) {x : M} (h : is_unit x) : is_unit (f x) :=
-by rcases h with ⟨y, rfl⟩; exact (units.map f y).is_unit
+@[to_additive] lemma is_unit.map {F : Type*} [monoid M] [monoid N] [monoid_hom_class F M N]
+  (f : F) {x : M} (h : is_unit x) : is_unit (f x) :=
+by rcases h with ⟨y, rfl⟩; exact (units.map (f : M →* N) y).is_unit
 
 /-- If a homomorphism `f : M →* N` sends each element to an `is_unit`, then it can be lifted
 to `f : M →* Nˣ`. See also `units.lift_right` for a computable version. -/

src/algebra/ring/basic.lean

@@ -520,7 +520,7 @@ lemma domain_nontrivial [nontrivial β] : nontrivial α :=
 end
 
 lemma is_unit_map [semiring α] [semiring β] (f : α →+* β) {a : α} (h : is_unit a) : is_unit (f a) :=
-h.map f.to_monoid_hom
+h.map f
 
 /-- The identity ring homomorphism from a semiring to itself. -/
 def id (α : Type*) [non_assoc_semiring α] : α →+* α :=

src/algebraic_geometry/Gamma_Spec_adjunction.lean

@@ -203,7 +203,7 @@ def to_Γ_Spec : X ⟶ Spec.LocallyRingedSpace_obj (Γ.obj (op X)) :=
     erw ← he,
     rw ring_hom.map_mul,
     exact ht.mul ((is_localization.map_units S s : _).map
-      (PresheafedSpace.stalk_map X.to_Γ_Spec_SheafedSpace x).to_monoid_hom)
+      (PresheafedSpace.stalk_map X.to_Γ_Spec_SheafedSpace x))
   end }
 
 lemma comp_ring_hom_ext {X : LocallyRingedSpace} {R : CommRing}

src/data/polynomial/field_division.lean

@@ -94,7 +94,7 @@ lemma degree_pos_of_ne_zero_of_nonunit (hp0 : p ≠ 0) (hp : ¬is_unit p) :
   0 < degree p :=
 lt_of_not_ge (λ h, begin
   rw [eq_C_of_degree_le_zero h] at hp0 hp,
-  exact hp (is_unit.map (C.to_monoid_hom : R →* _)
+  exact hp (is_unit.map C
     (is_unit.mk0 (coeff p 0) (mt C_inj.2 (by simpa using hp0)))),
 end)
 

src/data/polynomial/ring_division.lean

@@ -739,13 +739,13 @@ begin
   have dz := degree_eq_zero_of_is_unit H,
   rw degree_map_eq_of_leading_coeff_ne_zero at dz,
   { rw eq_C_of_degree_eq_zero dz,
-    refine is_unit.map (C.to_monoid_hom : R →* R[X]) _,
+    refine is_unit.map (C : R →+* R[X]) _,
     convert hf,
     rw (degree_eq_iff_nat_degree_eq _).1 dz,
     rintro rfl,
     simpa using H, },
   { intro h,
-    have u : is_unit (φ f.leading_coeff) := is_unit.map φ.to_monoid_hom hf,
+    have u : is_unit (φ f.leading_coeff) := is_unit.map φ hf,
     rw h at u,
     simpa using u, }
 end
@@ -767,7 +767,7 @@ lemma monic.irreducible_of_irreducible_map (f : R[X])
 begin
   fsplit,
   { intro h,
-    exact h_irr.not_unit (is_unit.map (map_ring_hom φ).to_monoid_hom h), },
+    exact h_irr.not_unit (is_unit.map (map_ring_hom φ) h), },
   { intros a b h,
 
     have q := (leading_coeff_mul a b).symm,

src/group_theory/monoid_localization.lean

@@ -999,7 +999,7 @@ begin
   rw ← hn,
   dsimp,
   rw [g.map_nsmul],
-  exact is_add_unit.map (nsmul_add_monoid_hom n) hg,
+  exact is_add_unit.map (nsmul_add_monoid_hom n : C →+ C) hg,
 end
 
 @[simp] lemma away_map.lift_eq (hg : is_add_unit (g x)) (a : A) :

src/ring_theory/ideal/local_ring.lean

@@ -212,7 +212,7 @@ is_local_ring_hom.map_nonunit a h
 
 theorem of_irreducible_map [semiring R] [semiring S] (f : R →+* S) [h : is_local_ring_hom f] {x : R}
   (hfx : irreducible (f x)) : irreducible x :=
-⟨λ h, hfx.not_unit $ is_unit.map f.to_monoid_hom h, λ p q hx, let ⟨H⟩ := h in
+⟨λ h, hfx.not_unit $ is_unit.map f 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

src/ring_theory/localization/away.lean

@@ -54,7 +54,7 @@ is_localization.lift $ λ (y : submonoid.powers x), show is_unit (g y.1),
 begin
   obtain ⟨n, hn⟩ := y.2,
   rw [←hn, g.map_pow],
-  exact is_unit.map (pow_monoid_hom n) hg,
+  exact is_unit.map (pow_monoid_hom n : P →* P) hg,
 end
 
 @[simp] lemma away_map.lift_eq (hg : is_unit (g x)) (a : R) :

src/ring_theory/localization/localization_localization.lean

@@ -65,7 +65,7 @@ begin
   obtain ⟨y', z, eq⟩ := mem_localization_localization_submodule.mp y.prop,
   rw [is_scalar_tower.algebra_map_apply R S T, eq, ring_hom.map_mul, is_unit.mul_iff],
   exact ⟨is_localization.map_units T y',
-    (is_localization.map_units _ z).map (algebra_map S T : S →* T)⟩,
+    (is_localization.map_units _ z).map (algebra_map S T)⟩,
 end
 
 lemma localization_localization_surj [is_localization N T] (x : T) :

src/ring_theory/polynomial/gauss_lemma.lean

@@ -51,7 +51,7 @@ end
 lemma is_primitive.irreducible_of_irreducible_map_of_injective (h_irr : irreducible (map φ f)) :
   irreducible f :=
 begin
-  refine ⟨λ h, h_irr.not_unit (is_unit.map ((map_ring_hom φ).to_monoid_hom) h), _⟩,
+  refine ⟨λ h, h_irr.not_unit (is_unit.map (map_ring_hom φ) h), _⟩,
   intros a b h,
   rcases h_irr.is_unit_or_is_unit (by rw [h, map_mul]) with hu | hu,
   { left,

src/ring_theory/power_series/basic.lean

@@ -384,7 +384,7 @@ lemma coeff_zero_eq_constant_coeff_apply (φ : mv_power_series σ R) :
  then so is its constant coefficient.-/
 lemma is_unit_constant_coeff (φ : mv_power_series σ R) (h : is_unit φ) :
   is_unit (constant_coeff σ R φ) :=
-h.map (constant_coeff σ R).to_monoid_hom
+h.map _
 
 @[simp]
 lemma coeff_smul (f : mv_power_series σ R) (n) (a : R) :