mathlib documentation

algebra.group.hom

monoid and group homomorphisms

This file defines the bundled structures for monoid and group homomorphisms. Namely, we define monoid_hom (resp., add_monoid_hom) to be bundled homomorphisms between multiplicative (resp., additive) monoids or groups.

We also define coercion to a function, and usual operations: composition, identity homomorphism, pointwise multiplication and pointwise inversion.

Notations

implementation notes

There's a coercion from bundled homs to fun, and the canonical notation is to use the bundled hom as a function via this coercion.

There is no group_hom -- the idea is that monoid_hom is used. The constructor for monoid_hom needs a proof of map_one as well as map_mul; a separate constructor monoid_hom.mk' will construct group homs (i.e. monoid homs between groups) given only a proof that multiplication is preserved,

Implicit {} brackets are often used instead of type class [] brackets. This is done when the instances can be inferred because they are implicit arguments to the type monoid_hom. When they can be inferred from the type it is faster to use this method than to use type class inference.

Historically this file also included definitions of unbundled homomorphism classes; they were deprecated and moved to deprecated/group.

Tags

monoid_hom, add_monoid_hom

structure zero_hom (M : Type u_6) (N : Type u_7) [has_zero M] [has_zero N] :
Type (max u_6 u_7)
  • to_fun : M → N
  • map_zero' : c.to_fun 0 = 0

Homomorphism that preserves zero

structure add_hom (M : Type u_6) (N : Type u_7) [has_add M] [has_add N] :
Type (max u_6 u_7)

Homomorphism that preserves addition

@[nolint]
def add_monoid_hom.to_add_hom {M : Type u_6} {N : Type u_7} [add_monoid M] [add_monoid N] :
(M →+ N)add_hom M N

structure add_monoid_hom (M : Type u_6) (N : Type u_7) [add_monoid M] [add_monoid N] :
Type (max u_6 u_7)

Bundled add_monoid homomorphisms; use this for bundled add_group homomorphisms too.

@[nolint]
def add_monoid_hom.to_zero_hom {M : Type u_6} {N : Type u_7} [add_monoid M] [add_monoid N] :
(M →+ N)zero_hom M N

structure one_hom (M : Type u_6) (N : Type u_7) [has_one M] [has_one N] :
Type (max u_6 u_7)
  • to_fun : M → N
  • map_one' : c.to_fun 1 = 1

Homomorphism that preserves one

structure mul_hom (M : Type u_6) (N : Type u_7) [has_mul M] [has_mul N] :
Type (max u_6 u_7)

Homomorphism that preserves multiplication

structure monoid_hom (M : Type u_6) (N : Type u_7) [monoid M] [monoid N] :
Type (max u_6 u_7)

Bundled monoid homomorphisms; use this for bundled group homomorphisms too.

@[nolint]
def monoid_hom.to_one_hom {M : Type u_6} {N : Type u_7} [monoid M] [monoid N] :
(M →* N)one_hom M N

@[nolint]
def monoid_hom.to_mul_hom {M : Type u_6} {N : Type u_7} [monoid M] [monoid N] :
(M →* N)mul_hom M N

@[instance]
def zero_hom.has_coe_to_fun {M : Type u_1} {N : Type u_2} {mM : has_zero M} {mN : has_zero N} :

@[instance]
def one_hom.has_coe_to_fun {M : Type u_1} {N : Type u_2} {mM : has_one M} {mN : has_one N} :

Equations
@[instance]
def mul_hom.has_coe_to_fun {M : Type u_1} {N : Type u_2} {mM : has_mul M} {mN : has_mul N} :

Equations
@[instance]
def add_hom.has_coe_to_fun {M : Type u_1} {N : Type u_2} {mM : has_add M} {mN : has_add N} :

@[instance]
def monoid_hom.has_coe_to_fun {M : Type u_1} {N : Type u_2} {mM : monoid M} {mN : monoid N} :

Equations
@[instance]
def add_monoid_hom.has_coe_to_fun {M : Type u_1} {N : Type u_2} {mM : add_monoid M} {mN : add_monoid N} :

@[simp]
theorem zero_hom.to_fun_eq_coe {M : Type u_1} {N : Type u_2} [has_zero M] [has_zero N] (f : zero_hom M N) :

@[simp]
theorem one_hom.to_fun_eq_coe {M : Type u_1} {N : Type u_2} [has_one M] [has_one N] (f : one_hom M N) :

@[simp]
theorem add_hom.to_fun_eq_coe {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] (f : add_hom M N) :

@[simp]
theorem mul_hom.to_fun_eq_coe {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] (f : mul_hom M N) :

@[simp]
theorem add_monoid_hom.to_fun_eq_coe {M : Type u_1} {N : Type u_2} [add_monoid M] [add_monoid N] (f : M →+ N) :

@[simp]
theorem monoid_hom.to_fun_eq_coe {M : Type u_1} {N : Type u_2} [monoid M] [monoid N] (f : M →* N) :

