mathlib documentation

algebra.hom.group

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

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

zero_hom M N is the type of functions M → N that preserve zero.

When possible, instead of parametrizing results over (f : zero_hom M N), you should parametrize over (F : Type*) [zero_hom_class F M N] (f : F).

When you extend this structure, make sure to also extend zero_hom_class.

source
@[instance]
def zero_hom_class.to_fun_like (F : Type u_7) (M : out_param (Type u_8)) (N : out_param (Type u_9)) [has_zero M] [has_zero N] [self : zero_hom_class F M N] :
fun_like F M (λ (_x : M), N)
source
@[class]
structure zero_hom_class (F : Type u_7) (M : out_param (Type u_8)) (N : out_param (Type u_9)) [has_zero M] [has_zero N] :
Type (max u_7 u_8 u_9)

zero_hom_class F M N states that F is a type of zero-preserving homomorphisms.

You should extend this typeclass when you extend zero_hom.

Instances
source
structure add_hom (M : Type u_7) (N : Type u_8) [has_add M] [has_add N] :
Type (max u_7 u_8)

add_hom M N is the type of functions M → N that preserve addition.

When possible, instead of parametrizing results over (f : add_hom M N), you should parametrize over (F : Type*) [add_hom_class F M N] (f : F).

When you extend this structure, make sure to extend add_hom_class.

source
@[class]
structure add_hom_class (F : Type u_7) (M : out_param (Type u_8)) (N : out_param (Type u_9)) [has_add M] [has_add N] :
Type (max u_7 u_8 u_9)

add_hom_class F M N states that F is a type of addition-preserving homomorphisms. You should declare an instance of this typeclass when you extend add_hom.

Instances
source
@[instance]
def add_hom_class.to_fun_like (F : Type u_7) (M : out_param (Type u_8)) (N : out_param (Type u_9)) [has_add M] [has_add N] [self : add_hom_class F M N] :
fun_like F M (λ (_x : M), N)
source
@[nolint]
def add_monoid_hom.to_add_hom {M : Type u_7} {N : Type u_8} [add_zero_class M] [add_zero_class N] (self : M →+ N) :
add_hom M N
source
structure add_monoid_hom (M : Type u_7) (N : Type u_8) [add_zero_class M] [add_zero_class N] :
Type (max u_7 u_8)

M →+ N is the type of functions M → N that preserve the add_zero_class structure.

add_monoid_hom is also used for group homomorphisms.

When possible, instead of parametrizing results over (f : M →+ N), you should parametrize over (F : Type*) [add_monoid_hom_class F M N] (f : F).

When you extend this structure, make sure to extend add_monoid_hom_class.

source
@[nolint]
def add_monoid_hom.to_zero_hom {M : Type u_7} {N : Type u_8} [add_zero_class M] [add_zero_class N] (self : M →+ N) :
zero_hom M N
source
@[class]
structure add_monoid_hom_class (F : Type u_7) (M : out_param (Type u_8)) (N : out_param (Type u_9)) [add_zero_class M] [add_zero_class N] :
Type (max u_7 u_8 u_9)

add_monoid_hom_class F M N states that F is a type of add_zero_class-preserving homomorphisms.

You should also extend this typeclass when you extend add_monoid_hom.

Instances
source
@[instance]
def add_monoid_hom_class.to_add_hom_class (F : Type u_7) (M : out_param (Type u_8)) (N : out_param (Type u_9)) [add_zero_class M] [add_zero_class N] [self : add_monoid_hom_class F M N] :
add_hom_class F M N
source
@[instance]
def add_monoid_hom_class.to_zero_hom_class (F : Type u_7) (M : out_param (Type u_8)) (N : out_param (Type u_9)) [add_zero_class M] [add_zero_class N] [self : add_monoid_hom_class F M N] :
zero_hom_class F M N
source
structure one_hom (M : Type u_7) (N : Type u_8) [has_one M] [has_one N] :
Type (max u_7 u_8)
  • to_fun : M → N
  • map_one' : self.to_fun 1 = 1

one_hom M N is the type of functions M → N that preserve one.

When possible, instead of parametrizing results over (f : one_hom M N), you should parametrize over (F : Type*) [one_hom_class F M N] (f : F).

When you extend this structure, make sure to also extend one_hom_class.

source
@[class]
structure one_hom_class (F : Type u_7) (M : out_param (Type u_8)) (N : out_param (Type u_9)) [has_one M] [has_one N] :
Type (max u_7 u_8 u_9)

one_hom_class F M N states that F is a type of one-preserving homomorphisms. You should extend this typeclass when you extend one_hom.

