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.

This file also defines the lesser-used (and notation-less) homomorphism types which are used as building blocks for other homomorphisms:

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_zero_class M] [add_zero_class N] (self : M →+ N) :
structure add_monoid_hom (M : Type u_6) (N : Type u_7) [add_zero_class M] [add_zero_class 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_zero_class M] [add_zero_class N] (self : 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) [mul_one_class M] [mul_one_class 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} [mul_one_class M] [mul_one_class N] (self : M →* N) :
@[nolint]
def monoid_hom.to_mul_hom {M : Type u_6} {N : Type u_7} [mul_one_class M] [mul_one_class N] (self : M →* N) :
@[nolint]
def monoid_with_zero_hom.to_zero_hom {M : Type u_6} {N : Type u_7} [mul_zero_one_class M] [mul_zero_one_class N] (self : monoid_with_zero_hom M N) :
structure monoid_with_zero_hom (M : Type u_6) (N : Type u_7) [mul_zero_one_class M] [mul_zero_one_class N] :
Type (max u_6 u_7)

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

@[nolint]
def monoid_with_zero_hom.to_monoid_hom {M : Type u_6} {N : Type u_7} [mul_zero_one_class M] [mul_zero_one_class N] (self : monoid_with_zero_hom M N) :
M →* N

Bundled morphisms can be down-cast to weaker bundlings

@[instance]
def add_monoid_hom.has_coe_to_zero_hom {M : Type u_1} {N : Type u_2} {mM : add_zero_class M} {mN : add_zero_class N} :
has_coe (M →+ N) (zero_hom M N)
@[instance]
def monoid_hom.has_coe_to_one_hom {M : Type u_1} {N : Type u_2} {mM : mul_one_class M} {mN : mul_one_class N} :
has_coe (M →* N) (one_hom M N)
Equations
@[instance]
def add_monoid_hom.has_coe_to_add_hom {M : Type u_1} {N : Type u_2} {mM : add_zero_class M} {mN : add_zero_class N} :
has_coe (M →+ N) (add_hom M N)
@[instance]
def monoid_hom.has_coe_to_mul_hom {M : Type u_1} {N : Type u_2} {mM : mul_one_class M} {mN : mul_one_class N} :
has_coe (M →* N) (mul_hom M N)
Equations

The simp-normal form of morphism coercion is f.to_..._hom. This choice is primarily because this is the way things were before the above coercions were introduced. Bundled morphisms defined elsewhere in Mathlib may choose ↑f as their simp-normal form instead.

