Quotients of groups by normal subgroups #
This file defines the group structure on the quotient by a normal subgroup.
Main definitions #
QuotientGroup.Quotient.Group
: the group structure onG/N
given a normal subgroupN
ofG
.mk'
: the canonical group homomorphismG →* G/N
given a normal subgroupN
ofG
.lift φ
: the group homomorphismG/N →* H
given a group homomorphismφ : G →* H
such thatN ⊆ ker φ
.map f
: the group homomorphismG/N →* H/M
given a group homomorphismf : G →* H
such thatN ⊆ f⁻¹(M)
.
Tags #
quotient groups
The additive congruence relation generated by a normal additive subgroup.
Equations
- QuotientAddGroup.con N = { toSetoid := QuotientAddGroup.leftRel N, add' := ⋯ }
Instances For
The congruence relation generated by a normal subgroup.
Equations
- QuotientGroup.con N = { toSetoid := QuotientGroup.leftRel N, mul' := ⋯ }
Instances For
Equations
- QuotientAddGroup.Quotient.addGroup N = (QuotientAddGroup.con N).addGroup
Equations
- QuotientGroup.Quotient.group N = (QuotientGroup.con N).group
The additive group homomorphism from G
to G/N
.
Equations
- QuotientAddGroup.mk' N = AddMonoidHom.mk' QuotientAddGroup.mk ⋯
Instances For
The group homomorphism from G
to G/N
.
Equations
- QuotientGroup.mk' N = MonoidHom.mk' QuotientGroup.mk ⋯
Instances For
Two AddMonoidHom
s from an additive quotient group are equal if
their compositions with AddQuotientGroup.mk'
are equal.
See note [partially-applied ext lemmas].
Two MonoidHom
s from a quotient group are equal if their compositions with
QuotientGroup.mk'
are equal.
See note [partially-applied ext lemmas].
Equations
Equations
An AddGroup
homomorphism φ : G →+ M
with N ⊆ ker(φ)
descends (i.e. lift
s)
to a group homomorphism G/N →* M
.
Equations
- QuotientAddGroup.lift N φ HN = (QuotientAddGroup.con N).lift φ ⋯
Instances For
A group homomorphism φ : G →* M
with N ⊆ ker(φ)
descends (i.e. lift
s) to a
group homomorphism G/N →* M
.
Equations
- QuotientGroup.lift N φ HN = (QuotientGroup.con N).lift φ ⋯
Instances For
An AddGroup
homomorphism f : G →+ H
induces a map G/N →+ H/M
if N ⊆ f⁻¹(M)
.
Equations
- QuotientAddGroup.map N M f h = QuotientAddGroup.lift N ((QuotientAddGroup.mk' M).comp f) ⋯
Instances For
A group homomorphism f : G →* H
induces a map G/N →* H/M
if N ⊆ f⁻¹(M)
.
Equations
- QuotientGroup.map N M f h = QuotientGroup.lift N ((QuotientGroup.mk' M).comp f) ⋯
Instances For
QuotientAddGroup.congr
lifts the isomorphism e : G ≃ H
to G ⧸ G' ≃ H ⧸ H'
,
given that e
maps G
to H
.
Equations
- QuotientAddGroup.congr G' H' e he = { toFun := ⇑(QuotientAddGroup.map G' H' ↑e ⋯), invFun := ⇑(QuotientAddGroup.map H' G' ↑e.symm ⋯), left_inv := ⋯, right_inv := ⋯, map_add' := ⋯ }
Instances For
QuotientGroup.congr
lifts the isomorphism e : G ≃ H
to G ⧸ G' ≃ H ⧸ H'
,
given that e
maps G
to H
.
Equations
- QuotientGroup.congr G' H' e he = { toFun := ⇑(QuotientGroup.map G' H' ↑e ⋯), invFun := ⇑(QuotientGroup.map H' G' ↑e.symm ⋯), left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ }