Monoid and group homomorphisms #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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.
This file also defines the lesser-used (and notation-less) homomorphism types which are used as building blocks for other homomorphisms:
Notations #
→+
: Bundledadd_monoid
homs. Also use foradd_group
homs.→*
: Bundledmonoid
homs. Also use forgroup
homs.→*₀
: Bundledmonoid_with_zero
homs. Also use forgroup_with_zero
homs.→ₙ*
: Bundledsemigroup
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
zero_hom M N
is the type of functions M → N
that preserve zero.
When possible, instead of parametrizing results over (f : zero_hom M N)
,
you should parametrize over (F : Type*) [zero_hom_class F M N] (f : F)
.
When you extend this structure, make sure to also extend zero_hom_class
.
Instances for zero_hom
- coe : F → Π (a : M), (λ (_x : M), N) a
- coe_injective' : function.injective zero_hom_class.coe
- map_zero : ∀ (f : F), ⇑f 0 = 0
zero_hom_class F M N
states that F
is a type of zero-preserving homomorphisms.
You should extend this typeclass when you extend zero_hom
.
Instances of this typeclass
Instances of other typeclasses for zero_hom_class
- zero_hom_class.has_sizeof_inst
add_hom M N
is the type of functions M → N
that preserve addition.
When possible, instead of parametrizing results over (f : add_hom M N)
,
you should parametrize over (F : Type*) [add_hom_class F M N] (f : F)
.
When you extend this structure, make sure to extend add_hom_class
.
Instances for add_hom
- coe : F → Π (a : M), (λ (_x : M), N) a
- coe_injective' : function.injective add_hom_class.coe
- map_add : ∀ (f : F) (x y : M), ⇑f (x + y) = ⇑f x + ⇑f y
add_hom_class F M N
states that F
is a type of addition-preserving homomorphisms.
You should declare an instance of this typeclass when you extend add_hom
.
Instances of this typeclass
Instances of other typeclasses for add_hom_class
- add_hom_class.has_sizeof_inst
- to_fun : M → N
- map_zero' : self.to_fun 0 = 0
- map_add' : ∀ (x y : M), self.to_fun (x + y) = self.to_fun x + self.to_fun y
M →+ N
is the type of functions M → N
that preserve the add_zero_class
structure.
add_monoid_hom
is also used for group homomorphisms.
When possible, instead of parametrizing results over (f : M →+ N)
,
you should parametrize over (F : Type*) [add_monoid_hom_class F M N] (f : F)
.
When you extend this structure, make sure to extend add_monoid_hom_class
.
Instances for add_monoid_hom
- add_monoid_hom.has_sizeof_inst
- add_monoid_hom.add_monoid_hom_class
- add_monoid_hom.has_coe_t
- add_monoid_hom.has_coe_to_zero_hom
- add_monoid_hom.has_coe_to_add_hom
- add_monoid_hom.has_coe_to_fun
- add_monoid_hom.has_zero
- add_monoid_hom.inhabited
- add_monoid_hom.has_add
- add_monoid_hom.has_neg
- add_monoid_hom.has_sub
- add_monoid_hom.add_comm_monoid
- add_monoid_hom.add_comm_group
- distrib_mul_action_hom.has_coe
- add_monoid_hom.distrib_mul_action
- add_monoid_hom.smul_comm_class
- add_monoid_hom.is_scalar_tower
- add_monoid_hom.is_central_scalar
- add_monoid_hom.module
- alg_hom.coe_add_monoid_hom
- module.finite.add_monoid_hom
- module.free.add_monoid_hom
- AddMon.bundled_hom
- coe : F → Π (a : M), (λ (_x : M), N) a
- coe_injective' : function.injective add_monoid_hom_class.coe
- map_add : ∀ (f : F) (x y : M), ⇑f (x + y) = ⇑f x + ⇑f y
- map_zero : ∀ (f : F), ⇑f 0 = 0
add_monoid_hom_class F M N
states that F
is a type of add_zero_class
-preserving
homomorphisms.
You should also extend this typeclass when you extend add_monoid_hom
.
Instances of this typeclass
- add_equiv_class.add_monoid_hom_class
- non_unital_ring_hom_class.to_add_monoid_hom_class
- ring_hom_class.to_add_monoid_hom_class
- distrib_mul_action_hom_class.to_add_monoid_hom_class
- semilinear_map_class.add_monoid_hom_class
- add_monoid_hom.add_monoid_hom_class
- add_monoid.End.add_monoid_hom_class
- normed_add_group_hom.add_monoid_hom_class
Instances of other typeclasses for add_monoid_hom_class
- add_monoid_hom_class.has_sizeof_inst
one_hom M N
is the type of functions M → N
that preserve one.
When possible, instead of parametrizing results over (f : one_hom M N)
,
you should parametrize over (F : Type*) [one_hom_class F M N] (f : F)
.
When you extend this structure, make sure to also extend one_hom_class
.
Instances for one_hom
- coe : F → Π (a : M), (λ (_x : M), N) a
- coe_injective' : function.injective one_hom_class.coe
- map_one : ∀ (f : F), ⇑f 1 = 1
one_hom_class F M N
states that F
is a type of one-preserving homomorphisms.
You should extend this typeclass when you extend one_hom
.
Instances of this typeclass
Instances of other typeclasses for one_hom_class
- one_hom_class.has_sizeof_inst
Equations
- one_hom.one_hom_class = {coe := one_hom.to_fun _inst_2, coe_injective' := _, map_one := _}
Equations
- zero_hom.zero_hom_class = {coe := zero_hom.to_fun _inst_2, coe_injective' := _, map_zero := _}
M →ₙ* N
is the type of functions M → N
that preserve multiplication. The ₙ
in the notation
stands for "non-unital" because it is intended to match the notation for non_unital_alg_hom
and
non_unital_ring_hom
, so a mul_hom
is a non-unital monoid hom.
When possible, instead of parametrizing results over (f : M →ₙ* N)
,
you should parametrize over (F : Type*) [mul_hom_class F M N] (f : F)
.
When you extend this structure, make sure to extend mul_hom_class
.
Instances for mul_hom
- coe : F → Π (a : M), (λ (_x : M), N) a
- coe_injective' : function.injective mul_hom_class.coe
- map_mul : ∀ (f : F) (x y : M), ⇑f (x * y) = ⇑f x * ⇑f y
mul_hom_class F M N
states that F
is a type of multiplication-preserving homomorphisms.
You should declare an instance of this typeclass when you extend mul_hom
.
Instances of this typeclass
Instances of other typeclasses for mul_hom_class
- mul_hom_class.has_sizeof_inst
Equations
- add_hom.add_hom_class = {coe := add_hom.to_fun _inst_2, coe_injective' := _, map_add := _}
Equations
- mul_hom.mul_hom_class = {coe := mul_hom.to_fun _inst_2, coe_injective' := _, map_mul := _}
- to_fun : M → N
- map_one' : self.to_fun 1 = 1
- map_mul' : ∀ (x y : M), self.to_fun (x * y) = self.to_fun x * self.to_fun y
M →* N
is the type of functions M → N
that preserve the monoid
structure.
monoid_hom
is also used for group homomorphisms.
When possible, instead of parametrizing results over (f : M →+ N)
,
you should parametrize over (F : Type*) [monoid_hom_class F M N] (f : F)
.
When you extend this structure, make sure to extend monoid_hom_class
.
Instances for monoid_hom
- monoid_hom.has_sizeof_inst
- monoid_hom.monoid_hom_class
- monoid_hom.has_coe_t
- monoid_hom.has_coe_to_one_hom
- monoid_hom.has_coe_to_mul_hom
- monoid_with_zero_hom.has_coe_to_monoid_hom
- monoid_hom.has_coe_to_fun
- monoid_hom.has_one
- monoid_hom.inhabited
- monoid_hom.has_mul
- monoid_hom.has_inv
- monoid_hom.has_div
- ring_hom.has_coe_monoid_hom
- monoid_hom.comm_monoid
- monoid_hom.comm_group
- alg_hom.coe_monoid_hom
- Mon.bundled_hom
- coe : F → Π (a : M), (λ (_x : M), N) a
- coe_injective' : function.injective monoid_hom_class.coe
- map_mul : ∀ (f : F) (x y : M), ⇑f (x * y) = ⇑f x * ⇑f y
- map_one : ∀ (f : F), ⇑f 1 = 1
monoid_hom_class F M N
states that F
is a type of monoid
-preserving homomorphisms.
You should also extend this typeclass when you extend monoid_hom
.
Instances of this typeclass
Instances of other typeclasses for monoid_hom_class
- monoid_hom_class.has_sizeof_inst
Equations
- add_monoid_hom.add_monoid_hom_class = {coe := add_monoid_hom.to_fun _inst_2, coe_injective' := _, map_add := _, map_zero := _}
Equations
- monoid_hom.monoid_hom_class = {coe := monoid_hom.to_fun _inst_2, coe_injective' := _, map_mul := _, map_one := _}
- to_fun : M → N
- map_zero' : self.to_fun 0 = 0
- map_one' : self.to_fun 1 = 1
- map_mul' : ∀ (x y : M), self.to_fun (x * y) = self.to_fun x * self.to_fun y
M →*₀ N
is the type of functions M → N
that preserve
the monoid_with_zero
structure.
monoid_with_zero_hom
is also used for group homomorphisms.
When possible, instead of parametrizing results over (f : M →*₀ N)
,
you should parametrize over (F : Type*) [monoid_with_zero_hom_class F M N] (f : F)
.
When you extend this structure, make sure to extend monoid_with_zero_hom_class
.
Instances for monoid_with_zero_hom
- coe : F → Π (a : M), (λ (_x : M), N) a
- coe_injective' : function.injective monoid_with_zero_hom_class.coe
- map_mul : ∀ (f : F) (x y : M), ⇑f (x * y) = ⇑f x * ⇑f y
- map_one : ∀ (f : F), ⇑f 1 = 1
- map_zero : ∀ (f : F), ⇑f 0 = 0
monoid_with_zero_hom_class F M N
states that F
is a type of
monoid_with_zero
-preserving homomorphisms.
You should also extend this typeclass when you extend monoid_with_zero_hom
.
Instances of this typeclass
Instances of other typeclasses for monoid_with_zero_hom_class
- monoid_with_zero_hom_class.has_sizeof_inst
Equations
- monoid_with_zero_hom.monoid_with_zero_hom_class = {coe := monoid_with_zero_hom.to_fun _inst_2, coe_injective' := _, map_mul := _, map_one := _, map_zero := _}
Bundled morphisms can be down-cast to weaker bundlings
Equations
Equations
Equations
Equations
Equations
The simp-normal form of morphism coercion is f.to_..._hom
. This choice is primarily because
this is the way things were before the above coercions were introduced. Bundled morphisms defined
elsewhere in Mathlib may choose ↑f
as their simp-normal form instead.
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Deprecated: use fun_like.congr_fun
instead.
Deprecated: use fun_like.congr_fun
instead.
Deprecated: use fun_like.congr_fun
instead.
Deprecated: use fun_like.congr_arg
instead.
Deprecated: use fun_like.congr_arg
instead.
Deprecated: use fun_like.congr_arg
instead.
Deprecated: use fun_like.coe_injective
instead.
Deprecated: use fun_like.coe_injective
instead.
Deprecated: use fun_like.coe_injective
instead.
Deprecated: use fun_like.ext_iff
instead.
Deprecated: use fun_like.ext_iff
instead.
Deprecated: use fun_like.ext_iff
instead.
Copy of an add_monoid_hom
with a new to_fun
equal to the old one. Useful to fix
definitional equalities.
Copy of a monoid_hom
with a new to_fun
equal to the old one. Useful to fix
definitional equalities.
Copy of a monoid_hom
with a new to_fun
equal to the old one. Useful to fix
definitional equalities.
If f
is an additive monoid homomorphism then f 0 = 0
.
If f
is a monoid homomorphism then f 1 = 1
.
If f
is a monoid homomorphism then f (a * b) = f a * f b
.
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
.
Negation on a commutative additive group, considered as an additive monoid homomorphism.
Equations
- neg_add_monoid_hom = {to_fun := has_neg.neg (sub_neg_monoid.to_has_neg α), map_zero' := _, map_add' := _}
Inversion on a commutative group, considered as a monoid homomorphism.
Equations
- inv_monoid_hom = {to_fun := has_inv.inv (div_inv_monoid.to_has_inv α), map_one' := _, map_mul' := _}
The identity map from an type with zero to itself.
Equations
- zero_hom.id M = {to_fun := λ (x : M), x, map_zero' := _}
The identity map from a type with 1 to itself.
Equations
- one_hom.id M = {to_fun := λ (x : M), x, map_one' := _}
The identity map from a type with multiplication to itself.
Equations
- mul_hom.id M = {to_fun := λ (x : M), x, map_mul' := _}
The identity map from an type with addition to itself.
Equations
- add_hom.id M = {to_fun := λ (x : M), x, map_add' := _}
The identity map from a monoid to itself.
The identity map from an additive monoid to itself.
The identity map from a monoid_with_zero to itself.
Composition of monoid morphisms as a monoid morphism.
Composition of additive monoid morphisms as an additive monoid morphism.
Composition of monoid_with_zero_hom
s as a monoid_with_zero_hom
.
The monoid of endomorphisms.
Equations
- monoid.End M = (M →* M)
Instances for monoid.End
Equations
- monoid.End.monoid M = {mul := monoid_hom.comp _inst_1, mul_assoc := _, one := monoid_hom.id M _inst_1, one_mul := _, mul_one := _, npow := npow_rec (mul_one_class.to_has_mul (monoid.End M)), npow_zero' := _, npow_succ' := _}
Equations
- monoid.End.inhabited M = {default := 1}
Equations
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 := _, npow := npow_rec (mul_one_class.to_has_mul (add_monoid.End A)), npow_zero' := _, npow_succ' := _}
Equations
- add_monoid.End.inhabited A = {default := 1}
1
is the multiplicative homomorphism sending all elements to 1
.
0
is the additive homomorphism sending all elements to 0
.
1
is the monoid homomorphism sending all elements to 1
.
0
is the additive monoid homomorphism sending all elements to 0
.
Equations
- add_hom.inhabited = {default := 0}
Equations
- mul_hom.inhabited = {default := 1}
Equations
Equations
- monoid_hom.inhabited = {default := 1}
Equations
- monoid_with_zero_hom.inhabited = {default := monoid_with_zero_hom.id M _inst_1}
Given two additive morphisms f
, g
to an additive commutative semigroup, f + g
is the
additive morphism sending x
to f x + g x
.
Given two mul morphisms f
, g
to a commutative semigroup, f * g
is the mul morphism
sending x
to f x * g x
.
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
.
A homomorphism from a group to a monoid is injective iff its kernel is trivial.
For the iff statement on the triviality of the kernel, see injective_iff_map_eq_one'
.
A homomorphism from an additive group to an additive monoid is injective iff
its kernel is trivial. For the iff statement on the triviality of the kernel,
see injective_iff_map_eq_zero'
.
A homomorphism from an additive group to an additive monoid is injective iff its
kernel is trivial, stated as an iff on the triviality of the kernel. For the implication, see
injective_iff_map_eq_zero
.
A homomorphism from a group to a monoid is injective iff its kernel is trivial,
stated as an iff on the triviality of the kernel.
For the implication, see injective_iff_map_eq_one
.
Makes an additive group homomorphism from a proof that the map preserves
the operation λ a b, a + -b
. See also add_monoid_hom.of_map_sub
for a version using
λ a b, a - b
.
Equations
- add_monoid_hom.of_map_add_neg f map_div = add_monoid_hom.mk' f _
Makes a group homomorphism from a proof that the map preserves right division λ x y, x * y⁻¹
.
See also monoid_hom.of_map_div
for a version using λ x y, x / y
.
Equations
- monoid_hom.of_map_mul_inv f map_div = monoid_hom.mk' f _
If f
is an additive monoid homomorphism to an additive commutative group, then -f
is the
homomorphism sending x
to -(f x)
.
Equations
- add_monoid_hom.has_neg = {neg := λ (f : M →+ G), add_monoid_hom.mk' (λ (g : M), -⇑f g) _}
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
and g
are monoid homomorphisms to an additive commutative group, then f - g
is the homomorphism sending x
to (f x) - (g x)
.
Equations
- add_monoid_hom.has_sub = {sub := λ (f g : M →+ G), add_monoid_hom.mk' (λ (x : M), ⇑f x - ⇑g x) _}
If f
and g
are monoid homomorphisms to a commutative group, then f / g
is the homomorphism
sending x
to (f x) / (g x)
.
Equations
- monoid_hom.has_div = {div := λ (f g : M →* G), monoid_hom.mk' (λ (x : M), ⇑f x / ⇑g x) _}
Given two monoid with zero morphisms f
, g
to a commutative monoid, f * g
is the monoid
with zero morphism sending x
to f x * g x
.