# mathlib3documentation

algebra.hom.group_instances

# Instances on spaces of monoid and group morphisms #

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

We endow the space of monoid morphisms M →* N with a comm_monoid structure when the target is commutative, through pointwise multiplication, and with a comm_group structure when the target is a commutative group. We also prove the same instances for additive situations.

Since these structures permit morphisms of morphisms, we also provide some composition-like operations.

Finally, we provide the ring structure on add_monoid.End.

@[protected, instance]
def add_monoid_hom.add_comm_monoid {M : Type uM} {N : Type uN}  :

(M →+ N) is an add_comm_monoid if N is commutative.

Equations
@[protected, instance]
def monoid_hom.comm_monoid {M : Type uM} {N : Type uN} [comm_monoid N] :

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

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

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

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

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

Equations
@[protected, instance]
Equations
@[protected, instance]
def add_monoid.End.semiring {M : Type uM}  :
Equations
@[simp]
theorem add_monoid.End.nat_cast_apply {M : Type uM} (n : ) (m : M) :
n m = n m

See also add_monoid.End.nat_cast_def.

@[protected, instance]
Equations
@[protected, instance]
def add_monoid.End.ring {M : Type uM}  :
Equations
@[simp]
theorem add_monoid.End.int_cast_apply {M : Type uM} (z : ) (m : M) :
z m = z m

See also add_monoid.End.int_cast_def.

### Morphisms of morphisms #

The structures above permit morphisms that themselves produce morphisms, provided the codomain is commutative.

theorem monoid_hom.ext_iff₂ {M : Type uM} {N : Type uN} {P : Type uP} {mM : mul_one_class M} {mN : mul_one_class N} {mP : comm_monoid P} {f g : M →* N →* P} :
f = g (x : M) (y : N), (f x) y = (g x) y
theorem add_monoid_hom.ext_iff₂ {M : Type uM} {N : Type uN} {P : Type uP} {mM : add_zero_class M} {mN : add_zero_class N} {mP : add_comm_monoid P} {f g : M →+ N →+ P} :
f = g (x : M) (y : N), (f x) y = (g x) y
def monoid_hom.flip {M : Type uM} {N : Type uN} {P : Type uP} {mM : mul_one_class M} {mN : mul_one_class N} {mP : comm_monoid P} (f : M →* N →* P) :
N →* M →* P

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

Equations
def add_monoid_hom.flip {M : Type uM} {N : Type uN} {P : Type uP} {mM : add_zero_class M} {mN : add_zero_class N} {mP : add_comm_monoid P} (f : M →+ N →+ P) :
N →+ M →+ P

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

Equations
@[simp]
theorem monoid_hom.flip_apply {M : Type uM} {N : Type uN} {P : Type uP} {mM : mul_one_class M} {mN : mul_one_class N} {mP : comm_monoid P} (f : M →* N →* P) (x : M) (y : N) :
((f.flip) y) x = (f x) y
@[simp]
theorem add_monoid_hom.flip_apply {M : Type uM} {N : Type uN} {P : Type uP} {mM : add_zero_class M} {mN : add_zero_class N} {mP : add_comm_monoid P} (f : M →+ N →+ P) (x : M) (y : N) :
((f.flip) y) x = (f x) y
theorem add_monoid_hom.map_one₂ {M : Type uM} {N : Type uN} {P : Type uP} {mM : add_zero_class M} {mN : add_zero_class N} {mP : add_comm_monoid P} (f : M →+ N →+ P) (n : N) :
(f 0) n = 0
theorem monoid_hom.map_one₂ {M : Type uM} {N : Type uN} {P : Type uP} {mM : mul_one_class M} {mN : mul_one_class N} {mP : comm_monoid P} (f : M →* N →* P) (n : N) :
(f 1) n = 1
theorem add_monoid_hom.map_mul₂ {M : Type uM} {N : Type uN} {P : Type uP} {mM : add_zero_class M} {mN : add_zero_class N} {mP : add_comm_monoid P} (f : M →+ N →+ P) (m₁ m₂ : M) (n : N) :
(f (m₁ + m₂)) n = (f m₁) n + (f m₂) n
theorem monoid_hom.map_mul₂ {M : Type uM} {N : Type uN} {P : Type uP} {mM : mul_one_class M} {mN : mul_one_class N} {mP : comm_monoid P} (f : M →* N →* P) (m₁ m₂ : M) (n : N) :
(f (m₁ * m₂)) n = (f m₁) n * (f m₂) n
theorem monoid_hom.map_inv₂ {M : Type uM} {N : Type uN} {P : Type uP} {mM : group M} {mN : mul_one_class N} {mP : comm_group P} (f : M →* N →* P) (m : M) (n : N) :
(f m⁻¹) n = ((f m) n)⁻¹
theorem add_monoid_hom.map_inv₂ {M : Type uM} {N : Type uN} {P : Type uP} {mM : add_group M} {mN : add_zero_class N} {mP : add_comm_group P} (f : M →+ N →+ P) (m : M) (n : N) :
(f (-m)) n = -(f m) n
theorem monoid_hom.map_div₂ {M : Type uM} {N : Type uN} {P : Type uP} {mM : group M} {mN : mul_one_class N} {mP : comm_group P} (f : M →* N →* P) (m₁ m₂ : M) (n : N) :
(f (m₁ / m₂)) n = (f m₁) n / (f m₂) n
theorem add_monoid_hom.map_div₂ {M : Type uM} {N : Type uN} {P : Type uP} {mM : add_group M} {mN : add_zero_class N} {mP : add_comm_group P} (f : M →+ N →+ P) (m₁ m₂ : M) (n : N) :
(f (m₁ - m₂)) n = (f m₁) n - (f m₂) n
@[simp]
theorem monoid_hom.eval_apply_apply {M : Type uM} {N : Type uN} [comm_monoid N] (y : M) (x : M →* N) :
x = x y
def add_monoid_hom.eval {M : Type uM} {N : Type uN}  :
M →+ (M →+ N) →+ N

