import algebra.ne_zero

import algebra.group.basic

import algebra.group_with_zero.defs

import data.fun_like.basic

variables {α β M N P : Type*} -- monoids

variables {G : Type*} {H : Type*} -- groups

variables {F : Type*} -- homs

set_option old_structure_cmd true

section zero

structure zero_hom (M : Type*) (N : Type*) [has_zero M] [has_zero N] :=

(to_fun : M → N)

(map_zero' : to_fun 0 = 0)

class zero_hom_class (F : Type*) (M N : out_param $ Type*)

[has_zero M] [has_zero N] extends fun_like F M (λ _, N) :=

(map_zero : ∀ (f : F), f 0 = 0)

end zero

namespace ne_zero

lemma of_map {R M} [has_zero R] [has_zero M] [zero_hom_class F R M] (f : F) {r : R}

[ne_zero (f r)] : ne_zero r := ⟨λ h, ne (f r) $ by convert zero_hom_class.map_zero f⟩

lemma of_injective {R M} [has_zero R] {r : R} [ne_zero r] [has_zero M] [zero_hom_class F R M]

{f : F} (hf : function.injective f) : ne_zero (f r) :=

⟨by { rw ← zero_hom_class.map_zero f, exact hf.ne (ne r) }⟩

end ne_zero

section add

structure add_hom (M : Type*) (N : Type*) [has_add M] [has_add N] :=

(to_fun : M → N)

(map_add' : ∀ x y, to_fun (x + y) = to_fun x + to_fun y)

class add_hom_class (F : Type*) (M N : out_param $ Type*)

[has_add M] [has_add N] extends fun_like F M (λ _, N) :=

(map_add : ∀ (f : F) (x y : M), f (x + y) = f x + f y)

end add

section add_zero

structure add_monoid_hom (M : Type*) (N : Type*) [add_zero_class M] [add_zero_class N]

extends zero_hom M N, add_hom M N

attribute [nolint doc_blame] add_monoid_hom.to_add_hom

attribute [nolint doc_blame] add_monoid_hom.to_zero_hom

infixr ` →+ `:25 := add_monoid_hom

class add_monoid_hom_class (F : Type*) (M N : out_param $ Type*)

[add_zero_class M] [add_zero_class N]

extends add_hom_class F M N, zero_hom_class F M N

end add_zero

section one

variables [has_one M] [has_one N]

structure one_hom (M : Type*) (N : Type*) [has_one M] [has_one N] :=

(to_fun : M → N)

(map_one' : to_fun 1 = 1)

class one_hom_class (F : Type*) (M N : out_param $ Type*)

[has_one M] [has_one N]

extends fun_like F M (λ _, N) :=

(map_one : ∀ (f : F), f 1 = 1)

instance one_hom.one_hom_class : one_hom_class (one_hom M N) M N :=

{ coe := one_hom.to_fun,

coe_injective' := λ f g h, by cases f; cases g; congr',

map_one := one_hom.map_one' }

@[simp, to_additive] lemma map_one [one_hom_class F M N] (f : F) : f 1 = 1 :=

one_hom_class.map_one f

@[to_additive] lemma map_eq_one_iff [one_hom_class F M N] (f : F)

(hf : function.injective f) {x : M} : f x = 1 ↔ x = 1 :=

hf.eq_iff' (map_one f)

lemma map_ne_one_iff {R S F : Type*} [has_one R] [has_one S] [one_hom_class F R S]

(f : F) (hf : function.injective f) {x : R} :

f x ≠ 1 ↔ x ≠ 1 :=

(map_eq_one_iff f hf).not

lemma ne_one_of_map {R S F : Type*} [has_one R] [has_one S] [one_hom_class F R S]

{f : F} {x : R} (hx : f x ≠ 1) : x ≠ 1 :=

ne_of_apply_ne f $ ne_of_ne_of_eq hx (map_one f).symm

instance [one_hom_class F M N] : has_coe_t F (one_hom M N) :=

⟨λ f, { to_fun := f, map_one' := map_one f }⟩

@[simp, to_additive] lemma one_hom.coe_coe [one_hom_class F M N] (f : F) :

((f : one_hom M N) : M → N) = f := rfl

end one

section mul

variables [has_mul M] [has_mul N]

structure mul_hom (M : Type*) (N : Type*) [has_mul M] [has_mul N] :=

(to_fun : M → N)

(map_mul' : ∀ x y, to_fun (x * y) = to_fun x * to_fun y)

infixr ` →ₙ* `:25 := mul_hom

class mul_hom_class (F : Type*) (M N : out_param $ Type*)

[has_mul M] [has_mul N] extends fun_like F M (λ _, N) :=

(map_mul : ∀ (f : F) (x y : M), f (x * y) = f x * f y)

instance mul_hom.mul_hom_class : mul_hom_class (M →ₙ* N) M N :=

{ coe := mul_hom.to_fun,

coe_injective' := λ f g h, by cases f; cases g; congr',

map_mul := mul_hom.map_mul' }

@[simp, to_additive] lemma map_mul [mul_hom_class F M N] (f : F) (x y : M) :

f (x * y) = f x * f y :=

mul_hom_class.map_mul f x y

instance [mul_hom_class F M N] : has_coe_t F (M →ₙ* N) :=

⟨λ f, { to_fun := f, map_mul' := map_mul f }⟩

@[simp, to_additive] lemma mul_hom.coe_coe [mul_hom_class F M N] (f : F) :

((f : mul_hom M N) : M → N) = f := rfl

end mul

section mul_one

variables [mul_one_class M] [mul_one_class N]

structure monoid_hom (M : Type*) (N : Type*) [mul_one_class M] [mul_one_class N]

extends one_hom M N, M →ₙ* N

attribute [nolint doc_blame] monoid_hom.to_mul_hom

attribute [nolint doc_blame] monoid_hom.to_one_hom

infixr ` →* `:25 := monoid_hom

class monoid_hom_class (F : Type*) (M N : out_param $ Type*)

[mul_one_class M] [mul_one_class N]

extends mul_hom_class F M N, one_hom_class F M N

instance monoid_hom.monoid_hom_class : monoid_hom_class (M →* N) M N :=

{ coe := monoid_hom.to_fun,

coe_injective' := λ f g h, by cases f; cases g; congr',

map_mul := monoid_hom.map_mul',

map_one := monoid_hom.map_one' }

instance [monoid_hom_class F M N] : has_coe_t F (M →* N) :=

⟨λ f, { to_fun := f, map_one' := map_one f, map_mul' := map_mul f }⟩

@[simp, to_additive] lemma monoid_hom.coe_coe [monoid_hom_class F M N] (f : F) :

((f : M →* N) : M → N) = f := rfl

lemma map_mul_eq_one [monoid_hom_class F M N] (f : F) {a b : M} (h : a * b = 1) :

f a * f b = 1 :=

by rw [← map_mul, h, map_one]

lemma map_div' [div_inv_monoid G] [div_inv_monoid H] [monoid_hom_class F G H] (f : F)

(hf : ∀ a, f a⁻¹ = (f a)⁻¹) (a b : G) : f (a / b) = f a / f b :=

by rw [div_eq_mul_inv, div_eq_mul_inv, map_mul, hf]

lemma map_inv [group G] [division_monoid H] [monoid_hom_class F G H] (f : F) (a : G) :

f a⁻¹ = (f a)⁻¹ :=

eq_inv_of_mul_eq_one_left $ map_mul_eq_one f $ inv_mul_self _

lemma map_mul_inv [group G] [division_monoid H] [monoid_hom_class F G H] (f : F) (a b : G) :

f (a * b⁻¹) = f a * (f b)⁻¹ :=

by rw [map_mul, map_inv]

lemma map_div [group G] [division_monoid H] [monoid_hom_class F G H] (f : F) :

∀ a b, f (a / b) = f a / f b :=

map_div' _ $ map_inv f

@[to_additive map_nsmul.aux, simp] theorem map_pow [monoid G] [monoid H] [monoid_hom_class F G H]

(f : F) (a : G) :

∀ (n : ℕ), f (a ^ n) = (f a) ^ n

| 0 := by rw [pow_zero, pow_zero, map_one]

| (n+1) := by rw [pow_succ, pow_succ, map_mul, map_pow]

@[simp] theorem map_nsmul [add_monoid G] [add_monoid H] [add_monoid_hom_class F G H]

(f : F) (n : ℕ) (a : G) : f (n • a) = n • (f a) :=

map_nsmul.aux f a n

attribute [to_additive_reorder 8, to_additive] map_pow

theorem map_zpow' [div_inv_monoid G] [div_inv_monoid H] [monoid_hom_class F G H]

(f : F) (hf : ∀ (x : G), f (x⁻¹) = (f x)⁻¹) (a : G) :

∀ n : ℤ, f (a ^ n) = (f a) ^ n

| (n : ℕ) := by rw [zpow_coe_nat, map_pow, zpow_coe_nat]

| -[1+n] := by rw [zpow_neg_succ_of_nat, hf, map_pow, ← zpow_neg_succ_of_nat]

theorem map_zpow [group G] [division_monoid H] [monoid_hom_class F G H] (f : F) (g : G) (n : ℤ) :

f (g ^ n) = (f g) ^ n :=

map_zpow' f (map_inv f) g n

theorem map_zsmul [add_group G] [subtraction_monoid H] [add_monoid_hom_class F G H] (f : F)

(n : ℤ) (g : G) :

f (n • g) = n • f g :=

map_zsmul.aux f g n

attribute [to_additive_reorder 8, to_additive] map_zpow

end mul_one

section mul_zero_one

variables [mul_zero_one_class M] [mul_zero_one_class N]

structure monoid_with_zero_hom (M : Type*) (N : Type*) [mul_zero_one_class M] [mul_zero_one_class N]

extends zero_hom M N, monoid_hom M N

attribute [nolint doc_blame] monoid_with_zero_hom.to_monoid_hom

attribute [nolint doc_blame] monoid_with_zero_hom.to_zero_hom

infixr ` →*₀ `:25 := monoid_with_zero_hom

class monoid_with_zero_hom_class (F : Type*) (M N : out_param $ Type*)

[mul_zero_one_class M] [mul_zero_one_class N]

extends monoid_hom_class F M N, zero_hom_class F M N

instance monoid_with_zero_hom.monoid_with_zero_hom_class :

monoid_with_zero_hom_class (M →*₀ N) M N :=

{ coe := monoid_with_zero_hom.to_fun,

coe_injective' := λ f g h, by cases f; cases g; congr',

map_mul := monoid_with_zero_hom.map_mul',

map_one := monoid_with_zero_hom.map_one',

map_zero := monoid_with_zero_hom.map_zero' }

instance [monoid_with_zero_hom_class F M N] : has_coe_t F (M →*₀ N) :=

⟨λ f, { to_fun := f, map_one' := map_one f, map_zero' := map_zero f, map_mul' := map_mul f }⟩

@[simp] lemma monoid_with_zero_hom.coe_coe [monoid_with_zero_hom_class F M N] (f : F) :

((f : M →*₀ N) : M → N) = f := rfl

end mul_zero_one

section coes

instance monoid_hom.has_coe_to_one_hom {mM : mul_one_class M} {mN : mul_one_class N} :

has_coe (M →* N) (one_hom M N) := ⟨monoid_hom.to_one_hom⟩

instance monoid_hom.has_coe_to_mul_hom {mM : mul_one_class M} {mN : mul_one_class N} :

has_coe (M →* N) (M →ₙ* N) := ⟨monoid_hom.to_mul_hom⟩

instance monoid_with_zero_hom.has_coe_to_monoid_hom

{mM : mul_zero_one_class M} {mN : mul_zero_one_class N} :

has_coe (M →*₀ N) (M →* N) := ⟨monoid_with_zero_hom.to_monoid_hom⟩

instance monoid_with_zero_hom.has_coe_to_zero_hom

{mM : mul_zero_one_class M} {mN : mul_zero_one_class N} :

has_coe (M →*₀ N) (zero_hom M N) := ⟨monoid_with_zero_hom.to_zero_hom⟩

lemma monoid_hom.coe_eq_to_one_hom {mM : mul_one_class M} {mN : mul_one_class N} (f : M →* N) :

(f : one_hom M N) = f.to_one_hom := rfl

lemma monoid_hom.coe_eq_to_mul_hom {mM : mul_one_class M} {mN : mul_one_class N} (f : M →* N) :

(f : M →ₙ* N) = f.to_mul_hom := rfl

lemma monoid_with_zero_hom.coe_eq_to_monoid_hom

{mM : mul_zero_one_class M} {mN : mul_zero_one_class N} (f : M →*₀ N) :

(f : M →* N) = f.to_monoid_hom := rfl

lemma monoid_with_zero_hom.coe_eq_to_zero_hom

{mM : mul_zero_one_class M} {mN : mul_zero_one_class N} (f : M →*₀ N) :

(f : zero_hom M N) = f.to_zero_hom := rfl

instance {mM : has_one M} {mN : has_one N} : has_coe_to_fun (one_hom M N) (λ _, M → N) :=

⟨one_hom.to_fun⟩

instance {mM : has_mul M} {mN : has_mul N} : has_coe_to_fun (M →ₙ* N) (λ _, M → N) :=

⟨mul_hom.to_fun⟩

instance {mM : mul_one_class M} {mN : mul_one_class N} : has_coe_to_fun (M →* N) (λ _, M → N) :=

⟨monoid_hom.to_fun⟩

instance {mM : mul_zero_one_class M} {mN : mul_zero_one_class N} :

has_coe_to_fun (M →*₀ N) (λ _, M → N) :=

⟨monoid_with_zero_hom.to_fun⟩

initialize_simps_projections zero_hom (to_fun → apply)

initialize_simps_projections add_hom (to_fun → apply)

initialize_simps_projections add_monoid_hom (to_fun → apply)

initialize_simps_projections one_hom (to_fun → apply)

initialize_simps_projections mul_hom (to_fun → apply)

initialize_simps_projections monoid_hom (to_fun → apply)

initialize_simps_projections monoid_with_zero_hom (to_fun → apply)

lemma one_hom.to_fun_eq_coe [has_one M] [has_one N] (f : one_hom M N) : f.to_fun = f := rfl

lemma mul_hom.to_fun_eq_coe [has_mul M] [has_mul N] (f : M →ₙ* N) : f.to_fun = f := rfl

lemma monoid_hom.to_fun_eq_coe [mul_one_class M] [mul_one_class N]

(f : M →* N) : f.to_fun = f := rfl

lemma monoid_with_zero_hom.to_fun_eq_coe [mul_zero_one_class M] [mul_zero_one_class N]

(f : M →*₀ N) : f.to_fun = f := rfl

lemma one_hom.coe_mk [has_one M] [has_one N]

(f : M → N) (h1) : (one_hom.mk f h1 : M → N) = f := rfl

lemma mul_hom.coe_mk [has_mul M] [has_mul N]

(f : M → N) (hmul) : (mul_hom.mk f hmul : M → N) = f := rfl

lemma monoid_hom.coe_mk [mul_one_class M] [mul_one_class N]

(f : M → N) (h1 hmul) : (monoid_hom.mk f h1 hmul : M → N) = f := rfl

lemma monoid_with_zero_hom.coe_mk [mul_zero_one_class M] [mul_zero_one_class N]

(f : M → N) (h0 h1 hmul) : (monoid_with_zero_hom.mk f h0 h1 hmul : M → N) = f := rfl

lemma monoid_hom.to_one_hom_coe [mul_one_class M] [mul_one_class N] (f : M →* N) :

(f.to_one_hom : M → N) = f := rfl

lemma monoid_hom.to_mul_hom_coe [mul_one_class M] [mul_one_class N] (f : M →* N) :

(f.to_mul_hom : M → N) = f := rfl

lemma monoid_with_zero_hom.to_zero_hom_coe [mul_zero_one_class M] [mul_zero_one_class N]

(f : M →*₀ N) :

(f.to_zero_hom : M → N) = f := rfl

lemma monoid_with_zero_hom.to_monoid_hom_coe [mul_zero_one_class M] [mul_zero_one_class N]

(f : M →*₀ N) :

(f.to_monoid_hom : M → N) = f := rfl

lemma one_hom.ext [has_one M] [has_one N] ⦃f g : one_hom M N⦄ (h : ∀ x, f x = g x) : f = g :=

fun_like.ext _ _ h

lemma mul_hom.ext [has_mul M] [has_mul N] ⦃f g : M →ₙ* N⦄ (h : ∀ x, f x = g x) : f = g :=

fun_like.ext _ _ h

lemma monoid_hom.ext [mul_one_class M] [mul_one_class N]

⦃f g : M →* N⦄ (h : ∀ x, f x = g x) : f = g :=

fun_like.ext _ _ h

lemma monoid_with_zero_hom.ext [mul_zero_one_class M] [mul_zero_one_class N] ⦃f g : M →*₀ N⦄

(h : ∀ x, f x = g x) : f = g :=

fun_like.ext _ _ h

section deprecated

theorem one_hom.congr_fun [has_one M] [has_one N]

{f g : one_hom M N} (h : f = g) (x : M) : f x = g x :=

fun_like.congr_fun h x

theorem mul_hom.congr_fun [has_mul M] [has_mul N]

{f g : M →ₙ* N} (h : f = g) (x : M) : f x = g x :=

fun_like.congr_fun h x

theorem monoid_hom.congr_fun [mul_one_class M] [mul_one_class N]

{f g : M →* N} (h : f = g) (x : M) : f x = g x :=

fun_like.congr_fun h x

theorem monoid_with_zero_hom.congr_fun [mul_zero_one_class M] [mul_zero_one_class N] {f g : M →*₀ N}

(h : f = g) (x : M) : f x = g x :=

fun_like.congr_fun h x

theorem one_hom.congr_arg [has_one M] [has_one N]

(f : one_hom M N) {x y : M} (h : x = y) : f x = f y :=

fun_like.congr_arg f h

theorem mul_hom.congr_arg [has_mul M] [has_mul N]

(f : M →ₙ* N) {x y : M} (h : x = y) : f x = f y :=

fun_like.congr_arg f h

theorem monoid_hom.congr_arg [mul_one_class M] [mul_one_class N]

(f : M →* N) {x y : M} (h : x = y) : f x = f y :=

fun_like.congr_arg f h

theorem monoid_with_zero_hom.congr_arg [mul_zero_one_class M] [mul_zero_one_class N] (f : M →*₀ N)

{x y : M} (h : x = y) : f x = f y :=

fun_like.congr_arg f h

lemma one_hom.coe_inj [has_one M] [has_one N] ⦃f g : one_hom M N⦄ (h : (f : M → N) = g) : f = g :=

fun_like.coe_injective h

lemma mul_hom.coe_inj [has_mul M] [has_mul N] ⦃f g : M →ₙ* N⦄ (h : (f : M → N) = g) : f = g :=

fun_like.coe_injective h

lemma monoid_hom.coe_inj [mul_one_class M] [mul_one_class N]

⦃f g : M →* N⦄ (h : (f : M → N) = g) : f = g :=

fun_like.coe_injective h

lemma monoid_with_zero_hom.coe_inj [mul_zero_one_class M] [mul_zero_one_class N]

⦃f g : M →*₀ N⦄ (h : (f : M → N) = g) : f = g :=

fun_like.coe_injective h

lemma one_hom.ext_iff [has_one M] [has_one N] {f g : one_hom M N} : f = g ↔ ∀ x, f x = g x :=

fun_like.ext_iff

lemma mul_hom.ext_iff [has_mul M] [has_mul N] {f g : M →ₙ* N} : f = g ↔ ∀ x, f x = g x :=

fun_like.ext_iff

lemma monoid_hom.ext_iff [mul_one_class M] [mul_one_class N]

{f g : M →* N} : f = g ↔ ∀ x, f x = g x :=

fun_like.ext_iff

lemma monoid_with_zero_hom.ext_iff [mul_zero_one_class M] [mul_zero_one_class N] {f g : M →*₀ N} :

f = g ↔ ∀ x, f x = g x :=

fun_like.ext_iff

end deprecated

lemma one_hom.mk_coe [has_one M] [has_one N]

(f : one_hom M N) (h1) : one_hom.mk f h1 = f :=

one_hom.ext $ λ _, rfl

lemma mul_hom.mk_coe [has_mul M] [has_mul N]

(f : M →ₙ* N) (hmul) : mul_hom.mk f hmul = f :=

mul_hom.ext $ λ _, rfl

lemma monoid_hom.mk_coe [mul_one_class M] [mul_one_class N]

(f : M →* N) (h1 hmul) : monoid_hom.mk f h1 hmul = f :=

monoid_hom.ext $ λ _, rfl

lemma monoid_with_zero_hom.mk_coe [mul_zero_one_class M] [mul_zero_one_class N] (f : M →*₀ N)

(h0 h1 hmul) : monoid_with_zero_hom.mk f h0 h1 hmul = f :=

monoid_with_zero_hom.ext $ λ _, rfl

end coes

protected def one_hom.copy {hM : has_one M} {hN : has_one N} (f : one_hom M N) (f' : M → N)

(h : f' = f) : one_hom M N :=

{ to_fun := f',

map_one' := h.symm ▸ f.map_one' }

@[simp, to_additive] lemma one_hom.coe_copy {hM : has_one M} {hN : has_one N} (f : one_hom M N)

(f' : M → N) (h : f' = f) : ⇑(f.copy f' h) = f' :=

rfl

@[to_additive] lemma one_hom.coe_copy_eq {hM : has_one M} {hN : has_one N} (f : one_hom M N)

(f' : M → N) (h : f' = f) : f.copy f' h = f :=

fun_like.ext' h

protected def mul_hom.copy {hM : has_mul M} {hN : has_mul N} (f : M →ₙ* N) (f' : M → N)

(h : f' = f) : M →ₙ* N :=

{ to_fun := f',

map_mul' := h.symm ▸ f.map_mul' }

lemma mul_hom.coe_copy {hM : has_mul M} {hN : has_mul N} (f : M →ₙ* N) (f' : M → N)

(h : f' = f) : ⇑(f.copy f' h) = f' := rfl

@[to_additive] lemma mul_hom.coe_copy_eq {hM : has_mul M} {hN : has_mul N} (f : M →ₙ* N)

(f' : M → N) (h : f' = f) : f.copy f' h = f :=

fun_like.ext' h

protected def monoid_hom.copy {hM : mul_one_class M} {hN : mul_one_class N} (f : M →* N)

(f' : M → N) (h : f' = f) : M →* N :=

{ ..f.to_one_hom.copy f' h, ..f.to_mul_hom.copy f' h }

@[simp, to_additive] lemma monoid_hom.coe_copy {hM : mul_one_class M} {hN : mul_one_class N}

(f : M →* N) (f' : M → N) (h : f' = f) : ⇑(f.copy f' h) = f' :=

rfl

@[to_additive] lemma monoid_hom.copy_eq {hM : mul_one_class M} {hN : mul_one_class N}

(f : M →* N) (f' : M → N) (h : f' = f) : f.copy f' h = f :=

fun_like.ext' h

protected def monoid_with_zero_hom.copy {hM : mul_zero_one_class M} {hN : mul_zero_one_class N}

(f : M →*₀ N) (f' : M → N) (h : f' = f) : M →* N :=

{ ..f.to_zero_hom.copy f' h, ..f.to_monoid_hom.copy f' h }

@[simp] lemma monoid_with_zero_hom.coe_copy {hM : mul_zero_one_class M} {hN : mul_zero_one_class N}

(f : M →*₀ N) (f' : M → N) (h : f' = f) : ⇑(f.copy f' h) = f' :=

rfl

lemma monoid_with_zero_hom.copy_eq {hM : mul_zero_one_class M} {hN : mul_zero_one_class N}

(f : M →*₀ N) (f' : M → N) (h : f' = f) : f.copy f' h = f :=

fun_like.ext' h

protected lemma one_hom.map_one [has_one M] [has_one N] (f : one_hom M N) : f 1 = 1 := f.map_one'

protected lemma monoid_hom.map_one [mul_one_class M] [mul_one_class N] (f : M →* N) :

f 1 = 1 := f.map_one'

protected lemma monoid_with_zero_hom.map_one [mul_zero_one_class M] [mul_zero_one_class N]

(f : M →*₀ N) : f 1 = 1 := f.map_one'

add_decl_doc add_monoid_hom.map_zero

protected lemma monoid_with_zero_hom.map_zero [mul_zero_one_class M] [mul_zero_one_class N]

(f : M →*₀ N) : f 0 = 0 := f.map_zero'

protected lemma mul_hom.map_mul [has_mul M] [has_mul N]

(f : M →ₙ* N) (a b : M) : f (a * b) = f a * f b := f.map_mul' a b

protected lemma monoid_hom.map_mul [mul_one_class M] [mul_one_class N]

(f : M →* N) (a b : M) : f (a * b) = f a * f b := f.map_mul' a b

protected lemma monoid_with_zero_hom.map_mul [mul_zero_one_class M] [mul_zero_one_class N]

(f : M →*₀ N) (a b : M) : f (a * b) = f a * f b := f.map_mul' a b

add_decl_doc add_monoid_hom.map_add

namespace monoid_hom

variables {mM : mul_one_class M} {mN : mul_one_class N} [monoid_hom_class F M N]

include mM mN

lemma map_exists_right_inv (f : F) {x : M} (hx : ∃ y, x * y = 1) :

∃ y, f x * y = 1 :=

let ⟨y, hy⟩ := hx in ⟨f y, map_mul_eq_one f hy⟩

lemma map_exists_left_inv (f : F) {x : M} (hx : ∃ y, y * x = 1) :

∃ y, y * f x = 1 :=

let ⟨y, hy⟩ := hx in ⟨f y, map_mul_eq_one f hy⟩

end monoid_hom

section division_comm_monoid

variables [division_comm_monoid α]

def inv_monoid_hom : α →* α :=

{ to_fun := has_inv.inv,

map_one' := inv_one,

map_mul' := mul_inv }

@[simp] lemma coe_inv_monoid_hom : (inv_monoid_hom : α → α) = has_inv.inv := rfl

@[simp] lemma inv_monoid_hom_apply (a : α) : inv_monoid_hom a = a⁻¹ := rfl

end division_comm_monoid

def one_hom.id (M : Type*) [has_one M] : one_hom M M :=

{ to_fun := λ x, x, map_one' := rfl, }

def mul_hom.id (M : Type*) [has_mul M] : M →ₙ* M :=

{ to_fun := λ x, x, map_mul' := λ _ _, rfl, }

def monoid_hom.id (M : Type*) [mul_one_class M] : M →* M :=

{ to_fun := λ x, x, map_one' := rfl, map_mul' := λ _ _, rfl, }

def monoid_with_zero_hom.id (M : Type*) [mul_zero_one_class M] : M →*₀ M :=

{ to_fun := λ x, x, map_zero' := rfl, map_one' := rfl, map_mul' := λ _ _, rfl, }

add_decl_doc zero_hom.id

add_decl_doc add_hom.id

add_decl_doc add_monoid_hom.id

def one_hom.comp [has_one M] [has_one N] [has_one P]

(hnp : one_hom N P) (hmn : one_hom M N) : one_hom M P :=

{ to_fun := hnp ∘ hmn, map_one' := by simp, }

def mul_hom.comp [has_mul M] [has_mul N] [has_mul P]

(hnp : N →ₙ* P) (hmn : M →ₙ* N) : M →ₙ* P :=

{ to_fun := hnp ∘ hmn, map_mul' := by simp, }

def monoid_hom.comp [mul_one_class M] [mul_one_class N] [mul_one_class P]

(hnp : N →* P) (hmn : M →* N) : M →* P :=

{ to_fun := hnp ∘ hmn, map_one' := by simp, map_mul' := by simp, }

def monoid_with_zero_hom.comp [mul_zero_one_class M] [mul_zero_one_class N] [mul_zero_one_class P]

(hnp : N →*₀ P) (hmn : M →*₀ N) : M →*₀ P :=

{ to_fun := hnp ∘ hmn, map_zero' := by simp, map_one' := by simp, map_mul' := by simp, }

add_decl_doc zero_hom.comp

add_decl_doc add_hom.comp

add_decl_doc add_monoid_hom.comp

@[simp, to_additive] lemma one_hom.coe_comp [has_one M] [has_one N] [has_one P]

(g : one_hom N P) (f : one_hom M N) :

⇑(g.comp f) = g ∘ f := rfl

@[simp, to_additive] lemma mul_hom.coe_comp [has_mul M] [has_mul N] [has_mul P]

(g : N →ₙ* P) (f : M →ₙ* N) :

⇑(g.comp f) = g ∘ f := rfl

@[simp, to_additive] lemma monoid_hom.coe_comp [mul_one_class M] [mul_one_class N] [mul_one_class P]

(g : N →* P) (f : M →* N) :

⇑(g.comp f) = g ∘ f := rfl

@[simp] lemma monoid_with_zero_hom.coe_comp [mul_zero_one_class M] [mul_zero_one_class N]

[mul_zero_one_class P] (g : N →*₀ P) (f : M →*₀ N) :

⇑(g.comp f) = g ∘ f := rfl

@[to_additive] lemma one_hom.comp_apply [has_one M] [has_one N] [has_one P]

(g : one_hom N P) (f : one_hom M N) (x : M) :

g.comp f x = g (f x) := rfl

@[to_additive] lemma mul_hom.comp_apply [has_mul M] [has_mul N] [has_mul P]

(g : N →ₙ* P) (f : M →ₙ* N) (x : M) :

g.comp f x = g (f x) := rfl

@[to_additive] lemma monoid_hom.comp_apply [mul_one_class M] [mul_one_class N] [mul_one_class P]

(g : N →* P) (f : M →* N) (x : M) :

g.comp f x = g (f x) := rfl

lemma monoid_with_zero_hom.comp_apply [mul_zero_one_class M] [mul_zero_one_class N]

[mul_zero_one_class P] (g : N →*₀ P) (f : M →*₀ N) (x : M) :

g.comp f x = g (f x) := rfl

lemma one_hom.comp_assoc {Q : Type*} [has_one M] [has_one N] [has_one P] [has_one Q]

(f : one_hom M N) (g : one_hom N P) (h : one_hom P Q) :

(h.comp g).comp f = h.comp (g.comp f) := rfl

@[to_additive] lemma mul_hom.comp_assoc {Q : Type*} [has_mul M] [has_mul N] [has_mul P] [has_mul Q]

(f : M →ₙ* N) (g : N →ₙ* P) (h : P →ₙ* Q) :

(h.comp g).comp f = h.comp (g.comp f) := rfl

@[to_additive] lemma monoid_hom.comp_assoc {Q : Type*}

[mul_one_class M] [mul_one_class N] [mul_one_class P] [mul_one_class Q]

(f : M →* N) (g : N →* P) (h : P →* Q) :

(h.comp g).comp f = h.comp (g.comp f) := rfl

lemma monoid_with_zero_hom.comp_assoc {Q : Type*}

[mul_zero_one_class M] [mul_zero_one_class N] [mul_zero_one_class P] [mul_zero_one_class Q]

(f : M →*₀ N) (g : N →*₀ P) (h : P →*₀ Q) :

(h.comp g).comp f = h.comp (g.comp f) := rfl

lemma one_hom.cancel_right [has_one M] [has_one N] [has_one P]

{g₁ g₂ : one_hom N P} {f : one_hom M N} (hf : function.surjective f) :

g₁.comp f = g₂.comp f ↔ g₁ = g₂ :=

⟨λ h, one_hom.ext $ hf.forall.2 (one_hom.ext_iff.1 h), λ h, h ▸ rfl⟩

lemma mul_hom.cancel_right [has_mul M] [has_mul N] [has_mul P]

{g₁ g₂ : N →ₙ* P} {f : M →ₙ* N} (hf : function.surjective f) :

g₁.comp f = g₂.comp f ↔ g₁ = g₂ :=

⟨λ h, mul_hom.ext $ hf.forall.2 (mul_hom.ext_iff.1 h), λ h, h ▸ rfl⟩

lemma monoid_hom.cancel_right

[mul_one_class M] [mul_one_class N] [mul_one_class P]

{g₁ g₂ : N →* P} {f : M →* N} (hf : function.surjective f) :

g₁.comp f = g₂.comp f ↔ g₁ = g₂ :=

⟨λ h, monoid_hom.ext $ hf.forall.2 (monoid_hom.ext_iff.1 h), λ h, h ▸ rfl⟩

lemma monoid_with_zero_hom.cancel_right [mul_zero_one_class M] [mul_zero_one_class N]

[mul_zero_one_class P] {g₁ g₂ : N →*₀ P} {f : M →*₀ N} (hf : function.surjective f) :

g₁.comp f = g₂.comp f ↔ g₁ = g₂ :=

⟨λ h, monoid_with_zero_hom.ext $ hf.forall.2 (monoid_with_zero_hom.ext_iff.1 h),

λ h, h ▸ rfl⟩

lemma one_hom.cancel_left [has_one M] [has_one N] [has_one P]

{g : one_hom N P} {f₁ f₂ : one_hom M N} (hg : function.injective g) :

g.comp f₁ = g.comp f₂ ↔ f₁ = f₂ :=

⟨λ h, one_hom.ext $ λ x, hg $ by rw [← one_hom.comp_apply, h, one_hom.comp_apply],

λ h, h ▸ rfl⟩

lemma mul_hom.cancel_left [has_mul M] [has_mul N] [has_mul P]

{g : N →ₙ* P} {f₁ f₂ : M →ₙ* N} (hg : function.injective g) :

g.comp f₁ = g.comp f₂ ↔ f₁ = f₂ :=

⟨λ h, mul_hom.ext $ λ x, hg $ by rw [← mul_hom.comp_apply, h, mul_hom.comp_apply],

λ h, h ▸ rfl⟩

lemma monoid_hom.cancel_left [mul_one_class M] [mul_one_class N] [mul_one_class P]

{g : N →* P} {f₁ f₂ : M →* N} (hg : function.injective g) :

g.comp f₁ = g.comp f₂ ↔ f₁ = f₂ :=

⟨λ h, monoid_hom.ext $ λ x, hg $ by rw [← monoid_hom.comp_apply, h, monoid_hom.comp_apply],

λ h, h ▸ rfl⟩

lemma monoid_with_zero_hom.cancel_left [mul_zero_one_class M] [mul_zero_one_class N]

[mul_zero_one_class P] {g : N →*₀ P} {f₁ f₂ : M →*₀ N} (hg : function.injective g) :

g.comp f₁ = g.comp f₂ ↔ f₁ = f₂ :=

⟨λ h, monoid_with_zero_hom.ext $ λ x, hg $ by rw [

← monoid_with_zero_hom.comp_apply, h, monoid_with_zero_hom.comp_apply],

λ h, h ▸ rfl⟩

lemma monoid_hom.to_one_hom_injective [mul_one_class M] [mul_one_class N] :

function.injective (monoid_hom.to_one_hom : (M →* N) → one_hom M N) :=

λ f g h, monoid_hom.ext $ one_hom.ext_iff.mp h

lemma monoid_hom.to_mul_hom_injective [mul_one_class M] [mul_one_class N] :

function.injective (monoid_hom.to_mul_hom : (M →* N) → M →ₙ* N) :=

λ f g h, monoid_hom.ext $ mul_hom.ext_iff.mp h

lemma monoid_with_zero_hom.to_monoid_hom_injective [mul_zero_one_class M] [mul_zero_one_class N] :

function.injective (monoid_with_zero_hom.to_monoid_hom : (M →*₀ N) → M →* N) :=

λ f g h, monoid_with_zero_hom.ext $ monoid_hom.ext_iff.mp h

lemma monoid_with_zero_hom.to_zero_hom_injective [mul_zero_one_class M] [mul_zero_one_class N] :

function.injective (monoid_with_zero_hom.to_zero_hom : (M →*₀ N) → zero_hom M N) :=

λ f g h, monoid_with_zero_hom.ext $ zero_hom.ext_iff.mp h

@[simp, to_additive] lemma one_hom.comp_id [has_one M] [has_one N]

(f : one_hom M N) : f.comp (one_hom.id M) = f := one_hom.ext $ λ x, rfl

@[simp, to_additive] lemma mul_hom.comp_id [has_mul M] [has_mul N]

(f : M →ₙ* N) : f.comp (mul_hom.id M) = f := mul_hom.ext $ λ x, rfl

@[simp, to_additive] lemma monoid_hom.comp_id [mul_one_class M] [mul_one_class N]

(f : M →* N) : f.comp (monoid_hom.id M) = f := monoid_hom.ext $ λ x, rfl

@[simp] lemma monoid_with_zero_hom.comp_id [mul_zero_one_class M] [mul_zero_one_class N]

(f : M →*₀ N) : f.comp (monoid_with_zero_hom.id M) = f :=

monoid_with_zero_hom.ext $ λ x, rfl

@[simp, to_additive] lemma one_hom.id_comp [has_one M] [has_one N]

(f : one_hom M N) : (one_hom.id N).comp f = f := one_hom.ext $ λ x, rfl

@[simp, to_additive] lemma mul_hom.id_comp [has_mul M] [has_mul N]

(f : M →ₙ* N) : (mul_hom.id N).comp f = f := mul_hom.ext $ λ x, rfl

@[simp, to_additive] lemma monoid_hom.id_comp [mul_one_class M] [mul_one_class N]

(f : M →* N) : (monoid_hom.id N).comp f = f := monoid_hom.ext $ λ x, rfl

@[simp] lemma monoid_with_zero_hom.id_comp [mul_zero_one_class M] [mul_zero_one_class N]

(f : M →*₀ N) : (monoid_with_zero_hom.id N).comp f = f :=

monoid_with_zero_hom.ext $ λ x, rfl

protected theorem monoid_hom.map_pow [monoid M] [monoid N] (f : M →* N) (a : M) (n : ℕ) :

f (a ^ n) = (f a) ^ n :=

map_pow f a n

protected theorem monoid_hom.map_zpow' [div_inv_monoid M] [div_inv_monoid N] (f : M →* N)

(hf : ∀ x, f (x⁻¹) = (f x)⁻¹) (a : M) (n : ℤ) :

f (a ^ n) = (f a) ^ n :=

map_zpow' f hf a n

section End

namespace monoid

variables (M) [mul_one_class M]

protected def End := M →* M

namespace End

instance : monoid (monoid.End M) :=

{ mul := monoid_hom.comp,

one := monoid_hom.id M,

mul_assoc := λ _ _ _, monoid_hom.comp_assoc _ _ _,

mul_one := monoid_hom.comp_id,

one_mul := monoid_hom.id_comp }

instance : inhabited (monoid.End M) := ⟨1⟩

instance : monoid_hom_class (monoid.End M) M M := monoid_hom.monoid_hom_class

end End

@[simp] lemma coe_one : ((1 : monoid.End M) : M → M) = id := rfl

@[simp] lemma coe_mul (f g) : ((f * g : monoid.End M) : M → M) = f ∘ g := rfl

end monoid

namespace add_monoid

variables (A : Type*) [add_zero_class A]

protected def End := A →+ A

namespace End

instance : monoid (add_monoid.End A) :=