Quotients of groups by normal subgroups #
This files develops the basic theory of quotients of groups by normal subgroups. In particular it proves Noether's first and second isomorphism theorems.
Main statements #
QuotientGroup.quotientKerEquivRange
: Noether's first isomorphism theorem, an explicit isomorphismG/ker φ → range φ
for every group homomorphismφ : G →* H
.QuotientGroup.quotientInfEquivProdNormalQuotient
: Noether's second isomorphism theorem, an explicit isomorphism betweenH/(H ∩ N)
and(HN)/N
given a subgroupH
and a normal subgroupN
of a groupG
.QuotientGroup.quotientQuotientEquivQuotient
: Noether's third isomorphism theorem, the canonical isomorphism between(G / N) / (M / N)
andG / M
, whereN ≤ M
.
Tags #
isomorphism theorems, quotient groups
The induced map from the quotient by the kernel to the codomain.
Equations
- QuotientGroup.kerLift φ = QuotientGroup.lift φ.ker φ ⋯
Instances For
The induced map from the quotient by the kernel to the codomain.
Equations
- QuotientAddGroup.kerLift φ = QuotientAddGroup.lift φ.ker φ ⋯
Instances For
The induced map from the quotient by the kernel to the range.
Equations
- QuotientGroup.rangeKerLift φ = QuotientGroup.lift φ.ker φ.rangeRestrict ⋯
Instances For
The induced map from the quotient by the kernel to the range.
Equations
- QuotientAddGroup.rangeKerLift φ = QuotientAddGroup.lift φ.ker φ.rangeRestrict ⋯
Instances For
The canonical isomorphism G/(ker φ) ≃* H
induced by a homomorphism φ : G →* H
with a right inverse ψ : H → G
.
Equations
- QuotientGroup.quotientKerEquivOfRightInverse φ ψ hφ = { toFun := ⇑(QuotientGroup.kerLift φ), invFun := QuotientGroup.mk ∘ ψ, left_inv := ⋯, right_inv := hφ, map_mul' := ⋯ }
Instances For
The canonical isomorphism G/(ker φ) ≃+ H
induced by a homomorphism
φ : G →+ H
with a right inverse ψ : H → G
.
Equations
- QuotientAddGroup.quotientKerEquivOfRightInverse φ ψ hφ = { toFun := ⇑(QuotientAddGroup.kerLift φ), invFun := QuotientAddGroup.mk ∘ ψ, left_inv := ⋯, right_inv := hφ, map_add' := ⋯ }
Instances For
The canonical isomorphism G/⊥ ≃* G
.
Equations
- QuotientGroup.quotientBot = QuotientGroup.quotientKerEquivOfRightInverse (MonoidHom.id G) id ⋯
Instances For
The canonical isomorphism G/⊥ ≃+ G
.
Equations
- QuotientAddGroup.quotientBot = QuotientAddGroup.quotientKerEquivOfRightInverse (AddMonoidHom.id G) id ⋯
Instances For
The canonical isomorphism G/(ker φ) ≃* H
induced by a surjection φ : G →* H
.
For a computable
version, see QuotientGroup.quotientKerEquivOfRightInverse
.
Equations
Instances For
The canonical isomorphism G/(ker φ) ≃+ H
induced by a surjection φ : G →+ H
.
For a computable
version, see QuotientAddGroup.quotientKerEquivOfRightInverse
.
Equations
Instances For
If two normal subgroups M
and N
of G
are the same, their quotient groups are
isomorphic.
Equations
- QuotientGroup.quotientMulEquivOfEq h = { toEquiv := Subgroup.quotientEquivOfEq h, map_mul' := ⋯ }
Instances For
If two normal subgroups M
and N
of G
are the same, their quotient groups are
isomorphic.
Equations
- QuotientAddGroup.quotientAddEquivOfEq h = { toEquiv := AddSubgroup.quotientEquivOfEq h, map_add' := ⋯ }
Instances For
Let A', A, B', B
be subgroups of G
. If A' ≤ B'
and A ≤ B
,
then there is a map A / (A' ⊓ A) →* B / (B' ⊓ B)
induced by the inclusions.
Equations
- QuotientGroup.quotientMapSubgroupOfOfLe h' h = QuotientGroup.map (A'.subgroupOf A) (B'.subgroupOf B) (Subgroup.inclusion h) ⋯
Instances For
Let A', A, B', B
be subgroups of G
. If A' ≤ B'
and A ≤ B
, then there is a map
A / (A' ⊓ A) →+ B / (B' ⊓ B)
induced by the inclusions.
Equations
- QuotientAddGroup.quotientMapAddSubgroupOfOfLe h' h = QuotientAddGroup.map (A'.addSubgroupOf A) (B'.addSubgroupOf B) (AddSubgroup.inclusion h) ⋯
Instances For
Let A', A, B', B
be subgroups of G
.
If A' = B'
and A = B
, then the quotients A / (A' ⊓ A)
and B / (B' ⊓ B)
are isomorphic.
Applying this equiv is nicer than rewriting along the equalities, since the type of
(A'.subgroupOf A : Subgroup A)
depends on A
.
Equations
- QuotientGroup.equivQuotientSubgroupOfOfEq h' h = (QuotientGroup.quotientMapSubgroupOfOfLe ⋯ ⋯).toMulEquiv (QuotientGroup.quotientMapSubgroupOfOfLe ⋯ ⋯) ⋯ ⋯
Instances For
Let A', A, B', B
be subgroups of G
. If A' = B'
and A = B
, then the quotients
A / (A' ⊓ A)
and B / (B' ⊓ B)
are isomorphic. Applying this equiv is nicer than rewriting along
the equalities, since the type of (A'.addSubgroupOf A : AddSubgroup A)
depends on A
.
Equations
- QuotientAddGroup.equivQuotientAddSubgroupOfOfEq h' h = (QuotientAddGroup.quotientMapAddSubgroupOfOfLe ⋯ ⋯).toAddEquiv (QuotientAddGroup.quotientMapAddSubgroupOfOfLe ⋯ ⋯) ⋯ ⋯
Instances For
The map of quotients by powers of an integer induced by a group homomorphism.
Equations
- QuotientGroup.homQuotientZPowOfHom f n = QuotientGroup.lift (zpowGroupHom n).range ((QuotientGroup.mk' (zpowGroupHom n).range).comp f) ⋯
Instances For
The map of quotients by multiples of an integer induced by an additive group homomorphism.
Equations
- QuotientAddGroup.homQuotientZSMulOfHom f n = QuotientAddGroup.lift (zsmulAddGroupHom n).range ((QuotientAddGroup.mk' (zsmulAddGroupHom n).range).comp f) ⋯
Instances For
The equivalence of quotients by powers of an integer induced by a group isomorphism.
Equations
- QuotientGroup.equivQuotientZPowOfEquiv e n = (QuotientGroup.homQuotientZPowOfHom (↑e) n).toMulEquiv (QuotientGroup.homQuotientZPowOfHom (↑e.symm) n) ⋯ ⋯
Instances For
The equivalence of quotients by multiples of an integer induced by an additive group isomorphism.
Equations
- QuotientAddGroup.equivQuotientZSMulOfEquiv e n = (QuotientAddGroup.homQuotientZSMulOfHom (↑e) n).toAddEquiv (QuotientAddGroup.homQuotientZSMulOfHom (↑e.symm) n) ⋯ ⋯
Instances For
Noether's second isomorphism theorem: given two subgroups H
and N
of a group G
, where
N
is normal, defines an isomorphism between H/(H ∩ N)
and (HN)/N
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The second isomorphism theorem: given two subgroups H
and N
of a group G
, where
N
is normal, defines an isomorphism between H/(H ∩ N)
and (H + N)/N
Equations
- One or more equations did not get rendered due to their size.
Instances For
The map from the third isomorphism theorem for groups: (G / N) / (M / N) → G / M
.
Equations
- QuotientGroup.quotientQuotientEquivQuotientAux N M h = QuotientGroup.lift (Subgroup.map (QuotientGroup.mk' N) M) (QuotientGroup.map N M (MonoidHom.id G) h) ⋯
Instances For
The map from the third isomorphism theorem for additive groups:
(A / N) / (M / N) → A / M
.
Equations
Instances For
Noether's third isomorphism theorem for groups: (G / N) / (M / N) ≃* G / M
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Noether's third isomorphism theorem for additive groups: (A / N) / (M / N) ≃+ A / M
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
If the quotient by a subgroup gives a singleton then the subgroup is the whole group.
If the quotient by an additive subgroup gives a singleton then the additive subgroup is the whole additive group.