# mathlibdocumentation

group_theory.quotient_group

# 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 homomorphism G →* G/N given a normal subgroup N of G.
• lift φ: the group homomorphism G/N →* H given a group homomorphism φ : G →* H such that N ⊆ ker φ.
• map f: the group homomorphism G/N →* H/M given a group homomorphism f : G →* H such that N ⊆ f⁻¹(M).

## Main statements #

• quotient_ker_equiv_range: Noether's first isomorphism theorem, an explicit isomorphism G/ker φ → range φ for every group homomorphism φ : G →* H.
• quotient_inf_equiv_prod_normal_quotient: Noether's second isomorphism theorem, an explicit isomorphism between H/(H ∩ N) and (HN)/N given a subgroup H and a normal subgroup N of a group G.
• quotient_group.quotient_quotient_equiv_quotient: Noether's third isomorphism theorem, the canonical isomorphism between (G / M) / (M / N) and G / N, where N ≤ M.

## Tags #

isomorphism theorems, quotient groups

@[instance]
@[instance]
def quotient_group.quotient.div_inv_monoid {G : Type u} [group G] (N : subgroup G) [nN : N.normal] :
Equations
@[instance]
def quotient_group.quotient.group {G : Type u} [group G] (N : subgroup G) [nN : N.normal] :
Equations
@[instance]
def quotient_group.mk' {G : Type u} [group G] (N : subgroup G) [nN : N.normal] :

The group homomorphism from G to G/N.

Equations

The additive group homomorphism from G to G/N.

@[simp]
theorem quotient_group.coe_mk' {G : Type u} [group G] (N : subgroup G) [nN : N.normal] :
@[simp]
theorem quotient_group.mk'_apply {G : Type u} [group G] (N : subgroup G) [nN : N.normal] (x : G) :
x = x
theorem quotient_add_group.mk'_apply {G : Type u} [add_group G] (N : add_subgroup G) [nN : N.normal] (x : G) :
= x
@[simp]
theorem quotient_add_group.eq_zero_iff {G : Type u} [add_group G] {N : add_subgroup G} [nN : N.normal] (x : G) :
x = 0 x N
@[simp]
theorem quotient_group.eq_one_iff {G : Type u} [group G] {N : subgroup G} [nN : N.normal] (x : G) :
x = 1 x N
@[simp]
@[simp]
theorem quotient_group.ker_mk {G : Type u} [group G] (N : subgroup G) [nN : N.normal] :
= N
theorem quotient_group.eq_iff_div_mem {G : Type u} [group G] {N : subgroup G} [nN : N.normal] {x y : G} :
x = y x / y N
theorem quotient_add_group.eq_iff_sub_mem {G : Type u} [add_group G] {N : add_subgroup G} [nN : N.normal] {x y : G} :
x = y x - y N
@[instance]
@[instance]
def quotient_group.quotient.comm_group {G : Type u_1} [comm_group G] (N : subgroup G) :
Equations
@[simp]
theorem quotient_group.coe_one {G : Type u} [group G] (N : subgroup G) [nN : N.normal] :
1 = 1
@[simp]
0 = 0
@[simp]
theorem quotient_group.coe_mul {G : Type u} [group G] (N : subgroup G) [nN : N.normal] (a b : G) :
a * b = (a) * b
@[simp]
(a + b) = a + b
@[simp]
theorem quotient_add_group.coe_neg {G : Type u} [add_group G] (N : add_subgroup G) [nN : N.normal] (a : G) :
@[simp]
theorem quotient_group.coe_inv {G : Type u} [group G] (N : subgroup G) [nN : N.normal] (a : G) :
@[simp]
theorem quotient_group.coe_pow {G : Type u} [group G] (N : subgroup G) [nN : N.normal] (a : G) (n : ) :
(a ^ n) = a ^ n
@[simp]
theorem quotient_group.coe_gpow {G : Type u} [group G] (N : subgroup G) [nN : N.normal] (a : G) (n : ) :
(a ^ n) = a ^ n
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
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.

@[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) :
HN) 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) :
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) :
HN) = φ 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) :
HN) = φ g
@[simp]
theorem quotient_group.lift_quot_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) :
HN) (quot.mk setoid.r 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) :
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 ) :

An add_group homomorphism f : G →+ H induces a map G/N →+ H/M if N ⊆ f⁻¹(M).

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 ) :

A group homomorphism f : G →* H induces a map G/N →* H/M if N ⊆ f⁻¹(M).

Equations
@[simp]
theorem quotient_group.map_coe {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 ) (x : G) :
f h) x = (f x)
@[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 ) (x : G) :
f h) x = (f x)
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 ) (x : G) :
f h) ( 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 ) (x : G) :
f h) 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.

def quotient_group.ker_lift {G : Type u} [group G] {H : Type v} [group H] (φ : G →* H) :

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) :
= φ g
@[simp]
theorem quotient_group.ker_lift_mk {G : Type u} [group G] {H : Type v} [group H] (φ : G →* H) (g : G) :
= φ g
@[simp]
theorem quotient_group.ker_lift_mk' {G : Type u} [group G] {H : Type v} [group H] (φ : G →* H) (g : 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) :
theorem quotient_group.ker_lift_injective {G : Type u} [group G] {H : Type v} [group H] (φ : G →* H) :
theorem quotient_add_group.injective_ker_lift {G : Type u} [add_group G] {H : Type v} [add_group H] (φ : G →+ H) :
def quotient_group.range_ker_lift {G : Type u} [group G] {H : Type v} [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.

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) :
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 φ.

Equations
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φ : φ)  :
def quotient_group.quotient_ker_equiv_of_right_inverse {G : Type u} [group G] {H : Type v} [group H] (φ : G →* H) (ψ : H → G) (hφ : φ) :

The canonical isomorphism G/(ker φ) ≃* H induced by a homomorphism φ : G →* H with a right inverse ψ : H → G.

Equations
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φ : φ) :

The canonical isomorphism G/(ker φ) ≃+ H induced by a homomorphism φ : G →+ H with a right inverse ψ : H → G.

@[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φ : φ) (ᾰ : quotient_group.quotient φ.ker) :
@[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φ : φ) (ᾰ : H) :
=
@[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φ : φ) (ᾰ : H) :
=
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.

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.

Equations
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
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.

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.

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) :

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.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) :

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.

Equations
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) :

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.

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

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

@[instance]
def quotient_group.map_normal {G : Type u} [group G] (N : subgroup G) [nN : N.normal] (M : subgroup G) [nM : M.normal] :
M).normal
@[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) :

The map from the third isomorphism theorem for additive groups: (A / N) / (M / N) → A / M.

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) :

The map from the third isomorphism theorem for groups: (G / N) / (M / N) → G / M.

Equations
@[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)  :
= 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 : quotient_group.quotient N) :
= h) x
theorem quotient_group.quotient_quotient_equiv_quotient_aux_coe_coe {G : Type u} [group G] (N : subgroup G) [nN : N.normal] (M : subgroup G) [nM : M.normal] (h : N M) (x : G) :
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) :

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) :

Noether's third isomorphism theorem for additive groups: (A / N) / (M / N) ≃ A / M.