# 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 / N) / (M / N) and G / M, where N ≤ M.

## 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]

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]
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
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]
@[simp]
theorem quotient_group.mk'_apply {G : Type u} [group G] (N : subgroup G) [nN : N.normal] (x : G) :
x = x
@[simp]
theorem quotient_add_group.mk'_apply {G : Type u} [add_group G] (N : add_subgroup G) [nN : N.normal] (x : G) :
= x
theorem quotient_group.mk'_surjective {G : Type u} [group G] (N : subgroup G) [nN : N.normal] :
theorem quotient_group.mk'_eq_mk' {G : Type u} [group G] (N : subgroup G) [nN : N.normal] {x y : G} :
x = 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} :
= ∃ (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 = 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 = g.comp ) :
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) :
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
@[protected, instance]
Equations
@[protected, instance]
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_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
• HN = φ _
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
• HN = _
@[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 ) :
G N →+ H M

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

Equations
• h = _
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 ) :
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 ) (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) :
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) :
= φ 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.ker_lift_injective {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) :
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
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) :
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φ : φ) (ᾰ : 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φ : φ) :
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φ : φ) :
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φ : φ) (ᾰ : 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φ : φ) (ᾰ : 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) :
=
@[simp]
theorem quotient_group.quotient_bot_symm_apply {G : Type u} [group G] (ᾰ : G) :

The canonical isomorphism G/⊥ ≃+ G.

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

The canonical isomorphism G/⊥ ≃* G.

Equations
@[simp]
theorem quotient_group.quotient_bot_apply {G : Type u} [group G] (ᾰ : G .ker) :
@[simp]
theorem quotient_add_group.quotient_bot_symm_apply {G : Type u} [add_group G] (ᾰ : G) :
@[simp]
theorem quotient_add_group.quotient_bot_apply {G : Type u} [add_group G] (ᾰ : 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 φ) :
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
@[simp]
theorem quotient_group.equiv_quotient_of_eq_mk {G : Type u} [group G] {M N : subgroup G} [M.normal] [N.normal] (h : M = N) (x : G) :
@[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) :

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_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) :
= ( 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) :

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
def quotient_group.hom_quotient_zpow_of_hom {A B : Type u} [comm_group A] [comm_group B] (f : A →* B) (n : ) :

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

Equations
def quotient_add_group.hom_quotient_zsmul_of_hom {A B : Type u} (f : A →+ B) (n : ) :

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

Equations
@[simp]
theorem quotient_group.hom_quotient_zpow_of_hom_id {A : Type u} [comm_group A] (n : ) :
@[simp]
theorem quotient_group.hom_quotient_zpow_of_hom_comp {A B : Type u} [comm_group A] [comm_group B] (f : A →* B) (g : B →* A) (n : ) :
theorem quotient_add_group.hom_quotient_zsmul_of_hom_comp {A B : Type u} (f : A →+ B) (g : B →+ A) (n : ) :
@[simp]
theorem quotient_group.hom_quotient_zpow_of_hom_comp_of_right_inverse {A B : Type u} [comm_group A] [comm_group B] (f : A →* B) (g : B →* A) (n : ) (i : f) :
theorem quotient_add_group.hom_quotient_zsmul_of_hom_comp_of_right_inverse {A B : Type u} (f : A →+ B) (g : B →+ A) (n : ) (i : f) :
def quotient_group.equiv_quotient_zpow_of_equiv {A B : Type u} [comm_group A] [comm_group B] (e : A ≃* B) (n : ) :

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

Equations
def quotient_add_group.equiv_quotient_zsmul_of_equiv {A B : Type u} (e : A ≃+ B) (n : ) :

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

Equations
@[simp]
@[simp]
theorem quotient_group.equiv_quotient_zpow_of_equiv_symm {A B : Type u} [comm_group A] [comm_group B] (e : A ≃* B) (n : ) :
theorem quotient_add_group.equiv_quotient_zsmul_of_equiv_symm {A B : Type u} (e : A ≃+ B) (n : ) :
@[simp]
theorem quotient_group.equiv_quotient_zpow_of_equiv_trans {A B C : Type u} [comm_group A] [comm_group B] [comm_group C] (e : A ≃* B) (d : B ≃* C) (n : ) :
theorem quotient_add_group.equiv_quotient_zsmul_of_equiv_trans {A B C : Type u} (e : A ≃+ B) (d : B ≃+ C) (n : ) :
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

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] :
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) →+ 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) →* G 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) (x : G N) :
= 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) :
= 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) :
(G N) ≃* 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) ≃+ G M

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.

theorem quotient_group.comap_comap_center {G : Type u} [group G] {H₁ : subgroup G} [H₁.normal] {H₂ : subgroup (G H₁)} [H₂.normal] :
(subgroup.center ((G H₁) H₂))) = (subgroup.center (G 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) :

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