Evaluation of an add_monoid_hom at a point as an additive monoid homomorphism. See also add_monoid_hom.apply for the evaluation of any function at a point.

Equations
@[simp]
theorem add_monoid_hom.eval_apply_apply {M : Type uM} {N : Type uN} (y : M) (x : M →+ N) :
= x y
def monoid_hom.eval {M : Type uM} {N : Type uN} [comm_monoid N] :
M →* (M →* N) →* N

Evaluation of a monoid_hom at a point as a monoid homomorphism. See also monoid_hom.apply for the evaluation of any function at a point.

Equations
@[simp]
theorem add_monoid_hom.comp_hom'_apply_apply {M : Type uM} {N : Type uN} {P : Type uP} (f : M →+ N) (y : N →+ P) (x : M) :
((f.comp_hom') y) x = y (f x)
def add_monoid_hom.comp_hom' {M : Type uM} {N : Type uN} {P : Type uP} (f : M →+ N) :
(N →+ P) →+ M →+ P

The expression λ g m, g (f m) as a add_monoid_hom. Equivalently, (λ g, monoid_hom.comp g f) as a add_monoid_hom.

This also exists in a linear_map version, linear_map.lcomp.

Equations
def monoid_hom.comp_hom' {M : Type uM} {N : Type uN} {P : Type uP} [comm_monoid P] (f : M →* N) :
(N →* P) →* M →* P

The expression λ g m, g (f m) as a monoid_hom. Equivalently, (λ g, monoid_hom.comp g f) as a monoid_hom.

Equations
@[simp]
theorem monoid_hom.comp_hom'_apply_apply {M : Type uM} {N : Type uN} {P : Type uP} [comm_monoid P] (f : M →* N) (y : N →* P) (x : M) :
((f.comp_hom') y) x = y (f x)
@[simp]
theorem monoid_hom.comp_hom_apply_apply {M : Type uM} {N : Type uN} {P : Type uP} [comm_monoid N] [comm_monoid P] (g : N →* P) (hmn : M →* N) :
hmn = g.comp hmn
def monoid_hom.comp_hom {M : Type uM} {N : Type uN} {P : Type uP} [comm_monoid N] [comm_monoid P] :
(N →* P) →* (M →* N) →* M →* P

Composition of monoid morphisms (monoid_hom.comp) as a monoid morphism.

Note that unlike monoid_hom.comp_hom' this requires commutativity of N.

Equations
def add_monoid_hom.comp_hom {M : Type uM} {N : Type uN} {P : Type uP}  :
(N →+ P) →+ (M →+ N) →+ M →+ P

Composition of additive monoid morphisms (add_monoid_hom.comp) as an additive monoid morphism.

Note that unlike add_monoid_hom.comp_hom' this requires commutativity of N.

This also exists in a linear_map version, linear_map.llcomp.

Equations
@[simp]
theorem add_monoid_hom.comp_hom_apply_apply {M : Type uM} {N : Type uN} {P : Type uP} (g : N →+ P) (hmn : M →+ N) :
hmn = g.comp hmn
def add_monoid_hom.flip_hom {M : Type uM} {N : Type uN} {P : Type uP} {mM : add_zero_class M} {mN : add_zero_class N} {mP : add_comm_monoid P} :
(M →+ N →+ P) →+ N →+ M →+ P

Flipping arguments of additive monoid morphisms (add_monoid_hom.flip) as an additive monoid morphism.

Equations
@[simp]
theorem monoid_hom.flip_hom_apply {M : Type uM} {N : Type uN} {P : Type uP} {mM : mul_one_class M} {mN : mul_one_class N} {mP : comm_monoid P} (f : M →* N →* P) :
def monoid_hom.flip_hom {M : Type uM} {N : Type uN} {P : Type uP} {mM : mul_one_class M} {mN : mul_one_class N} {mP : comm_monoid P} :
(M →* N →* P) →* N →* M →* P

Flipping arguments of monoid morphisms (monoid_hom.flip) as a monoid morphism.

Equations
@[simp]
theorem add_monoid_hom.flip_hom_apply {M : Type uM} {N : Type uN} {P : Type uP} {mM : add_zero_class M} {mN : add_zero_class N} {mP : add_comm_monoid P} (f : M →+ N →+ P) :
def add_monoid_hom.compl₂ {M : Type uM} {N : Type uN} {P : Type uP} {Q : Type uQ} (f : M →+ N →+ P) (g : Q →+ N) :
M →+ Q →+ P

The expression λ m q, f m (g q) as an add_monoid_hom.

Note that the expression λ q n, f (g q) n is simply add_monoid_hom.comp.

This also exists as a linear_map version, linear_map.compl₂

Equations
def monoid_hom.compl₂ {M : Type uM} {N : Type uN} {P : Type uP} {Q : Type uQ} [comm_monoid P] (f : M →* N →* P) (g : Q →* N) :
M →* Q →* P

The expression λ m q, f m (g q) as a monoid_hom.

Note that the expression λ q n, f (g q) n is simply monoid_hom.comp.

Equations
@[simp]
theorem monoid_hom.compl₂_apply {M : Type uM} {N : Type uN} {P : Type uP} {Q : Type uQ} [comm_monoid P] (f : M →* N →* P) (g : Q →* N) (m : M) (q : Q) :
((f.compl₂ g) m) q = (f m) (g q)
@[simp]
theorem add_monoid_hom.compl₂_apply {M : Type uM} {N : Type uN} {P : Type uP} {Q : Type uQ} (f : M →+ N →+ P) (g : Q →+ N) (m : M) (q : Q) :
((f.compl₂ g) m) q = (f m) (g q)
def monoid_hom.compr₂ {M : Type uM} {N : Type uN} {P : Type uP} {Q : Type uQ} [comm_monoid P] [comm_monoid Q] (f : M →* N →* P) (g : P →* Q) :
M →* N →* Q

The expression λ m n, g (f m n) as a monoid_hom.

Equations
def add_monoid_hom.compr₂ {M : Type uM} {N : Type uN} {P : Type uP} {Q : Type uQ} (f : M →+ N →+ P) (g : P →+ Q) :
M →+ N →+ Q

The expression λ m n, g (f m n) as an add_monoid_hom.

This also exists as a linear_map version, linear_map.compr₂

Equations
@[simp]
theorem monoid_hom.compr₂_apply {M : Type uM} {N : Type uN} {P : Type uP} {Q : Type uQ} [comm_monoid P] [comm_monoid Q] (f : M →* N →* P) (g : P →* Q) (m : M) (n : N) :
((f.compr₂ g) m) n = g ((f m) n)
@[simp]
theorem add_monoid_hom.compr₂_apply {M : Type uM} {N : Type uN} {P : Type uP} {Q : Type uQ} (f : M →+ N →+ P) (g : P →+ Q) (m : M) (n : N) :
((f.compr₂ g) m) n = g ((f m) n)

### Miscellaneous definitions #

Due to the fact this file imports algebra.group_power.basic, it is not possible to import it in some of the lower-level files like algebra.ring.basic. The following lemmas should be rehomed if the import structure permits them to be.

def add_monoid_hom.mul {R : Type u_1}  :
R →+ R →+ R

Multiplication of an element of a (semi)ring is an add_monoid_hom in both arguments.

This is a more-strongly bundled version of add_monoid_hom.mul_left and add_monoid_hom.mul_right.

Stronger versions of this exists for algebras as linear_map.mul, non_unital_alg_hom.mul and algebra.lmul.

Equations
theorem add_monoid_hom.mul_apply {R : Type u_1} (x y : R) :
y = x * y
@[simp]
@[simp]
theorem add_monoid_hom.coe_flip_mul {R : Type u_1}  :
theorem add_monoid_hom.map_mul_iff {R : Type u_1} {S : Type u_2} (f : R →+ S) :
( (x y : R), f (x * y) = f x * f y)

An add_monoid_hom preserves multiplication if pre- and post- composition with add_monoid_hom.mul are equivalent. By converting the statement into an equality of add_monoid_homs, this lemma allows various specialized ext lemmas about →+ to then be applied.

@[simp]
theorem add_monoid.End.mul_left_apply_apply {R : Type u_1} (r ᾰ : R) :
= r *
def add_monoid.End.mul_left {R : Type u_1}  :

The left multiplication map: (a, b) ↦ a * b. See also add_monoid_hom.mul_left.

Equations
def add_monoid.End.mul_right {R : Type u_1}  :

The right multiplication map: (a, b) ↦ b * a. See also add_monoid_hom.mul_right.

Equations
@[simp]
theorem add_monoid.End.mul_right_apply_apply {R : Type u_1} (y x : R) :
= x * y