mathlib3 documentation

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.

source
@[protected, instance]
def add_monoid_hom.add_comm_monoid {M : Type uM} {N : Type uN} [add_zero_class M] [add_comm_monoid N] :
add_comm_monoid (M →+ N)

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

Equations
source
@[protected, instance]
def monoid_hom.comm_monoid {M : Type uM} {N : Type uN} [mul_one_class M] [comm_monoid N] :
comm_monoid (M →* N)

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

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

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

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

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

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

See also add_monoid.End.nat_cast_def.

source
@[protected, instance]
def add_monoid.End.add_comm_group {M : Type uM} [add_comm_group M] :
add_comm_group (add_monoid.End M)
Equations
source
@[protected, instance]
def add_monoid.End.ring {M : Type uM} [add_comm_group M] :
ring (add_monoid.End M)
Equations
source
@[simp]
theorem add_monoid.End.int_cast_apply {M : Type uM} [add_comm_group M] (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.

source
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
source
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
source
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
source
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
source
@[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
source
@[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
source
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
source
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
source
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
source
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
source
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)⁻¹
source
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
source
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
source
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
source
@[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) :
⇑(⇑monoid_hom.eval y) x = ⇑x y
source
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.

Equations
source
@[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) :
⇑(⇑add_monoid_hom.eval y) x = ⇑x y
source
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
source
@[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)
source
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.

Equations
source
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
source
@[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)
source
@[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) :
⇑(⇑monoid_hom.comp_hom g) hmn = g.comp hmn
source
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
source
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.

Equations
source
@[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) :
⇑(⇑add_monoid_hom.comp_hom g) hmn = g.comp hmn
source
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
source
@[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) :
⇑monoid_hom.flip_hom f = f.flip
source
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
source
@[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) :
⇑add_monoid_hom.flip_hom f = f.flip
source
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_zero_class 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₂

Equations
source
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] [mul_one_class 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
source
@[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] [mul_one_class Q] (f : M →* N →* P) (g : Q →* N) (m : M) (q : Q) :
⇑(⇑(f.compl₂ g) m) q = ⇑(⇑f m) (⇑g q)
source
@[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_zero_class Q] (f : M →+ N →+ P) (g : Q →+ N) (m : M) (q : Q) :
⇑(⇑(f.compl₂ g) m) q = ⇑(⇑f m) (⇑g q)
source
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
source
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₂

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

source
def add_monoid_hom.mul {R : Type u_1} [non_unital_non_assoc_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.

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

Equations
source
theorem add_monoid_hom.mul_apply {R : Type u_1} [non_unital_non_assoc_semiring R] (x y : R) :
⇑(⇑add_monoid_hom.mul x) y = x * y
source
@[simp]
theorem add_monoid_hom.coe_mul {R : Type u_1} [non_unital_non_assoc_semiring R] :
⇑add_monoid_hom.mul = add_monoid_hom.mul_left
source
@[simp]
theorem add_monoid_hom.coe_flip_mul {R : Type u_1} [non_unital_non_assoc_semiring R] :
⇑(add_monoid_hom.mul.flip) = add_monoid_hom.mul_right
source
theorem add_monoid_hom.map_mul_iff {R : Type u_1} {S : Type u_2} [non_unital_non_assoc_semiring R] [non_unital_non_assoc_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.

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

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

Equations
source
def add_monoid.End.mul_right {R : Type u_1} [non_unital_non_assoc_semiring R] :
R →+ add_monoid.End R

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

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