mathlib documentation

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 #

Main statements #

Tags #

isomorphism theorems, quotient groups

@[protected]
def quotient_group.con {G : Type u} [group G] (N : subgroup G) [nN : N.normal] :
con G

The congruence relation generated by a normal subgroup.

Equations
@[protected]
def quotient_add_group.con {G : Type u} [add_group G] (N : add_subgroup G) [nN : N.normal] :

The additive congruence relation generated by a normal additive subgroup.

Equations
@[protected, instance]
def quotient_group.quotient.group {G : Type u} [group G] (N : subgroup G) [nN : N.normal] :
group (G N)
Equations
@[protected, instance]
def quotient_add_group.add_group {G : Type u} [add_group G] (N : add_subgroup G) [nN : N.normal] :
Equations
def quotient_group.mk' {G : Type u} [group G] (N : subgroup G) [nN : N.normal] :
G →* G N

The group homomorphism from G to G/N.

Equations
def quotient_add_group.mk' {G : Type u} [add_group G] (N : add_subgroup G) [nN : N.normal] :
G →+ G N

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] :
@[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) :
@[simp]
theorem quotient_add_group.mk'_apply {G : Type u} [add_group G] (N : add_subgroup G) [nN : N.normal] (x : G) :
theorem quotient_group.mk'_eq_mk' {G : Type u} [group G] (N : subgroup G) [nN : N.normal] {x y : G} :
(quotient_group.mk' N) x = (quotient_group.mk' N) y ∃ (z : G) (H : z N), x * z = y
theorem quotient_add_group.mk'_eq_mk' {G : Type u} [add_group G] (N : add_subgroup G) [nN : N.normal] {x y : G} :
(quotient_add_group.mk' N) x = (quotient_add_group.mk' N) y ∃ (z : G) (H : z N), x + z = y
@[ext]
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.

See note [partially-applied ext lemmas].

@[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.

See note [partially-applied ext lemmas].

@[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]
theorem quotient_add_group.ker_mk {G : Type u} [add_group G] (N : add_subgroup G) [nN : N.normal] :
@[simp]
theorem quotient_group.ker_mk {G : Type u} [group G] (N : subgroup G) [nN : N.normal] :
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
@[simp]
theorem quotient_group.coe_one {G : Type u} [group G] (N : subgroup G) [nN : N.normal] :
1 = 1
@[simp]
theorem quotient_add_group.coe_zero {G : Type u} [add_group G] (N : add_subgroup G) [nN : N.normal] :
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]
theorem quotient_add_group.coe_add {G : Type u} [add_group G] (N : add_subgroup G) [nN : N.normal] (a b : G) :
(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_div {G : Type u} [group G] (N : subgroup G) [nN : N.normal] (a b : G) :
(a / b) = a / b
@[simp]
theorem quotient_add_group.coe_sub {G : Type u} [add_group G] (N : add_subgroup G) [nN : N.normal] (a b : G) :
(a - b) = a - b
@[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_add_group.coe_nsmul {G : Type u} [add_group G] (N : add_subgroup G) [nN : N.normal] (a : G) (n : ) :
(n a) = n a
@[simp]
theorem quotient_group.coe_zpow {G : Type u} [group G] (N : subgroup G) [nN : N.normal] (a : G) (n : ) :
(a ^ n) = a ^ n
@[simp]
theorem quotient_add_group.coe_zsmul {G : Type u} [add_group G] (N : add_subgroup G) [nN : N.normal] (a : G) (n : ) :
(n a) = n a
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) :
G N →* H

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) :
G N →+ H

An add_group homomorphism φ : G →+ H with N ⊆ ker(φ) descends (i.e. lifts) to a group homomorphism G/N →* H.

Equations
@[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) :
@[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) :
@[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) :
@[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) :
@[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) :
(quotient_group.lift N φ 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) :
(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) :
G N →+ H M

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

Equations
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) :
G N →* H M

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 subgroup.comap f M) (x : G) :
@[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) :
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) :
def quotient_add_group.ker_lift {G : Type u} [add_group G] {H : Type v} [add_group H] (φ : G →+ H) :
G φ.ker →+ H

The induced map from the quotient by the kernel to the codomain.

