mathlib3 documentation

algebra.hom.group

Monoid and group homomorphisms #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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_9) (N : Type u_10) [has_zero M] [has_zero N] :
Type (max u_10 u_9)

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.

Instances for zero_hom
source
@[instance]
def zero_hom_class.to_fun_like (F : Type u_9) (M : out_param (Type u_10)) (N : out_param (Type u_11)) [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_9) (M : out_param (Type u_10)) (N : out_param (Type u_11)) [has_zero M] [has_zero N] :
Type (max u_10 u_11 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 of this typeclass
Instances of other typeclasses for zero_hom_class
  • zero_hom_class.has_sizeof_inst
source
theorem ne_zero.of_map {F : Type u_8} {R : Type u_1} {M : Type u_2} [has_zero R] [has_zero M] [zero_hom_class F R M] (f : F) {r : R} [ne_zero (⇑f r)] :
ne_zero r
source
theorem ne_zero.of_injective {F : Type u_8} {R : Type u_1} {M : Type u_2} [has_zero R] {r : R} [ne_zero r] [has_zero M] [zero_hom_class F R M] {f : F} (hf : function.injective ⇑f) :
ne_zero (⇑f r)
source
structure add_hom (M : Type u_9) (N : Type u_10) [has_add M] [has_add N] :
Type (max u_10 u_9)

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.

Instances for add_hom
source
@[class]
structure add_hom_class (F : Type u_9) (M : out_param (Type u_10)) (N : out_param (Type u_11)) [has_add M] [has_add N] :
Type (max u_10 u_11 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 of this typeclass
Instances of other typeclasses for add_hom_class
  • add_hom_class.has_sizeof_inst
source
@[instance]
def add_hom_class.to_fun_like (F : Type u_9) (M : out_param (Type u_10)) (N : out_param (Type u_11)) [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_9} {N : Type u_10} [add_zero_class M] [add_zero_class N] (self : M →+ N) :
add_hom M N
source
structure add_monoid_hom (M : Type u_9) (N : Type u_10) [add_zero_class M] [add_zero_class N] :
Type (max u_10 u_9)

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.

Instances for add_monoid_hom
source
@[nolint]
def add_monoid_hom.to_zero_hom {M : Type u_9} {N : Type u_10} [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_9) (M : out_param (Type u_10)) (N : out_param (Type u_11)) [add_zero_class M] [add_zero_class N] :
Type (max u_10 u_11 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 of this typeclass
Instances of other typeclasses for add_monoid_hom_class
  • add_monoid_hom_class.has_sizeof_inst
source
@[instance]
def add_monoid_hom_class.to_add_hom_class (F : Type u_9) (M : out_param (Type u_10)) (N : out_param (Type u_11)) [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_9) (M : out_param (Type u_10)) (N : out_param (Type u_11)) [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_9) (N : Type u_10) [has_one M] [has_one N] :
Type (max u_10 u_9)

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.

Instances for one_hom
source
@[class]
structure one_hom_class (F : Type u_9) (M : out_param (Type u_10)) (N : out_param (Type u_11)) [has_one M] [has_one N] :
Type (max u_10 u_11 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 of this typeclass
Instances of other typeclasses for one_hom_class
  • one_hom_class.has_sizeof_inst
source
@[instance]
def one_hom_class.to_fun_like (F : Type u_9) (M : out_param (Type u_10)) (N : out_param (Type u_11)) [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_3} {N : Type u_4} [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_3} {N : Type u_4} [has_zero M] [has_zero N] :
zero_hom_class (zero_hom M N) M N
Equations
source
@[simp]
theorem map_one {M : Type u_3} {N : Type u_4} {F : Type u_8} [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_3} {N : Type u_4} {F : Type u_8} [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_3} {N : Type u_4} {F : Type u_8} [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_3} {N : Type u_4} {F : Type u_8} [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_3} {N : Type u_4} {F : Type u_8} [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_3} {N : Type u_4} {F : Type u_8} [has_one M] [has_one N] [one_hom_class F M N] :
has_coe_t F (one_hom M N)
Equations
source
@[simp]
theorem one_hom.coe_coe {M : Type u_3} {N : Type u_4} {F : Type u_8} [has_one M] [has_one N] [one_hom_class F M N] (f : F) :
⇑↑f = ⇑f
source
@[simp]
theorem zero_hom.coe_coe {M : Type u_3} {N : Type u_4} {F : Type u_8} [has_zero M] [has_zero N] [zero_hom_class F M N] (f : F) :
⇑↑f = ⇑f
source
structure mul_hom (M : Type u_9) (N : Type u_10) [has_mul M] [has_mul N] :
Type (max u_10 u_9)

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.

Instances for mul_hom
source
@[instance]
def mul_hom_class.to_fun_like (F : Type u_9) (M : out_param (Type u_10)) (N : out_param (Type u_11)) [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_9) (M : out_param (Type u_10)) (N : out_param (Type u_11)) [has_mul M] [has_mul N] :
Type (max u_10 u_11 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 of this typeclass
Instances of other typeclasses for mul_hom_class
  • mul_hom_class.has_sizeof_inst
source
@[protected, instance]
def add_hom.add_hom_class {M : Type u_3} {N : Type u_4} [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_3} {N : Type u_4} [has_mul M] [has_mul N] :
mul_hom_class (M →ₙ* N) M N
Equations
source
@[simp]
theorem map_add {M : Type u_3} {N : Type u_4} {F : Type u_8} [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_3} {N : Type u_4} {F : Type u_8} [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_3} {N : Type u_4} {F : Type u_8} [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_3} {N : Type u_4} {F : Type u_8} [has_add M] [has_add N] [add_hom_class F M N] :
has_coe_t F (add_hom M N)
Equations
source
@[simp]
theorem add_hom.coe_coe {M : Type u_3} {N : Type u_4} {F : Type u_8} [has_add M] [has_add N] [add_hom_class F M N] (f : F) :
⇑↑f = ⇑f
source
@[simp]
theorem mul_hom.coe_coe {M : Type u_3} {N : Type u_4} {F : Type u_8} [has_mul M] [has_mul N] [mul_hom_class F M N] (f : F) :
⇑↑f = ⇑f
source
structure monoid_hom (M : Type u_9) (N : Type u_10) [mul_one_class M] [mul_one_class N] :
Type (max u_10 u_9)

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.

Instances for monoid_hom
source
@[nolint]
def monoid_hom.to_one_hom {M : Type u_9} {N : Type u_10} [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_9} {N : Type u_10} [mul_one_class M] [mul_one_class N] (self : M →* N) :
M →ₙ* N
source
@[class]
structure monoid_hom_class (F : Type u_9) (M : out_param (Type u_10)) (N : out_param (Type u_11)) [mul_one_class M] [mul_one_class N] :
Type (max u_10 u_11 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 of this typeclass
Instances of other typeclasses for monoid_hom_class
  • monoid_hom_class.has_sizeof_inst
source
@[instance]
def monoid_hom_class.to_one_hom_class (F : Type u_9) (M : out_param (Type u_10)) (N : out_param (Type u_11)) [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_9) (M : out_param (Type u_10)) (N : out_param (Type u_11)) [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_3} {N : Type u_4} [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_3} {N : Type u_4} [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_3} {N : Type u_4} {F : Type u_8} [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_3} {N : Type u_4} {F : Type u_8} [mul_one_class M] [mul_one_class N] [monoid_hom_class F M N] :
has_coe_t F (M →* N)
Equations
source
@[simp]
theorem monoid_hom.coe_coe {M : Type u_3} {N : Type u_4} {F : Type u_8} [mul_one_class M] [mul_one_class N] [monoid_hom_class F M N] (f : F) :
⇑↑f = ⇑f
source
@[simp]
theorem add_monoid_hom.coe_coe {M : Type u_3} {N : Type u_4} {F : Type u_8} [add_zero_class M] [add_zero_class N] [add_monoid_hom_class F M N] (f : F) :
⇑↑f = ⇑f
source
theorem map_mul_eq_one {M : Type u_3} {N : Type u_4} {F : Type u_8} [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_3} {N : Type u_4} {F : Type u_8} [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
theorem map_div' {G : Type u_6} {H : Type u_7} {F : Type u_8} [div_inv_monoid G] [div_inv_monoid H] [monoid_hom_class F G H] (f : F) (hf : ∀ (a : G), ⇑f a⁻¹ = (⇑f a)⁻¹) (a b : G) :
⇑f (a / b) = ⇑f a / ⇑f b
source
theorem map_sub' {G : Type u_6} {H : Type u_7} {F : Type u_8} [sub_neg_monoid G] [sub_neg_monoid H] [add_monoid_hom_class F G H] (f : F) (hf : ∀ (a : G), ⇑f (-a) = -⇑f a) (a b : G) :
⇑f (a - b) = ⇑f a - ⇑f b
source
@[simp]
theorem map_inv {G : Type u_6} {H : Type u_7} {F : Type u_8} [group G] [division_monoid H] [monoid_hom_class F G H] (f : F) (a : G) :
⇑f a⁻¹ = (⇑f a)⁻¹

Group homomorphisms preserve inverse.

source
@[simp]
theorem map_neg {G : Type u_6} {H : Type u_7} {F : Type u_8} [add_group G] [subtraction_monoid H] [add_monoid_hom_class F G H] (f : F) (a : G) :
⇑f (-a) = -⇑f a

Additive group homomorphisms preserve negation.

source
@[simp]
theorem map_mul_inv {G : Type u_6} {H : Type u_7} {F : Type u_8} [group G] [division_monoid H] [monoid_hom_class F G H] (f : F) (a b : G) :
⇑f (a * b⁻¹) = ⇑f a * (⇑f b)⁻¹

Group homomorphisms preserve division.

source
@[simp]
theorem map_add_neg {G : Type u_6} {H : Type u_7} {F : Type u_8} [add_group G] [subtraction_monoid H] [add_monoid_hom_class F G H] (f : F) (a b : G) :
⇑f (a + -b) = ⇑f a + -⇑f b

Additive group homomorphisms preserve subtraction.

source
@[simp]
theorem map_div {G : Type u_6} {H : Type u_7} {F : Type u_8} [group G] [division_monoid H] [monoid_hom_class F G H] (f : F) (a b : G) :
⇑f (a / b) = ⇑f a / ⇑f b

Group homomorphisms preserve division.

source
@[simp]
theorem map_sub {G : Type u_6} {H : Type u_7} {F : Type u_8} [add_group G] [subtraction_monoid H] [add_monoid_hom_class F G H] (f : F) (a b : G) :
⇑f (a - b) = ⇑f a - ⇑f b

Additive group homomorphisms preserve subtraction.

source
@[simp]
theorem map_pow {G : Type u_6} {H : Type u_7} {F : Type u_8} [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_6} {H : Type u_7} {F : Type u_8} [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_6} {H : Type u_7} {F : Type u_8} [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_6} {H : Type u_7} {F : Type u_8} [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_6} {H : Type u_7} {F : Type u_8} [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_6} {H : Type u_7} {F : Type u_8} [group G] [division_monoid 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_6} {H : Type u_7} {F : Type u_8} [add_group G] [subtraction_monoid 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_6} {H : Type u_7} {F : Type u_8} [add_group G] [subtraction_monoid 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_9} {N : Type u_10} [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_9) (N : Type u_10) [mul_zero_one_class M] [mul_zero_one_class N] :
Type (max u_10 u_9)

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.

Instances for monoid_with_zero_hom
source
@[nolint]
def monoid_with_zero_hom.to_monoid_hom {M : Type u_9} {N : Type u_10} [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_9) (M : out_param (Type u_10)) (N : out_param (Type u_11)) [mul_zero_one_class M] [mul_zero_one_class N] :
Type (max u_10 u_11 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 of this typeclass
Instances of other typeclasses for monoid_with_zero_hom_class
  • monoid_with_zero_hom_class.has_sizeof_inst
source
@[instance]
def monoid_with_zero_hom_class.to_monoid_hom_class (F : Type u_9) (M : out_param (Type u_10)) (N : out_param (Type u_11)) [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_9) (M : out_param (Type u_10)) (N : out_param (Type u_11)) [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_3} {N : Type u_4} [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_3} {N : Type u_4} {F : Type u_8} [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
source
@[simp]
theorem monoid_with_zero_hom.coe_coe {M : Type u_3} {N : Type u_4} {F : Type u_8} [mul_zero_one_class M] [mul_zero_one_class N] [monoid_with_zero_hom_class F M N] (f : F) :
⇑↑f = ⇑f

Bundled morphisms can be down-cast to weaker bundlings

source
@[protected, instance]
def add_monoid_hom.has_coe_to_zero_hom {M : Type u_3} {N : Type u_4} {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_3} {N : Type u_4} {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_3} {N : Type u_4} {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_3} {N : Type u_4} {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_3} {N : Type u_4} {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_3} {N : Type u_4} {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_3} {N : Type u_4} {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_3} {N : Type u_4} {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_3} {N : Type u_4} {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_3} {N : Type u_4} {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_3} {N : Type u_4} {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_3} {N : Type u_4} {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_3} {N : Type u_4} {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_3} {N : Type u_4} {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_3} {N : Type u_4} {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_3} {N : Type u_4} {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_3} {N : Type u_4} {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_3} {N : Type u_4} {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_3} {N : Type u_4} {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_3} {N : Type u_4} [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_3} {N : Type u_4} [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_3} {N : Type u_4} [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_3} {N : Type u_4} [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_3} {N : Type u_4} [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_3} {N : Type u_4} [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_3} {N : Type u_4} [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_3} {N : Type u_4} [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_3} {N : Type u_4} [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_3} {N : Type u_4} [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_3} {N : Type u_4} [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_3} {N : Type u_4} [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_3} {N : Type u_4} [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_3} {N : Type u_4} [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_3} {N : Type u_4} [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_3} {N : Type u_4} [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_3} {N : Type u_4} [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_3} {N : Type u_4} [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_3} {N : Type u_4} [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_3} {N : Type u_4} [mul_zero_one_class M] [mul_zero_one_class N] (f : M →*₀ N) :
⇑(f.to_monoid_hom) = ⇑f
source
@[ext]
theorem zero_hom.ext {M : Type u_3} {N : Type u_4} [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_3} {N : Type u_4} [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_3} {N : Type u_4} [has_mul M] [has_mul N] ⦃f g : M →ₙ* N⦄ (h : ∀ (x : M), ⇑f x = ⇑g x) :
f = g
source
@[ext]
theorem add_hom.ext {M : Type u_3} {N : Type u_4} [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_3} {N : Type u_4} [mul_one_class M] [mul_one_class N] ⦃f g : M →* N⦄ (h : ∀ (x : M), ⇑f x = ⇑g x) :
f = g
source
@[ext]
theorem add_monoid_hom.ext {M : Type u_3} {N : Type u_4} [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_3} {N : Type u_4} [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_3} {N : Type u_4} [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_3} {N : Type u_4} [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_3} {N : Type u_4} [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_3} {N : Type u_4} [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_3} {N : Type u_4} [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_3} {N : Type u_4} [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_3} {N : Type u_4} [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_3} {N : Type u_4} [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_3} {N : Type u_4} [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_3} {N : Type u_4} [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_3} {N : Type u_4} [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_3} {N : Type u_4} [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_3} {N : Type u_4} [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_3} {N : Type u_4} [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_3} {N : Type u_4} [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_3} {N : Type u_4} [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_3} {N : Type u_4} [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_3} {N : Type u_4} [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_3} {N : Type u_4} [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_3} {N : Type u_4} [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_3} {N : Type u_4} [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_3} {N : Type u_4} [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_3} {N : Type u_4} [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_3} {N : Type u_4} [has_add M] [has_add N] {f g : add_hom M N} :
f = g ↔ ∀ (x : M), ⇑f x = ⇑g x

Deprecated: use fun_like.ext_iff instead.

source
theorem mul_hom.ext_iff {M : Type u_3} {N : Type u_4} [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_3} {N : Type u_4} [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_3} {N : Type u_4} [add_zero_class M] [add_zero_class N] {f g : M →+ N} :
f = g ↔ ∀ (x : M), ⇑f x = ⇑g x

Deprecated: use fun_like.ext_iff instead.

source
theorem monoid_with_zero_hom.ext_iff {M : Type u_3} {N : Type u_4} [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_3} {N : Type u_4} [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_3} {N : Type u_4} [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_3} {N : Type u_4} [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_3} {N : Type u_4} [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_3} {N : Type u_4} [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_3} {N : Type u_4} [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_3} {N : Type u_4} [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_3} {N : Type u_4} {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_3} {N : Type u_4} {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
@[simp]
theorem zero_hom.coe_copy {M : Type u_3} {N : Type u_4} {hM : has_zero M} {hN : has_zero N} (f : zero_hom M N) (f' : M → N) (h : f' = ⇑f) :
⇑(f.copy f' h) = f'
source
@[simp]
theorem one_hom.coe_copy {M : Type u_3} {N : Type u_4} {hM : has_one M} {hN : has_one N} (f : one_hom M N) (f' : M → N) (h : f' = ⇑f) :
⇑(f.copy f' h) = f'
source
theorem zero_hom.coe_copy_eq {M : Type u_3} {N : Type u_4} {hM : has_zero M} {hN : has_zero N} (f : zero_hom M N) (f' : M → N) (h : f' = ⇑f) :
f.copy f' h = f
source
theorem one_hom.coe_copy_eq {M : Type u_3} {N : Type u_4} {hM : has_one M} {hN : has_one N} (f : one_hom M N) (f' : M → N) (h : f' = ⇑f) :
f.copy f' h = f
source
@[protected]
def add_hom.copy {M : Type u_3} {N : Type u_4} {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_3} {N : Type u_4} {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
@[simp]
theorem mul_hom.coe_copy {M : Type u_3} {N : Type u_4} {hM : has_mul M} {hN : has_mul N} (f : M →ₙ* N) (f' : M → N) (h : f' = ⇑f) :
⇑(f.copy f' h) = f'
source
@[simp]
theorem add_hom.coe_copy {M : Type u_3} {N : Type u_4} {hM : has_add M} {hN : has_add N} (f : add_hom M N) (f' : M → N) (h : f' = ⇑f) :
⇑(f.copy f' h) = f'
source
theorem mul_hom.coe_copy_eq {M : Type u_3} {N : Type u_4} {hM : has_mul M} {hN : has_mul N} (f : M →ₙ* N) (f' : M → N) (h : f' = ⇑f) :
f.copy f' h = f
source
theorem add_hom.coe_copy_eq {M : Type u_3} {N : Type u_4} {hM : has_add M} {hN : has_add N} (f : add_hom M N) (f' : M → N) (h : f' = ⇑f) :
f.copy f' h = f
source
@[protected]
def add_monoid_hom.copy {M : Type u_3} {N : Type u_4} {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_3} {N : Type u_4} {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
@[simp]
theorem add_monoid_hom.coe_copy {M : Type u_3} {N : Type u_4} {hM : add_zero_class M} {hN : add_zero_class N} (f : M →+ N) (f' : M → N) (h : f' = ⇑f) :
⇑(f.copy f' h) = f'
source
@[simp]
theorem monoid_hom.coe_copy {M : Type u_3} {N : Type u_4} {hM : mul_one_class M} {hN : mul_one_class N} (f : M →* N) (f' : M → N) (h : f' = ⇑f) :
⇑(f.copy f' h) = f'
source
theorem monoid_hom.copy_eq {M : Type u_3} {N : Type u_4} {hM : mul_one_class M} {hN : mul_one_class N} (f : M →* N) (f' : M → N) (h : f' = ⇑f) :
f.copy f' h = f
source
theorem add_monoid_hom.copy_eq {M : Type u_3} {N : Type u_4} {hM : add_zero_class M} {hN : add_zero_class N} (f : M →+ N) (f' : M → N) (h : f' = ⇑f) :
f.copy f' h = f
source
@[protected]
def monoid_with_zero_hom.copy {M : Type u_3} {N : Type u_4} {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
@[simp]
theorem monoid_with_zero_hom.coe_copy {M : Type u_3} {N : Type u_4} {hM : mul_zero_one_class M} {hN : mul_zero_one_class N} (f : M →*₀ N) (f' : M → N) (h : f' = ⇑f) :
⇑(f.copy f' h) = f'
source
theorem monoid_with_zero_hom.copy_eq {M : Type u_3} {N : Type u_4} {hM : mul_zero_one_class M} {hN : mul_zero_one_class N} (f : M →*₀ N) (f' : M → N) (h : f' = ⇑f) :
f.copy f' h = ↑f
source
@[protected]
theorem one_hom.map_one {M : Type u_3} {N : Type u_4} [has_one M] [has_one N] (f : one_hom M N) :
⇑f 1 = 1
source
@[protected]
theorem zero_hom.map_zero {M : Type u_3} {N : Type u_4} [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_3} {N : Type u_4} [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_3} {N : Type u_4} [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_3} {N : Type u_4} [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_3} {N : Type u_4} [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_3} {N : Type u_4} [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_3} {N : Type u_4} [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_3} {N : Type u_4} [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_3} {N : Type u_4} [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_3} {N : Type u_4} [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_3} {N : Type u_4} {F : Type u_8} {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_3} {N : Type u_4} {F : Type u_8} {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_3} {N : Type u_4} {F : Type u_8} {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_3} {N : Type u_4} {F : Type u_8} {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 neg_add_monoid_hom {α : Type u_1} [subtraction_comm_monoid α] :
α →+ α

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

Equations
source
def inv_monoid_hom {α : Type u_1} [division_comm_monoid α] :
α →* α

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

Equations
source
@[simp]
theorem coe_inv_monoid_hom {α : Type u_1} [division_comm_monoid α] :
⇑inv_monoid_hom = has_inv.inv
source
@[simp]
theorem inv_monoid_hom_apply {α : Type u_1} [division_comm_monoid α] (a : α) :
⇑inv_monoid_hom a = a⁻¹
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_3} {N : Type u_4} {P : Type u_5} [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_3} {N : Type u_4} {P : Type u_5} [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_3} {N : Type u_4} {P : Type u_5} [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_3} {N : Type u_4} {P : Type u_5} [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_3} {N : Type u_4} {P : Type u_5} [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_3} {N : Type u_4} {P : Type u_5} [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_3} {N : Type u_4} {P : Type u_5} [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_3} {N : Type u_4} {P : Type u_5} [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_3} {N : Type u_4} {P : Type u_5} [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_3} {N : Type u_4} {P : Type u_5} [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_3} {N : Type u_4} {P : Type u_5} [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_3} {N : Type u_4} {P : Type u_5} [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_3} {N : Type u_4} {P : Type u_5} [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_3} {N : Type u_4} {P : Type u_5} [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_3} {N : Type u_4} {P : Type u_5} [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_3} {N : Type u_4} {P : Type u_5} [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_3} {N : Type u_4} {P : Type u_5} [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_3} {N : Type u_4} {P : Type u_5} [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_3} {N : Type u_4} {P : Type u_5} [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_3} {N : Type u_4} {P : Type u_5} [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_3} {N : Type u_4} {P : Type u_5} [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_3} {N : Type u_4} {P : Type u_5} {Q : Type u_1} [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_3} {N : Type u_4} {P : Type u_5} {Q : Type u_1} [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)

Composition of additive monoid homomorphisms is associative.

source
theorem add_hom.comp_assoc {M : Type u_3} {N : Type u_4} {P : Type u_5} {Q : Type u_1} [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_3} {N : Type u_4} {P : Type u_5} {Q : Type u_1} [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_3} {N : Type u_4} {P : Type u_5} {Q : Type u_1} [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_3} {N : Type u_4} {P : Type u_5} {Q : Type u_1} [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_3} {N : Type u_4} {P : Type u_5} {Q : Type u_1} [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_3} {N : Type u_4} {P : Type u_5} [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_3} {N : Type u_4} {P : Type u_5} [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_3} {N : Type u_4} {P : Type u_5} [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_3} {N : Type u_4} {P : Type u_5} [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_3} {N : Type u_4} {P : Type u_5} [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_3} {N : Type u_4} {P : Type u_5} [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_3} {N : Type u_4} {P : Type u_5} [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_3} {N : Type u_4} {P : Type u_5} [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_3} {N : Type u_4} {P : Type u_5} [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_3} {N : Type u_4} {P : Type u_5} [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_3} {N : Type u_4} {P : Type u_5} [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_3} {N : Type u_4} {P : Type u_5} [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_3} {N : Type u_4} {P : Type u_5} [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_3} {N : Type u_4} {P : Type u_5} [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_3} {N : Type u_4} [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_3} {N : Type u_4} [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_3} {N : Type u_4} [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_3} {N : Type u_4} [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_3} {N : Type u_4} [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_3} {N : Type u_4} [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_3} {N : Type u_4} [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_3} {N : Type u_4} [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_3} {N : Type u_4} [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_3} {N : Type u_4} [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_3} {N : Type u_4} [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_3} {N : Type u_4} [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_3} {N : Type u_4} [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_3} {N : Type u_4} [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_3} {N : Type u_4} [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_3} {N : Type u_4} [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_3} {N : Type u_4} [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_3} {N : Type u_4} [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_3} {N : Type u_4} [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_3} {N : Type u_4} [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_3} {N : Type u_4} [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_3} {N : Type u_4} [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_3} {N : Type u_4} [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_3} {N : Type u_4} [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_3) [mul_one_class M] :
Type u_3

The monoid of endomorphisms.

Equations
Instances for monoid.End
source
@[protected, instance]
def monoid.End.monoid (M : Type u_3) [mul_one_class M] :
monoid (monoid.End M)
Equations
source
@[protected, instance]
def monoid.End.inhabited (M : Type u_3) [mul_one_class M] :
inhabited (monoid.End M)
Equations
source
@[protected, instance]
def monoid.End.monoid_hom_class (M : Type u_3) [mul_one_class M] :
monoid_hom_class (monoid.End M) M M
Equations
source
@[simp]
theorem monoid.coe_one (M : Type u_3) [mul_one_class M] :
⇑1 = id
source
@[simp]
theorem monoid.coe_mul (M : Type u_3) [mul_one_class M] (f g : monoid.End M) :
⇑(f * g) = ⇑f ∘ ⇑g
source
@[protected]
def add_monoid.End (A : Type u_9) [add_zero_class A] :
Type u_9

The monoid of endomorphisms.

Equations
Instances for add_monoid.End
source
@[protected, instance]
def add_monoid.End.monoid (A : Type u_9) [add_zero_class A] :
monoid (add_monoid.End A)
Equations
source
@[protected, instance]
def add_monoid.End.inhabited (A : Type u_9) [add_zero_class A] :
inhabited (add_monoid.End A)
Equations
source
@[protected, instance]
def add_monoid.End.add_monoid_hom_class (A : Type u_9) [add_zero_class A] :
add_monoid_hom_class (add_monoid.End A) A A
Equations
source
@[simp]
theorem add_monoid.coe_one (A : Type u_9) [add_zero_class A] :
⇑1 = id
source
@[simp]
theorem add_monoid.coe_mul (A : Type u_9) [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_3} {N : Type u_4} [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_3} {N : Type u_4} [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_3} {N : Type u_4} [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_3} {N : Type u_4} [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_3} {N : Type u_4} [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_3} {N : Type u_4} [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_3} {N : Type u_4} [has_one M] [has_one N] (x : M) :
⇑1 x = 1
source
@[simp]
theorem zero_hom.zero_apply {M : Type u_3} {N : Type u_4} [has_zero M] [has_zero N] (x : M) :
⇑0 x = 0
source
@[simp]
theorem add_monoid_hom.zero_apply {M : Type u_3} {N : Type u_4} [add_zero_class M] [add_zero_class N] (x : M) :
⇑0 x = 0
source
@[simp]
theorem monoid_hom.one_apply {M : Type u_3} {N : Type u_4} [mul_one_class M] [mul_one_class N] (x : M) :
⇑1 x = 1
source
@[simp]
theorem one_hom.one_comp {M : Type u_3} {N : Type u_4} {P : Type u_5} [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_3} {N : Type u_4} {P : Type u_5} [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_3} {N : Type u_4} {P : Type u_5} [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_3} {N : Type u_4} {P : Type u_5} [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_3} {N : Type u_4} [has_one M] [has_one N] :
inhabited (one_hom M N)
Equations
source
@[protected, instance]
def zero_hom.inhabited {M : Type u_3} {N : Type u_4} [has_zero M] [has_zero N] :
inhabited (zero_hom M N)
Equations
source
@[protected, instance]
def add_hom.inhabited {M : Type u_3} {N : Type u_4} [has_add M] [add_zero_class N] :
inhabited (add_hom M N)
Equations
source
@[protected, instance]
def mul_hom.inhabited {M : Type u_3} {N : Type u_4} [has_mul M] [mul_one_class N] :
inhabited (M →ₙ* N)
Equations
source
@[protected, instance]
def add_monoid_hom.inhabited {M : Type u_3} {N : Type u_4} [add_zero_class M] [add_zero_class N] :
inhabited (M →+ N)
Equations
source
@[protected, instance]
def monoid_hom.inhabited {M : Type u_3} {N : Type u_4} [mul_one_class M] [mul_one_class N] :
inhabited (M →* N)
Equations
source
@[protected, instance]
def monoid_with_zero_hom.inhabited {M : Type u_3} [mul_zero_one_class M] :
inhabited (M →*₀ M)
Equations
source
@[protected, instance]
def add_hom.has_add {M : Type u_3} {N : Type u_4} [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_3} {N : Type u_4} [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_3} {N : Type u_4} {P : Type u_5} [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_3} {N : Type u_4} {P : Type u_5} [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_3} {N : Type u_4} {P : Type u_5} [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_3} {N : Type u_4} {P : Type u_5} [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_3} {N : Type u_4} {P : Type u_5} [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_3} {N : Type u_4} {P : Type u_5} [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_3} {N : Type u_4} {P : Type u_5} [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_3} {N : Type u_4} {P : Type u_5} [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_3} {N : Type u_4} {P : Type u_5} [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_3} {N : Type u_4} {P : Type u_5} [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_3} {N : Type u_4} {P : Type u_5} [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_3} {N : Type u_4} {P : Type u_5} [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
@[protected]
theorem add_monoid_hom.map_neg {α : Type u_1} {β : Type u_2} [add_group α] [subtraction_monoid β] (f : α →+ β) (a : α) :
⇑f (-a) = -⇑f a

Additive group homomorphisms preserve negation.

source
@[protected]
theorem monoid_hom.map_inv {α : Type u_1} {β : Type u_2} [group α] [division_monoid β] (f : α →* β) (a : α) :
⇑f a⁻¹ = (⇑f a)⁻¹

Group homomorphisms preserve inverse.

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

Additive group homomorphisms preserve integer scaling.

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

Group homomorphisms preserve integer power.

source
@[protected]
theorem monoid_hom.map_div {α : Type u_1} {β : Type u_2} [group α] [division_monoid β] (f : α →* β) (g h : α) :
⇑f (g / h) = ⇑f g / ⇑f h

Group homomorphisms preserve division.

source
@[protected]
theorem add_monoid_hom.map_sub {α : Type u_1} {β : Type u_2} [add_group α] [subtraction_monoid β] (f : α →+ β) (g h : α) :
⇑f (g - h) = ⇑f g - ⇑f h

Additive group homomorphisms preserve subtraction.

source
@[protected]
theorem add_monoid_hom.map_add_neg {α : Type u_1} {β : Type u_2} [add_group α] [subtraction_monoid β] (f : α →+ β) (g h : α) :
⇑f (g + -h) = ⇑f g + -⇑f h

Additive group homomorphisms preserve subtraction.

source
@[protected]
theorem monoid_hom.map_mul_inv {α : Type u_1} {β : Type u_2} [group α] [division_monoid β] (f : α →* β) (g h : α) :
⇑f (g * h⁻¹) = ⇑f g * (⇑f h)⁻¹

Group homomorphisms preserve division.

source
theorem injective_iff_map_eq_one {F : Type u_8} {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_8} {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_8} {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_8} {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_3} {G : Type u_6} [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_3} {G : Type u_6} [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_3} {G : Type u_6} [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_3} {G : Type u_6} [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_6} [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_6} [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_6} [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_6} [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_6} [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_6} [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_6} [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_6} [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