feat(algebra/hom/group and *): introduce mul_hom M N notation `M →ₙ…

…* N` (#13526)

The discussion and poll related to this new notation can be found in this [Zulip thread](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/ring_hom.20notation.20and.20friends/near/279313301)

src/algebra/category/Semigroup/basic.lean

@@ -56,13 +56,13 @@ def of (M : Type u) [has_mul M] : Magma := bundled.of M
 add_decl_doc AddMagma.of
 
 /-- Typecheck a `mul_hom` as a morphism in `Magma`. -/
-@[to_additive] def of_hom {X Y : Type u} [has_mul X] [has_mul Y] (f : mul_hom X Y) :
+@[to_additive] def of_hom {X Y : Type u} [has_mul X] [has_mul Y] (f : X →ₙ* Y) :
   of X ⟶ of Y := f
 
 /-- Typecheck a `add_hom` as a morphism in `AddMagma`. -/
 add_decl_doc AddMagma.of_hom
 
-@[simp, to_additive] lemma of_hom_apply {X Y : Type u} [has_mul X] [has_mul Y] (f : mul_hom X Y)
+@[simp, to_additive] lemma of_hom_apply {X Y : Type u} [has_mul X] [has_mul Y] (f : X →ₙ* Y)
   (x : X) : of_hom f x = f x := rfl
 
 @[to_additive]
@@ -100,13 +100,13 @@ def of (M : Type u) [semigroup M] : Semigroup := bundled.of M
 add_decl_doc AddSemigroup.of
 
 /-- Typecheck a `mul_hom` as a morphism in `Semigroup`. -/
-@[to_additive] def of_hom {X Y : Type u} [semigroup X] [semigroup Y] (f : mul_hom X Y) :
+@[to_additive] def of_hom {X Y : Type u} [semigroup X] [semigroup Y] (f : X →ₙ* Y) :
   of X ⟶ of Y := f
 
 /-- Typecheck a `add_hom` as a morphism in `AddSemigroup`. -/
 add_decl_doc AddSemigroup.of_hom
 
-@[simp, to_additive] lemma of_hom_apply {X Y : Type u} [semigroup X] [semigroup Y] (f : mul_hom X Y)
+@[simp, to_additive] lemma of_hom_apply {X Y : Type u} [semigroup X] [semigroup Y] (f : X →ₙ* Y)
   (x : X) : of_hom f x = f x := rfl
 
 @[to_additive]

src/algebra/divisibility.lean

@@ -77,7 +77,7 @@ variables {M N : Type*} [monoid M] [monoid N]
 lemma map_dvd {F : Type*} [mul_hom_class F M N] (f : F) {a b} : a ∣ b → f a ∣ f b
 | ⟨c, h⟩ := ⟨f c, h.symm ▸ map_mul f a c⟩
 
-lemma mul_hom.map_dvd (f : mul_hom M N) {a b} : a ∣ b → f a ∣ f b := map_dvd f
+lemma mul_hom.map_dvd (f : M →ₙ* N) {a b} : a ∣ b → f a ∣ f b := map_dvd f
 
 lemma monoid_hom.map_dvd (f : M →* N) {a b} : a ∣ b → f a ∣ f b := map_dvd f
 

src/algebra/free.lean

@@ -82,13 +82,13 @@ namespace free_magma
 variables {α : Type u} {β : Type v} [has_mul β] (f : α → β)
 
 @[to_additive]
-theorem lift_aux_unique (F : mul_hom (free_magma α) β) : ⇑F = lift_aux (F ∘ of) :=
+theorem lift_aux_unique (F : free_magma α →ₙ* β) : ⇑F = lift_aux (F ∘ of) :=
 funext $ λ x, free_magma.rec_on x (λ x, rfl) $ λ x y ih1 ih2,
 (F.map_mul x y).trans $ congr (congr_arg _ ih1) ih2
 
 /-- The universal property of the free magma expressing its adjointness. -/
 @[to_additive "The universal property of the free additive magma expressing its adjointness."]
-def lift : (α → β) ≃ mul_hom (free_magma α) β :=
+def lift : (α → β) ≃ (free_magma α →ₙ* β) :=
 { to_fun    := λ f,
   { to_fun := lift_aux f,
     map_mul' := λ x y, rfl, },

src/algebra/group/pi.lean

@@ -126,7 +126,7 @@ end pi
 namespace mul_hom
 
 @[to_additive] lemma coe_mul {M N} {mM : has_mul M} {mN : comm_semigroup N}
-  (f g : mul_hom M N) :
+  (f g : M →ₙ* N) :
   (f * g : M → N) = λ x, f x * g x := rfl
 
 end mul_hom
@@ -219,7 +219,7 @@ lemma monoid_hom.single_apply [Π i, mul_one_class $ f i] (i : I) (x : f i) :
 into a dependent family of `mul_zero_class`es, as functions supported at a point.
 
 This is the `mul_hom` version of `pi.single`. -/
-@[simps] def mul_hom.single [Π i, mul_zero_class $ f i] (i : I) : mul_hom (f i) (Π i, f i) :=
+@[simps] def mul_hom.single [Π i, mul_zero_class $ f i] (i : I) : (f i) →ₙ* (Π i, f i) :=
 { to_fun := single i,
   map_mul' := pi.single_op₂ (λ _, (*)) (λ _, zero_mul _) _, }
 

src/algebra/group/prod.lean

@@ -194,42 +194,42 @@ variables (M N) [has_mul M] [has_mul N] [has_mul P]
 /-- Given magmas `M`, `N`, the natural projection homomorphism from `M × N` to `M`.-/
 @[to_additive "Given additive magmas `A`, `B`, the natural projection homomorphism
 from `A × B` to `A`"]
-def fst : mul_hom (M × N) M := ⟨prod.fst, λ _ _, rfl⟩
+def fst : (M × N) →ₙ* M := ⟨prod.fst, λ _ _, rfl⟩
 
 /-- Given magmas `M`, `N`, the natural projection homomorphism from `M × N` to `N`.-/
 @[to_additive "Given additive magmas `A`, `B`, the natural projection homomorphism
 from `A × B` to `B`"]
-def snd : mul_hom (M × N) N := ⟨prod.snd, λ _ _, rfl⟩
+def snd : (M × N) →ₙ* N := ⟨prod.snd, λ _ _, rfl⟩
 
 variables {M N}
 
 @[simp, to_additive] lemma coe_fst : ⇑(fst M N) = prod.fst := rfl
 @[simp, to_additive] lemma coe_snd : ⇑(snd M N) = prod.snd := rfl
 
-/-- Combine two `monoid_hom`s `f : mul_hom M N`, `g : mul_hom M P` into
-`f.prod g : mul_hom M (N × P)` given by `(f.prod g) x = (f x, g x)`. -/
+/-- Combine two `monoid_hom`s `f : M →ₙ* N`, `g : M →ₙ* P` into
+`f.prod g : M →ₙ* (N × P)` given by `(f.prod g) x = (f x, g x)`. -/
 @[to_additive prod "Combine two `add_monoid_hom`s `f : add_hom M N`, `g : add_hom M P` into
 `f.prod g : add_hom M (N × P)` given by `(f.prod g) x = (f x, g x)`"]
-protected def prod (f : mul_hom M N) (g : mul_hom M P) : mul_hom M (N × P) :=
+protected def prod (f : M →ₙ* N) (g : M →ₙ* P) : M →ₙ* (N × P) :=
 { to_fun := pi.prod f g,
   map_mul' := λ x y, prod.ext (f.map_mul x y) (g.map_mul x y) }
 
 @[to_additive coe_prod]
-lemma coe_prod (f : mul_hom M N) (g : mul_hom M P) : ⇑(f.prod g) = pi.prod f g := rfl
+lemma coe_prod (f : M →ₙ* N) (g : M →ₙ* P) : ⇑(f.prod g) = pi.prod f g := rfl
 
 @[simp, to_additive prod_apply]
-lemma prod_apply (f : mul_hom M N) (g : mul_hom M P) (x) : f.prod g x = (f x, g x) := rfl
+lemma prod_apply (f : M →ₙ* N) (g : M →ₙ* P) (x) : f.prod g x = (f x, g x) := rfl
 
 @[simp, to_additive fst_comp_prod]
-lemma fst_comp_prod (f : mul_hom M N) (g : mul_hom M P) : (fst N P).comp (f.prod g) = f :=
+lemma fst_comp_prod (f : M →ₙ* N) (g : M →ₙ* P) : (fst N P).comp (f.prod g) = f :=
 ext $ λ x, rfl
 
 @[simp, to_additive snd_comp_prod]
-lemma snd_comp_prod (f : mul_hom M N) (g : mul_hom M P) : (snd N P).comp (f.prod g) = g :=
+lemma snd_comp_prod (f : M →ₙ* N) (g : M →ₙ* P) : (snd N P).comp (f.prod g) = g :=
 ext $ λ x, rfl
 
 @[simp, to_additive prod_unique]
-lemma prod_unique (f : mul_hom M (N × P)) :
+lemma prod_unique (f : M →ₙ* (N × P)) :
   ((fst N P).comp f).prod ((snd N P).comp f) = f :=
 ext $ λ x, by simp only [prod_apply, coe_fst, coe_snd, comp_apply, prod.mk.eta]
 
@@ -238,11 +238,11 @@ end prod
 section prod_map
 
 variables {M' : Type*} {N' : Type*} [has_mul M] [has_mul N] [has_mul M'] [has_mul N'] [has_mul P]
-  (f : mul_hom M M') (g : mul_hom N N')
+  (f : M →ₙ* M') (g : N →ₙ* N')
 
 /-- `prod.map` as a `monoid_hom`. -/
 @[to_additive prod_map "`prod.map` as an `add_monoid_hom`"]
-def prod_map : mul_hom (M × N) (M' × N') := (f.comp (fst M N)).prod (g.comp (snd M N))
+def prod_map : (M × N) →ₙ* (M' × N') := (f.comp (fst M N)).prod (g.comp (snd M N))
 
 @[to_additive prod_map_def]
 lemma prod_map_def : prod_map f g = (f.comp (fst M N)).prod (g.comp (snd M N)) := rfl
@@ -251,29 +251,29 @@ lemma prod_map_def : prod_map f g = (f.comp (fst M N)).prod (g.comp (snd M N)) :
 lemma coe_prod_map : ⇑(prod_map f g) = prod.map f g := rfl
 
 @[to_additive prod_comp_prod_map]
-lemma prod_comp_prod_map (f : mul_hom P M) (g : mul_hom P N)
-  (f' : mul_hom M M') (g' : mul_hom N N') :
+lemma prod_comp_prod_map (f : P →ₙ* M) (g : P →ₙ* N)
+  (f' : M →ₙ* M') (g' : N →ₙ* N') :
   (f'.prod_map g').comp (f.prod g) = (f'.comp f).prod (g'.comp g) :=
 rfl
 
 end prod_map
 
 section coprod
 
-variables [has_mul M] [has_mul N] [comm_semigroup P] (f : mul_hom M P) (g : mul_hom N P)
+variables [has_mul M] [has_mul N] [comm_semigroup P] (f : M →ₙ* P) (g : N →ₙ* P)
 
 /-- Coproduct of two `mul_hom`s with the same codomain:
 `f.coprod g (p : M × N) = f p.1 * g p.2`. -/
 @[to_additive "Coproduct of two `add_hom`s with the same codomain:
 `f.coprod g (p : M × N) = f p.1 + g p.2`."]
-def coprod : mul_hom (M × N) P := f.comp (fst M N) * g.comp (snd M N)
+def coprod : (M × N) →ₙ* P := f.comp (fst M N) * g.comp (snd M N)
 
 @[simp, to_additive]
 lemma coprod_apply (p : M × N) : f.coprod g p = f p.1 * g p.2 := rfl
 
 @[to_additive]
 lemma comp_coprod {Q : Type*} [comm_semigroup Q]
-  (h : mul_hom P Q) (f : mul_hom M P) (g : mul_hom N P) :
+  (h : P →ₙ* Q) (f : M →ₙ* P) (g : N →ₙ* P) :
   h.comp (f.coprod g) = (h.comp f).coprod (h.comp g) :=
 ext $ λ x, by simp
 
@@ -475,7 +475,7 @@ variables {α : Type*}
 
 /-- Multiplication as a multiplicative homomorphism. -/
 @[to_additive "Addition as an additive homomorphism.", simps]
-def mul_mul_hom [comm_semigroup α] : mul_hom (α × α) α :=
+def mul_mul_hom [comm_semigroup α] : (α × α) →ₙ* α :=
 { to_fun := λ a, a.1 * a.2,
   map_mul' := λ a b, mul_mul_mul_comm _ _ _ _ }
 

src/algebra/group/with_one.lean

@@ -116,7 +116,7 @@ section
 local attribute [irreducible] with_one with_zero
 /-- `coe` as a bundled morphism -/
 @[to_additive "`coe` as a bundled morphism", simps apply]
-def coe_mul_hom [has_mul α] : mul_hom α (with_one α) :=
+def coe_mul_hom [has_mul α] : α →ₙ* (with_one α) :=
 { to_fun := coe, map_mul' := λ x y, rfl }
 
 end
@@ -127,7 +127,7 @@ variables [has_mul α] [mul_one_class β]
 
 /-- 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 : mul_hom α β ≃ (with_one α →* β) :=
+def lift : (α →ₙ* β) ≃ (with_one α →* β) :=
 { to_fun := λ f,
   { to_fun := λ x, option.cases_on x 1 f,
     map_one' := rfl,
@@ -139,7 +139,7 @@ def lift : mul_hom α β ≃ (with_one α →* β) :=
   left_inv := λ f, mul_hom.ext $ λ x, rfl,
   right_inv := λ F, monoid_hom.ext $ λ x, with_one.cases_on x F.map_one.symm $ λ x, rfl }
 
-variables (f : mul_hom α β)
+variables (f : α →ₙ* β)
 
 @[simp, to_additive]
 lemma lift_coe (x : α) : lift f x = f x := rfl
@@ -163,23 +163,23 @@ variables [has_mul α] [has_mul β] [has_mul γ]
   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 : mul_hom α β) : with_one α →* with_one β :=
+def map (f : α →ₙ* β) : with_one α →* with_one β :=
 lift (coe_mul_hom.comp f)
 
-@[simp, to_additive] lemma map_coe (f : mul_hom α β) (a : α) : map f (a : with_one α) = f a :=
+@[simp, to_additive] lemma map_coe (f : α →ₙ* β) (a : α) : map f (a : with_one α) = f a :=
 lift_coe _ _
 
 @[simp, to_additive]
 lemma map_id : map (mul_hom.id α) = monoid_hom.id (with_one α) :=
 by { ext, induction x using with_one.cases_on; refl }
 
 @[to_additive]
-lemma map_map (f : mul_hom α β) (g : mul_hom β γ) (x) :
+lemma map_map (f : α →ₙ* β) (g : β →ₙ* γ) (x) :
   map g (map f x) = map (g.comp f) x :=
 by { induction x using with_one.cases_on; refl }
 
 @[simp, to_additive]
-lemma map_comp (f : mul_hom α β) (g : mul_hom β γ) :
+lemma map_comp (f : α →ₙ* β) (g : β →ₙ* γ) :
   map (g.comp f) = (map g).comp (map f) :=
 monoid_hom.ext $ λ x, (map_map f g x).symm
 

src/algebra/hom/equiv.lean

@@ -35,8 +35,8 @@ variables {F α β A B M N P Q G H : Type*}
 
 /-- Makes a multiplicative inverse from a bijection which preserves multiplication. -/
 @[to_additive "Makes an additive inverse from a bijection which preserves addition."]
-def mul_hom.inverse [has_mul M] [has_mul N] (f : mul_hom M N) (g : N → M)
-  (h₁ : function.left_inverse g f) (h₂ : function.right_inverse g f) : mul_hom N M :=
+def mul_hom.inverse [has_mul M] [has_mul N] (f : M →ₙ* N) (g : N → M)
+  (h₁ : function.left_inverse g f) (h₂ : function.right_inverse g f) : N →ₙ* M :=
 { to_fun   := g,
   map_mul' := λ x y,
     calc g (x * y) = g (f (g x) * f (g y)) : by rw [h₂ x, h₂ y]
@@ -50,7 +50,7 @@ def monoid_hom.inverse {A B : Type*} [monoid A] [monoid B] (f : A →* B) (g : B
   B →* A :=
 { to_fun   := g,
   map_one' := by rw [← f.map_one, h₁],
-  .. (f : mul_hom A B).inverse g h₁ h₂, }
+  .. (f : A →ₙ* B).inverse g h₁ h₂, }
 
 set_option old_structure_cmd true
 
@@ -71,7 +71,7 @@ add_decl_doc add_equiv.to_add_hom
 
 /-- `mul_equiv α β` is the type of an equiv `α ≃ β` which preserves multiplication. -/
 @[ancestor equiv mul_hom, to_additive]
-structure mul_equiv (M N : Type*) [has_mul M] [has_mul N] extends M ≃ N, mul_hom M N
+structure mul_equiv (M N : Type*) [has_mul M] [has_mul N] extends M ≃ N, M →ₙ* N
 
 /-- The `equiv` underlying a `mul_equiv`. -/
 add_decl_doc mul_equiv.to_equiv