Equations
def quotient_group.ker_lift {G : Type u} [group G] {H : Type v} [group H] (φ : G →* H) :
G φ.ker →* 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) :
@[simp]
theorem quotient_group.ker_lift_mk {G : Type u} [group G] {H : Type v} [group H] (φ : G →* H) (g : G) :
@[simp]
theorem quotient_group.ker_lift_mk' {G : Type u} [group G] {H : Type v} [group H] (φ : G →* H) (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) :
def quotient_group.range_ker_lift {G : Type u} [group G] {H : Type v} [group H] (φ : G →* H) :
G φ.ker →* (φ.range)

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) :
G φ.ker →+ (φ.range)

The induced map from the quotient by the kernel to the range.

Equations
noncomputable def quotient_group.quotient_ker_equiv_range {G : Type u} [group G] {H : Type v} [group H] (φ : G →* H) :
G φ.ker ≃* (φ.range)

Noether's first isomorphism theorem (a definition): the canonical isomorphism between G/(ker φ) to range φ.

Equations
noncomputable def quotient_add_group.quotient_ker_equiv_range {G : Type u} [add_group G] {H : Type v} [add_group H] (φ : G →+ H) :
G φ.ker ≃+ (φ.range)

The first isomorphism theorem (a definition): the canonical isomorphism between G/(ker φ) to range φ.

Equations
@[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 ψ φ) :
G φ.ker ≃* 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φ : function.right_inverse ψ φ) :
G φ.ker ≃+ H

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

Equations
@[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) :
@[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) :
@[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) :
def quotient_add_group.quotient_bot {G : Type u} [add_group G] :

The canonical isomorphism G/⊥ ≃+ G.

Equations
def quotient_group.quotient_bot {G : Type u} [group G] :

The canonical isomorphism G/⊥ ≃* G.

Equations
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 φ) :
G φ.ker ≃+ H

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.

Equations
noncomputable def quotient_group.quotient_ker_equiv_of_surjective {G : Type u} [group G] {H : Type v} [group H] (φ : G →* H) (hφ : function.surjective φ) :
G φ.ker ≃* H

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) :
G M ≃* G 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) :
G M ≃+ G N

If two normal subgroups M and N of G are the same, their quotient groups are isomorphic.

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

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

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

Equations

The map of quotients by powers of an integer induced by a group homomorphism.

Equations

The map of quotients by multiples of an integer induced by an additive group homomorphism.

Equations

The equivalence of quotients by powers of an integer induced by a group isomorphism.

Equations

The equivalence of quotients by multiples of an integer induced by an additive group isomorphism.

Equations

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

Equations
@[protected, instance]
def quotient_group.map_normal {G : Type u} [group G] (N : subgroup G) [nN : N.normal] (M : subgroup G) [nM : M.normal] :
@[protected, instance]

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

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

Equations
@[simp]
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

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

Equations

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

If the quotient by a subgroup gives a singleton then the subgroup is the whole group.

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

If F and H are finite such that ker(G →* H) ≤ im(F →* G), then G is finite.

Equations
noncomputable def add_group.fintype_of_ker_le_range {F G H : Type u} [add_group F] [add_group G] [add_group H] [fintype F] [fintype H] (f : F →+ G) (g : G →+ H) (h : g.ker f.range) :

If F and H are finite such that ker(G →+ H) ≤ im(F →+ G), then G is finite.

Equations
noncomputable def add_group.fintype_of_ker_eq_range {F G H : Type u} [add_group F] [add_group G] [add_group H] [fintype F] [fintype H] (f : F →+ G) (g : G →+ H) (h : g.ker = f.range) :

If F and H are finite such that ker(G →+ H) = im(F →+ G), then G is finite.

Equations
noncomputable def group.fintype_of_ker_eq_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) :

If F and H are finite such that ker(G →* H) = im(F →* G), then G is finite.

Equations
noncomputable def add_group.fintype_of_ker_of_codom {G H : Type u} [add_group G] [add_group H] [fintype H] (g : G →+ H) [fintype (g.ker)] :

If ker(G →+ H) and H are finite, then G is finite.

Equations
noncomputable def group.fintype_of_ker_of_codom {G H : Type u} [group G] [group H] [fintype H] (g : G →* H) [fintype (g.ker)] :

If ker(G →* H) and H are finite, then G is finite.

Equations
noncomputable def add_group.fintype_of_dom_of_coker {F G : Type u} [add_group F] [add_group G] [fintype F] (f : F →+ G) [f.range.normal] [fintype (G f.range)] :

If F and coker(F →+ G) are finite, then G is finite.

Equations
noncomputable def group.fintype_of_dom_of_coker {F G : Type u} [group F] [group G] [fintype F] (f : F →* G) [f.range.normal] [fintype (G f.range)] :

If F and coker(F →* G) are finite, then G is finite.

Equations