<commit_before>/-
Copyright (c) 2018 <NAME>. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: <NAME>, <NAME>, <NAME>, <NAME>, <NAME>,
  <NAME>, <NAME>
-/

import algebra.group_power.basic

/-!
# Instances on spaces of monoid and group morphisms

We endow the space of monoid morphisms `M →* N` with a `comm_monoid` structure when the target is
commutative, through pointwise multipliplication, and with a `comm_group` structure when the target
is a commutative group. We also prove the same instances for additive situations.
-/

universes uM uN uP
variables {M : Type uM} {N : Type uN} {P : Type uP}

lemma nat.succ_eq_one_add (n : ℕ) : n.succ = 1 + n :=
by rw [nat.succ_eq_add_one, nat.add_comm]

/-- `(M →* N)` is a `comm_monoid` if `N` is commutative. -/
instance [mul_one_class M] [comm_monoid N] : comm_monoid (M →* N) :=
{ mul := (*),
  mul_assoc := by intros; ext; apply mul_assoc,
  one := 1,
  one_mul := by intros; ext; apply one_mul,
  mul_one := by intros; ext; apply mul_one,
  mul_comm := by intros; ext; apply mul_comm,
  npow := λ n f,
  { to_fun := λ x, npow n (f x),
    map_one' := by simp,
    map_mul' := λ x y, by simp [mul_pow] },
  npow_zero' := λ f, by { ext x, simp },
  npow_succ' := λ n f, by { ext x, simp [pow_succ] } }

/-- `(M →+ N)` is an `add_comm_monoid` if `N` is commutative. -/
instance [add_zero_class M] [add_comm_monoid N] : add_comm_monoid (M →+ N) :=
{ add := (+),
  add_assoc := by intros; ext; apply add_assoc,
  zero := 0,
  zero_add := by intros; ext; apply zero_add,
  add_zero := by intros; ext; apply add_zero,
  add_comm := by intros; ext; apply add_comm,
  nsmul := λ n f,
  { to_fun := λ x, nsmul n (f x),
    map_zero' := by simp [nsmul_zero],
    map_add' := λ x y, by simp [nsmul_add] },
  nsmul_zero' := λ f, by { ext x, simp [zero_nsmul], },
  nsmul_succ' := λ n f, by { ext x, simp [nat.succ_eq_one_add, add_nsmul] } }

attribute [to_additive] monoid_hom.comm_monoid

namespace monoid_hom

/-- `flip` arguments of `f : M →* N →* P` -/
@[to_additive "`flip` arguments of `f : M →+ N →+ P`"]
def flip {mM : mul_one_class M} {mN : mul_one_class N} {mP : comm_monoid P} (f : M →* N →* P) :
  N →* M →* P :=
{ to_fun := λ y, ⟨λ x, f x y, by rw [f.map_one, one_apply], λ x₁ x₂, by rw [f.map_mul, mul_apply]⟩,
  map_one' := ext $ λ x, (f x).map_one,
  map_mul' := λ y₁ y₂, ext $ λ x, (f x).map_mul y₁ y₂ }

@[simp, to_additive] lemma flip_apply
  {mM : mul_one_class M} {mN : mul_one_class N} {mP : comm_monoid P}
  (f : M →* N →* P) (x : M) (y : N) :
  f.flip y x = f x y :=
rfl

/-- Evaluation of a `monoid_hom` at a point as a monoid homomorphism. See also `monoid_hom.apply`
for the evaluation of any function at a point. -/
@[to_additive "Evaluation of an `add_monoid_hom` at a point as an additive monoid homomorphism.
See also `add_monoid_hom.apply` for the evaluation of any function at a point.", simps]
def eval [mul_one_class M] [comm_monoid N] : M →* (M →* N) →* N := (monoid_hom.id (M →* N)).flip

/-- Composition of monoid morphisms (`monoid_hom.comp`) as a monoid morphism. -/
@[to_additive "Composition of additive monoid morphisms
(`add_monoid_hom.comp`) as an additive monoid morphism.", simps]
def comp_hom [mul_one_class M] [comm_monoid N] [comm_monoid P] :
  (N →* P) →* (M →* N) →* (M →* P) :=
{ to_fun := λ g, { to_fun := g.comp, map_one' := comp_one g, map_mul' := comp_mul g },
  map_one' := by { ext1 f, exact one_comp f },
  map_mul' := λ g₁ g₂, by { ext1 f, exact mul_comp g₁ g₂ f } }

/-- Flipping arguments of monoid morphisms (`monoid_hom.flip`) as a monoid morphism. -/
@[to_additive "Flipping arguments of additive monoid morphisms (`add_monoid_hom.flip`)
as an additive monoid morphism.", simps]
def flip_hom {mM : mul_one_class M} {mN : mul_one_class N} {mP : comm_monoid P}
  : (M →* N →* P) →* (N →* M →* P) :=
{ to_fun := monoid_hom.flip, map_one' := rfl, map_mul' := λ f g, rfl }

end monoid_hom

/-- If `G` is a commutative group, then `M →* G` a commutative group too. -/
instance {M G} [mul_one_class M] [comm_group G] : comm_group (M →* G) :=
{ inv := has_inv.inv,
  div := has_div.div,
  div_eq_mul_inv := by { intros, ext, apply div_eq_mul_inv },
  mul_left_inv := by intros; ext; apply mul_left_inv,
  gpow := λ n f, { to_fun := λ x, gpow n (f x),
    map_one' := by simp,
    map_mul' := λ x y, by simp [mul_gpow] },
  gpow_zero' := λ f, by { ext x, simp },
  gpow_succ' := λ n f, by { ext x, simp [gpow_of_nat, pow_succ] },
  gpow_neg'  := λ n f, by { ext x, simp },
  ..monoid_hom.comm_monoid }

/-- If `G` is an additive commutative group, then `M →+ G` an additive commutative group too. -/
instance {M G} [add_zero_class M] [add_comm_group G] : add_comm_group (M →+ G) :=
{ neg := has_neg.neg,
  sub := has_sub.sub,
  sub_eq_add_neg := by { intros, ext, apply sub_eq_add_neg },
  add_left_neg := by intros; ext; apply add_left_neg,
  gsmul := λ n f, { to_fun := λ x, gsmul n (f x),
    map_zero' := by simp,
    map_add' := λ x y, by simp [gsmul_add] },
  gsmul_zero' := λ f, by { ext x, simp },
  gsmul_succ' := λ n f, by { ext x, simp [gsmul_of_nat, nat.succ_eq_one_add, add_nsmul] },
  gsmul_neg'  := λ n f, by { ext x, simp },
  ..add_monoid_hom.add_comm_monoid }

attribute [to_additive] monoid_hom.comm_group<commit_msg>feat(algebra/group/hom_instance): add add_monoid_hom.mul (#7382)<commit_after>/-
Copyright (c) 2018 <NAME>. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: <NAME>, <NAME>, <NAME>, <NAME>, <NAME>,
  <NAME>, <NAME>
-/

import algebra.group_power.basic

/-!
# Instances on spaces of monoid and group morphisms

We endow the space of monoid morphisms `M →* N` with a `comm_monoid` structure when the target is
commutative, through pointwise multiplication, and with a `comm_group` structure when the target
is a commutative group. We also prove the same instances for additive situations.
-/

universes uM uN uP
variables {M : Type uM} {N : Type uN} {P : Type uP}

lemma nat.succ_eq_one_add (n : ℕ) : n.succ = 1 + n :=
by rw [nat.succ_eq_add_one, nat.add_comm]

/-- `(M →* N)` is a `comm_monoid` if `N` is commutative. -/
instance [mul_one_class M] [comm_monoid N] : comm_monoid (M →* N) :=
{ mul := (*),
  mul_assoc := by intros; ext; apply mul_assoc,
  one := 1,
  one_mul := by intros; ext; apply one_mul,
  mul_one := by intros; ext; apply mul_one,
  mul_comm := by intros; ext; apply mul_comm,
  npow := λ n f,
  { to_fun := λ x, npow n (f x),
    map_one' := by simp,
    map_mul' := λ x y, by simp [mul_pow] },
  npow_zero' := λ f, by { ext x, simp },
  npow_succ' := λ n f, by { ext x, simp [pow_succ] } }

/-- `(M →+ N)` is an `add_comm_monoid` if `N` is commutative. -/
instance [add_zero_class M] [add_comm_monoid N] : add_comm_monoid (M →+ N) :=
{ add := (+),
  add_assoc := by intros; ext; apply add_assoc,
  zero := 0,
  zero_add := by intros; ext; apply zero_add,
  add_zero := by intros; ext; apply add_zero,
  add_comm := by intros; ext; apply add_comm,
  nsmul := λ n f,
  { to_fun := λ x, nsmul n (f x),
    map_zero' := by simp [nsmul_zero],
    map_add' := λ x y, by simp [nsmul_add] },
  nsmul_zero' := λ f, by { ext x, simp [zero_nsmul], },
  nsmul_succ' := λ n f, by { ext x, simp [nat.succ_eq_one_add, add_nsmul] } }

attribute [to_additive] monoid_hom.comm_monoid

namespace monoid_hom

/-- `flip` arguments of `f : M →* N →* P` -/
@[to_additive "`flip` arguments of `f : M →+ N →+ P`"]
def flip {mM : mul_one_class M} {mN : mul_one_class N} {mP : comm_monoid P} (f : M →* N →* P) :
  N →* M →* P :=
{ to_fun := λ y, ⟨λ x, f x y, by rw [f.map_one, one_apply], λ x₁ x₂, by rw [f.map_mul, mul_apply]⟩,
  map_one' := ext $ λ x, (f x).map_one,
  map_mul' := λ y₁ y₂, ext $ λ x, (f x).map_mul y₁ y₂ }

@[simp, to_additive] lemma flip_apply
  {mM : mul_one_class M} {mN : mul_one_class N} {mP : comm_monoid P}
  (f : M →* N →* P) (x : M) (y : N) :
  f.flip y x = f x y :=
rfl

/-- Evaluation of a `monoid_hom` at a point as a monoid homomorphism. See also `monoid_hom.apply`
for the evaluation of any function at a point. -/
@[to_additive "Evaluation of an `add_monoid_hom` at a point as an additive monoid homomorphism.
See also `add_monoid_hom.apply` for the evaluation of any function at a point.", simps]
def eval [mul_one_class M] [comm_monoid N] : M →* (M →* N) →* N := (monoid_hom.id (M →* N)).flip

/-- Composition of monoid morphisms (`monoid_hom.comp`) as a monoid morphism. -/
@[to_additive "Composition of additive monoid morphisms
(`add_monoid_hom.comp`) as an additive monoid morphism.", simps]
def comp_hom [mul_one_class M] [comm_monoid N] [comm_monoid P] :
  (N →* P) →* (M →* N) →* (M →* P) :=
{ to_fun := λ g, { to_fun := g.comp, map_one' := comp_one g, map_mul' := comp_mul g },
  map_one' := by { ext1 f, exact one_comp f },
  map_mul' := λ g₁ g₂, by { ext1 f, exact mul_comp g₁ g₂ f } }

/-- Flipping arguments of monoid morphisms (`monoid_hom.flip`) as a monoid morphism. -/
@[to_additive "Flipping arguments of additive monoid morphisms (`add_monoid_hom.flip`)
as an additive monoid morphism.", simps]
def flip_hom {mM : mul_one_class M} {mN : mul_one_class N} {mP : comm_monoid P}
  : (M →* N →* P) →* (N →* M →* P) :=
{ to_fun := monoid_hom.flip, map_one' := rfl, map_mul' := λ f g, rfl }

end monoid_hom

/-- If `G` is a commutative group, then `M →* G` a commutative group too. -/
instance {M G} [mul_one_class M] [comm_group G] : comm_group (M →* G) :=
{ inv := has_inv.inv,
  div := has_div.div,
  div_eq_mul_inv := by { intros, ext, apply div_eq_mul_inv },
  mul_left_inv := by intros; ext; apply mul_left_inv,
  gpow := λ n f, { to_fun := λ x, gpow n (f x),
    map_one' := by simp,
    map_mul' := λ x y, by simp [mul_gpow] },
  gpow_zero' := λ f, by { ext x, simp },
  gpow_succ' := λ n f, by { ext x, simp [gpow_of_nat, pow_succ] },
  gpow_neg'  := λ n f, by { ext x, simp },
  ..monoid_hom.comm_monoid }

/-- If `G` is an additive commutative group, then `M →+ G` an additive commutative group too. -/
instance {M G} [add_zero_class M] [add_comm_group G] : add_comm_group (M →+ G) :=
{ neg := has_neg.neg,
  sub := has_sub.sub,
  sub_eq_add_neg := by { intros, ext, apply sub_eq_add_neg },
  add_left_neg := by intros; ext; apply add_left_neg,
  gsmul := λ n f, { to_fun := λ x, gsmul n (f x),
    map_zero' := by simp,
    map_add' := λ x y, by simp [gsmul_add] },
  gsmul_zero' := λ f, by { ext x, simp },
  gsmul_succ' := λ n f, by { ext x, simp [gsmul_of_nat, nat.succ_eq_one_add, add_nsmul] },
  gsmul_neg'  := λ n f, by { ext x, simp },
  ..add_monoid_hom.add_comm_monoid }

attribute [to_additive] monoid_hom.comm_group

/-!
### Miscellaneous definitions

Due to the fact this file imports `algebra.group_power.basic`, it is not possible to import it in
some of the lower-level files like `algebra.ring.basic`. The following lemmas should be rehomed
if the import structure permits them to be.
-/

section semiring

variables {R : Type*} [semiring R]

/-- Multiplication of an element of a (semi)ring is an `add_monoid_hom` in both arguments.

This is a more-strongly bundled version of `add_monoid_hom.mul_left` and `add_monoid_hom.mul_right`.

A stronger version of this exists for algebras as `algebra.lmul`.
-/
def add_monoid_hom.mul : R →+ R →+ R :=
{ to_fun := add_monoid_hom.mul_left,
  map_zero' := add_monoid_hom.ext $ zero_mul,
  map_add' := λ a b, add_monoid_hom.ext $ add_mul a b }

lemma add_monoid_hom.mul_apply (x y : R) : add_monoid_hom.mul x y = x * y := rfl

@[simp]
lemma add_monoid_hom.coe_mul :
  ⇑(add_monoid_hom.mul : R →+ R →+ R) = add_monoid_hom.mul_left := rfl

@[simp]
lemma add_monoid_hom.coe_flip_mul :
  ⇑(add_monoid_hom.mul : R →+ R →+ R).flip = add_monoid_hom.mul_right := rfl

end semiring
{'fraction_non_alphanumeric': 0.14789514132012638, 'fraction_numerical': 0.0022201349158910426, 'mean_word_length': 3.5325077399380804, 'pattern_counts': {'":': 0, '<': 19, '<?xml version=': 0, '>': 19, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '2348107', 'n_tokens_mistral': 5006, 'n_tokens_neox': 4807, 'n_words': 1660}