@[simp]
theorem one_hom.coe_mk {M : Type u_1} {N : Type u_2} [has_one M] [has_one N] (f : M → N) (h1 : f 1 = 1) :
{to_fun := f, map_one' := h1} = f

@[simp]
theorem zero_hom.coe_mk {M : Type u_1} {N : Type u_2} [has_zero M] [has_zero N] (f : M → N) (h1 : f 0 = 0) :
{to_fun := f, map_zero' := h1} = f

@[simp]
theorem mul_hom.coe_mk {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] (f : M → N) (hmul : ∀ (x y : M), f (x * y) = (f x) * f y) :
{to_fun := f, map_mul' := hmul} = f

@[simp]
theorem add_hom.coe_mk {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] (f : M → N) (hmul : ∀ (x y : M), f (x + y) = f x + f y) :
{to_fun := f, map_add' := hmul} = f

@[simp]
theorem add_monoid_hom.coe_mk {M : Type u_1} {N : Type u_2} [add_monoid M] [add_monoid N] (f : M → N) (h1 : f 0 = 0) (hmul : ∀ (x y : M), f (x + y) = f x + f y) :
{to_fun := f, map_zero' := h1, map_add' := hmul} = f

@[simp]
theorem monoid_hom.coe_mk {M : Type u_1} {N : Type u_2} [monoid M] [monoid N] (f : M → N) (h1 : f 1 = 1) (hmul : ∀ (x y : M), f (x * y) = (f x) * f y) :
{to_fun := f, map_one' := h1, map_mul' := hmul} = f

theorem zero_hom.congr_fun {M : Type u_1} {N : Type u_2} [has_zero M] [has_zero N] {f g : zero_hom M N} (h : f = g) (x : M) :
f x = g x

theorem one_hom.congr_fun {M : Type u_1} {N : Type u_2} [has_one M] [has_one N] {f g : one_hom M N} (h : f = g) (x : M) :
f x = g x

theorem mul_hom.congr_fun {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] {f g : mul_hom M N} (h : f = g) (x : M) :
f x = g x

theorem add_hom.congr_fun {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] {f g : add_hom M N} (h : f = g) (x : M) :
f x = g x

theorem monoid_hom.congr_fun {M : Type u_1} {N : Type u_2} [monoid M] [monoid N] {f g : M →* N} (h : f = g) (x : M) :
f x = g x

theorem add_monoid_hom.congr_fun {M : Type u_1} {N : Type u_2} [add_monoid M] [add_monoid N] {f g : M →+ N} (h : f = g) (x : M) :
f x = g x

theorem one_hom.congr_arg {M : Type u_1} {N : Type u_2} [has_one M] [has_one N] (f : one_hom M N) {x y : M} :
x = yf x = f y

theorem zero_hom.congr_arg {M : Type u_1} {N : Type u_2} [has_zero M] [has_zero N] (f : zero_hom M N) {x y : M} :
x = yf x = f y

theorem mul_hom.congr_arg {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] (f : mul_hom M N) {x y : M} :
x = yf x = f y

theorem add_hom.congr_arg {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] (f : add_hom M N) {x y : M} :
x = yf x = f y

theorem monoid_hom.congr_arg {M : Type u_1} {N : Type u_2} [monoid M] [monoid N] (f : M →* N) {x y : M} :
x = yf x = f y

theorem add_monoid_hom.congr_arg {M : Type u_1} {N : Type u_2} [add_monoid M] [add_monoid N] (f : M →+ N) {x y : M} :
x = yf x = f y

theorem zero_hom.coe_inj {M : Type u_1} {N : Type u_2} [has_zero M] [has_zero N] ⦃f g : zero_hom M N⦄ :
f = gf = g

theorem one_hom.coe_inj {M : Type u_1} {N : Type u_2} [has_one M] [has_one N] ⦃f g : one_hom M N⦄ :
f = gf = g

theorem add_hom.coe_inj {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] ⦃f g : add_hom M N⦄ :
f = gf = g

theorem mul_hom.coe_inj {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] ⦃f g : mul_hom M N⦄ :
f = gf = g

theorem add_monoid_hom.coe_inj {M : Type u_1} {N : Type u_2} [add_monoid M] [add_monoid N] ⦃f g : M →+ N⦄ :
f = gf = g

theorem monoid_hom.coe_inj {M : Type u_1} {N : Type u_2} [monoid M] [monoid N] ⦃f g : M →* N⦄ :
f = gf = g

@[ext]
theorem zero_hom.ext {M : Type u_1} {N : Type u_2} [has_zero M] [has_zero N] ⦃f g : zero_hom M N⦄ :
(∀ (x : M), f x = g x)f = g

@[ext]
theorem one_hom.ext {M : Type u_1} {N : Type u_2} [has_one M] [has_one N] ⦃f g : one_hom M N⦄ :
(∀ (x : M), f x = g x)f = g

@[ext]
theorem mul_hom.ext {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] ⦃f g : mul_hom M N⦄ :
(∀ (x : M), f x = g x)f = g

@[ext]
theorem add_hom.ext {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] ⦃f g : add_hom M N⦄ :
(∀ (x : M), f x = g x)f = g

@[ext]
theorem monoid_hom.ext {M : Type u_1} {N : Type u_2} [monoid M] [monoid N] ⦃f g : M →* N⦄ :
(∀ (x : M), f x = g x)f = g

@[ext]
theorem add_monoid_hom.ext {M : Type u_1} {N : Type u_2} [add_monoid M] [add_monoid N] ⦃f g : M →+ N⦄ :
(∀ (x : M), f x = g x)f = g

theorem zero_hom.ext_iff {M : Type u_1} {N : Type u_2} [has_zero M] [has_zero N] {f g : zero_hom M N} :
f = g ∀ (x : M), f x = g x

theorem one_hom.ext_iff {M : Type u_1} {N : Type u_2} [has_one M] [has_one N] {f g : one_hom M N} :
f = g ∀ (x : M), f x = g x

theorem add_hom.ext_iff {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] {f g : add_hom M N} :
f = g ∀ (x : M), f x = g x

theorem mul_hom.ext_iff {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] {f g : mul_hom M N} :
f = g ∀ (x : M), f x = g x

theorem monoid_hom.ext_iff {M : Type u_1} {N : Type u_2} [monoid M] [monoid N] {f g : M →* N} :
f = g ∀ (x : M), f x = g x

theorem add_monoid_hom.ext_iff {M : Type u_1} {N : Type u_2} [add_monoid M] [add_monoid N] {f g : M →+ N} :
f = g ∀ (x : M), f x = g x

@[simp]
theorem one_hom.map_one {M : Type u_1} {N : Type u_2} [has_one M] [has_one N] (f : one_hom M N) :
f 1 = 1

@[simp]
theorem zero_hom.map_zero {M : Type u_1} {N : Type u_2} [has_zero M] [has_zero N] (f : zero_hom M N) :
f 0 = 0

@[simp]
theorem add_monoid_hom.map_zero {M : Type u_1} {N : Type u_2} [add_monoid M] [add_monoid N] (f : M →+ N) :
f 0 = 0

If f is an additive monoid homomorphism then f 0 = 0.

@[simp]
theorem monoid_hom.map_one {M : Type u_1} {N : Type u_2} [monoid M] [monoid N] (f : M →* N) :
f 1 = 1

If f is a monoid homomorphism then f 1 = 1.

@[simp]
theorem mul_hom.map_mul {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] (f : mul_hom M N) (a b : M) :
f (a * b) = (f a) * f b

@[simp]
theorem add_hom.map_add {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] (f : add_hom M N) (a b : M) :
f (a + b) = f a + f b

@[simp]
theorem monoid_hom.map_mul {M : Type u_1} {N : Type u_2} [monoid M] [monoid N] (f : M →* N) (a b : M) :
f (a * b) = (f a) * f b

If f is a monoid homomorphism then f (a * b) = f a * f b.

@[simp]
theorem add_monoid_hom.map_add {M : Type u_1} {N : Type u_2} [add_monoid M] [add_monoid N] (f : M →+ N) (a b : M) :
f (a + b) = f a + f b

If f is an additive monoid homomorphism then f (a + b) = f a + f b.

theorem add_monoid_hom.map_add_eq_zero {M : Type u_1} {N : Type u_2} {mM : add_monoid M} {mN : add_monoid N} (f : M →+ N) {a b : M} :
a + b = 0f a + f b = 0

theorem monoid_hom.map_mul_eq_one {M : Type u_1} {N : Type u_2} {mM : monoid M} {mN : monoid N} (f : M →* N) {a b : M} :
a * b = 1(f a) * f b = 1

theorem monoid_hom.map_exists_right_inv {M : Type u_1} {N : Type u_2} {mM : monoid M} {mN : monoid N} (f : M →* N) {x : M} :
(∃ (y : M), x * y = 1)(∃ (y : N), (f x) * y = 1)

Given a monoid homomorphism f : M →* N and an element x : M, if x has a right inverse, then f x has a right inverse too. For elements invertible on both sides see is_unit.map.

theorem add_monoid_hom.map_exists_right_neg {M : Type u_1} {N : Type u_2} {mM : add_monoid M} {mN : add_monoid N} (f : M →+ N) {x : M} :
(∃ (y : M), x + y = 0)(∃ (y : N), f x + y = 0)

Given an add_monoid homomorphism f : M →+ N and an element x : M, if x has a right inverse, then f x has a right inverse too.

theorem add_monoid_hom.map_exists_left_neg {M : Type u_1} {N : Type u_2} {mM : add_monoid M} {mN : add_monoid N} (f : M →+ N) {x : M} :
(∃ (y : M), y + x = 0)(∃ (y : N), y + f x = 0)

Given an add_monoid homomorphism f : M →+ N and an element x : M, if x has a left inverse, then f x has a left inverse too. For elements invertible on both sides see is_add_unit.map.

theorem monoid_hom.map_exists_left_inv {M : Type u_1} {N : Type u_2} {mM : monoid M} {mN : monoid N} (f : M →* N) {x : M} :
(∃ (y : M), y * x = 1)(∃ (y : N), y * f x = 1)

Given a monoid homomorphism f : M →* N and an element x : M, if x has a left inverse, then f x has a left inverse too. For elements invertible on both sides see is_unit.map.

def zero_hom.id (M : Type u_1) [has_zero M] :

The identity map from an type with zero to itself.

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

The identity map from a type with 1 to itself.

Equations
def mul_hom.id (M : Type u_1) [has_mul M] :

The identity map from a type with multiplication to itself.

Equations
def add_hom.id (M : Type u_1) [has_add M] :

The identity map from an type with addition to itself.

def monoid_hom.id (M : Type u_1) [monoid M] :
M →* M

The identity map from a monoid to itself.

Equations
def add_monoid_hom.id (M : Type u_1) [add_monoid M] :
M →+ M

The identity map from an additive monoid to itself.

@[simp]
theorem one_hom.id_apply {M : Type u_1} [has_one M] (x : M) :

@[simp]
theorem zero_hom.id_apply {M : Type u_1} [has_zero M] (x : M) :

@[simp]
theorem mul_hom.id_apply {M : Type u_1} [has_mul M] (x : M) :

@[simp]
theorem add_hom.id_apply {M : Type u_1} [has_add M] (x : M) :

@[simp]
theorem monoid_hom.id_apply {M : Type u_1} [monoid M] (x : M) :

@[simp]
theorem add_monoid_hom.id_apply {M : Type u_1} [add_monoid M] (x : M) :

def zero_hom.comp {M : Type u_1} {N : Type u_2} {P : Type u_3} [has_zero M] [has_zero N] [has_zero P] :
zero_hom N Pzero_hom M Nzero_hom M P

Composition of zero_homs as a zero_hom.

def one_hom.comp {M : Type u_1} {N : Type u_2} {P : Type u_3} [has_one M] [has_one N] [has_one P] :
one_hom N Pone_hom M None_hom M P

Composition of one_homs as a one_hom.

Equations
def mul_hom.comp {M : Type u_1} {N : Type u_2} {P : Type u_3} [has_mul M] [has_mul N] [has_mul P] :
mul_hom N Pmul_hom M Nmul_hom M P

Composition of mul_homs as a mul_hom.

Equations
def add_hom.comp {M : Type u_1} {N : Type u_2} {P : Type u_3} [has_add M] [has_add N] [has_add P] :
add_hom N Padd_hom M Nadd_hom M P

Composition of add_homs as a add_hom.

def monoid_hom.comp {M : Type u_1} {N : Type u_2} {P : Type u_3} [monoid M] [monoid N] [monoid P] :
(N →* P)(M →* N)M →* P

Composition of monoid morphisms as a monoid morphism.

Equations
def add_monoid_hom.comp {M : Type u_1} {N : Type u_2} {P : Type u_3} [add_monoid M] [add_monoid N] [add_monoid P] :
(N →+ P)(M →+ N)M →+ P

Composition of additive monoid morphisms as an additive monoid morphism.

@[simp]
theorem zero_hom.coe_comp {M : Type u_1} {N : Type u_2} {P : Type u_3} [has_zero M] [has_zero N] [has_zero P] (g : zero_hom N P) (f : zero_hom M N) :
(g.comp f) = g f

@[simp]
theorem one_hom.coe_comp {M : Type u_1} {N : Type u_2} {P : Type u_3} [has_one M] [has_one N] [has_one P] (g : one_hom N P) (f : one_hom M N) :
(g.comp f) = g f

@[simp]
theorem mul_hom.coe_comp {M : Type u_1} {N : Type u_2} {P : Type u_3} [has_mul M] [has_mul N] [has_mul P] (g : mul_hom N P) (f : mul_hom M N) :
(g.comp f) = g f

@[simp]
theorem add_hom.coe_comp {M : Type u_1} {N : Type u_2} {P : Type u_3} [has_add M] [has_add N] [has_add P] (g : add_hom N P) (f : add_hom M N) :
(g.comp f) = g f

@[simp]
theorem add_monoid_hom.coe_comp {M : Type u_1} {N : Type u_2} {P : Type u_3} [add_monoid M] [add_monoid N] [add_monoid P] (g : N →+ P) (f : M →+ N) :
(g.comp f) = g f

@[simp]
theorem monoid_hom.coe_comp {M : Type u_1} {N : Type u_2} {P : Type u_3} [monoid M] [monoid N] [monoid P] (g : N →* P) (f : M →* N) :
(g.comp f) = g f

theorem one_hom.comp_apply {M : Type u_1} {N : Type u_2} {P : Type u_3} [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)

theorem zero_hom.comp_apply {M : Type u_1} {N : Type u_2} {P : Type u_3} [has_zero M] [has_zero N] [has_zero P] (g : zero_hom N P) (f : zero_hom M N) (x : M) :
(g.comp f) x = g (f x)

theorem add_hom.comp_apply {M : Type u_1} {N : Type u_2} {P : Type u_3} [has_add M] [has_add N] [has_add P] (g : add_hom N P) (f : add_hom M N) (x : M) :
(g.comp f) x = g (f x)

theorem mul_hom.comp_apply {M : Type u_1} {N : Type u_2} {P : Type u_3} [has_mul M] [has_mul N] [has_mul P] (g : mul_hom N P) (f : mul_hom M N) (x : M) :
(g.comp f) x = g (f x)

theorem monoid_hom.comp_apply {M : Type u_1} {N : Type u_2} {P : Type u_3} [monoid M] [monoid N] [monoid P] (g : N →* P) (f : M →* N) (x : M) :
(g.comp f) x = g (f x)

theorem add_monoid_hom.comp_apply {M : Type u_1} {N : Type u_2} {P : Type u_3} [add_monoid M] [add_monoid N] [add_monoid P] (g : N →+ P) (f : M →+ N) (x : M) :
(g.comp f) x = g (f x)

theorem one_hom.comp_assoc {M : Type u_1} {N : Type u_2} {P : Type u_3} {Q : Type u_4} [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)

Composition of monoid homomorphisms is associative.

theorem zero_hom.comp_assoc {M : Type u_1} {N : Type u_2} {P : Type u_3} {Q : Type u_4} [has_zero M] [has_zero N] [has_zero P] [has_zero Q] (f : zero_hom M N) (g : zero_hom N P) (h : zero_hom P Q) :
(h.comp g).comp f = h.comp (g.comp f)

theorem add_hom.comp_assoc {M : Type u_1} {N : Type u_2} {P : Type u_3} {Q : Type u_4} [has_add M] [has_add N] [has_add P] [has_add Q] (f : add_hom M N) (g : add_hom N P) (h : add_hom P Q) :
(h.comp g).comp f = h.comp (g.comp f)

theorem mul_hom.comp_assoc {M : Type u_1} {N : Type u_2} {P : Type u_3} {Q : Type u_4} [has_mul M] [has_mul N] [has_mul P] [has_mul Q] (f : mul_hom M N) (g : mul_hom N P) (h : mul_hom P Q) :
(h.comp g).comp f = h.comp (g.comp f)

theorem add_monoid_hom.comp_assoc {M : Type u_1} {N : Type u_2} {P : Type u_3} {Q : Type u_4} [add_monoid M] [add_monoid N] [add_monoid P] [add_monoid Q] (f : M →+ N) (g : N →+ P) (h : P →+ Q) :
(h.comp g).comp f = h.comp (g.comp f)

theorem monoid_hom.comp_assoc {M : Type u_1} {N : Type u_2} {P : Type u_3} {Q : Type u_4} [monoid M] [monoid N] [monoid P] [monoid Q] (f : M →* N) (g : N →* P) (h : P →* Q) :
(h.comp g).comp f = h.comp (g.comp f)

theorem zero_hom.cancel_right {M : Type u_1} {N : Type u_2} {P : Type u_3} [has_zero M] [has_zero N] [has_zero P] {g₁ g₂ : zero_hom N P} {f : zero_hom M N} :
function.surjective f(g₁.comp f = g₂.comp f g₁ = g₂)

theorem one_hom.cancel_right {M : Type u_1} {N : Type u_2} {P : Type u_3} [has_one M] [has_one N] [has_one P] {g₁ g₂ : one_hom N P} {f : one_hom M N} :
function.surjective f(g₁.comp f = g₂.comp f g₁ = g₂)

theorem add_hom.cancel_right {M : Type u_1} {N : Type u_2} {P : Type u_3} [has_add M] [has_add N] [has_add P] {g₁ g₂ : add_hom N P} {f : add_hom M N} :
function.surjective f(g₁.comp f = g₂.comp f g₁ = g₂)

theorem mul_hom.cancel_right {M : Type u_1} {N : Type u_2} {P : Type u_3} [has_mul M] [has_mul N] [has_mul P] {g₁ g₂ : mul_hom N P} {f : mul_hom M N} :
function.surjective f(g₁.comp f = g₂.comp f g₁ = g₂)

theorem add_monoid_hom.cancel_right {M : Type u_1} {N : Type u_2} {P : Type u_3} [add_monoid M] [add_monoid N] [add_monoid P] {g₁ g₂ : N →+ P} {f : M →+ N} :
function.surjective f(g₁.comp f = g₂.comp f g₁ = g₂)

theorem monoid_hom.cancel_right {M : Type u_1} {N : Type u_2} {P : Type u_3} [monoid M] [monoid N] [monoid P] {g₁ g₂ : N →* P} {f : M →* N} :
function.surjective f(g₁.comp f = g₂.comp f g₁ = g₂)

theorem one_hom.cancel_left {M : Type u_1} {N : Type u_2} {P : Type u_3} [has_one M] [has_one N] [has_one P] {g : one_hom N P} {f₁ f₂ : one_hom M N} :
function.injective g(g.comp f₁ = g.comp f₂ f₁ = f₂)

theorem zero_hom.cancel_left {M : Type u_1} {N : Type u_2} {P : Type u_3} [has_zero M] [has_zero N] [has_zero P] {g : zero_hom N P} {f₁ f₂ : zero_hom M N} :
function.injective g(g.comp f₁ = g.comp f₂ f₁ = f₂)

theorem mul_hom.cancel_left {M : Type u_1} {N : Type u_2} {P : Type u_3} [has_one M] [has_one N] [has_one P] {g : one_hom N P} {f₁ f₂ : one_hom M N} :
function.injective g(g.comp f₁ = g.comp f₂ f₁ = f₂)

theorem add_hom.cancel_left {M : Type u_1} {N : Type u_2} {P : Type u_3} [has_zero M] [has_zero N] [has_zero P] {g : zero_hom N P} {f₁ f₂ : zero_hom M N} :
function.injective g(g.comp f₁ = g.comp f₂ f₁ = f₂)

theorem monoid_hom.cancel_left {M : Type u_1} {N : Type u_2} {P : Type u_3} [monoid M] [monoid N] [monoid P] {g : N →* P} {f₁ f₂ : M →* N} :
function.injective g(g.comp f₁ = g.comp f₂ f₁ = f₂)

theorem add_monoid_hom.cancel_left {M : Type u_1} {N : Type u_2} {P : Type u_3} [add_monoid M] [add_monoid N] [add_monoid P] {g : N →+ P} {f₁ f₂ : M →+ N} :
function.injective g(g.comp f₁ = g.comp f₂ f₁ = f₂)

@[simp]
theorem zero_hom.comp_id {M : Type u_1} {N : Type u_2} [has_zero M] [has_zero N] (f : zero_hom M N) :

@[simp]
theorem one_hom.comp_id {M : Type u_1} {N : Type u_2} [has_one M] [has_one N] (f : one_hom M N) :
f.comp (one_hom.id M) = f

@[simp]
theorem add_hom.comp_id {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] (f : add_hom M N) :
f.comp (add_hom.id M) = f

@[simp]
theorem mul_hom.comp_id {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] (f : mul_hom M N) :
f.comp (mul_hom.id M) = f

@[simp]
theorem monoid_hom.comp_id {M : Type u_1} {N : Type u_2} [monoid M] [monoid N] (f : M →* N) :

@[simp]
theorem add_monoid_hom.comp_id {M : Type u_1} {N : Type u_2} [add_monoid M] [add_monoid N] (f : M →+ N) :

@[simp]
theorem zero_hom.id_comp {M : Type u_1} {N : Type u_2} [has_zero M] [has_zero N] (f : zero_hom M N) :

@[simp]
theorem one_hom.id_comp {M : Type u_1} {N : Type u_2} [has_one M] [has_one N] (f : one_hom M N) :
(one_hom.id N).comp f = f

@[simp]
theorem mul_hom.id_comp {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] (f : mul_hom M N) :
(mul_hom.id N).comp f = f

@[simp]
theorem add_hom.id_comp {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] (f : add_hom M N) :
(add_hom.id N).comp f = f

@[simp]
theorem add_monoid_hom.id_comp {M : Type u_1} {N : Type u_2} [add_monoid M] [add_monoid N] (f : M →+ N) :

@[simp]
theorem monoid_hom.id_comp {M : Type u_1} {N : Type u_2} [monoid M] [monoid N] (f : M →* N) :

def monoid.End (M : Type u_1) [monoid M] :
Type u_1

The monoid of endomorphisms.

Equations
@[instance]
def monoid.End.monoid (M : Type u_1) [monoid M] :

Equations
@[instance]
def monoid.End.inhabited (M : Type u_1) [monoid M] :

Equations
@[instance]

Equations
@[simp]
theorem monoid.coe_one (M : Type u_1) [monoid M] :

@[simp]
theorem monoid.coe_mul (M : Type u_1) [monoid M] (f g : monoid.End M) :
f * g = f g

def add_monoid.End (A : Type u_6) [add_monoid A] :
Type u_6

The monoid of endomorphisms.

Equations
@[instance]
def add_monoid.End.monoid (A : Type u_6) [add_monoid A] :

Equations
@[instance]

Equations
@[instance]

Equations
@[simp]
theorem add_monoid.coe_one (A : Type u_6) [add_monoid A] :

@[simp]
theorem add_monoid.coe_mul (A : Type u_6) [add_monoid A] (f g : add_monoid.End A) :
f * g = f g

@[instance]
def one_hom.has_one {M : Type u_1} {N : Type u_2} [has_one M] [has_one N] :

1 is the homomorphism sending all elements to 1.

Equations
@[instance]
def zero_hom.has_zero {M : Type u_1} {N : Type u_2} [has_zero M] [has_zero N] :

0 is the homomorphism sending all elements to 0.

@[instance]
def mul_hom.has_one {M : Type u_1} {N : Type u_2} [has_mul M] [monoid N] :

1 is the multiplicative homomorphism sending all elements to 1.

Equations
@[instance]
def add_hom.has_zero {M : Type u_1} {N : Type u_2} [has_add M] [add_monoid N] :

0 is the additive homomorphism sending all elements to 0.

@[instance]
def monoid_hom.has_one {M : Type u_1} {N : Type u_2} [monoid M] [monoid N] :

1 is the monoid homomorphism sending all elements to 1.

Equations
@[instance]
def add_monoid_hom.has_zero {M : Type u_1} {N : Type u_2} [add_monoid M] [add_monoid N] :

0 is the additive monoid homomorphism sending all elements to 0.

@[simp]
theorem one_hom.one_apply {M : Type u_1} {N : Type u_2} [has_one M] [has_one N] (x : M) :
1 x = 1

@[simp]
theorem zero_hom.zero_apply {M : Type u_1} {N : Type u_2} [has_zero M] [has_zero N] (x : M) :
0 x = 0

@[simp]
theorem add_monoid_hom.zero_apply {M : Type u_1} {N : Type u_2} [add_monoid M] [add_monoid N] (x : M) :
0 x = 0

@[simp]
theorem monoid_hom.one_apply {M : Type u_1} {N : Type u_2} [monoid M] [monoid N] (x : M) :
1 x = 1

@[instance]
def one_hom.inhabited {M : Type u_1} {N : Type u_2} [has_one M] [has_one N] :

Equations
@[instance]
def zero_hom.inhabited {M : Type u_1} {N : Type u_2} [has_zero M] [has_zero N] :

@[instance]
def add_hom.inhabited {M : Type u_1} {N : Type u_2} [has_add M] [add_monoid N] :

@[instance]
def mul_hom.inhabited {M : Type u_1} {N : Type u_2} [has_mul M] [monoid N] :

Equations
@[instance]
def add_monoid_hom.inhabited {M : Type u_1} {N : Type u_2} [add_monoid M] [add_monoid N] :

@[instance]
def monoid_hom.inhabited {M : Type u_1} {N : Type u_2} [monoid M] [monoid N] :

Equations
@[instance]
def monoid_hom.has_mul {M : Type u_1} {N : Type u_2} {mM : monoid M} [comm_monoid N] :

Given two monoid morphisms f, g to a commutative monoid, f * g is the monoid morphism sending x to f x * g x.

Equations
@[instance]
def add_monoid_hom.has_add {M : Type u_1} {N : Type u_2} {mM : add_monoid M} [add_comm_monoid N] :

Given two additive monoid morphisms f, g to an additive commutative monoid, f + g is the additive monoid morphism sending x to f x + g x.

@[simp]
theorem add_monoid_hom.add_apply {M : Type u_1} {N : Type u_2} {mM : add_monoid M} {mN : add_comm_monoid N} (f g : M →+ N) (x : M) :
(f + g) x = f x + g x

@[simp]
theorem monoid_hom.mul_apply {M : Type u_1} {N : Type u_2} {mM : monoid M} {mN : comm_monoid N} (f g : M →* N) (x : M) :
(f * g) x = (f x) * g x

@[instance]
def add_monoid_hom.add_comm_monoid {M : Type u_1} {N : Type u_2} [add_monoid M] [add_comm_monoid N] :

@[instance]
def monoid_hom.comm_monoid {M : Type u_1} {N : Type u_2} [monoid M] [comm_monoid N] :

(M →* N) is a comm_monoid if N is commutative.

Equations
def monoid_hom.flip {M : Type u_1} {N : Type u_2} {P : Type u_3} {mM : monoid M} {mN : monoid N} {mP : comm_monoid P} :
(M →* N →* P)N →* M →* P

flip arguments of f : M →* N →* P

Equations
def add_monoid_hom.flip {M : Type u_1} {N : Type u_2} {P : Type u_3} {mM : add_monoid M} {mN : add_monoid N} {mP : add_comm_monoid P} :
(M →+ N →+ P)N →+ M →+ P

flip arguments of f : M →+ N →+ P

@[simp]
theorem monoid_hom.flip_apply {M : Type u_1} {N : Type u_2} {P : Type u_3} {mM : monoid M} {mN : monoid N} {mP : comm_monoid P} (f : M →* N →* P) (x : M) (y : N) :
((f.flip) y) x = (f x) y

@[simp]
theorem add_monoid_hom.flip_apply {M : Type u_1} {N : Type u_2} {P : Type u_3} {mM : add_monoid M} {mN : add_monoid N} {mP : add_comm_monoid P} (f : M →+ N →+ P) (x : M) (y : N) :
((f.flip) y) x = (f x) y

def add_monoid_hom.eval {M : Type u_1} {N : Type u_2} [add_monoid M] [add_comm_monoid N] :
M →+ (M →+ N) →+ N

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.

def monoid_hom.eval {M : Type u_1} {N : Type u_2} [monoid M] [comm_monoid N] :
M →* (M →* N) →* N

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.

Equations
@[simp]
theorem add_monoid_hom.eval_apply {M : Type u_1} {N : Type u_2} [add_monoid M] [add_comm_monoid N] (x : M) (f : M →+ N) :

@[simp]
theorem monoid_hom.eval_apply {M : Type u_1} {N : Type u_2} [monoid M] [comm_monoid N] (x : M) (f : M →* N) :

theorem add_monoid_hom.eq_on_neg {M : Type u_1} {G : Type u_2} [add_group G] [add_monoid M] {f g : G →+ M} {x : G} :
f x = g xf (-x) = g (-x)

If two homomorphism from an additive group to an additive monoid are equal at x, then they are equal at -x.

theorem monoid_hom.eq_on_inv {M : Type u_1} {G : Type u_2} [group G] [monoid M] {f g : G →* M} {x : G} :
f x = g xf x⁻¹ = g x⁻¹

If two homomorphism from a group to a monoid are equal at x, then they are equal at x⁻¹.

@[simp]
theorem add_monoid_hom.map_neg {G : Type u_1} {H : Type u_2} [add_group G] [add_group H] (f : G →+ H) (g : G) :
f (-g) = -f g

@[simp]
theorem monoid_hom.map_inv {G : Type u_1} {H : Type u_2} [group G] [group H] (f : G →* H) (g : G) :

Group homomorphisms preserve inverse.

@[simp]
theorem add_monoid_hom.map_add_neg {G : Type u_1} {H : Type u_2} [add_group G] [add_group H] (f : G →+ H) (g h : G) :
f (g + -h) = f g + -f h

@[simp]
theorem monoid_hom.map_mul_inv {G : Type u_1} {H : Type u_2} [group G] [group H] (f : G →* H) (g h : G) :
f (g * h⁻¹) = (f g) * (f h)⁻¹

Group homomorphisms preserve division.

theorem monoid_hom.injective_iff {G : Type u_1} {H : Type u_2} [group G] [monoid H] (f : G →* H) :
function.injective f ∀ (a : G), f a = 1a = 1

A homomorphism from a group to a monoid is injective iff its kernel is trivial.

theorem add_monoid_hom.injective_iff {G : Type u_1} {H : Type u_2} [add_group G] [add_monoid H] (f : G →+ H) :
function.injective f ∀ (a : G), f a = 0a = 0

def add_monoid_hom.mk' {M : Type u_1} {G : Type u_4} [mM : add_monoid M] [add_group G] (f : M → G) :
(∀ (a b : M), f (a + b) = f a + f b)M →+ G

Makes an additive group homomomorphism from a proof that the map preserves multiplication.

def monoid_hom.mk' {M : Type u_1} {G : Type u_4} [mM : monoid M] [group G] (f : M → G) :
(∀ (a b : M), f (a * b) = (f a) * f b)M →* G

Makes a group homomomorphism from a proof that the map preserves multiplication.

Equations
@[simp]
theorem monoid_hom.coe_mk' {M : Type u_1} {G : Type u_4} [mM : monoid M] [group G] {f : M → G} (map_mul : ∀ (a b : M), f (a * b) = (f a) * f b) :
(monoid_hom.mk' f map_mul) = f

@[simp]
theorem add_monoid_hom.coe_mk' {M : Type u_1} {G : Type u_4} [mM : add_monoid M] [add_group G] {f : M → G} (map_mul : ∀ (a b : M), f (a + b) = f a + f b) :
(add_monoid_hom.mk' f map_mul) = f

def add_monoid_hom.of_map_add_neg {G : Type u_4} [add_group G] {H : Type u_1} [add_group H] (f : G → H) :
(∀ (a b : G), f (a + -b) = f a + -f b)G →+ H

Makes an additive group homomorphism from a proof that the map preserves the operation λ a b, a + -b. See also add_monoid_hom.of_map_sub for a version using λ a b, a - b.

def monoid_hom.of_map_mul_inv {G : Type u_4} [group G] {H : Type u_1} [group H] (f : G → H) :
(∀ (a b : G), f (a * b⁻¹) = (f a) * (f b)⁻¹)G →* H

Makes a group homomorphism from a proof that the map preserves right division λ x y, x * y⁻¹.

Equations
@[simp]
theorem monoid_hom.coe_of_map_mul_inv {G : Type u_4} [group G] {H : Type u_1} [group H] (f : G → H) (map_div : ∀ (a b : G), f (a * b⁻¹) = (f a) * (f b)⁻¹) :

@[simp]
theorem add_monoid_hom.coe_of_map_add_neg {G : Type u_4} [add_group G] {H : Type u_1} [add_group H] (f : G → H) (map_div : ∀ (a b : G), f (a + -b) = f a + -f b) :

@[instance]
def add_monoid_hom.has_neg {M : Type u_1} {G : Type u_2} [add_monoid M] [add_comm_group G] :

If f is an additive monoid homomorphism to an additive commutative group, then -f is the homomorphism sending x to -(f x).

@[instance]
def monoid_hom.has_inv {M : Type u_1} {G : Type u_2} [monoid M] [comm_group G] :

If f is a monoid homomorphism to a commutative group, then f⁻¹ is the homomorphism sending x to (f x)⁻¹.

Equations
@[simp]
theorem monoid_hom.inv_apply {M : Type u_1} {G : Type u_2} {mM : monoid M} {gG : comm_group G} (f : M →* G) (x : M) :

@[simp]
theorem add_monoid_hom.neg_apply {M : Type u_1} {G : Type u_2} {mM : add_monoid M} {gG : add_comm_group G} (f : M →+ G) (x : M) :
(-f) x = -f x

@[instance]
def monoid_hom.comm_group {M : Type u_1} {G : Type u_2} [monoid M] [comm_group G] :

If G is a commutative group, then M →* G a commutative group too.

Equations
@[instance]
def add_monoid_hom.add_comm_group {M : Type u_1} {G : Type u_2} [add_monoid M] [add_comm_group G] :

If G is an additive commutative group, then M →+ G an additive commutative group too.

@[simp]
theorem add_monoid_hom.map_sub {G : Type u_4} {H : Type u_5} [add_group G] [add_group H] (f : G →+ H) (g h : G) :
f (g - h) = f g - f h

Additive group homomorphisms preserve subtraction.

def add_monoid_hom.of_map_sub {G : Type u_4} {H : Type u_5} [add_group G] [add_group H] (f : G → H) :
(∀ (x y : G), f (x - y) = f x - f y)G →+ H

Define a morphism of additive groups given a map which respects difference.

Equations
@[simp]
theorem add_monoid_hom.coe_of_map_sub {G : Type u_4} {H : Type u_5} [add_group G] [add_group H] (f : G → H) (hf : ∀ (x y : G), f (x - y) = f x - f y) :

@[simp]
theorem add_semiconj_by.map {M : Type u_1} {N : Type u_2} [add_monoid M] [add_monoid N] {a x y : M} (h : add_semiconj_by a x y) (f : M →+ N) :
add_semiconj_by (f a) (f x) (f y)

@[simp]
theorem semiconj_by.map {M : Type u_1} {N : Type u_2} [monoid M] [monoid N] {a x y : M} (h : semiconj_by a x y) (f : M →* N) :
semiconj_by (f a) (f x) (f y)

@[simp]
theorem add_commute.map {M : Type u_1} {N : Type u_2} [add_monoid M] [add_monoid N] {x y : M} (h : add_commute x y) (f : M →+ N) :
add_commute (f x) (f y)

@[simp]
theorem commute.map {M : Type u_1} {N : Type u_2} [monoid M] [monoid N] {x y : M} (h : commute x y) (f : M →* N) :
commute (f x) (f y)