chore(algebra/group/with_one): Use bundled morphisms (#4957)

The comment "We have no bundled semigroup homomorphisms" has become false, these exist as `mul_hom`.

This also adds `with_one.coe_mul_hom` and `with_zero.coe_add_hom`

Author: eric-wieser

src/algebra/group/hom.lean

@@ -86,8 +86,8 @@ structure mul_hom (M : Type*) (N : Type*) [has_mul M] [has_mul N] :=
 @[to_additive]
 structure monoid_hom (M : Type*) (N : Type*) [monoid M] [monoid N] extends one_hom M N, mul_hom M N
 
-attribute [nolint doc_blame] monoid_hom.to_mul_hom
-attribute [nolint doc_blame] monoid_hom.to_one_hom
+attribute [nolint doc_blame, to_additive] monoid_hom.to_mul_hom
+attribute [nolint doc_blame, to_additive] monoid_hom.to_one_hom
 
 infixr ` →* `:25 := monoid_hom
 

src/algebra/group/with_one.lean

@@ -79,35 +79,35 @@ instance [comm_semigroup α] : comm_monoid (with_one α) :=
 { mul_comm := (option.lift_or_get_comm _).1,
   ..with_one.monoid }
 
+/-- `coe` as a bundled morphism -/
+@[simps apply, to_additive "`coe` as a bundled morphism"]
+def coe_mul_hom [has_mul α] : mul_hom α (with_one α) :=
+{ to_fun := coe, map_mul' := λ x y, rfl }
+
 section lift
 
 variables [semigroup α] {β : Type v} [monoid β]
 
-/-- Lift a semigroup homomorphism `f` to a bundled monoid homorphism.
-We have no bundled semigroup homomorphisms, so this function
-takes `∀ x y, f (x * y) = f x * f y` as an explicit argument. -/
-@[to_additive "Lift an add_semigroup homomorphism `f` to a bundled add_monoid homorphism.
-  We have no bundled add_semigroup homomorphisms, so this function
-  takes `∀ x y, f (x + y) = f x + f y` as an explicit argument."]
-def lift (f : α → β) (hf : ∀ x y, f (x * y) = f x * f y) :
-  (with_one α) →* β :=
+/-- Lift a semigroup homomorphism `f` to a bundled monoid homorphism. -/
+@[to_additive "Lift an add_semigroup homomorphism `f` to a bundled add_monoid homorphism."]
+def lift (f : mul_hom α β) : (with_one α) →* β :=
 { to_fun := λ x, option.cases_on x 1 f,
   map_one' := rfl,
   map_mul' := λ x y,
     with_one.cases_on x (by { rw one_mul, exact (one_mul _).symm }) $ λ x,
     with_one.cases_on y (by { rw mul_one, exact (mul_one _).symm }) $ λ y,
-    hf x y }
+    f.map_mul x y }
 
-variables (f : α → β) (hf : ∀ x y, f (x * y) = f x * f y)
+variables (f : mul_hom α β)
 
 @[simp, to_additive]
-lemma lift_coe (x : α) : lift f hf x = f x := rfl
+lemma lift_coe (x : α) : lift f x = f x := rfl
 
 @[simp, to_additive]
-lemma lift_one : lift f hf 1 = 1 := rfl
+lemma lift_one : lift f 1 = 1 := rfl
 
 @[to_additive]
-theorem lift_unique (f : with_one α →* β) : f = lift (f ∘ coe) (λ x y, f.map_mul x y) :=
+theorem lift_unique (f : with_one α →* β) : f = lift (f.to_mul_hom.comp coe_mul_hom) :=
 monoid_hom.ext $ λ x, with_one.cases_on x f.map_one $ λ x, rfl
 
 end lift
@@ -120,9 +120,8 @@ variables {β : Type v} [semigroup α] [semigroup β]
   from `with_one α` to `with_one β` -/
 @[to_additive "Given an additive map from `α → β` returns an add_monoid homomorphism
   from `with_zero α` to `with_zero β`"]
-def map (f : α → β) (hf : ∀ x y, f (x * y) = f x * f y) :
-  with_one α →* with_one β :=
-lift (coe ∘ f) (λ x y, coe_inj.2 $ hf x y)
+def map (f : mul_hom α β) : with_one α →* with_one β :=
+lift (coe_mul_hom.comp f)
 
 end map