Instances
source
@[instance]
def one_hom_class.to_fun_like (F : Type u_7) (M : out_param (Type u_8)) (N : out_param (Type u_9)) [has_one M] [has_one N] [self : one_hom_class F M N] :
fun_like F M (λ (_x : M), N)
source
@[protected, instance]
def one_hom.one_hom_class {M : Type u_1} {N : Type u_2} [has_one M] [has_one N] :
one_hom_class (one_hom M N) M N
Equations
source
@[protected, instance]
def zero_hom.zero_hom_class {M : Type u_1} {N : Type u_2} [has_zero M] [has_zero N] :
zero_hom_class (zero_hom M N) M N
Equations
source
@[simp]
theorem map_one {M : Type u_1} {N : Type u_2} {F : Type u_6} [has_one M] [has_one N] [one_hom_class F M N] (f : F) :
⇑f 1 = 1
source
@[simp]
theorem map_zero {M : Type u_1} {N : Type u_2} {F : Type u_6} [has_zero M] [has_zero N] [zero_hom_class F M N] (f : F) :
⇑f 0 = 0
source
theorem map_eq_one_iff {M : Type u_1} {N : Type u_2} {F : Type u_6} [has_one M] [has_one N] [one_hom_class F M N] (f : F) (hf : function.injective ⇑f) {x : M} :
⇑f x = 1 ↔ x = 1
source
theorem map_eq_zero_iff {M : Type u_1} {N : Type u_2} {F : Type u_6} [has_zero M] [has_zero N] [zero_hom_class F M N] (f : F) (hf : function.injective ⇑f) {x : M} :
⇑f x = 0 ↔ x = 0
source
theorem map_ne_zero_iff {R : Type u_1} {S : Type u_2} {F : Type u_3} [has_zero R] [has_zero S] [zero_hom_class F R S] (f : F) (hf : function.injective ⇑f) {x : R} :
⇑f x ≠ 0 ↔ x ≠ 0
source
theorem map_ne_one_iff {R : Type u_1} {S : Type u_2} {F : Type u_3} [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
source
theorem ne_zero_of_map {R : Type u_1} {S : Type u_2} {F : Type u_3} [has_zero R] [has_zero S] [zero_hom_class F R S] {f : F} {x : R} (hx : ⇑f x ≠ 0) :
x ≠ 0
source
theorem ne_one_of_map {R : Type u_1} {S : Type u_2} {F : Type u_3} [has_one R] [has_one S] [one_hom_class F R S] {f : F} {x : R} (hx : ⇑f x ≠ 1) :
x ≠ 1
source
@[protected, instance]
def zero_hom.has_coe_t {M : Type u_1} {N : Type u_2} {F : Type u_6} [has_zero M] [has_zero N] [zero_hom_class F M N] :
has_coe_t F (zero_hom M N)
Equations
source
@[protected, instance]
def one_hom.has_coe_t {M : Type u_1} {N : Type u_2} {F : Type u_6} [has_one M] [has_one N] [one_hom_class F M N] :
has_coe_t F (one_hom M N)
Equations
source
structure mul_hom (M : Type u_7) (N : Type u_8) [has_mul M] [has_mul N] :
Type (max u_7 u_8)

M →ₙ* N is the type of functions M → N that preserve multiplication. The ₙ in the notation stands for "non-unital" because it is intended to match the notation for non_unital_alg_hom and non_unital_ring_hom, so a mul_hom is a non-unital monoid hom.

When possible, instead of parametrizing results over (f : M →ₙ* N), you should parametrize over (F : Type*) [mul_hom_class F M N] (f : F). When you extend this structure, make sure to extend mul_hom_class.

source
@[instance]
def mul_hom_class.to_fun_like (F : Type u_7) (M : out_param (Type u_8)) (N : out_param (Type u_9)) [has_mul M] [has_mul N] [self : mul_hom_class F M N] :
fun_like F M (λ (_x : M), N)
source
@[class]
structure mul_hom_class (F : Type u_7) (M : out_param (Type u_8)) (N : out_param (Type u_9)) [has_mul M] [has_mul N] :
Type (max u_7 u_8 u_9)

mul_hom_class F M N states that F is a type of multiplication-preserving homomorphisms.

You should declare an instance of this typeclass when you extend mul_hom.

Instances
source
@[protected, instance]
def add_hom.add_hom_class {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] :
add_hom_class (add_hom M N) M N
Equations
source
@[protected, instance]
def mul_hom.mul_hom_class {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] :
mul_hom_class (M →ₙ* N) M N
Equations
source
@[simp]
theorem map_add {M : Type u_1} {N : Type u_2} {F : Type u_6} [has_add M] [has_add N] [add_hom_class F M N] (f : F) (x y : M) :
⇑f (x + y) = ⇑f x + ⇑f y
source
@[simp]
theorem map_mul {M : Type u_1} {N : Type u_2} {F : Type u_6} [has_mul M] [has_mul N] [mul_hom_class F M N] (f : F) (x y : M) :
⇑f (x * y) = (⇑f x) * ⇑f y
source
@[protected, instance]
def mul_hom.has_coe_t {M : Type u_1} {N : Type u_2} {F : Type u_6} [has_mul M] [has_mul N] [mul_hom_class F M N] :
has_coe_t F (M →ₙ* N)
Equations
source
@[protected, instance]
def add_hom.has_coe_t {M : Type u_1} {N : Type u_2} {F : Type u_6} [has_add M] [has_add N] [add_hom_class F M N] :
has_coe_t F (add_hom M N)
Equations
source
structure monoid_hom (M : Type u_7) (N : Type u_8) [mul_one_class M] [mul_one_class N] :
Type (max u_7 u_8)

M →* N is the type of functions M → N that preserve the monoid structure. monoid_hom is also used for group homomorphisms.

When possible, instead of parametrizing results over (f : M →+ N), you should parametrize over (F : Type*) [monoid_hom_class F M N] (f : F).

When you extend this structure, make sure to extend monoid_hom_class.

source
@[nolint]
def monoid_hom.to_one_hom {M : Type u_7} {N : Type u_8} [mul_one_class M] [mul_one_class N] (self : M →* N) :
one_hom M N
source
@[nolint]
def monoid_hom.to_mul_hom {M : Type u_7} {N : Type u_8} [mul_one_class M] [mul_one_class N] (self : M →* N) :
M →ₙ* N
source
@[class]
structure monoid_hom_class (F : Type u_7) (M : out_param (Type u_8)) (N : out_param (Type u_9)) [mul_one_class M] [mul_one_class N] :
Type (max u_7 u_8 u_9)

monoid_hom_class F M N states that F is a type of monoid-preserving homomorphisms. You should also extend this typeclass when you extend monoid_hom.

Instances
source
@[instance]
def monoid_hom_class.to_one_hom_class (F : Type u_7) (M : out_param (Type u_8)) (N : out_param (Type u_9)) [mul_one_class M] [mul_one_class N] [self : monoid_hom_class F M N] :
one_hom_class F M N
source
@[instance]
def monoid_hom_class.to_mul_hom_class (F : Type u_7) (M : out_param (Type u_8)) (N : out_param (Type u_9)) [mul_one_class M] [mul_one_class N] [self : monoid_hom_class F M N] :
mul_hom_class F M N
source
@[protected, instance]
def add_monoid_hom.add_monoid_hom_class {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] :
add_monoid_hom_class (M →+ N) M N
Equations
source
@[protected, instance]
def monoid_hom.monoid_hom_class {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] :
monoid_hom_class (M →* N) M N
Equations
source
@[protected, instance]
def add_monoid_hom.has_coe_t {M : Type u_1} {N : Type u_2} {F : Type u_6} [add_zero_class M] [add_zero_class N] [add_monoid_hom_class F M N] :
has_coe_t F (M →+ N)
Equations
source
@[protected, instance]
def monoid_hom.has_coe_t {M : Type u_1} {N : Type u_2} {F : Type u_6} [mul_one_class M] [mul_one_class N] [monoid_hom_class F M N] :
has_coe_t F (M →* N)
Equations
source
theorem map_mul_eq_one {M : Type u_1} {N : Type u_2} {F : Type u_6} [mul_one_class M] [mul_one_class N] [monoid_hom_class F M N] (f : F) {a b : M} (h : a * b = 1) :
(⇑f a) * ⇑f b = 1
source
theorem map_add_eq_zero {M : Type u_1} {N : Type u_2} {F : Type u_6} [add_zero_class M] [add_zero_class N] [add_monoid_hom_class F M N] (f : F) {a b : M} (h : a + b = 0) :
⇑f a + ⇑f b = 0
source
@[simp]
theorem map_inv {G : Type u_4} {H : Type u_5} {F : Type u_6} [group G] [group H] [monoid_hom_class F G H] (f : F) (g : G) :
⇑f g⁻¹ = (⇑f g)⁻¹

Group homomorphisms preserve inverse.

source
@[simp]
theorem map_neg {G : Type u_4} {H : Type u_5} {F : Type u_6} [add_group G] [add_group H] [add_monoid_hom_class F G H] (f : F) (g : G) :
⇑f (-g) = -⇑f g

Additive group homomorphisms preserve negation.

source
@[simp]
theorem map_mul_inv {G : Type u_4} {H : Type u_5} {F : Type u_6} [group G] [group H] [monoid_hom_class F G H] (f : F) (g h : G) :
⇑f (g * h⁻¹) = (⇑f g) * (⇑f h)⁻¹

Group homomorphisms preserve division.

source
@[simp]
theorem map_add_neg {G : Type u_4} {H : Type u_5} {F : Type u_6} [add_group G] [add_group H] [add_monoid_hom_class F G H] (f : F) (g h : G) :
⇑f (g + -h) = ⇑f g + -⇑f h

Additive group homomorphisms preserve subtraction.

source
@[simp]
theorem map_div {G : Type u_4} {H : Type u_5} {F : Type u_6} [group G] [group H] [monoid_hom_class F G H] (f : F) (x y : G) :
⇑f (x / y) = ⇑f x / ⇑f y

Group homomorphisms preserve division.

source
@[simp]
theorem map_sub {G : Type u_4} {H : Type u_5} {F : Type u_6} [add_group G] [add_group H] [add_monoid_hom_class F G H] (f : F) (x y : G) :
⇑f (x - y) = ⇑f x - ⇑f y

Additive group homomorphisms preserve subtraction.

source
theorem map_div' {G : Type u_4} {H : Type u_5} {F : Type u_6} [div_inv_monoid G] [div_inv_monoid H] [monoid_hom_class F G H] (f : F) (hf : ∀ (x : G), ⇑f x⁻¹ = (⇑f x)⁻¹) (a b : G) :
⇑f (a / b) = ⇑f a / ⇑f b
source
theorem map_sub' {G : Type u_4} {H : Type u_5} {F : Type u_6} [sub_neg_monoid G] [sub_neg_monoid H] [add_monoid_hom_class F G H] (f : F) (hf : ∀ (x : G), ⇑f (-x) = -⇑f x) (a b : G) :
⇑f (a - b) = ⇑f a - ⇑f b
source
@[simp]
theorem map_pow {G : Type u_4} {H : Type u_5} {F : Type u_6} [monoid G] [monoid H] [monoid_hom_class F G H] (f : F) (a : G) (n : ℕ) :
⇑f (a ^ n) = ⇑f a ^ n
source
theorem map_nsmul.aux {G : Type u_4} {H : Type u_5} {F : Type u_6} [add_monoid G] [add_monoid H] [add_monoid_hom_class F G H] (f : F) (a : G) (n : ℕ) :
⇑f (n • a) = n • ⇑f a
source
@[simp]
theorem map_nsmul {G : Type u_4} {H : Type u_5} {F : Type u_6} [add_monoid G] [add_monoid H] [add_monoid_hom_class F G H] (f : F) (n : ℕ) (a : G) :
⇑f (n • a) = n • ⇑f a
source
theorem map_zpow' {G : Type u_4} {H : Type u_5} {F : Type u_6} [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
source
theorem map_zsmul' {G : Type u_4} {H : Type u_5} {F : Type u_6} [sub_neg_monoid G] [sub_neg_monoid H] [add_monoid_hom_class F G H] (f : F) (hf : ∀ (x : G), ⇑f (-x) = -⇑f x) (a : G) (n : ℤ) :
⇑f (n • a) = n • ⇑f a
source
@[simp]
theorem map_zpow {G : Type u_4} {H : Type u_5} {F : Type u_6} [group G] [group H] [monoid_hom_class F G H] (f : F) (g : G) (n : ℤ) :
⇑f (g ^ n) = ⇑f g ^ n

Group homomorphisms preserve integer power.

source
theorem map_zsmul.aux {G : Type u_4} {H : Type u_5} {F : Type u_6} [add_group G] [add_group H] [add_monoid_hom_class F G H] (f : F) (g : G) (n : ℤ) :
⇑f (n • g) = n • ⇑f g
source
theorem map_zsmul {G : Type u_4} {H : Type u_5} {F : Type u_6} [add_group G] [add_group H] [add_monoid_hom_class F G H] (f : F) (n : ℤ) (g : G) :
⇑f (n • g) = n • ⇑f g

Additive group homomorphisms preserve integer scaling.

source
@[nolint]
def monoid_with_zero_hom.to_zero_hom {M : Type u_7} {N : Type u_8} [mul_zero_one_class M] [mul_zero_one_class N] (self : M →*₀ N) :
zero_hom M N
source
structure monoid_with_zero_hom (M : Type u_7) (N : Type u_8) [mul_zero_one_class M] [mul_zero_one_class N] :
Type (max u_7 u_8)

M →*₀ N is the type of functions M → N that preserve the monoid_with_zero structure.

monoid_with_zero_hom is also used for group homomorphisms.

When possible, instead of parametrizing results over (f : M →*₀ N), you should parametrize over (F : Type*) [monoid_with_zero_hom_class F M N] (f : F).

When you extend this structure, make sure to extend monoid_with_zero_hom_class.

source
@[nolint]
def monoid_with_zero_hom.to_monoid_hom {M : Type u_7} {N : Type u_8} [mul_zero_one_class M] [mul_zero_one_class N] (self : M →*₀ N) :
M →* N
source
@[class]
structure monoid_with_zero_hom_class (F : Type u_7) (M : out_param (Type u_8)) (N : out_param (Type u_9)) [mul_zero_one_class M] [mul_zero_one_class N] :
Type (max u_7 u_8 u_9)

monoid_with_zero_hom_class F M N states that F is a type of monoid_with_zero-preserving homomorphisms.

You should also extend this typeclass when you extend monoid_with_zero_hom.

Instances
source
@[instance]
def monoid_with_zero_hom_class.to_monoid_hom_class (F : Type u_7) (M : out_param (Type u_8)) (N : out_param (Type u_9)) [mul_zero_one_class M] [mul_zero_one_class N] [self : monoid_with_zero_hom_class F M N] :
monoid_hom_class F M N
source
@[instance]
def monoid_with_zero_hom_class.to_zero_hom_class (F : Type u_7) (M : out_param (Type u_8)) (N : out_param (Type u_9)) [mul_zero_one_class M] [mul_zero_one_class N] [self : monoid_with_zero_hom_class F M N] :
zero_hom_class F M N
source
@[protected, instance]
def monoid_with_zero_hom.monoid_with_zero_hom_class {M : Type u_1} {N : Type u_2} [mul_zero_one_class M] [mul_zero_one_class N] :
monoid_with_zero_hom_class (M →*₀ N) M N
Equations
source
@[protected, instance]
def monoid_with_zero_hom.has_coe_t {M : Type u_1} {N : Type u_2} {F : Type u_6} [mul_zero_one_class M] [mul_zero_one_class N] [monoid_with_zero_hom_class F M N] :
has_coe_t F (M →*₀ N)
Equations

Bundled morphisms can be down-cast to weaker bundlings

source
@[protected, 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)
Equations
source
@[protected, 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
source
@[protected, 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)
Equations
source
@[protected, 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) (M →ₙ* N)
Equations
source
@[protected, instance]
def monoid_with_zero_hom.has_coe_to_monoid_hom {M : Type u_1} {N : Type u_2} {mM : mul_zero_one_class M} {mN : mul_zero_one_class N} :
has_coe (M →*₀ N) (M →* N)
Equations
source
@[protected, instance]
def monoid_with_zero_hom.has_coe_to_zero_hom {M : Type u_1} {N : Type u_2} {mM : mul_zero_one_class M} {mN : mul_zero_one_class N} :
has_coe (M →*₀ N) (zero_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.

source
@[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) :
↑f = f.to_zero_hom
source
@[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) :
↑f = f.to_one_hom
source
@[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) :
↑f = f.to_mul_hom
source
@[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) :
↑f = f.to_add_hom
source
@[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 : M →*₀ N) :
↑f = f.to_monoid_hom
source
@[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 : M →*₀ N) :
↑f = f.to_zero_hom
source
@[protected, instance]
def zero_hom.has_coe_to_fun {M : Type u_1} {N : Type u_2} {mM : has_zero M} {mN : has_zero N} :
has_coe_to_fun (zero_hom M N) (λ (_x : zero_hom M N), M → N)
Equations
source
@[protected, instance]
def one_hom.has_coe_to_fun {M : Type u_1} {N : Type u_2} {mM : has_one M} {mN : has_one N} :
has_coe_to_fun (one_hom M N) (λ (_x : one_hom M N), M → N)
Equations
source
@[protected, instance]
def mul_hom.has_coe_to_fun {M : Type u_1} {N : Type u_2} {mM : has_mul M} {mN : has_mul N} :
has_coe_to_fun (M →ₙ* N) (λ (_x : M →ₙ* N), M → N)
Equations
source
@[protected, instance]
def add_hom.has_coe_to_fun {M : Type u_1} {N : Type u_2} {mM : has_add M} {mN : has_add N} :
has_coe_to_fun (add_hom M N) (λ (_x : add_hom M N), M → N)
Equations
source
@[protected, 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} :
has_coe_to_fun (M →* N) (λ (_x : M →* N), M → N)
Equations
source
@[protected, 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} :
has_coe_to_fun (M →+ N) (λ (_x : M →+ N), M → N)
Equations
source
@[protected, instance]
def monoid_with_zero_hom.has_coe_to_fun {M : Type u_1} {N : Type u_2} {mM : mul_zero_one_class M} {mN : mul_zero_one_class N} :
has_coe_to_fun (M →*₀ N) (λ (_x : M →*₀ N), M → N)
Equations
source
@[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) :
f.to_fun = ⇑f
source
@[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) :
f.to_fun = ⇑f
source
@[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) :
f.to_fun = ⇑f
source
@[simp]
theorem mul_hom.to_fun_eq_coe {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] (f : M →ₙ* N) :
f.to_fun = ⇑f
source
@[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) :
f.to_fun = ⇑f
source
@[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) :
f.to_fun = ⇑f
source
@[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 : M →*₀ N) :
f.to_fun = ⇑f
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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) :
⇑(f.to_zero_hom) = ⇑f
source
@[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) :
⇑(f.to_one_hom) = ⇑f
source
@[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) :
⇑(f.to_add_hom) = ⇑f
source
@[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) :
⇑(f.to_mul_hom) = ⇑f
source
@[simp]
theorem monoid_with_zero_hom.to_zero_hom_coe {M : Type u_1} {N : Type u_2} [mul_zero_one_class M] [mul_zero_one_class N] (f : M →*₀ N) :
⇑(f.to_zero_hom) = ⇑f
source
@[simp]
theorem monoid_with_zero_hom.to_monoid_hom_coe {M : Type u_1} {N : Type u_2} [mul_zero_one_class M] [mul_zero_one_class N] (f : M →*₀ N) :
⇑(f.to_monoid_hom) = ⇑f
source
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
source
@[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
source
@[ext]
theorem mul_hom.ext {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] ⦃f g : M →ₙ* N⦄ (h : ∀ (x : M), ⇑f x = ⇑g x) :
f = g
source
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
source
@[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
source
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
source
@[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 : M →*₀ N⦄ (h : ∀ (x : M), ⇑f x = ⇑g x) :
f = g
source
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

Deprecated: use fun_like.congr_fun instead.

source
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

Deprecated: use fun_like.congr_fun instead.

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

Deprecated: use fun_like.congr_fun instead.

source
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

Deprecated: use fun_like.congr_fun instead.

source
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

Deprecated: use fun_like.congr_fun instead.

source
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

Deprecated: use fun_like.congr_fun instead.

source
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 : M →*₀ N} (h : f = g) (x : M) :
⇑f x = ⇑g x

Deprecated: use fun_like.congr_fun instead.

source
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

Deprecated: use fun_like.congr_arg instead.

source
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

Deprecated: use fun_like.congr_arg instead.

source
theorem mul_hom.congr_arg {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] (f : M →ₙ* N) {x y : M} (h : x = y) :
⇑f x = ⇑f y

Deprecated: use fun_like.congr_arg instead.

source
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

Deprecated: use fun_like.congr_arg instead.

source
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

Deprecated: use fun_like.congr_arg instead.

source
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

Deprecated: use fun_like.congr_arg instead.

source
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 : M →*₀ N) {x y : M} (h : x = y) :
⇑f x = ⇑f y

Deprecated: use fun_like.congr_arg instead.

source
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

Deprecated: use fun_like.coe_injective instead.

source
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

Deprecated: use fun_like.coe_injective instead.

source
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

Deprecated: use fun_like.coe_injective instead.

source
theorem mul_hom.coe_inj {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] ⦃f g : M →ₙ* N⦄ (h : ⇑f = ⇑g) :
f = g

Deprecated: use fun_like.coe_injective instead.

source
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

Deprecated: use fun_like.coe_injective instead.

source
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

Deprecated: use fun_like.coe_injective instead.

source
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 : M →*₀ N⦄ (h : ⇑f = ⇑g) :
f = g

Deprecated: use fun_like.coe_injective instead.

source
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

Deprecated: use fun_like.ext_iff instead.

source
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

Deprecated: use fun_like.ext_iff instead.

source
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
source
theorem mul_hom.ext_iff {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] {f g : M →ₙ* N} :
f = g ↔ ∀ (x : M), ⇑f x = ⇑g x

Deprecated: use fun_like.ext_iff instead.

source
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

Deprecated: use fun_like.ext_iff instead.

source
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
source
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 : M →*₀ N} :
f = g ↔ ∀ (x : M), ⇑f x = ⇑g x

Deprecated: use fun_like.ext_iff instead.

source
@[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
source
@[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
source
@[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
source
@[simp]
theorem mul_hom.mk_coe {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
source
@[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
source
@[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
source
@[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 : 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
source
@[protected]
def zero_hom.copy {M : Type u_1} {N : Type u_2} {hM : has_zero M} {hN : has_zero N} (f : zero_hom M N) (f' : M → N) (h : f' = ⇑f) :
zero_hom M N

Copy of a zero_hom with a new to_fun equal to the old one. Useful to fix definitional equalities.

Equations
source
@[protected]
def one_hom.copy {M : Type u_1} {N : Type u_2} {hM : has_one M} {hN : has_one N} (f : one_hom M N) (f' : M → N) (h : f' = ⇑f) :
one_hom M N

Copy of a one_hom with a new to_fun equal to the old one. Useful to fix definitional equalities.

Equations
source
@[protected]
def add_hom.copy {M : Type u_1} {N : Type u_2} {hM : has_add M} {hN : has_add N} (f : add_hom M N) (f' : M → N) (h : f' = ⇑f) :
add_hom M N

Copy of an add_hom with a new to_fun equal to the old one. Useful to fix definitional equalities.

Equations
source
@[protected]
def mul_hom.copy {M : Type u_1} {N : Type u_2} {hM : has_mul M} {hN : has_mul N} (f : M →ₙ* N) (f' : M → N) (h : f' = ⇑f) :
M →ₙ* N

Copy of a mul_hom with a new to_fun equal to the old one. Useful to fix definitional equalities.

Equations
source
@[protected]
def add_monoid_hom.copy {M : Type u_1} {N : Type u_2} {hM : add_zero_class M} {hN : add_zero_class N} (f : M →+ N) (f' : M → N) (h : f' = ⇑f) :
M →+ N

Copy of an add_monoid_hom with a new to_fun equal to the old one. Useful to fix definitional equalities.

Equations
source
@[protected]
def monoid_hom.copy {M : Type u_1} {N : Type u_2} {hM : mul_one_class M} {hN : mul_one_class N} (f : M →* N) (f' : M → N) (h : f' = ⇑f) :
M →* N

Copy of a monoid_hom with a new to_fun equal to the old one. Useful to fix definitional equalities.

Equations
source
@[protected]
def monoid_with_zero_hom.copy {M : Type u_1} {N : Type u_2} {hM : mul_zero_one_class M} {hN : mul_zero_one_class N} (f : M →*₀ N) (f' : M → N) (h : f' = ⇑f) :
M →* N

Copy of a monoid_hom with a new to_fun equal to the old one. Useful to fix definitional equalities.

Equations
source
@[protected]
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
source
@[protected]
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
source
@[protected]
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.

source
@[protected]
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.

source
@[protected]
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 : M →*₀ N) :
⇑f 1 = 1
source
@[protected]
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 : M →*₀ N) :
⇑f 0 = 0
source
@[protected]
theorem mul_hom.map_mul {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] (f : M →ₙ* N) (a b : M) :
⇑f (a * b) = (⇑f a) * ⇑f b
source
@[protected]
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
source
@[protected]
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.

source
@[protected]
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.

source
@[protected]
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 : M →*₀ N) (a b : M) :
⇑f (a * b) = (⇑f a) * ⇑f b
source
theorem monoid_hom.map_exists_right_inv {M : Type u_1} {N : Type u_2} {F : Type u_6} {mM : mul_one_class M} {mN : mul_one_class N} [monoid_hom_class F M N] (f : F) {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.

source
theorem add_monoid_hom.map_exists_right_neg {M : Type u_1} {N : Type u_2} {F : Type u_6} {mM : add_zero_class M} {mN : add_zero_class N} [add_monoid_hom_class F M N] (f : F) {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.

source
theorem add_monoid_hom.map_exists_left_neg {M : Type u_1} {N : Type u_2} {F : Type u_6} {mM : add_zero_class M} {mN : add_zero_class N} [add_monoid_hom_class F M N] (f : F) {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.

source
theorem monoid_hom.map_exists_left_inv {M : Type u_1} {N : Type u_2} {F : Type u_6} {mM : mul_one_class M} {mN : mul_one_class N} [monoid_hom_class F M N] (f : F) {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.

source
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.

Equations
source
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
source
def zero_hom.id (M : Type u_1) [has_zero M] :
zero_hom M M

The identity map from an type with zero to itself.

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

The identity map from a type with 1 to itself.

Equations
source
@[simp]
theorem zero_hom.id_apply (M : Type u_1) [has_zero M] (x : M) :
⇑(zero_hom.id M) x = x
source
@[simp]
theorem mul_hom.id_apply (M : Type u_1) [has_mul M] (x : M) :
⇑(mul_hom.id M) x = x
source
def mul_hom.id (M : Type u_1) [has_mul M] :
M →ₙ* M

The identity map from a type with multiplication to itself.

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

The identity map from an type with addition to itself.

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

The identity map from a monoid to itself.

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

The identity map from an additive monoid to itself.

Equations
source
def monoid_with_zero_hom.id (M : Type u_1) [mul_zero_one_class M] :
M →*₀ M

The identity map from a monoid_with_zero to itself.

Equations
source
@[simp]
theorem monoid_with_zero_hom.id_apply (M : Type u_1) [mul_zero_one_class M] (x : M) :
⇑(monoid_with_zero_hom.id M) x = x
source
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) :
zero_hom M P

Composition of zero_homs as a zero_hom.

Equations
source
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) :
one_hom M P

Composition of one_homs as a one_hom.

Equations
source
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 : N →ₙ* P) (hmn : M →ₙ* N) :
M →ₙ* P

Composition of mul_homs as a mul_hom.

Equations
source
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) :
add_hom M P

Composition of add_homs as a add_hom.

Equations
source
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
source
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.

Equations
source
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 : N →*₀ P) (hmn : M →*₀ N) :
M →*₀ P

Composition of monoid_with_zero_homs as a monoid_with_zero_hom.

Equations
source
@[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
source
@[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
source
@[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 : N →ₙ* P) (f : M →ₙ* N) :
⇑(g.comp f) = ⇑g ∘ ⇑f
source
@[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
source
@[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
source
@[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
source
@[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 : N →*₀ P) (f : M →*₀ N) :
⇑(g.comp f) = ⇑g ∘ ⇑f
source
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)
source
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)
source
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)
source
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 : N →ₙ* P) (f : M →ₙ* N) (x : M) :
⇑(g.comp f) x = ⇑g (⇑f x)
source
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)
source
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)
source
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 : N →*₀ P) (f : M →*₀ N) (x : M) :
⇑(g.comp f) x = ⇑g (⇑f x)
source
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.

source
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)
source
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)
source
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 : M →ₙ* N) (g : N →ₙ* P) (h : P →ₙ* Q) :
(h.comp g).comp f = h.comp (g.comp f)
source
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)
source
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)
source
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 : M →*₀ N) (g : N →*₀ P) (h : P →*₀ Q) :
(h.comp g).comp f = h.comp (g.comp f)
source
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₂
source
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₂
source
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₂
source
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₂ : N →ₙ* P} {f : M →ₙ* N} (hf : function.surjective ⇑f) :
g₁.comp f = g₂.comp f ↔ g₁ = g₂
source
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₂
source
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₂
source
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₂ : N →*₀ P} {f : M →*₀ N} (hf : function.surjective ⇑f) :
g₁.comp f = g₂.comp f ↔ g₁ = g₂
source
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₂
source
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₂
source
theorem mul_hom.cancel_left {M : Type u_1} {N : Type u_2} {P : Type u_3} [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₂
source
theorem add_hom.cancel_left {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₁ f₂ : add_hom M N} (hg : function.injective ⇑g) :
g.comp f₁ = g.comp f₂ ↔ f₁ = f₂
source
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₂
source
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₂
source
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 : N →*₀ P} {f₁ f₂ : M →*₀ N} (hg : function.injective ⇑g) :
g.comp f₁ = g.comp f₂ ↔ f₁ = f₂
source
theorem add_monoid_hom.to_zero_hom_injective {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] :
function.injective add_monoid_hom.to_zero_hom
source
theorem monoid_hom.to_one_hom_injective {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] :
function.injective monoid_hom.to_one_hom
source
theorem monoid_hom.to_mul_hom_injective {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] :
function.injective monoid_hom.to_mul_hom
source
theorem add_monoid_hom.to_add_hom_injective {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] :
function.injective add_monoid_hom.to_add_hom
source
theorem monoid_with_zero_hom.to_monoid_hom_injective {M : Type u_1} {N : Type u_2} [mul_zero_one_class M] [mul_zero_one_class N] :
function.injective monoid_with_zero_hom.to_monoid_hom
source
theorem monoid_with_zero_hom.to_zero_hom_injective {M : Type u_1} {N : Type u_2} [mul_zero_one_class M] [mul_zero_one_class N] :
function.injective monoid_with_zero_hom.to_zero_hom
source
@[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) :
f.comp (zero_hom.id M) = f
source
@[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
source
@[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
source
@[simp]
theorem mul_hom.comp_id {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] (f : M →ₙ* N) :
f.comp (mul_hom.id M) = f
source
@[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) :
f.comp (monoid_hom.id M) = f
source
@[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) :
f.comp (add_monoid_hom.id M) = f
source
@[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 : M →*₀ N) :
f.comp (monoid_with_zero_hom.id M) = f
source
@[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) :
(zero_hom.id N).comp f = f
source
@[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
source
@[simp]
theorem mul_hom.id_comp {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] (f : M →ₙ* N) :
(mul_hom.id N).comp f = f
source
@[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
source
@[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) :
(add_monoid_hom.id N).comp f = f
source
@[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) :
(monoid_hom.id N).comp f = f
source
@[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 : M →*₀ N) :
(monoid_with_zero_hom.id N).comp f = f
source
@[protected]
theorem monoid_hom.map_pow {M : Type u_1} {N : Type u_2} [monoid M] [monoid N] (f : M →* N) (a : M) (n : ℕ) :
⇑f (a ^ n) = ⇑f a ^ n
source
@[protected]
theorem add_monoid_hom.map_nsmul {M : Type u_1} {N : Type u_2} [add_monoid M] [add_monoid N] (f : M →+ N) (a : M) (n : ℕ) :
⇑f (n • a) = n • ⇑f a
source
@[protected]
theorem add_monoid_hom.map_zsmul' {M : Type u_1} {N : Type u_2} [sub_neg_monoid M] [sub_neg_monoid N] (f : M →+ N) (hf : ∀ (x : M), ⇑f (-x) = -⇑f x) (a : M) (n : ℤ) :
⇑f (n • a) = n • ⇑f a
source
@[protected]
theorem monoid_hom.map_zpow' {M : Type u_1} {N : Type u_2} [div_inv_monoid M] [div_inv_monoid N] (f : M →* N) (hf : ∀ (x : M), ⇑f x⁻¹ = (⇑f x)⁻¹) (a : M) (n : ℤ) :
⇑f (a ^ n) = ⇑f a ^ n
source
@[protected]
def monoid.End (M : Type u_1) [mul_one_class M] :
Type u_1

The monoid of endomorphisms.

Equations
source
@[protected, instance]
def monoid.End.monoid (M : Type u_1) [mul_one_class M] :
monoid (monoid.End M)
Equations
source
@[protected, instance]
def monoid.End.inhabited (M : Type u_1) [mul_one_class M] :
inhabited (monoid.End M)
Equations
source
@[protected, instance]
def monoid.End.has_coe_to_fun (M : Type u_1) [mul_one_class M] :
has_coe_to_fun (monoid.End M) (λ (_x : monoid.End M), M → M)
Equations
source
@[simp]
theorem monoid.coe_one (M : Type u_1) [mul_one_class M] :
⇑1 = id
source
@[simp]
theorem monoid.coe_mul (M : Type u_1) [mul_one_class M] (f g : monoid.End M) :
⇑f * g = ⇑f ∘ ⇑g
source
@[protected]
def add_monoid.End (A : Type u_7) [add_zero_class A] :
Type u_7

The monoid of endomorphisms.

Equations
source
@[protected, instance]
def add_monoid.End.monoid (A : Type u_7) [add_zero_class A] :
monoid (add_monoid.End A)
Equations
source
@[protected, instance]
def add_monoid.End.inhabited (A : Type u_7) [add_zero_class A] :
inhabited (add_monoid.End A)
Equations
source
@[protected, instance]
def add_monoid.End.has_coe_to_fun (A : Type u_7) [add_zero_class A] :
has_coe_to_fun (add_monoid.End A) (λ (_x : add_monoid.End A), A → A)
Equations
source
@[simp]
theorem add_monoid.coe_one (A : Type u_7) [add_zero_class A] :
⇑1 = id
source
@[simp]
theorem add_monoid.coe_mul (A : Type u_7) [add_zero_class A] (f g : add_monoid.End A) :
⇑f * g = ⇑f ∘ ⇑g
source
@[protected, instance]
def one_hom.has_one {M : Type u_1} {N : Type u_2} [has_one M] [has_one N] :
has_one (one_hom M N)

1 is the homomorphism sending all elements to 1.

Equations
source
@[protected, instance]
def zero_hom.has_zero {M : Type u_1} {N : Type u_2} [has_zero M] [has_zero N] :
has_zero (zero_hom M N)

0 is the homomorphism sending all elements to 0.

Equations
source
@[protected, instance]
def mul_hom.has_one {M : Type u_1} {N : Type u_2} [has_mul M] [mul_one_class N] :
has_one (M →ₙ* N)

1 is the multiplicative homomorphism sending all elements to 1.

Equations
source
@[protected, instance]
def add_hom.has_zero {M : Type u_1} {N : Type u_2} [has_add M] [add_zero_class N] :
has_zero (add_hom M N)

0 is the additive homomorphism sending all elements to 0.

Equations
source
@[protected, instance]
def monoid_hom.has_one {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] :
has_one (M →* N)

1 is the monoid homomorphism sending all elements to 1.

Equations
source
@[protected, instance]
def add_monoid_hom.has_zero {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] :
has_zero (M →+ N)

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

Equations
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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
source
@[protected, instance]
def one_hom.inhabited {M : Type u_1} {N : Type u_2} [has_one M] [has_one N] :
inhabited (one_hom M N)
Equations
source
@[protected, instance]
def zero_hom.inhabited {M : Type u_1} {N : Type u_2} [has_zero M] [has_zero N] :
inhabited (zero_hom M N)
Equations
source
@[protected, instance]
def add_hom.inhabited {M : Type u_1} {N : Type u_2} [has_add M] [add_zero_class N] :
inhabited (add_hom M N)
Equations
source
@[protected, instance]
def mul_hom.inhabited {M : Type u_1} {N : Type u_2} [has_mul M] [mul_one_class N] :
inhabited (M →ₙ* N)
Equations
source
@[protected, instance]
def add_monoid_hom.inhabited {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] :
inhabited (M →+ N)
Equations
source
@[protected, instance]
def monoid_hom.inhabited {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] :
inhabited (M →* N)
Equations
source
@[protected, instance]
def monoid_with_zero_hom.inhabited {M : Type u_1} [mul_zero_one_class M] :
inhabited (M →*₀ M)
Equations
source
@[protected, instance]
def add_hom.has_add {M : Type u_1} {N : Type u_2} [has_add M] [add_comm_semigroup N] :
has_add (add_hom M N)

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

Equations
source
@[protected, instance]
def mul_hom.has_mul {M : Type u_1} {N : Type u_2} [has_mul M] [comm_semigroup N] :
has_mul (M →ₙ* N)

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

Equations
source
@[simp]
theorem mul_hom.mul_apply {M : Type u_1} {N : Type u_2} {mM : has_mul M} {mN : comm_semigroup N} (f g : M →ₙ* N) (x : M) :
(⇑f * g) x = (⇑f x) * ⇑g x
source
@[simp]
theorem add_hom.add_apply {M : Type u_1} {N : Type u_2} {mM : has_add M} {mN : add_comm_semigroup N} (f g : add_hom M N) (x : M) :
⇑(f + g) x = ⇑f x + ⇑g x
source
theorem add_hom.add_comp {M : Type u_1} {N : Type u_2} {P : Type u_3} [has_add M] [has_add N] [add_comm_semigroup P] (g₁ g₂ : add_hom N P) (f : add_hom M N) :
(g₁ + g₂).comp f = g₁.comp f + g₂.comp f
source
theorem mul_hom.mul_comp {M : Type u_1} {N : Type u_2} {P : Type u_3} [has_mul M] [has_mul N] [comm_semigroup P] (g₁ g₂ : N →ₙ* P) (f : M →ₙ* N) :
(g₁ * g₂).comp f = (g₁.comp f) * g₂.comp f
source
theorem mul_hom.comp_mul {M : Type u_1} {N : Type u_2} {P : Type u_3} [has_mul M] [comm_semigroup N] [comm_semigroup P] (g : N →ₙ* P) (f₁ f₂ : M →ₙ* N) :
g.comp (f₁ * f₂) = (g.comp f₁) * g.comp f₂
source
theorem add_hom.comp_add {M : Type u_1} {N : Type u_2} {P : Type u_3} [has_add M] [add_comm_semigroup N] [add_comm_semigroup P] (g : add_hom N P) (f₁ f₂ : add_hom M N) :
g.comp (f₁ + f₂) = g.comp f₁ + g.comp f₂
source
@[protected, instance]
def monoid_hom.has_mul {M : Type u_1} {N : Type u_2} {mM : mul_one_class M} [comm_monoid N] :
has_mul (M →* 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
source
@[protected, instance]
def add_monoid_hom.has_add {M : Type u_1} {N : Type u_2} {mM : add_zero_class M} [add_comm_monoid N] :
has_add (M →+ 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.

Equations
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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
source
theorem add_monoid_hom.add_comp {M : Type u_1} {N : Type u_2} {P : Type u_3} [add_zero_class M] [add_zero_class N] [add_comm_monoid P] (g₁ g₂ : N →+ P) (f : M →+ N) :
(g₁ + g₂).comp f = g₁.comp f + g₂.comp f
source
theorem monoid_hom.mul_comp {M : Type u_1} {N : Type u_2} {P : Type u_3} [mul_one_class M] [mul_one_class N] [comm_monoid P] (g₁ g₂ : N →* P) (f : M →* N) :
(g₁ * g₂).comp f = (g₁.comp f) * g₂.comp f
source
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₂
source
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₂
source
theorem add_monoid_hom.eq_on_neg {M : Type u_1} {F : Type u_6} {G : Type u_2} [add_group G] [add_monoid M] [add_monoid_hom_class F G M] {f g : F} {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.

source
theorem monoid_hom.eq_on_inv {M : Type u_1} {F : Type u_6} {G : Type u_2} [group G] [monoid M] [monoid_hom_class F G M] {f g : F} {x : G} (h : ⇑f x = ⇑g x) :
⇑f x⁻¹ = ⇑g x⁻¹

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

source
@[protected]
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
source
@[protected]
theorem monoid_hom.map_inv {G : Type u_1} {H : Type u_2} [group G] [group H] (f : G →* H) (g : G) :
⇑f g⁻¹ = (⇑f g)⁻¹

Group homomorphisms preserve inverse.

source
@[protected]
theorem add_monoid_hom.map_zsmul {G : Type u_1} {H : Type u_2} [add_group G] [add_group H] (f : G →+ H) (g : G) (n : ℤ) :
⇑f (n • g) = n • ⇑f g

Additive group homomorphisms preserve integer scaling.

source
@[protected]
theorem monoid_hom.map_zpow {G : Type u_1} {H : Type u_2} [group G] [group H] (f : G →* H) (g : G) (n : ℤ) :
⇑f (g ^ n) = ⇑f g ^ n

Group homomorphisms preserve integer power.

source
@[protected]
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.

source
@[protected]
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.

source
@[protected]
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
source
@[protected]
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.

source
theorem injective_iff_map_eq_one {F : Type u_6} {G : Type u_1} {H : Type u_2} [group G] [mul_one_class H] [monoid_hom_class F G H] (f : F) :
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. For the iff statement on the triviality of the kernel, see injective_iff_map_eq_one'.

source
theorem injective_iff_map_eq_zero {F : Type u_6} {G : Type u_1} {H : Type u_2} [add_group G] [add_zero_class H] [add_monoid_hom_class F G H] (f : F) :
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. For the iff statement on the triviality of the kernel, see injective_iff_map_eq_zero'.

source
theorem injective_iff_map_eq_zero' {F : Type u_6} {G : Type u_1} {H : Type u_2} [add_group G] [add_zero_class H] [add_monoid_hom_class F G H] (f : F) :
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 injective_iff_map_eq_zero.

source
theorem injective_iff_map_eq_one' {F : Type u_6} {G : Type u_1} {H : Type u_2} [group G] [mul_one_class H] [monoid_hom_class F G H] (f : F) :
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 injective_iff_map_eq_one.

source
@[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
source
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.

Equations
source
@[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
source
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
source
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.

Equations
source
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
source
@[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)⁻¹) :
⇑(monoid_hom.of_map_mul_inv f map_div) = f
source
@[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) :
⇑(add_monoid_hom.of_map_add_neg f map_div) = f
source
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
source
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.

Equations
source
@[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) :
⇑(monoid_hom.of_map_div f hf) = f
source
@[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) :
⇑(add_monoid_hom.of_map_sub f hf) = f
source
@[protected, instance]
def add_monoid_hom.has_neg {M : Type u_1} {G : Type u_2} [add_zero_class M] [add_comm_group G] :
has_neg (M →+ G)

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

Equations
source
@[protected, instance]
def monoid_hom.has_inv {M : Type u_1} {G : Type u_2} [mul_one_class M] [comm_group G] :
has_inv (M →* G)

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

Equations
source
@[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) :
⇑f⁻¹ x = (⇑f x)⁻¹
source
@[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
source
@[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 ψ
source
@[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 ψ)⁻¹
source
@[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 ψ
source
@[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 ψ)⁻¹
source
@[protected, instance]
def add_monoid_hom.has_sub {M : Type u_1} {G : Type u_2} [add_zero_class M] [add_comm_group G] :
has_sub (M →+ 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).

Equations
source
@[protected, instance]
def monoid_hom.has_div {M : Type u_1} {G : Type u_2} [mul_one_class M] [comm_group G] :
has_div (M →* 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
source
@[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
source
@[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
source
@[protected, instance]
def monoid_with_zero_hom.has_mul {M : Type u_1} {N : Type u_2} {hM : mul_zero_one_class M} [comm_monoid_with_zero N] :
has_mul (M →*₀ N)

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

Equations
source
@[protected, simp]
theorem add_semiconj_by.map {M : Type u_1} {N : Type u_2} {F : Type u_6} [has_add M] [has_add N] {a x y : M} [add_hom_class F M N] (h : add_semiconj_by a x y) (f : F) :
add_semiconj_by (⇑f a) (⇑f x) (⇑f y)
source
@[protected, simp]
theorem semiconj_by.map {M : Type u_1} {N : Type u_2} {F : Type u_6} [has_mul M] [has_mul N] {a x y : M} [mul_hom_class F M N] (h : semiconj_by a x y) (f : F) :
semiconj_by (⇑f a) (⇑f x) (⇑f y)
source
@[protected, simp]
theorem add_commute.map {M : Type u_1} {N : Type u_2} {F : Type u_6} [has_add M] [has_add N] {x y : M} [add_hom_class F M N] (h : add_commute x y) (f : F) :
add_commute (⇑f x) (⇑f y)
source
@[protected, simp]
theorem commute.map {M : Type u_1} {N : Type u_2} {F : Type u_6} [has_mul M] [has_mul N] {x y : M} [mul_hom_class F M N] (h : commute x y) (f : F) :
commute (⇑f x) (⇑f y)