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

TODO #

Noether's third isomorphism theorem

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

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 subgroup.comap f M) :

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

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

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.

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

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

Equations

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

The canonical isomorphism G/(ker φ) ≃+ H induced by a surjection φ : G →+ H.

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.

Equations

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

Equations

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

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 (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