mathlib documentation

algebra.group.hom_instances

Instances on spaces of monoid and group morphisms #

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.

theorem nat.succ_eq_one_add (n : ) :
n.succ = 1 + n
@[instance]
def monoid_hom.comm_monoid {M : Type uM} {N : Type uN} [mul_one_class M] [comm_monoid N] :

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

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

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

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

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

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

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

Equations

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

@[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
@[simp]
theorem monoid_hom.eval_apply_apply {M : Type uM} {N : Type uN} [mul_one_class M] [comm_monoid N] (y : M) (x : M →* N) :
def add_monoid_hom.eval {M : Type uM} {N : Type uN} [add_zero_class M] [add_comm_monoid N] :
M →+ (M →+ N) →+ N

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

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

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

Equations
@[simp]
theorem add_monoid_hom.comp_hom'_apply_apply {M : Type uM} {N : Type uN} {P : Type uP} [add_zero_class M] [add_zero_class N] [add_comm_monoid P] (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} [add_zero_class M] [add_zero_class N] [add_comm_monoid P] (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.

def monoid_hom.comp_hom' {M : Type uM} {N : Type uN} {P : Type uP} [mul_one_class M] [mul_one_class N] [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} [mul_one_class M] [mul_one_class N] [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} [mul_one_class M] [comm_monoid N] [comm_monoid P] (g : N →* P) (hmn : M →* N) :
def monoid_hom.comp_hom {M : Type uM} {N : Type uN} {P : Type uP} [mul_one_class M] [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} [add_zero_class M] [add_comm_monoid N] [add_comm_monoid P] :
(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.

@[simp]
theorem add_monoid_hom.comp_hom_apply_apply {M : Type uM} {N : Type uN} {P : Type uP} [add_zero_class M] [add_comm_monoid N] [add_comm_monoid P] (g : N →+ P) (hmn : M →+ N) :
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.

@[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} [add_zero_class M] [add_zero_class N] [add_comm_monoid P] [add_comm_monoid Q] (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₂

def monoid_hom.compl₂ {M : Type uM} {N : Type uN} {P : Type uP} {Q : Type uQ} [mul_one_class M] [mul_one_class N] [comm_monoid P] [comm_monoid Q] (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} [mul_one_class M] [mul_one_class N] [comm_monoid P] [comm_monoid Q] (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} [add_zero_class M] [add_zero_class N] [add_comm_monoid P] [add_comm_monoid Q] (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} [mul_one_class M] [mul_one_class N] [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} [add_zero_class M] [add_zero_class N] [add_comm_monoid P] [add_comm_monoid Q] (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₂

@[simp]
theorem monoid_hom.compr₂_apply {M : Type uM} {N : Type uN} {P : Type uP} {Q : Type uQ} [mul_one_class M] [mul_one_class N] [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} [add_zero_class M] [add_zero_class N] [add_comm_monoid P] [add_comm_monoid Q] (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} [semiring R] :
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.

A stronger version of this exists for algebras as algebra.lmul.

Equations
theorem add_monoid_hom.mul_apply {R : Type u_1} [semiring R] (x y : R) :
theorem add_monoid_hom.map_mul_iff {R : Type u_1} {S : Type u_2} [semiring R] [semiring S] (f : R →+ S) :
(∀ (x y : R), f (x * y) = (f x) * f y) add_monoid_hom.mul.compr₂ f = (add_monoid_hom.mul.comp f).compl₂ f

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.