map
and comap
for subgroups #
We prove results about images and preimages of subgroups under group homomorphisms. The bundled subgroups use bundled monoid homomorphisms.
Special thanks goes to Amelia Livingston and Yury Kudryashov for their help and inspiration.
Main definitions #
Notation used here:
G N
areGroup
sH
is aSubgroup
ofG
x
is an element of typeG
or typeA
f g : N →* G
are group homomorphismss k
are sets of elements of typeG
Definitions in the file:
Subgroup.comap H f
: the preimage of a subgroupH
along the group homomorphismf
is also a subgroupSubgroup.map f H
: the image of a subgroupH
along the group homomorphismf
is also a subgroup
Implementation notes #
Subgroup inclusion is denoted ≤
rather than ⊆
, although ∈
is defined as
membership of a subgroup's underlying set.
Tags #
subgroup, subgroups
The preimage of an AddSubgroup
along an AddMonoid
homomorphism
is an AddSubgroup
.
Equations
- AddSubgroup.comap f H = { carrier := ⇑f ⁻¹' ↑H, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯ }
The image of an AddSubgroup
along an AddMonoid
homomorphism
is an AddSubgroup
.
Equations
- AddSubgroup.map f H = { carrier := ⇑f '' ↑H, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯ }
For any subgroups H
and K
, view H ⊓ K
as a subgroup of K
.
Equations
- H.subgroupOf K = Subgroup.comap K.subtype H
For any subgroups H
and K
, view H ⊓ K
as a subgroup of K
.
Equations
- H.addSubgroupOf K = AddSubgroup.comap K.subtype H
If H ≤ K
, then H
as a subgroup of K
is isomorphic to H
.
Equations
- Subgroup.subgroupOfEquivOfLe h = { toFun := fun (g : ↥(H.subgroupOf K)) => ⟨↑↑g, ⋯⟩, invFun := fun (g : ↥H) => ⟨⟨↑g, ⋯⟩, ⋯⟩, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ }
If H ≤ K
, then H
as a subgroup of K
is isomorphic to H
.
Equations
- AddSubgroup.addSubgroupOfEquivOfLe h = { toFun := fun (g : ↥(H.addSubgroupOf K)) => ⟨↑↑g, ⋯⟩, invFun := fun (g : ↥H) => ⟨⟨↑g, ⋯⟩, ⋯⟩, left_inv := ⋯, right_inv := ⋯, map_add' := ⋯ }
An isomorphism of groups gives an order isomorphism between the lattices of subgroups, defined by sending subgroups to their inverse images.
See also MulEquiv.mapSubgroup
which maps subgroups to their forward images.
Equations
- f.comapSubgroup = { toFun := Subgroup.comap ↑f, invFun := Subgroup.comap ↑f.symm, left_inv := ⋯, right_inv := ⋯, map_rel_iff' := ⋯ }
An isomorphism of groups gives an order isomorphism between the lattices of subgroups, defined by sending subgroups to their forward images.
See also MulEquiv.comapSubgroup
which maps subgroups to their inverse images.
Equations
- f.mapSubgroup = { toFun := Subgroup.map ↑f, invFun := Subgroup.map ↑f.symm, left_inv := ⋯, right_inv := ⋯, map_rel_iff' := ⋯ }
A subgroup is isomorphic to its image under an injective function. If you have an isomorphism,
use MulEquiv.subgroupMap
for better definitional equalities.
Equations
- H.equivMapOfInjective f hf = { toEquiv := Equiv.Set.image (⇑f) (↑H) hf, map_mul' := ⋯ }
An additive subgroup is isomorphic to its image under an injective function. If you
have an isomorphism, use AddEquiv.addSubgroupMap
for better definitional equalities.
Equations
- H.equivMapOfInjective f hf = { toEquiv := Equiv.Set.image (⇑f) (↑H) hf, map_add' := ⋯ }
The MonoidHom
from the preimage of a subgroup to itself.
Equations
- f.subgroupComap H' = f.submonoidComap H'.toSubmonoid
the AddMonoidHom
from the preimage of an
additive subgroup to itself.
Equations
- f.addSubgroupComap H' = f.addSubmonoidComap H'.toAddSubmonoid
The MonoidHom
from a subgroup to its image.
Equations
- f.subgroupMap H = f.submonoidMap H.toSubmonoid
the AddMonoidHom
from an additive subgroup to its image
Equations
- f.addSubgroupMap H = f.addSubmonoidMap H.toAddSubmonoid
Makes the identity isomorphism from a proof two subgroups of a multiplicative group are equal.
Equations
- MulEquiv.subgroupCongr h = { toEquiv := Equiv.setCongr ⋯, map_mul' := ⋯ }
Makes the identity additive isomorphism from a proof two subgroups of an additive group are equal.
Equations
- AddEquiv.addSubgroupCongr h = { toEquiv := Equiv.setCongr ⋯, map_add' := ⋯ }
A subgroup is isomorphic to its image under an isomorphism. If you only have an injective map,
use Subgroup.equiv_map_of_injective
.
Equations
- e.subgroupMap H = e.submonoidMap H.toSubmonoid
An additive subgroup is isomorphic to its image under an isomorphism. If you only
have an injective map, use AddSubgroup.equiv_map_of_injective
.
Equations
- e.addSubgroupMap H = e.addSubmonoidMap H.toAddSubmonoid
The image under an AddMonoid
hom of the AddSubgroup
generated by a set equals
the AddSubgroup
generated by the image of the set.