monoid and group homomorphisms
This file defines the bundled structures for monoid and group homomorphisms. Namely, we define
monoid_hom (resp., add_monoid_hom) to be bundled homomorphisms between multiplicative (resp.,
additive) monoids or groups.
We also define coercion to a function, and usual operations: composition, identity homomorphism, pointwise multiplication and pointwise inversion.
Notations
→*for bundled monoid homs (also use for group homs)→+for bundled add_monoid homs (also use for add_group homs)
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
- to_fun : M → N
- map_zero' : c.to_fun 0 = 0
- map_add' : ∀ (x y : M), c.to_fun (x + y) = c.to_fun x + c.to_fun y
Bundled add_monoid homomorphisms; use this for bundled add_group homomorphisms too.
Equations
- monoid_hom.has_coe_to_fun = {F := λ (x : M →* N), M → N, coe := monoid_hom.to_fun mN}
If f is an additive monoid homomorphism then f 0 = 0.
If f is an additive monoid homomorphism then f (a + b) = f a + f b.
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.
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.
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.
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.
The identity map from an additive monoid to itself.
Composition of additive monoid morphisms as an additive monoid morphism.
The monoid of endomorphisms.
Equations
- monoid.End M = (M →* M)
Equations
- monoid.End.monoid M = {mul := monoid_hom.comp _inst_1, mul_assoc := _, one := monoid_hom.id M _inst_1, one_mul := _, mul_one := _}
Equations
- monoid.End.inhabited M = {default := 1}
Equations
- monoid.End.has_coe_to_fun M = {F := λ (x : monoid.End M), M → M, coe := monoid_hom.to_fun _inst_1}
The monoid of endomorphisms.
Equations
- add_monoid.End A = (A →+ A)
Equations
- add_monoid.End.monoid A = {mul := add_monoid_hom.comp _inst_1, mul_assoc := _, one := add_monoid_hom.id A _inst_1, one_mul := _, mul_one := _}
Equations
- add_monoid.End.inhabited A = {default := 1}
Equations
- add_monoid.End.has_coe_to_fun A = {F := λ (x : add_monoid.End A), A → A, coe := add_monoid_hom.to_fun _inst_1}
0 is the additive monoid homomorphism sending all elements to 0.
Equations
- monoid_hom.inhabited = {default := 1}
Given two monoid morphisms f, g to a commutative monoid, f * g is the monoid morphism
sending x to f x * g x.
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.
(M →* N) is a comm_monoid if N is commutative.
Equations
- monoid_hom.comm_monoid = {mul := has_mul.mul monoid_hom.has_mul, mul_assoc := _, one := 1, one_mul := _, mul_one := _, mul_comm := _}
flip arguments of f : M →+ N →+ P
flip arguments of f : M →* N →* P
Makes an additive group homomomorphism from a proof that the map preserves multiplication.
Makes a group homomomorphism from a proof that the map preserves multiplication.
If f is a monoid homomorphism to a commutative group, then f⁻¹ is the homomorphism sending
x to (f x)⁻¹.
Equations
- monoid_hom.has_inv = {inv := λ (f : M →* G), monoid_hom.mk' (λ (g : M), (⇑f g)⁻¹) _}
If f is an additive monoid homomorphism to an additive commutative group, then -f is the
homomorphism sending x to -(f x).
If G is an additive commutative group, then M →+ G an additive commutative group too.
If G is a commutative group, then M →* G a commutative group too.
Equations
- monoid_hom.comm_group = {mul := comm_monoid.mul monoid_hom.comm_monoid, mul_assoc := _, one := comm_monoid.one monoid_hom.comm_monoid, one_mul := _, mul_one := _, inv := has_inv.inv monoid_hom.has_inv, mul_left_inv := _, mul_comm := _}