chore(*): migrate units.map to bundled homs (#1331)

Author: urkud

src/algebra/associated.lean

@@ -15,6 +15,15 @@ def is_unit [monoid α] (a : α) : Prop := ∃u:units α, a = u
 
 @[simp] lemma is_unit_unit [monoid α] (u : units α) : is_unit (u : α) := ⟨u, rfl⟩
 
+theorem is_unit.mk0 [division_ring α] (x : α) (hx : x ≠ 0) : is_unit x := is_unit_unit (units.mk0 x hx)
+
+lemma is_unit.map [monoid α] [monoid β] (f : α →* β) {x : α} (h : is_unit x) : is_unit (f x) :=
+by rcases h with ⟨y, rfl⟩; exact is_unit_unit (units.map f y)
+
+lemma is_unit.map' [monoid α] [monoid β] (f : α → β) {x : α} (h : is_unit x) [is_monoid_hom f] :
+  is_unit (f x) :=
+h.map (as_monoid_hom f)
+
 @[simp] theorem is_unit_zero_iff [semiring α] : is_unit (0 : α) ↔ (0:α) = 1 :=
 ⟨λ ⟨⟨_, a, (a0 : 0 * a = 1), _⟩, rfl⟩, by rwa zero_mul at a0,
  λ h, begin

src/algebra/group/hom.lean

@@ -275,6 +275,17 @@ infixr ` →* `:25 := monoid_hom
 instance {M : Type*} {N : Type*} [monoid M] [monoid N] : has_coe_to_fun (M →* N) :=
 ⟨_, monoid_hom.to_fun⟩
 
+/-- Reinterpret a map `f : M → N` as a homomorphism `M →* N` -/
+def as_monoid_hom {M : Type u} {N : Type v} [monoid M] [monoid N]
+  (f : M → N) [h : is_monoid_hom f] : M →* N :=
+{ to_fun := f,
+  map_one' := h.2,
+  map_mul' := h.1.1 }
+
+@[simp] lemma coe_as_monoid_hom {M : Type u} {N : Type v} [monoid M] [monoid N]
+  (f : M → N) [is_monoid_hom f] : ⇑ (as_monoid_hom f) = f :=
+rfl
+
 /-- Bundled add_monoid homomorphisms; use this for bundled add_group homomorphisms too. -/
 structure add_monoid_hom (M : Type*) (N : Type*) [add_monoid M] [add_monoid N] :=
 (to_fun : M → N)
@@ -301,6 +312,8 @@ attribute [to_additive add_monoid_hom.rec] monoid_hom.rec
 attribute [to_additive add_monoid_hom.rec_on] monoid_hom.rec_on
 attribute [to_additive add_monoid_hom.sizeof] monoid_hom.sizeof
 attribute [to_additive add_monoid_hom.to_fun] monoid_hom.to_fun
+attribute [to_additive as_add_monoid_hom._proof_1] as_monoid_hom._proof_1
+attribute [to_additive as_add_monoid_hom] as_monoid_hom
 
 namespace monoid_hom
 variables {M : Type*} {N : Type*} {P : Type*} [monoid M] [monoid N] [monoid P]

src/algebra/group/units_hom.lean

@@ -7,27 +7,38 @@ Lift monoid homomorphisms to group homomorphisms of their units subgroups.
 -/
 import algebra.group.units algebra.group.hom
 
+universes u v w
+
 namespace units
-variables {α : Type*} {β : Type*}
+variables {α : Type u} {β : Type v} {γ : Type w} [monoid α] [monoid β] [monoid γ]
+
+def map (f : α →* β) : units α →* units β :=
+monoid_hom.mk'
+  (λ u, ⟨f u.val, f u.inv,
+                  by rw [← f.map_mul, u.val_inv, f.map_one],
+                  by rw [← f.map_mul, u.inv_val, f.map_one]⟩)
+  (λ x y, ext (f.map_mul x y))
+
+@[reducible] def map' (f : α → β) [is_monoid_hom f] : units α →* units β :=
+  map (as_monoid_hom f)
 
-variables {γ : Type*} [monoid α] [monoid β] [monoid γ] (f : α → β) (g : β → γ)
-[is_monoid_hom f] [is_monoid_hom g]
+@[simp] lemma coe_map (f : α →* β) (x : units α) : ↑(map f x) = f x := rfl
 
-definition map : units α → units β :=
-λ u, ⟨f u.val, f u.inv,
-      by rw [← is_monoid_hom.map_mul f, u.val_inv, is_monoid_hom.map_one f],
-      by rw [← is_monoid_hom.map_mul f, u.inv_val, is_monoid_hom.map_one f] ⟩
+@[simp] lemma coe_map' (f : α → β) [is_monoid_hom f] (x : units α) :
+  ↑((map' f : units α → units β) x) = f x :=
+rfl
 
-instance : is_group_hom (units.map f) :=
-{ map_mul := λ a b, by ext; exact is_monoid_hom.map_mul f a b }
+@[simp] lemma map_comp (f : α →* β) (g : β →* γ) : map (g.comp f) = (map g).comp (map f) := rfl
 
-instance coe_is_monoid_hom : is_monoid_hom (coe : units α → α) :=
-{ map_one := rfl, map_mul := by simp }
+variables (α)
+@[simp] lemma map_id : map (monoid_hom.id α) = monoid_hom.id (units α) :=
+by ext; refl
 
-@[simp] lemma coe_map (u : units α) : (map f u : β) = f u := rfl
+/-- Coercion `units α → α` as a monoid homomorphism. -/
+def coe_hom : units α →* α := ⟨coe, coe_one, coe_mul⟩
 
-@[simp] lemma map_id : map (id : α → α) = id := by ext; refl
+@[simp] lemma coe_hom_apply (x : units α) : coe_hom α x = ↑x := rfl
 
-lemma map_comp : map (g ∘ f) = map g ∘ map f := rfl
+instance coe_is_monoid_hom : is_monoid_hom (coe : units α → α) := (coe_hom α).is_monoid_hom
 
 end units

src/data/equiv/algebra.lean

@@ -434,11 +434,10 @@ variables [monoid α] [monoid β] [monoid γ]
 (f : α → β) (g : β → γ) [is_monoid_hom f] [is_monoid_hom g]
 
 def map_equiv (h : α ≃* β) : units α ≃* units β :=
-{ to_fun := map h,
-  inv_fun := map h.symm,
+{ inv_fun := map h.symm.to_monoid_hom,
   left_inv := λ u, ext $ h.left_inv u,
   right_inv := λ u, ext $ h.right_inv u,
-  map_mul' := λ a b, units.ext $ h.map_mul a b}
+  .. map h.to_monoid_hom }
 
 end units
 

src/data/polynomial.lean

@@ -1898,7 +1898,8 @@ lemma is_unit_iff_degree_eq_zero : is_unit p ↔ degree p = 0 :=
 lemma degree_pos_of_ne_zero_of_nonunit (hp0 : p ≠ 0) (hp : ¬is_unit p) :
   0 < degree p :=
 lt_of_not_ge (λ h, by rw [eq_C_of_degree_le_zero h] at hp0 hp;
-  exact hp ⟨units.map C (units.mk0 (coeff p 0) (mt C_inj.2 (by simpa using hp0))), rfl⟩)
+  exact (hp $ is_unit.map' C $
+    is_unit.mk0 (coeff p 0) (mt C_inj.2 (by simpa using hp0))))
 
 lemma irreducible_of_degree_eq_one (hp1 : degree p = 1) : irreducible p :=
 ⟨mt is_unit_iff_dvd_one.1 (λ ⟨q, hq⟩,

src/field_theory/splitting_field.lean

@@ -136,7 +136,7 @@ else
       (λ p, by simp [@eq_comm _ _ p, -sub_eq_add_neg,
           irreducible_of_degree_eq_one (degree_X_sub_C _)] {contextual := tt})
       (associated.symm $ calc _ ~ᵤ f.map i :
-        ⟨units.map C (units.mk0 (f.map i).leading_coeff
+        ⟨(units.map' C : units β →* units (polynomial β)) (units.mk0 (f.map i).leading_coeff
             (mt leading_coeff_eq_zero.1 (mt (map_eq_zero i).1 hf0))),
           by conv_rhs {rw [hs, ← leading_coeff_map i, mul_comm]}; refl⟩
         ... ~ᵤ _ : associated.symm (unique_factorization_domain.factors_prod (by simpa using hf0))),

src/ring_theory/localization.lean

@@ -282,14 +282,15 @@ by simp [lift', quotient.lift_on_beta, of, mk, this]
 @[simp] lemma lift'_apply_coe (f : localization α S → β) [is_ring_hom f]
   (g : S → units β) (hg : ∀ s, (g s : β) = f s) :
   lift' (λ a : α, f a) g hg = f :=
-have g = (λ s, units.map f (to_units s)),
-  from funext $ λ x, units.ext_iff.2 $ (hg x).symm ▸ rfl,
+have g = (λ s, (units.map' f : units (localization α S) → units β) (to_units s)),
+  from funext $ λ x, units.ext $ (hg x).symm ▸ rfl,
 funext $ λ x, localization.induction_on x
-  (λ r s, by subst this; rw [lift'_mk, ← is_group_hom.map_inv (units.map f), units.coe_map];
+  (λ r s, by subst this; rw [lift'_mk, ← (units.map' f).map_inv, units.coe_map'];
     simp [is_ring_hom.map_mul f])
 
 @[simp] lemma lift_apply_coe (f : localization α S → β) [is_ring_hom f] :
-  lift (λ a : α, f a) (λ s hs, is_unit_unit (units.map f (to_units ⟨s, hs⟩))) = f :=
+  lift (λ a : α, f a)
+    (λ s hs, is_unit.map' f (is_unit_unit (to_units ⟨s, hs⟩))) = f :=
 by rw [lift, lift'_apply_coe]
 
 /-- Function extensionality for localisations:

src/ring_theory/power_series.lean

@@ -292,7 +292,7 @@ instance coeff_zero.is_semiring_hom :
  then so is its constant coefficient.-/
 lemma is_unit_coeff_zero (φ : mv_power_series σ α) (h : is_unit φ) :
   is_unit (coeff 0 φ) :=
-by { rcases h with ⟨φ, rfl⟩, exact ⟨units.map (coeff 0) φ, rfl⟩ }
+h.map' (coeff 0)
 
 instance : semimodule α (mv_power_series σ α) :=
 { smul := λ a φ, C a * φ,