feat(algebra/group/{pi, opposite}): add missing pi and opposite defs …

…for `mul_hom` (#13956)

The declaration names and the contents of these definitions are all copied from the corresponding ones for `monoid_hom`.

src/algebra/group/opposite.lean

@@ -228,6 +228,26 @@ def mul_equiv.inv' (G : Type*) [group G] : G ≃* Gᵐᵒᵖ :=
 { map_mul' := λ x y, unop_injective $ mul_inv_rev x y,
   .. (equiv.inv G).trans op_equiv }
 
+/-- A semigroup homomorphism `f : M →ₙ* N` such that `f x` commutes with `f y` for all `x, y`
+defines a semigroup homomorphism to `Nᵐᵒᵖ`. -/
+@[to_additive "An additive semigroup homomorphism `f : add_hom M N` such that `f x` additively
+commutes with `f y` for all `x, y` defines an additive semigroup homomorphism to `Sᵃᵒᵖ`.",
+  simps {fully_applied := ff}]
+def mul_hom.to_opposite {M N : Type*} [has_mul M] [has_mul N] (f : M →ₙ* N)
+  (hf : ∀ x y, commute (f x) (f y)) : M →ₙ* Nᵐᵒᵖ :=
+{ to_fun := mul_opposite.op ∘ f,
+  map_mul' := λ x y, by simp [(hf x y).eq] }
+
+/-- A semigroup homomorphism `f : M →ₙ* N` such that `f x` commutes with `f y` for all `x, y`
+defines a semigroup homomorphism from `Mᵐᵒᵖ`. -/
+@[to_additive "An additive semigroup homomorphism `f : add_hom M N` such that `f x` additively
+commutes with `f y` for all `x`, `y` defines an additive semigroup homomorphism from `Mᵃᵒᵖ`.",
+  simps {fully_applied := ff}]
+def mul_hom.from_opposite {M N : Type*} [has_mul M] [has_mul N] (f : M →ₙ* N)
+  (hf : ∀ x y, commute (f x) (f y)) : Mᵐᵒᵖ →ₙ* N :=
+{ to_fun := f ∘ mul_opposite.unop,
+  map_mul' := λ x y, (f.map_mul _ _).trans (hf _ _).eq }
+
 /-- A monoid homomorphism `f : M →* N` such that `f x` commutes with `f y` for all `x, y` defines
 a monoid homomorphism to `Nᵐᵒᵖ`. -/
 @[to_additive "An additive monoid homomorphism `f : M →+ N` such that `f x` additively commutes
@@ -270,6 +290,44 @@ lemma units.coe_op_equiv_symm {M} [monoid M] (u : (Mˣ)ᵐᵒᵖ) :
   (units.op_equiv.symm u : Mᵐᵒᵖ) = op (u.unop : M) :=
 rfl
 
+/-- A semigroup homomorphism `M →ₙ* N` can equivalently be viewed as a semigroup homomorphism
+`Mᵐᵒᵖ →ₙ* Nᵐᵒᵖ`. This is the action of the (fully faithful) `ᵐᵒᵖ`-functor on morphisms. -/
+@[to_additive "An additive semigroup homomorphism `add_hom M N` can equivalently be viewed as an
+additive semigroup homomorphism `add_hom Mᵃᵒᵖ Nᵃᵒᵖ`. This is the action of the (fully faithful)
+`ᵃᵒᵖ`-functor on morphisms.", simps]
+def mul_hom.op {M N} [has_mul M] [has_mul N] :
+  (M →ₙ* N) ≃ (Mᵐᵒᵖ →ₙ* Nᵐᵒᵖ) :=
+{ to_fun    := λ f, { to_fun   := op ∘ f ∘ unop,
+                      map_mul' := λ x y, unop_injective (f.map_mul y.unop x.unop) },
+  inv_fun   := λ f, { to_fun   := unop ∘ f ∘ op,
+                      map_mul' := λ x y, congr_arg unop (f.map_mul (op y) (op x)) },
+  left_inv  := λ f, by { ext, refl },
+  right_inv := λ f, by { ext x, simp } }
+
+/-- The 'unopposite' of a semigroup homomorphism `Mᵐᵒᵖ →ₙ* Nᵐᵒᵖ`. Inverse to `mul_hom.op`. -/
+@[simp, to_additive "The 'unopposite' of an additive semigroup homomorphism `Mᵃᵒᵖ →ₙ+ Nᵃᵒᵖ`. Inverse
+to `add_hom.op`."]
+def mul_hom.unop {M N} [has_mul M] [has_mul N] :
+  (Mᵐᵒᵖ →ₙ* Nᵐᵒᵖ) ≃ (M →ₙ* N) := mul_hom.op.symm
+
+/-- An additive semigroup homomorphism `add_hom M N` can equivalently be viewed as an additive
+homomorphism `add_hom Mᵐᵒᵖ Nᵐᵒᵖ`. This is the action of the (fully faithful) `ᵐᵒᵖ`-functor on
+morphisms. -/
+@[simps]
+def add_hom.mul_op {M N} [has_add M] [has_add N] :
+  (add_hom M N) ≃ (add_hom Mᵐᵒᵖ Nᵐᵒᵖ) :=
+{ to_fun    := λ f, { to_fun    := op ∘ f ∘ unop,
+                      map_add'  := λ x y, unop_injective (f.map_add x.unop y.unop) },
+  inv_fun   := λ f, { to_fun    := unop ∘ f ∘ op,
+                      map_add'  := λ x y, congr_arg unop (f.map_add (op x) (op y)) },
+  left_inv  := λ f, by { ext, refl },
+  right_inv := λ f, by { ext, simp } }
+
+/-- The 'unopposite' of an additive semigroup hom `αᵐᵒᵖ →+ βᵐᵒᵖ`. Inverse to
+`add_hom.mul_op`. -/
+@[simp] def add_hom.mul_unop {α β} [has_add α] [has_add β] :
+  (add_hom αᵐᵒᵖ βᵐᵒᵖ) ≃ (add_hom α β) := add_hom.mul_op.symm
+
 /-- A monoid homomorphism `M →* N` can equivalently be viewed as a monoid homomorphism
 `Mᵐᵒᵖ →* Nᵐᵒᵖ`. This is the action of the (fully faithful) `ᵐᵒᵖ`-functor on morphisms. -/
 @[to_additive "An additive monoid homomorphism `M →+ N` can equivalently be viewed as an

src/algebra/group/pi.lean

@@ -131,6 +131,46 @@ namespace mul_hom
 
 end mul_hom
 
+section mul_hom
+
+variables (f) [Π i, has_mul (f i)]
+
+/-- Evaluation of functions into an indexed collection of semigroups at a point is a semigroup
+homomorphism.
+This is `function.eval i` as a `mul_hom`. -/
+@[to_additive "Evaluation of functions into an indexed collection of additive semigroups at a
+point is an additive semigroup homomorphism.
+This is `function.eval i` as an `add_hom`.", simps]
+def pi.eval_mul_hom (i : I) : (Π i, f i) →ₙ* f i :=
+{ to_fun := λ g, g i,
+  map_mul' := λ x y, pi.mul_apply _ _ i, }
+
+/-- `function.const` as a `mul_hom`. -/
+@[to_additive "`function.const` as an `add_hom`.", simps]
+def pi.const_mul_hom (α β : Type*) [has_mul β] : β →ₙ* (α → β) :=
+{ to_fun := function.const α,
+  map_mul' := λ _ _, rfl }
+
+/-- Coercion of a `mul_hom` into a function is itself a `mul_hom`.
+See also `mul_hom.eval`. -/
+@[to_additive "Coercion of an `add_hom` into a function is itself a `add_hom`.
+See also `add_hom.eval`. ", simps]
+def mul_hom.coe_fn (α β : Type*) [has_mul α] [comm_semigroup β] : (α →ₙ* β) →ₙ* (α → β) :=
+{ to_fun := λ g, g,
+  map_mul' := λ x y, rfl, }
+
+/-- Semigroup homomorphism between the function spaces `I → α` and `I → β`, induced by a semigroup
+homomorphism `f` between `α` and `β`. -/
+@[to_additive "Additive semigroup homomorphism between the function spaces `I → α` and `I → β`,
+induced by an additive semigroup homomorphism `f` between `α` and `β`", simps]
+protected def mul_hom.comp_left {α β : Type*} [has_mul α] [has_mul β] (f : α →ₙ* β)
+  (I : Type*) :
+  (I → α) →ₙ* (I → β) :=
+{ to_fun := λ h, f ∘ h,
+  map_mul' := λ _ _, by ext; simp }
+
+end mul_hom
+
 section monoid_hom
 
 variables (f) [Π i, mul_one_class (f i)]