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 definitions #
mk': the canonical group homomorphismG →* G/Ngiven a normal subgroupNofG.lift φ: the group homomorphismG/N →* Hgiven a group homomorphismφ : G →* Hsuch thatN ⊆ ker φ.map f: the group homomorphismG/N →* H/Mgiven a group homomorphismf : G →* Hsuch thatN ⊆ f⁻¹(M).
Main statements #
quotient_ker_equiv_range: Noether's first isomorphism theorem, an explicit isomorphismG/ker φ → range φfor every group homomorphismφ : G →* H.quotient_inf_equiv_prod_normal_quotient: Noether's second isomorphism theorem, an explicit isomorphism betweenH/(H ∩ N)and(HN)/Ngiven a subgroupHand a normal subgroupNof a groupG.quotient_group.quotient_quotient_equiv_quotient: Noether's third isomorphism theorem, the canonical isomorphism between(G / N) / (M / N)andG / M, whereN ≤ M.
Tags #
isomorphism theorems, quotient groups
@[protected]
The congruence relation generated by a normal subgroup.
Equations
- quotient_group.con N = {to_setoid := quotient_group.left_rel N, mul' := _}
@[protected]
def
quotient_add_group.con
{G : Type u}
[add_group G]
(N : add_subgroup G)
[nN : N.normal] :
add_con G
The additive congruence relation generated by a normal additive subgroup.
Equations
- quotient_add_group.con N = {to_setoid := quotient_add_group.left_rel N, add' := _}
@[protected, instance]
Equations
@[protected, instance]
Equations
The group homomorphism from G to G/N.
Equations
The additive group homomorphism from G to G/N.
Equations
@[simp]
theorem
quotient_group.coe_mk'
{G : Type u}
[group G]
(N : subgroup G)
[nN : N.normal] :
⇑(quotient_group.mk' N) = coe
@[simp]
theorem
quotient_add_group.coe_mk'
{G : Type u}
[add_group G]
(N : add_subgroup G)
[nN : N.normal] :
@[simp]
theorem
quotient_group.mk'_apply
{G : Type u}
[group G]
(N : subgroup G)
[nN : N.normal]
(x : G) :
⇑(quotient_group.mk' N) x = ↑x
@[simp]
theorem
quotient_add_group.mk'_apply
{G : Type u}
[add_group G]
(N : add_subgroup G)
[nN : N.normal]
(x : G) :
⇑(quotient_add_group.mk' N) x = ↑x
theorem
quotient_add_group.mk'_surjective
{G : Type u}
[add_group G]
(N : add_subgroup G)
[nN : N.normal] :
theorem
quotient_add_group.add_monoid_hom_ext
{G : Type u}
[add_group G]
(N : add_subgroup G)
[nN : N.normal]
{H : Type v}
[add_group H]
⦃f g : G ⧸ N →+ H⦄
(h : f.comp (quotient_add_group.mk' N) = g.comp (quotient_add_group.mk' N)) :
f = g
Two add_monoid_homs from an additive quotient group are equal if their
compositions with add_quotient_group.mk' are equal.
@[ext]
theorem
quotient_group.monoid_hom_ext
{G : Type u}
[group G]
(N : subgroup G)
[nN : N.normal]
{H : Type v}
[group H]
⦃f g : G ⧸ N →* H⦄
(h : f.comp (quotient_group.mk' N) = g.comp (quotient_group.mk' N)) :
f = g
Two monoid_homs from a quotient group are equal if their compositions with
quotient_group.mk' are equal.
@[simp]
theorem
quotient_add_group.eq_zero_iff
{G : Type u}
[add_group G]
{N : add_subgroup G}
[nN : N.normal]
(x : G) :
@[simp]
theorem
quotient_add_group.ker_mk
{G : Type u}
[add_group G]
(N : add_subgroup G)
[nN : N.normal] :
(quotient_add_group.mk' N).ker = N
@[simp]
theorem
quotient_group.ker_mk
{G : Type u}
[group G]
(N : subgroup G)
[nN : N.normal] :
(quotient_group.mk' N).ker = N
@[protected, instance]
def
quotient_group.has_quotient.quotient.comm_group
{G : Type u_1}
[comm_group G]
(N : subgroup G) :
comm_group (G ⧸ N)
Equations
- quotient_group.has_quotient.quotient.comm_group N = {mul := group.mul (quotient_group.quotient.group N), mul_assoc := _, one := group.one (quotient_group.quotient.group N), one_mul := _, mul_one := _, npow := group.npow (quotient_group.quotient.group N), npow_zero' := _, npow_succ' := _, inv := group.inv (quotient_group.quotient.group N), div := group.div (quotient_group.quotient.group N), div_eq_mul_inv := _, zpow := group.zpow (quotient_group.quotient.group N), zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, mul_left_inv := _, mul_comm := _}
@[protected, instance]
def
quotient_add_group.add_comm_group
{G : Type u_1}
[add_comm_group G]
(N : add_subgroup G) :
add_comm_group (G ⧸ N)
Equations
- quotient_add_group.add_comm_group N = {add := add_group.add (quotient_add_group.add_group N), add_assoc := _, zero := add_group.zero (quotient_add_group.add_group N), zero_add := _, add_zero := _, nsmul := add_group.nsmul (quotient_add_group.add_group N), nsmul_zero' := _, nsmul_succ' := _, neg := add_group.neg (quotient_add_group.add_group N), sub := add_group.sub (quotient_add_group.add_group N), sub_eq_add_neg := _, zsmul := add_group.zsmul (quotient_add_group.add_group N), zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _}
@[simp]
theorem
quotient_add_group.coe_zero
{G : Type u}
[add_group G]
(N : add_subgroup G)
[nN : N.normal] :
@[simp]
theorem
quotient_add_group.coe_neg
{G : Type u}
[add_group G]
(N : add_subgroup G)
[nN : N.normal]
(a : G) :
def
quotient_group.lift
{G : Type u}
[group G]
(N : subgroup G)
[nN : N.normal]
{H : Type v}
[group H]
(φ : G →* H)
(HN : ∀ (x : G), x ∈ N → ⇑φ x = 1) :
A group homomorphism φ : G →* H with N ⊆ ker(φ) descends (i.e. lifts) to a
group homomorphism G/N →* H.
Equations
- quotient_group.lift N φ HN = (quotient_group.con N).lift φ _
def
quotient_add_group.lift
{G : Type u}
[add_group G]
(N : add_subgroup G)
[nN : N.normal]
{H : Type v}
[add_group H]
(φ : G →+ H)
(HN : ∀ (x : G), x ∈ N → ⇑φ x = 0) :
An add_group homomorphism φ : G →+ H with N ⊆ ker(φ)
descends (i.e. lifts) to a group homomorphism G/N →* H.
Equations
- quotient_add_group.lift N φ HN = (quotient_add_group.con N).lift φ _
@[simp]
theorem
quotient_add_group.lift_mk
{G : Type u}
[add_group G]
(N : add_subgroup G)
[nN : N.normal]
{H : Type v}
[add_group H]
{φ : G →+ H}
(HN : ∀ (x : G), x ∈ N → ⇑φ x = 0)
(g : G) :
⇑(quotient_add_group.lift N φ HN) ↑g = ⇑φ g
@[simp]
theorem
quotient_add_group.lift_mk'
{G : Type u}
[add_group G]
(N : add_subgroup G)
[nN : N.normal]
{H : Type v}
[add_group H]
{φ : G →+ H}
(HN : ∀ (x : G), x ∈ N → ⇑φ x = 0)
(g : G) :
⇑(quotient_add_group.lift N φ HN) (quotient_add_group.mk g) = ⇑φ g
@[simp]
theorem
quotient_group.lift_mk'
{G : Type u}
[group G]
(N : subgroup G)
[nN : N.normal]
{H : Type v}
[group H]
{φ : G →* H}
(HN : ∀ (x : G), x ∈ N → ⇑φ x = 1)
(g : G) :
⇑(quotient_group.lift N φ HN) (quotient_group.mk g) = ⇑φ g
@[simp]
theorem
quotient_add_group.lift_quot_mk
{G : Type u}
[add_group G]
(N : add_subgroup G)
[nN : N.normal]
{H : Type v}
[add_group H]
{φ : G →+ H}
(HN : ∀ (x : G), x ∈ N → ⇑φ x = 0)
(g : G) :
⇑(quotient_add_group.lift N φ HN) (quot.mk setoid.r g) = ⇑φ g
def
quotient_add_group.map
{G : Type u}
[add_group G]
(N : add_subgroup G)
[nN : N.normal]
{H : Type v}
[add_group H]
(M : add_subgroup H)
[M.normal]
(f : G →+ H)
(h : N ≤ add_subgroup.comap f M) :
An add_group homomorphism f : G →+ H induces a map
G/N →+ H/M if N ⊆ f⁻¹(M).
Equations
- quotient_add_group.map N M f h = quotient_add_group.lift N ((quotient_add_group.mk' M).comp f) _
def
quotient_group.map
{G : Type u}
[group G]
(N : subgroup G)
[nN : N.normal]
{H : Type v}
[group H]
(M : subgroup H)
[M.normal]
(f : G →* H)
(h : N ≤ subgroup.comap f M) :
A group homomorphism f : G →* H induces a map G/N →* H/M if N ⊆ f⁻¹(M).
Equations
- quotient_group.map N M f h = quotient_group.lift N ((quotient_group.mk' M).comp f) _
@[simp]
theorem
quotient_add_group.map_coe
{G : Type u}
[add_group G]
(N : add_subgroup G)
[nN : N.normal]
{H : Type v}
[add_group H]
(M : add_subgroup H)
[M.normal]
(f : G →+ H)
(h : N ≤ add_subgroup.comap f M)
(x : G) :
theorem
quotient_group.map_mk'
{G : Type u}
[group G]
(N : subgroup G)
[nN : N.normal]
{H : Type v}
[group H]
(M : subgroup H)
[M.normal]
(f : G →* H)
(h : N ≤ subgroup.comap f M)
(x : G) :
⇑(quotient_group.map N M f h) (⇑(quotient_group.mk' N) x) = ↑(⇑f x)
theorem
quotient_add_group.map_mk'
{G : Type u}
[add_group G]
(N : add_subgroup G)
[nN : N.normal]
{H : Type v}
[add_group H]
(M : add_subgroup H)
[M.normal]
(f : G →+ H)
(h : N ≤ add_subgroup.comap f M)
(x : G) :
⇑(quotient_add_group.map N M f h) (⇑(quotient_add_group.mk' N) x) = ↑(⇑f x)
def
quotient_add_group.ker_lift
{G : Type u}
[add_group G]
{H : Type v}
[add_group H]
(φ : G →+ H) :
The induced map from the quotient by the kernel to the codomain.
Equations
The induced map from the quotient by the kernel to the codomain.
Equations
@[simp]
theorem
quotient_add_group.ker_lift_mk
{G : Type u}
[add_group G]
{H : Type v}
[add_group H]
(φ : G →+ H)
(g : G) :
⇑(quotient_add_group.ker_lift φ) ↑g = ⇑φ g
@[simp]
theorem
quotient_group.ker_lift_mk
{G : Type u}
[group G]
{H : Type v}
[group H]
(φ : G →* H)
(g : G) :
⇑(quotient_group.ker_lift φ) ↑g = ⇑φ g
@[simp]
theorem
quotient_group.ker_lift_mk'
{G : Type u}
[group G]
{H : Type v}
[group H]
(φ : G →* H)
(g : G) :
⇑(quotient_group.ker_lift φ) (quotient_group.mk g) = ⇑φ g
@[simp]
theorem
quotient_add_group.ker_lift_mk'
{G : Type u}
[add_group G]
{H : Type v}
[add_group H]
(φ : G →+ H)
(g : G) :
⇑(quotient_add_group.ker_lift φ) (quotient_add_group.mk g) = ⇑φ g
theorem
quotient_group.ker_lift_injective
{G : Type u}
[group G]
{H : Type v}
[group H]
(φ : G →* H) :
theorem
quotient_add_group.ker_lift_injective
{G : Type u}
[add_group G]
{H : Type v}
[add_group H]
(φ : G →+ H) :
The induced map from the quotient by the kernel to the range.
Equations
def
quotient_add_group.range_ker_lift
{G : Type u}
[add_group G]
{H : Type v}
[add_group H]
(φ : G →+ H) :
The induced map from the quotient by the kernel to the range.
Equations
theorem
quotient_group.range_ker_lift_injective
{G : Type u}
[group G]
{H : Type v}
[group H]
(φ : G →* H) :
theorem
quotient_add_group.range_ker_lift_injective
{G : Type u}
[add_group G]
{H : Type v}
[add_group H]
(φ : G →+ H) :
theorem
quotient_group.range_ker_lift_surjective
{G : Type u}
[group G]
{H : Type v}
[group H]
(φ : G →* H) :
theorem
quotient_add_group.range_ker_lift_surjective
{G : Type u}
[add_group G]
{H : Type v}
[add_group H]
(φ : G →+ H) :
noncomputable
def
quotient_group.quotient_ker_equiv_range
{G : Type u}
[group G]
{H : Type v}
[group H]
(φ : G →* H) :
Noether's first isomorphism theorem (a definition): the canonical isomorphism between
G/(ker φ) to range φ.
noncomputable
def
quotient_add_group.quotient_ker_equiv_range
{G : Type u}
[add_group G]
{H : Type v}
[add_group H]
(φ : G →+ H) :
The first isomorphism theorem
(a definition): the canonical isomorphism between G/(ker φ) to range φ.
@[simp]
theorem
quotient_add_group.quotient_ker_equiv_of_right_inverse_apply
{G : Type u}
[add_group G]
{H : Type v}
[add_group H]
(φ : G →+ H)
(ψ : H → G)
(hφ : function.right_inverse ψ ⇑φ)
(ᾰ : G ⧸ φ.ker) :
def
quotient_group.quotient_ker_equiv_of_right_inverse
{G : Type u}
[group G]
{H : Type v}
[group H]
(φ : G →* H)
(ψ : H → G)
(hφ : function.right_inverse ψ ⇑φ) :
The canonical isomorphism G/(ker φ) ≃* H induced by a homomorphism φ : G →* H
with a right inverse ψ : H → G.
Equations
- quotient_group.quotient_ker_equiv_of_right_inverse φ ψ hφ = {to_fun := ⇑(quotient_group.ker_lift φ), inv_fun := quotient_group.mk ∘ ψ, left_inv := _, right_inv := hφ, map_mul' := _}
def
quotient_add_group.quotient_ker_equiv_of_right_inverse
{G : Type u}
[add_group G]
{H : Type v}
[add_group H]
(φ : G →+ H)
(ψ : H → G)
(hφ : function.right_inverse ψ ⇑φ) :
The canonical isomorphism
G/(ker φ) ≃+ H induced by a homomorphism φ : G →+ H with a right inverse ψ : H → G.
Equations
- quotient_add_group.quotient_ker_equiv_of_right_inverse φ ψ hφ = {to_fun := ⇑(quotient_add_group.ker_lift φ), inv_fun := quotient_add_group.mk ∘ ψ, left_inv := _, right_inv := hφ, map_add' := _}
@[simp]
theorem
quotient_group.quotient_ker_equiv_of_right_inverse_apply
{G : Type u}
[group G]
{H : Type v}
[group H]
(φ : G →* H)
(ψ : H → G)
(hφ : function.right_inverse ψ ⇑φ)
(ᾰ : G ⧸ φ.ker) :
⇑(quotient_group.quotient_ker_equiv_of_right_inverse φ ψ hφ) ᾰ = ⇑(quotient_group.ker_lift φ) ᾰ
@[simp]
theorem
quotient_add_group.quotient_ker_equiv_of_right_inverse_symm_apply
{G : Type u}
[add_group G]
{H : Type v}
[add_group H]
(φ : G →+ H)
(ψ : H → G)
(hφ : function.right_inverse ψ ⇑φ)
(ᾰ : H) :
⇑((quotient_add_group.quotient_ker_equiv_of_right_inverse φ ψ hφ).symm) ᾰ = (quotient_add_group.mk ∘ ψ) ᾰ
@[simp]
theorem
quotient_group.quotient_ker_equiv_of_right_inverse_symm_apply
{G : Type u}
[group G]
{H : Type v}
[group H]
(φ : G →* H)
(ψ : H → G)
(hφ : function.right_inverse ψ ⇑φ)
(ᾰ : H) :
⇑((quotient_group.quotient_ker_equiv_of_right_inverse φ ψ hφ).symm) ᾰ = (quotient_group.mk ∘ ψ) ᾰ
@[simp]
The canonical isomorphism G/⊥ ≃+ G.
Equations
- quotient_add_group.quotient_bot = quotient_add_group.quotient_ker_equiv_of_right_inverse (add_monoid_hom.id G) id quotient_add_group.quotient_bot._proof_2
The canonical isomorphism G/⊥ ≃* G.
Equations
- quotient_group.quotient_bot = quotient_group.quotient_ker_equiv_of_right_inverse (monoid_hom.id G) id quotient_group.quotient_bot._proof_2
@[simp]
@[simp]
@[simp]
theorem
quotient_add_group.quotient_bot_apply
{G : Type u}
[add_group G]
(ᾰ : G ⧸ (add_monoid_hom.id G).ker) :
noncomputable
def
quotient_add_group.quotient_ker_equiv_of_surjective
{G : Type u}
[add_group G]
{H : Type v}
[add_group H]
(φ : G →+ H)
(hφ : function.surjective ⇑φ) :
The canonical isomorphism
G/(ker φ) ≃+ H induced by a surjection φ : G →+ H.
For a computable version, see quotient_add_group.quotient_ker_equiv_of_right_inverse.
noncomputable
def
quotient_group.quotient_ker_equiv_of_surjective
{G : Type u}
[group G]
{H : Type v}
[group H]
(φ : G →* H)
(hφ : function.surjective ⇑φ) :
The canonical isomorphism G/(ker φ) ≃* H induced by a surjection φ : G →* H.
For a computable version, see quotient_group.quotient_ker_equiv_of_right_inverse.
def
quotient_group.equiv_quotient_of_eq
{G : Type u}
[group G]
{M N : subgroup G}
[M.normal]
[N.normal]
(h : M = N) :
If two normal subgroups M and N of G are the same, their quotient groups are
isomorphic.
Equations
- quotient_group.equiv_quotient_of_eq h = {to_fun := ⇑(quotient_group.lift M (quotient_group.mk' N) _), inv_fun := ⇑(quotient_group.lift N (quotient_group.mk' M) _), left_inv := _, right_inv := _, map_mul' := _}
def
quotient_add_group.equiv_quotient_of_eq
{G : Type u}
[add_group G]
{M N : add_subgroup G}
[M.normal]
[N.normal]
(h : M = N) :
If two normal subgroups M and N of G are the same, their quotient groups are
isomorphic.
Equations
- quotient_add_group.equiv_quotient_of_eq h = {to_fun := ⇑(quotient_add_group.lift M (quotient_add_group.mk' N) _), inv_fun := ⇑(quotient_add_group.lift N (quotient_add_group.mk' M) _), left_inv := _, right_inv := _, map_add' := _}
@[simp]
theorem
quotient_add_group.equiv_quotient_of_eq_mk
{G : Type u}
[add_group G]
{M N : add_subgroup G}
[M.normal]
[N.normal]
(h : M = N)
(x : G) :
def
quotient_add_group.quotient_map_add_subgroup_of_of_le
{G : Type u}
[add_group G]
{A' A B' B : add_subgroup G}
[hAN : (A'.add_subgroup_of A).normal]
[hBN : (B'.add_subgroup_of B).normal]
(h' : A' ≤ B')
(h : A ≤ B) :
↥A ⧸ A'.add_subgroup_of A →+ ↥B ⧸ B'.add_subgroup_of B
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
def
quotient_group.quotient_map_subgroup_of_of_le
{G : Type u}
[group G]
{A' A B' B : subgroup G}
[hAN : (A'.subgroup_of A).normal]
[hBN : (B'.subgroup_of B).normal]
(h' : A' ≤ B')
(h : A ≤ B) :
↥A ⧸ A'.subgroup_of A →* ↥B ⧸ B'.subgroup_of B
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
- quotient_group.quotient_map_subgroup_of_of_le h' h = quotient_group.map (A'.subgroup_of A) (B'.subgroup_of B) (subgroup.inclusion h) _
@[simp]
theorem
quotient_add_group.quotient_map_add_subgroup_of_of_le_coe
{G : Type u}
[add_group G]
{A' A B' B : add_subgroup G}
[hAN : (A'.add_subgroup_of A).normal]
[hBN : (B'.add_subgroup_of B).normal]
(h' : A' ≤ B')
(h : A ≤ B)
(x : ↥A) :
@[simp]
theorem
quotient_group.quotient_map_subgroup_of_of_le_coe
{G : Type u}
[group G]
{A' A B' B : subgroup G}
[hAN : (A'.subgroup_of A).normal]
[hBN : (B'.subgroup_of B).normal]
(h' : A' ≤ B')
(h : A ≤ B)
(x : ↥A) :
⇑(quotient_group.quotient_map_subgroup_of_of_le h' h) ↑x = ↑(⇑(subgroup.inclusion h) x)
def
quotient_group.equiv_quotient_subgroup_of_of_eq
{G : Type u}
[group G]
{A' A B' B : subgroup G}
[hAN : (A'.subgroup_of A).normal]
[hBN : (B'.subgroup_of B).normal]
(h' : A' = B')
(h : A = B) :
↥A ⧸ A'.subgroup_of A ≃* ↥B ⧸ B'.subgroup_of B
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'.subgroup_of A : subgroup A) depends on on A.
def
quotient_add_group.equiv_quotient_add_subgroup_of_of_eq
{G : Type u}
[add_group G]
{A' A B' B : add_subgroup G}
[hAN : (A'.add_subgroup_of A).normal]
[hBN : (B'.add_subgroup_of B).normal]
(h' : A' = B')
(h : A = B) :
↥A ⧸ A'.add_subgroup_of A ≃+ ↥B ⧸ B'.add_subgroup_of B
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'.add_subgroup_of A : add_subgroup A) depends on on A.
def
quotient_group.hom_quotient_zpow_of_hom
{G' H' : Type u}
[comm_group G']
[comm_group H']
(φ' : G' →* H')
(n : ℤ) :
G' ⧸ (zpow_group_hom n).range →* H' ⧸ (zpow_group_hom n).range
The map of quotients by powers of an integer induced by a group homomorphism.
Equations
- quotient_group.hom_quotient_zpow_of_hom φ' n = quotient_group.lift (zpow_group_hom n).range ((quotient_group.mk' (zpow_group_hom n).range).comp φ') _
def
quotient_add_group.hom_quotient_zsmul_of_hom
{G' H' : Type u}
[add_comm_group G']
[add_comm_group H']
(φ' : G' →+ H')
(n : ℤ) :
G' ⧸ (zsmul_add_group_hom n).range →+ H' ⧸ (zsmul_add_group_hom n).range
The map of quotients by multiples of an integer induced by an additive group homomorphism.
Equations
theorem
quotient_add_group.hom_quotient_zsmul_of_hom_right_inverse
{G' H' : Type u}
[add_comm_group G']
[add_comm_group H']
(φ' : G' →+ H')
(ψ' : H' →+ G')
(h : function.right_inverse ⇑ψ' ⇑φ')
(n : ℤ) :
@[simp]
theorem
quotient_group.hom_quotient_zpow_of_hom_right_inverse
{G' H' : Type u}
[comm_group G']
[comm_group H']
(φ' : G' →* H')
(ψ' : H' →* G')
(h : function.right_inverse ⇑ψ' ⇑φ')
(n : ℤ) :
(quotient_group.hom_quotient_zpow_of_hom φ' n).comp (quotient_group.hom_quotient_zpow_of_hom ψ' n) = monoid_hom.id (H' ⧸ (zpow_group_hom n).range)
def
quotient_group.equiv_quotient_zpow_of_equiv
{G' H' : Type u}
[comm_group G']
[comm_group H']
(χ : G' ≃* H')
(n : ℤ) :
G' ⧸ (zpow_group_hom n).range ≃* H' ⧸ (zpow_group_hom n).range
The equivalence of quotients by powers of an integer induced by a group isomorphism.
Equations
def
quotient_add_group.equiv_quotient_zsmul_of_equiv
{G' H' : Type u}
[add_comm_group G']
[add_comm_group H']
(χ : G' ≃+ H')
(n : ℤ) :
G' ⧸ (zsmul_add_group_hom n).range ≃+ H' ⧸ (zsmul_add_group_hom n).range
The equivalence of quotients by multiples of an integer induced by an additive group isomorphism.
noncomputable
def
quotient_group.quotient_inf_equiv_prod_normal_quotient
{G : Type u}
[group G]
(H N : subgroup G)
[N.normal] :
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
- quotient_group.quotient_inf_equiv_prod_normal_quotient H N = let φ : ↥H →* ↥(H ⊔ N) ⧸ subgroup.comap (H ⊔ N).subtype N := (quotient_group.mk' (subgroup.comap (H ⊔ N).subtype N)).comp (subgroup.inclusion _) in have φ_surjective : function.surjective ⇑φ, from _, (quotient_group.equiv_quotient_of_eq _).trans (quotient_group.quotient_ker_equiv_of_surjective φ φ_surjective)
noncomputable
def
quotient_add_group.quotient_inf_equiv_sum_normal_quotient
{G : Type u}
[add_group G]
(H N : add_subgroup G)
[N.normal] :
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
- quotient_add_group.quotient_inf_equiv_sum_normal_quotient H N = let φ : ↥H →+ ↥(H ⊔ N) ⧸ add_subgroup.comap (H ⊔ N).subtype N := (quotient_add_group.mk' (add_subgroup.comap (H ⊔ N).subtype N)).comp (add_subgroup.inclusion _) in have φ_surjective : function.surjective ⇑φ, from _, (quotient_add_group.equiv_quotient_of_eq _).trans (quotient_add_group.quotient_ker_equiv_of_surjective φ φ_surjective)
@[protected, instance]
def
quotient_group.map_normal
{G : Type u}
[group G]
(N : subgroup G)
[nN : N.normal]
(M : subgroup G)
[nM : M.normal] :
(subgroup.map (quotient_group.mk' N) M).normal
@[protected, instance]
def
quotient_add_group.map_normal
{G : Type u}
[add_group G]
(N : add_subgroup G)
[nN : N.normal]
(M : add_subgroup G)
[nM : M.normal] :
def
quotient_add_group.quotient_quotient_equiv_quotient_aux
{G : Type u}
[add_group G]
(N : add_subgroup G)
[nN : N.normal]
(M : add_subgroup G)
[nM : M.normal]
(h : N ≤ M) :
(G ⧸ N) ⧸ add_subgroup.map (quotient_add_group.mk' N) M →+ G ⧸ M
The map from the third isomorphism theorem for additive groups: (A / N) / (M / N) → A / M.
Equations
def
quotient_group.quotient_quotient_equiv_quotient_aux
{G : Type u}
[group G]
(N : subgroup G)
[nN : N.normal]
(M : subgroup G)
[nM : M.normal]
(h : N ≤ M) :
(G ⧸ N) ⧸ subgroup.map (quotient_group.mk' N) M →* G ⧸ M
The map from the third isomorphism theorem for groups: (G / N) / (M / N) → G / M.
Equations
- quotient_group.quotient_quotient_equiv_quotient_aux N M h = quotient_group.lift (subgroup.map (quotient_group.mk' N) M) (quotient_group.map N M (monoid_hom.id G) h) _
@[simp]
theorem
quotient_add_group.quotient_quotient_equiv_quotient_aux_coe
{G : Type u}
[add_group G]
(N : add_subgroup G)
[nN : N.normal]
(M : add_subgroup G)
[nM : M.normal]
(h : N ≤ M)
(x : G ⧸ N) :
⇑(quotient_add_group.quotient_quotient_equiv_quotient_aux N M h) ↑x = ⇑(quotient_add_group.map N M (add_monoid_hom.id G) h) x
@[simp]
theorem
quotient_group.quotient_quotient_equiv_quotient_aux_coe
{G : Type u}
[group G]
(N : subgroup G)
[nN : N.normal]
(M : subgroup G)
[nM : M.normal]
(h : N ≤ M)
(x : G ⧸ N) :
⇑(quotient_group.quotient_quotient_equiv_quotient_aux N M h) ↑x = ⇑(quotient_group.map N M (monoid_hom.id G) h) x
theorem
quotient_add_group.quotient_quotient_equiv_quotient_aux_coe_coe
{G : Type u}
[add_group G]
(N : add_subgroup G)
[nN : N.normal]
(M : add_subgroup G)
[nM : M.normal]
(h : N ≤ M)
(x : G) :
def
quotient_group.quotient_quotient_equiv_quotient
{G : Type u}
[group G]
(N : subgroup G)
[nN : N.normal]
(M : subgroup G)
[nM : M.normal]
(h : N ≤ M) :
(G ⧸ N) ⧸ subgroup.map (quotient_group.mk' N) M ≃* G ⧸ M
Noether's third isomorphism theorem for groups: (G / N) / (M / N) ≃ G / M.
Equations
def
quotient_add_group.quotient_quotient_equiv_quotient
{G : Type u}
[add_group G]
(N : add_subgroup G)
[nN : N.normal]
(M : add_subgroup G)
[nM : M.normal]
(h : N ≤ M) :
(G ⧸ N) ⧸ add_subgroup.map (quotient_add_group.mk' N) M ≃+ G ⧸ M
Noether's third isomorphism theorem for additive groups: (A / N) / (M / N) ≃ A / M.
Equations
theorem
quotient_add_group.subsingleton_quotient_top
{G : Type u}
[add_group G] :
subsingleton (G ⧸ ⊤)
theorem
quotient_add_group.add_subgroup_eq_top_of_subsingleton
{G : Type u}
[add_group G]
(H : add_subgroup G)
(h : subsingleton (G ⧸ H)) :
If the quotient by an additive subgroup gives a singleton then the additive subgroup is the whole additive group.
theorem
quotient_group.subgroup_eq_top_of_subsingleton
{G : Type u}
[group G]
(H : subgroup G)
(h : subsingleton (G ⧸ H)) :
If the quotient by a subgroup gives a singleton then the subgroup is the whole group.
theorem
quotient_group.comap_comap_center
{G : Type u}
[group G]
{H₁ : subgroup G}
[H₁.normal]
{H₂ : subgroup (G ⧸ H₁)}
[H₂.normal] :
subgroup.comap (quotient_group.mk' H₁) (subgroup.comap (quotient_group.mk' H₂) (subgroup.center ((G ⧸ H₁) ⧸ H₂))) = subgroup.comap (quotient_group.mk' (subgroup.comap (quotient_group.mk' H₁) H₂)) (subgroup.center (G ⧸ subgroup.comap (quotient_group.mk' H₁) H₂))
theorem
quotient_add_group.comap_comap_center
{G : Type u}
[add_group G]
{H₁ : add_subgroup G}
[H₁.normal]
{H₂ : add_subgroup (G ⧸ H₁)}
[H₂.normal] :
add_subgroup.comap (quotient_add_group.mk' H₁) (add_subgroup.comap (quotient_add_group.mk' H₂) (add_subgroup.center ((G ⧸ H₁) ⧸ H₂))) = add_subgroup.comap (quotient_add_group.mk' (add_subgroup.comap (quotient_add_group.mk' H₁) H₂)) (add_subgroup.center (G ⧸ add_subgroup.comap (quotient_add_group.mk' H₁) H₂))
noncomputable
def
group.fintype_of_ker_le_range
{F G H : Type u}
[group F]
[group G]
[group H]
[fintype F]
[fintype H]
(f : F →* G)
(g : G →* H)
(h : g.ker ≤ f.range) :
fintype G
If F and H are finite such that ker(G →* H) ≤ im(F →* G), then G is finite.
Equations
- group.fintype_of_ker_le_range f g h = fintype.of_equiv ((G ⧸ g.ker) × ↥(g.ker)) subgroup.group_equiv_quotient_times_subgroup.symm