This file defines the basic structures for monoid and group homomorphisms, both unbundled (e.g. is_monoid_hom f) and bundled (e.g. monoid_hom M N, a.k.a. M →* N). The unbundled ones are deprecated and the plan is to slowly remove them from mathlib.
monoid_hom, is_monoid_hom (deprecated), is_group_hom (deprecated)
→* for bundled monoid homs (also use for group homs) →+ for bundled add_monoid homs (also use for add_group homs)
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,
Throughout the monoid_hom section 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.
is_group_hom, is_monoid_hom, monoid_hom
Predicate for maps which preserve an addition.
Predicate for maps which preserve a multiplication.
The identity map preserves multiplication.
The identity map preserves addition
The composition of maps which preserve multiplication, also preserves multiplication.
The composition of addition preserving maps also preserves addition
A product of maps which preserve multiplication, preserves multiplication when the target is commutative.
The inverse of a map which preserves multiplication, preserves multiplication when the target is commutative.
Predicate for add_monoid homomorphisms (deprecated -- use the bundled monoid_hom version).
Predicate for monoid homomorphisms (deprecated -- use the bundled monoid_hom version).
A monoid homomorphism preserves multiplication.
A map to a group preserving multiplication is a monoid homomorphism.
The identity map is a monoid homomorphism.
The composite of two monoid homomorphisms is a monoid homomorphism.
Left multiplication in a ring is an additive monoid morphism.
Right multiplication in a ring is an additive monoid morphism.
Predicate for additive group homomorphism (deprecated -- use bundled monoid_hom).
Predicate for group homomorphisms (deprecated -- use bundled monoid_hom).
Construct is_group_hom from its only hypothesis. The default constructor tries to get is_mul_hom from class instances, and this makes some proofs fail.
A group homomorphism is a monoid homomorphism.
A group homomorphism sends 1 to 1.
A group homomorphism sends inverses to inverses.
The identity is a group homomorphism.
The composition of two group homomomorphisms is a group homomorphism.
A group homomorphism is injective iff its kernel is trivial.
The product of group homomorphisms is a group homomorphism if the target is commutative.
The inverse of a group homomorphism is a group homomorphism if the target is commutative.
Inversion is a group homomorphism if the group is commutative.
Additive group homomorphisms commute with subtraction.
The difference of two additive group homomorphisms is an additive group homomorphism if the target is commutative.
Bundled add_monoid homomorphisms; use this for bundled add_group homomorphisms too.
Bundled monoid homomorphisms; use this for bundled group homomorphisms too.
Interpret a map f : M → N as a homomorphism M →* N.
Interpret a map f : M → N as a homomorphism M →+ N.
If f is a monoid homomorphism then f 1 = 1.
If f is a monoid homomorphism then f (a * b) = f a * f b.
The identity map from a monoid to itself.
Composition of monoid morphisms is a monoid morphism.
The product of two monoid morphisms is a monoid morphism if the target is commutative.
(M →* N) is a comm_monoid if N is commutative.
Group homomorphisms preserve inverse.
Group homomorphisms preserve division.
Makes a group homomomorphism from a proof that the map preserves multiplication.
The inverse of a monoid homomorphism is a monoid homomorphism if the target is a commutative group.
(M →* G) is a comm_group if G is a comm_group
Additive group homomorphisms preserve subtraction.