Kernel and range of group homomorphisms #
We define and prove results about the kernel and range of group homomorphisms.
Special thanks goes to Amelia Livingston and Yury Kudryashov for their help and inspiration.
Main definitions #
Notation used here:
G N
areGroup
sx
is an element of typeG
f g : N →* G
are group homomorphisms
Definitions in the file:
MonoidHom.range f
: the range of the group homomorphismf
is a subgroupMonoidHom.ker f
: the kernel of a group homomorphismf
is the subgroup of elementsx : G
such thatf x = 1
MonoidHom.eqLocus f g
: given group homomorphismsf
,g
, the elements ofG
such thatf x = g x
form a subgroup ofG
Implementation notes #
Subgroup inclusion is denoted ≤
rather than ⊆
, although ∈
is defined as
membership of a subgroup's underlying set.
Tags #
subgroup, subgroups
The range of an AddMonoidHom
from an AddGroup
is an AddSubgroup
.
Instances For
Alias of MonoidHom.range_eq_top
.
Alias of MonoidHom.range_eq_top_of_surjective
.
The range of a surjective monoid homomorphism is the whole of the codomain.
Alias of Subgroup.range_subtype
.
Computable alternative to MonoidHom.ofInjective
.
Equations
- MonoidHom.ofLeftInverse h = { toFun := ⇑f.rangeRestrict, invFun := ⇑g ∘ ⇑f.range.subtype, left_inv := h, right_inv := ⋯, map_mul' := ⋯ }
Instances For
Computable alternative to AddMonoidHom.ofInjective
.
Equations
- AddMonoidHom.ofLeftInverse h = { toFun := ⇑f.rangeRestrict, invFun := ⇑g ∘ ⇑f.range.subtype, left_inv := h, right_inv := ⋯, map_add' := ⋯ }
Instances For
The range of an injective group homomorphism is isomorphic to its domain.
Instances For
The range of an injective additive group homomorphism is isomorphic to its domain.
Instances For
The multiplicative kernel of a monoid homomorphism is the subgroup of elements x : G
such that
f x = 1
Equations
- f.ker = { toSubmonoid := MonoidHom.mker f, inv_mem' := ⋯ }
Instances For
The additive kernel of an AddMonoid
homomorphism is the AddSubgroup
of elements
such that f x = 0
Equations
- f.ker = { toAddSubmonoid := AddMonoidHom.mker f, neg_mem' := ⋯ }