@[simp]
theorem add_monoid_hom.coe_eq_to_zero_hom {M : Type u_1} {N : Type u_2} {mM : add_zero_class M} {mN : add_zero_class N} (f : M →+ N) :
@[simp]
theorem monoid_hom.coe_eq_to_one_hom {M : Type u_1} {N : Type u_2} {mM : mul_one_class M} {mN : mul_one_class N} (f : M →* N) :
@[simp]
theorem monoid_hom.coe_eq_to_mul_hom {M : Type u_1} {N : Type u_2} {mM : mul_one_class M} {mN : mul_one_class N} (f : M →* N) :
@[simp]
theorem add_monoid_hom.coe_eq_to_add_hom {M : Type u_1} {N : Type u_2} {mM : add_zero_class M} {mN : add_zero_class N} (f : M →+ N) :
@[simp]
theorem monoid_with_zero_hom.coe_eq_to_monoid_hom {M : Type u_1} {N : Type u_2} {mM : mul_zero_one_class M} {mN : mul_zero_one_class N} (f : monoid_with_zero_hom M N) :
@[simp]
theorem monoid_with_zero_hom.coe_eq_to_zero_hom {M : Type u_1} {N : Type u_2} {mM : mul_zero_one_class M} {mN : mul_zero_one_class N} (f : monoid_with_zero_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 : mul_one_class M} {mN : mul_one_class N} :
Equations
@[instance]
def add_monoid_hom.has_coe_to_fun {M : Type u_1} {N : Type u_2} {mM : add_zero_class M} {mN : add_zero_class 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_zero_class M] [add_zero_class N] (f : M →+ N) :
@[simp]
theorem monoid_hom.to_fun_eq_coe {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] (f : M →* N) :
@[simp]
theorem monoid_with_zero_hom.to_fun_eq_coe {M : Type u_1} {N : Type u_2} [mul_zero_one_class M] [mul_zero_one_class N] (f : monoid_with_zero_hom 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_zero_class M] [add_zero_class 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} [mul_one_class M] [mul_one_class 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
@[simp]
theorem monoid_with_zero_hom.coe_mk {M : Type u_1} {N : Type u_2} [mul_zero_one_class M] [mul_zero_one_class N] (f : M → N) (h0 : f 0 = 0) (h1 : f 1 = 1) (hmul : ∀ (x y : M), f (x * y) = (f x) * f y) :
{to_fun := f, map_zero' := h0, map_one' := h1, map_mul' := hmul} = f
@[simp]
theorem add_monoid_hom.to_zero_hom_coe {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] (f : M →+ N) :
@[simp]
theorem monoid_hom.to_one_hom_coe {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] (f : M →* N) :
@[simp]
theorem add_monoid_hom.to_add_hom_coe {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] (f : M →+ N) :
@[simp]
theorem monoid_hom.to_mul_hom_coe {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] (f : M →* N) :
@[simp]
@[simp]
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} [mul_one_class M] [mul_one_class 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_zero_class M] [add_zero_class N] {f g : M →+ N} (h : f = g) (x : M) :
f x = g x
theorem monoid_with_zero_hom.congr_fun {M : Type u_1} {N : Type u_2} [mul_zero_one_class M] [mul_zero_one_class N] {f g : monoid_with_zero_hom 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} (h : x = y) :
f 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} (h : x = y) :
f 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} (h : x = y) :
f 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} (h : x = y) :
f x = f y
theorem monoid_hom.congr_arg {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] (f : M →* N) {x y : M} (h : x = y) :
f x = f y
theorem add_monoid_hom.congr_arg {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] (f : M →+ N) {x y : M} (h : x = y) :
f x = f y
theorem monoid_with_zero_hom.congr_arg {M : Type u_1} {N : Type u_2} [mul_zero_one_class M] [mul_zero_one_class N] (f : monoid_with_zero_hom M N) {x y : M} (h : x = y) :
f 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⦄ (h : f = g) :
f = 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⦄ (h : f = g) :
f = 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⦄ (h : f = g) :
f = 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⦄ (h : f = g) :
f = g
theorem add_monoid_hom.coe_inj {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] ⦃f g : M →+ N⦄ (h : f = g) :
f = g
theorem monoid_hom.coe_inj {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] ⦃f g : M →* N⦄ (h : f = g) :
f = g
theorem monoid_with_zero_hom.coe_inj {M : Type u_1} {N : Type u_2} [mul_zero_one_class M] [mul_zero_one_class N] ⦃f g : monoid_with_zero_hom M N⦄ (h : f = g) :
f = 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⦄ (h : ∀ (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⦄ (h : ∀ (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⦄ (h : ∀ (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⦄ (h : ∀ (x : M), f x = g x) :
f = g
@[ext]
theorem monoid_hom.ext {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] ⦃f g : M →* N⦄ (h : ∀ (x : M), f x = g x) :
f = g
@[ext]
theorem add_monoid_hom.ext {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] ⦃f g : M →+ N⦄ (h : ∀ (x : M), f x = g x) :
f = g
@[ext]
theorem monoid_with_zero_hom.ext {M : Type u_1} {N : Type u_2} [mul_zero_one_class M] [mul_zero_one_class N] ⦃f g : monoid_with_zero_hom M N⦄ (h : ∀ (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} [mul_one_class M] [mul_one_class 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_zero_class M] [add_zero_class N] {f g : M →+ N} :
f = g ∀ (x : M), f x = g x
theorem monoid_with_zero_hom.ext_iff {M : Type u_1} {N : Type u_2} [mul_zero_one_class M] [mul_zero_one_class N] {f g : monoid_with_zero_hom M N} :
f = g ∀ (x : M), f x = g x
@[simp]
theorem zero_hom.mk_coe {M : Type u_1} {N : Type u_2} [has_zero M] [has_zero N] (f : zero_hom M N) (h1 : f 0 = 0) :
{to_fun := f, map_zero' := h1} = f
@[simp]
theorem one_hom.mk_coe {M : Type u_1} {N : Type u_2} [has_one M] [has_one N] (f : one_hom M N) (h1 : f 1 = 1) :
{to_fun := f, map_one' := h1} = f
@[simp]
theorem add_hom.mk_coe {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] (f : add_hom M N) (hmul : ∀ (x y : M), f (x + y) = f x + f y) :
{to_fun := f, map_add' := hmul} = f
@[simp]
theorem mul_hom.mk_coe {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] (f : mul_hom M N) (hmul : ∀ (x y : M), f (x * y) = (f x) * f y) :
{to_fun := f, map_mul' := hmul} = f
@[simp]
theorem add_monoid_hom.mk_coe {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class 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.mk_coe {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class 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
@[simp]
theorem monoid_with_zero_hom.mk_coe {M : Type u_1} {N : Type u_2} [mul_zero_one_class M] [mul_zero_one_class N] (f : monoid_with_zero_hom M N) (h0 : f 0 = 0) (h1 : f 1 = 1) (hmul : ∀ (x y : M), f (x * y) = (f x) * f y) :
{to_fun := f, map_zero' := h0, map_one' := h1, map_mul' := hmul} = f
@[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_zero_class M] [add_zero_class 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} [mul_one_class M] [mul_one_class N] (f : M →* N) :
f 1 = 1

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

@[simp]
theorem monoid_with_zero_hom.map_one {M : Type u_1} {N : Type u_2} [mul_zero_one_class M] [mul_zero_one_class N] (f : monoid_with_zero_hom M N) :
f 1 = 1
@[simp]
theorem monoid_with_zero_hom.map_zero {M : Type u_1} {N : Type u_2} [mul_zero_one_class M] [mul_zero_one_class N] (f : monoid_with_zero_hom M N) :
f 0 = 0
@[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} [mul_one_class M] [mul_one_class 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_zero_class M] [add_zero_class 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.

@[simp]
theorem monoid_with_zero_hom.map_mul {M : Type u_1} {N : Type u_2} [mul_zero_one_class M] [mul_zero_one_class N] (f : monoid_with_zero_hom M N) (a b : M) :
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_zero_class M} {mN : add_zero_class N} (f : M →+ N) {a b : M} (h : a + b = 0) :
f a + f b = 0
theorem monoid_hom.map_mul_eq_one {M : Type u_1} {N : Type u_2} {mM : mul_one_class M} {mN : mul_one_class N} (f : M →* N) {a b : M} (h : a * b = 1) :
(f a) * f b = 1
theorem monoid_hom.map_exists_right_inv {M : Type u_1} {N : Type u_2} {mM : mul_one_class M} {mN : mul_one_class N} (f : M →* N) {x : M} (hx : ∃ (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_zero_class M} {mN : add_zero_class N} (f : M →+ N) {x : M} (hx : ∃ (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_zero_class M} {mN : add_zero_class N} (f : M →+ N) {x : M} (hx : ∃ (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 : mul_one_class M} {mN : mul_one_class N} (f : M →* N) {x : M} (hx : ∃ (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 add_comm_group.neg_add_monoid_hom {G : Type u_1} [add_comm_group G] :
G →+ G

Inversion on a commutative additive group, considered as an additive monoid homomorphism.

def comm_group.inv_monoid_hom {G : Type u_1} [comm_group G] :
G →* G

Inversion on a commutative group, considered as a monoid homomorphism.

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

The identity map from an type with zero to itself.

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

The identity map from a type with 1 to itself.

Equations
@[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) :
def mul_hom.id (M : Type u_1) [has_mul M] :

The identity map from a type with multiplication to itself.

Equations
@[simp]
theorem add_hom.id_apply (M : Type u_1) [has_add M] (x : M) :
def add_hom.id (M : Type u_1) [has_add M] :

The identity map from an type with addition to itself.

@[simp]
theorem monoid_hom.id_apply (M : Type u_1) [mul_one_class M] (x : M) :
def monoid_hom.id (M : Type u_1) [mul_one_class M] :
M →* M

The identity map from a monoid to itself.

Equations
@[simp]
theorem add_monoid_hom.id_apply (M : Type u_1) [add_zero_class M] (x : M) :
def add_monoid_hom.id (M : Type u_1) [add_zero_class M] :
M →+ M

The identity map from an additive monoid to itself.

The identity map from a monoid_with_zero to itself.

Equations
@[simp]
theorem monoid_with_zero_hom.id_apply (M : Type u_1) [mul_zero_one_class 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] (hnp : zero_hom N P) (hmn : zero_hom M N) :

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] (hnp : one_hom N P) (hmn : one_hom M N) :

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] (hnp : mul_hom N P) (hmn : mul_hom M N) :

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] (hnp : add_hom N P) (hmn : add_hom M N) :

Composition of add_homs as a add_hom.

def monoid_hom.comp {M : Type u_1} {N : Type u_2} {P : Type u_3} [mul_one_class M] [mul_one_class N] [mul_one_class P] (hnp : N →* P) (hmn : 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_zero_class M] [add_zero_class N] [add_zero_class P] (hnp : N →+ P) (hmn : M →+ N) :
M →+ P

Composition of additive monoid morphisms as an additive monoid morphism.

def monoid_with_zero_hom.comp {M : Type u_1} {N : Type u_2} {P : Type u_3} [mul_zero_one_class M] [mul_zero_one_class N] [mul_zero_one_class P] (hnp : monoid_with_zero_hom N P) (hmn : monoid_with_zero_hom M N) :

Composition of monoid_with_zero_homs as a monoid_with_zero_hom.

Equations
@[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_zero_class M] [add_zero_class N] [add_zero_class 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} [mul_one_class M] [mul_one_class N] [mul_one_class P] (g : N →* P) (f : M →* N) :
(g.comp f) = g f
@[simp]
theorem monoid_with_zero_hom.coe_comp {M : Type u_1} {N : Type u_2} {P : Type u_3} [mul_zero_one_class M] [mul_zero_one_class N] [mul_zero_one_class P] (g : monoid_with_zero_hom N P) (f : monoid_with_zero_hom 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} [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)
theorem add_monoid_hom.comp_apply {M : Type u_1} {N : Type u_2} {P : Type u_3} [add_zero_class M] [add_zero_class N] [add_zero_class P] (g : N →+ P) (f : M →+ N) (x : M) :
(g.comp f) x = g (f x)
theorem monoid_with_zero_hom.comp_apply {M : Type u_1} {N : Type u_2} {P : Type u_3} [mul_zero_one_class M] [mul_zero_one_class N] [mul_zero_one_class P] (g : monoid_with_zero_hom N P) (f : monoid_with_zero_hom 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_zero_class M] [add_zero_class N] [add_zero_class P] [add_zero_class 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} [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)
theorem monoid_with_zero_hom.comp_assoc {M : Type u_1} {N : Type u_2} {P : Type u_3} {Q : Type u_4} [mul_zero_one_class M] [mul_zero_one_class N] [mul_zero_one_class P] [mul_zero_one_class Q] (f : monoid_with_zero_hom M N) (g : monoid_with_zero_hom N P) (h : monoid_with_zero_hom 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} (hf : 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} (hf : 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} (hf : 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} (hf : 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_zero_class M] [add_zero_class N] [add_zero_class P] {g₁ g₂ : N →+ P} {f : M →+ N} (hf : 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} [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₂
theorem monoid_with_zero_hom.cancel_right {M : Type u_1} {N : Type u_2} {P : Type u_3} [mul_zero_one_class M] [mul_zero_one_class N] [mul_zero_one_class P] {g₁ g₂ : monoid_with_zero_hom N P} {f : monoid_with_zero_hom M N} (hf : 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} (hg : 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} (hg : 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} (hg : 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} (hg : 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} [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₂
theorem add_monoid_hom.cancel_left {M : Type u_1} {N : Type u_2} {P : Type u_3} [add_zero_class M] [add_zero_class N] [add_zero_class P] {g : N →+ P} {f₁ f₂ : M →+ N} (hg : function.injective g) :
g.comp f₁ = g.comp f₂ f₁ = f₂
theorem monoid_with_zero_hom.cancel_left {M : Type u_1} {N : Type u_2} {P : Type u_3} [mul_zero_one_class M] [mul_zero_one_class N] [mul_zero_one_class P] {g : monoid_with_zero_hom N P} {f₁ f₂ : monoid_with_zero_hom M N} (hg : 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} [mul_one_class M] [mul_one_class N] (f : M →* N) :
@[simp]
theorem add_monoid_hom.comp_id {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] (f : M →+ N) :
@[simp]
theorem monoid_with_zero_hom.comp_id {M : Type u_1} {N : Type u_2} [mul_zero_one_class M] [mul_zero_one_class N] (f : monoid_with_zero_hom 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_zero_class M] [add_zero_class N] (f : M →+ N) :
@[simp]
theorem monoid_hom.id_comp {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] (f : M →* N) :
@[simp]
theorem monoid_with_zero_hom.id_comp {M : Type u_1} {N : Type u_2} [mul_zero_one_class M] [mul_zero_one_class N] (f : monoid_with_zero_hom M N) :
def monoid.End (M : Type u_1) [mul_one_class M] :
Type u_1

The monoid of endomorphisms.

Equations
@[instance]
def monoid.End.monoid (M : Type u_1) [mul_one_class M] :
Equations
@[instance]
def monoid.End.inhabited (M : Type u_1) [mul_one_class M] :
Equations
@[instance]
Equations
@[simp]
theorem monoid.coe_one (M : Type u_1) [mul_one_class M] :
@[simp]
theorem monoid.coe_mul (M : Type u_1) [mul_one_class M] (f g : monoid.End M) :
f * g = f g
def add_monoid.End (A : Type u_6) [add_zero_class A] :
Type u_6

The monoid of endomorphisms.

Equations
@[instance]
Equations
@[instance]
Equations
@[simp]
theorem add_monoid.coe_one (A : Type u_6) [add_zero_class A] :
@[simp]
theorem add_monoid.coe_mul (A : Type u_6) [add_zero_class 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] [mul_one_class 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_zero_class 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} [mul_one_class M] [mul_one_class 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_zero_class M] [add_zero_class 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_zero_class M] [add_zero_class N] (x : M) :
0 x = 0
@[simp]
theorem monoid_hom.one_apply {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] (x : M) :
1 x = 1
@[simp]
theorem one_hom.one_comp {M : Type u_1} {N : Type u_2} {P : Type u_3} [has_one M] [has_one N] [has_one P] (f : one_hom M N) :
1.comp f = 1
@[simp]
theorem zero_hom.zero_comp {M : Type u_1} {N : Type u_2} {P : Type u_3} [has_zero M] [has_zero N] [has_zero P] (f : zero_hom M N) :
0.comp f = 0
@[simp]
theorem one_hom.comp_one {M : Type u_1} {N : Type u_2} {P : Type u_3} [has_one M] [has_one N] [has_one P] (f : one_hom N P) :
f.comp 1 = 1
@[simp]
theorem zero_hom.comp_zero {M : Type u_1} {N : Type u_2} {P : Type u_3} [has_zero M] [has_zero N] [has_zero P] (f : zero_hom N P) :
f.comp 0 = 0
@[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_zero_class N] :
@[instance]
def mul_hom.inhabited {M : Type u_1} {N : Type u_2} [has_mul M] [mul_one_class N] :
Equations
@[instance]
def add_monoid_hom.inhabited {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] :
@[instance]
def monoid_hom.inhabited {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] :
Equations
@[instance]
def monoid_hom.has_mul {M : Type u_1} {N : Type u_2} {mM : mul_one_class 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_zero_class 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_zero_class 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 : mul_one_class M} {mN : comm_monoid N} (f g : M →* N) (x : M) :
(f * g) x = (f x) * g x
@[simp]
theorem monoid_hom.one_comp {M : Type u_1} {N : Type u_2} {P : Type u_3} [mul_one_class M] [mul_one_class N] [mul_one_class P] (f : M →* N) :
1.comp f = 1
@[simp]
theorem add_monoid_hom.zero_comp {M : Type u_1} {N : Type u_2} {P : Type u_3} [add_zero_class M] [add_zero_class N] [add_zero_class P] (f : M →+ N) :
0.comp f = 0
@[simp]
theorem monoid_hom.comp_one {M : Type u_1} {N : Type u_2} {P : Type u_3} [mul_one_class M] [mul_one_class N] [mul_one_class P] (f : N →* P) :
f.comp 1 = 1
@[simp]
theorem add_monoid_hom.comp_zero {M : Type u_1} {N : Type u_2} {P : Type u_3} [add_zero_class M] [add_zero_class N] [add_zero_class P] (f : N →+ P) :
f.comp 0 = 0
theorem add_monoid_hom.add_comp {M : Type u_1} {N : Type u_2} {P : Type u_3} [add_zero_class M] [add_comm_monoid N] [add_comm_monoid P] (g₁ g₂ : N →+ P) (f : M →+ N) :
(g₁ + g₂).comp f = g₁.comp f + g₂.comp f
theorem monoid_hom.mul_comp {M : Type u_1} {N : Type u_2} {P : Type u_3} [mul_one_class M] [comm_monoid N] [comm_monoid P] (g₁ g₂ : N →* P) (f : M →* N) :
(g₁ * g₂).comp f = (g₁.comp f) * g₂.comp f
theorem add_monoid_hom.comp_add {M : Type u_1} {N : Type u_2} {P : Type u_3} [add_zero_class M] [add_comm_monoid N] [add_comm_monoid P] (g : N →+ P) (f₁ f₂ : M →+ N) :
g.comp (f₁ + f₂) = g.comp f₁ + g.comp f₂
theorem monoid_hom.comp_mul {M : Type u_1} {N : Type u_2} {P : Type u_3} [mul_one_class M] [comm_monoid N] [comm_monoid P] (g : N →* P) (f₁ f₂ : M →* N) :
g.comp (f₁ * f₂) = (g.comp f₁) * g.comp f₂
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} (h : f x = g x) :
f (-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} (h : f 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.

@[simp]
theorem monoid_hom.map_div {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.

@[simp]
theorem add_monoid_hom.map_sub {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

Additive group homomorphisms preserve subtraction.

theorem monoid_hom.injective_iff {G : Type u_1} {H : Type u_2} [group G] [mul_one_class 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. For the iff statement on the triviality of the kernel, see monoid_hom.injective_iff'.

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

A homomorphism from an additive group to an additive monoid is injective iff its kernel is trivial. For the iff statement on the triviality of the kernel, see add_monoid_hom.injective_iff'.

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

A homomorphism from an additive group to an additive monoid is injective iff its kernel is trivial, stated as an iff on the triviality of the kernel. For the implication, see add_monoid_hom.injective_iff.

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

A homomorphism from a group to a monoid is injective iff its kernel is trivial, stated as an iff on the triviality of the kernel. For the implication, see monoid_hom.injective_iff.

@[simp]
theorem monoid_hom.mk'_apply {M : Type u_1} {G : Type u_4} [mM : mul_one_class 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
def add_monoid_hom.mk' {M : Type u_1} {G : Type u_4} [mM : add_zero_class M] [add_group G] (f : M → G) (map_mul : ∀ (a b : M), f (a + b) = f a + f b) :
M →+ G

Makes an additive group homomorphism from a proof that the map preserves addition.

@[simp]
theorem add_monoid_hom.mk'_apply {M : Type u_1} {G : Type u_4} [mM : add_zero_class 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 monoid_hom.mk' {M : Type u_1} {G : Type u_4} [mM : mul_one_class M] [group G] (f : M → G) (map_mul : ∀ (a b : M), f (a * b) = (f a) * f b) :
M →* G

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

Equations
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) (map_div : ∀ (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) (map_div : ∀ (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⁻¹. See also monoid_hom.of_map_div for a version using λ 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) :
def monoid_hom.of_map_div {G : Type u_4} [group G] {H : Type u_1} [group H] (f : G → H) (hf : ∀ (x y : G), f (x / y) = f x / f y) :
G →* H

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

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

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

@[simp]
theorem monoid_hom.coe_of_map_div {G : Type u_4} [group G] {H : Type u_1} [group H] (f : G → H) (hf : ∀ (x y : G), f (x / y) = f x / f y) :
@[simp]
theorem add_monoid_hom.coe_of_map_sub {G : Type u_4} [add_group G] {H : Type u_1} [add_group H] (f : G → H) (hf : ∀ (x y : G), f (x - y) = f x - f y) :
@[instance]
def add_monoid_hom.has_neg {M : Type u_1} {G : Type u_2} [add_zero_class 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} [mul_one_class 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 : mul_one_class 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_zero_class M} {gG : add_comm_group G} (f : M →+ G) (x : M) :
(-f) x = -f x
@[simp]
theorem add_monoid_hom.neg_comp {M : Type u_1} {N : Type u_2} {A : Type u_3} {mM : add_zero_class M} {gN : add_zero_class N} {gA : add_comm_group A} (φ : N →+ A) (ψ : M →+ N) :
(-φ).comp ψ = -φ.comp ψ
@[simp]
theorem monoid_hom.inv_comp {M : Type u_1} {N : Type u_2} {A : Type u_3} {mM : mul_one_class M} {gN : mul_one_class N} {gA : comm_group A} (φ : N →* A) (ψ : M →* N) :
φ⁻¹.comp ψ = (φ.comp ψ)⁻¹
@[simp]
theorem add_monoid_hom.comp_neg {M : Type u_1} {A : Type u_2} {B : Type u_3} {mM : add_zero_class M} {mA : add_comm_group A} {mB : add_comm_group B} (φ : A →+ B) (ψ : M →+ A) :
φ.comp (-ψ) = -φ.comp ψ
@[simp]
theorem monoid_hom.comp_inv {M : Type u_1} {A : Type u_2} {B : Type u_3} {mM : mul_one_class M} {mA : comm_group A} {mB : comm_group B} (φ : A →* B) (ψ : M →* A) :
φ.comp ψ⁻¹ = (φ.comp ψ)⁻¹
@[instance]
def add_monoid_hom.has_sub {M : Type u_1} {G : Type u_2} [add_zero_class M] [add_comm_group G] :

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

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

If f and g are monoid homomorphisms to a commutative group, then f / g is the homomorphism sending x to (f x) / (g x).

Equations
@[simp]
theorem add_monoid_hom.sub_apply {M : Type u_1} {G : Type u_2} {mM : add_zero_class M} {gG : add_comm_group G} (f g : M →+ G) (x : M) :
(f - g) x = f x - g x
@[simp]
theorem monoid_hom.div_apply {M : Type u_1} {G : Type u_2} {mM : mul_one_class M} {gG : comm_group G} (f g : M →* G) (x : M) :
(f / g) x = f x / g x
@[simp]
theorem add_semiconj_by.map {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class 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} [mul_one_class M] [mul_one_class 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_zero_class M] [add_zero_class 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} [mul_one_class M] [mul_one_class N] {x y : M} (h : commute x y) (f : M →* N) :
commute (f x) (f y)