# mathlib3documentation

group_theory.quotient_group

# Quotients of groups by normal subgroups #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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_hom`s 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_hom`s 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. `lift`s) 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. `lift`s) 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)
theorem quotient_add_group.map_id_apply {G : Type u} [add_group G] (N : add_subgroup G) [nN : N.normal] (h : := _) (x : G N) :
h) x = x
theorem quotient_group.map_id_apply {G : Type u} [group G] (N : subgroup G) [nN : N.normal] (h : N := _) (x : G N) :
h) x = x
@[simp]
theorem quotient_add_group.map_id {G : Type u} [add_group G] (N : add_subgroup G) [nN : N.normal] (h : := _) :
@[simp]
theorem quotient_group.map_id {G : Type u} [group G] (N : subgroup G) [nN : N.normal] (h : N := _) :
@[simp]
theorem quotient_add_group.map_map {G : Type u} [add_group G] (N : add_subgroup G) [nN : N.normal] {H : Type v} [add_group H] {I : Type u_1} [add_group I] (M : add_subgroup H) (O : add_subgroup I) [M.normal] [O.normal] (f : G →+ H) (g : H →+ I) (hf : N ) (hg : M ) (hgf : N add_subgroup.comap (g.comp f) O := _) (x : G N) :
g hg) ( f hf) x) = (g.comp f) hgf) x
@[simp]
theorem quotient_group.map_map {G : Type u} [group G] (N : subgroup G) [nN : N.normal] {H : Type v} [group H] {I : Type u_1} [group I] (M : subgroup H) (O : subgroup I) [M.normal] [O.normal] (f : G →* H) (g : H →* I) (hf : N ) (hg : M ) (hgf : N subgroup.comap (g.comp f) O := _) (x : G N) :
g hg) ( f hf) x) = (g.comp f) hgf) x
@[simp]
theorem quotient_add_group.map_comp_map {G : Type u} [add_group G] (N : add_subgroup G) [nN : N.normal] {H : Type v} [add_group H] {I : Type u_1} [add_group I] (M : add_subgroup H) (O : add_subgroup I) [M.normal] [O.normal] (f : G →+ H) (g : H →+ I) (hf : N ) (hg : M ) (hgf : N add_subgroup.comap (g.comp f) O := _) :
g hg).comp f hf) = (g.comp f) hgf
@[simp]
theorem quotient_group.map_comp_map {G : Type u} [group G] (N : subgroup G) [nN : N.normal] {H : Type v} [group H] {I : Type u_1} [group I] (M : subgroup H) (O : subgroup I) [M.normal] [O.normal] (f : G →* H) (g : H →* I) (hf : N ) (hg : M ) (hgf : N subgroup.comap (g.comp f) O := _) :
g hg).comp f hf) = (g.comp f) hgf
def quotient_add_group.congr {G : Type u} [add_group G] {H : Type v} [add_group H] (G' : add_subgroup G) (H' : add_subgroup H) [G'.normal] [H'.normal] (e : G ≃+ H) (he : = H') :
G G' ≃+ H H'

`quotient_add_group.congr` lifts the isomorphism `e : G ≃ H` to `G ⧸ G' ≃ H ⧸ H'`, given that `e` maps `G` to `H`.

Equations
def quotient_group.congr {G : Type u} [group G] {H : Type v} [group H] (G' : subgroup G) (H' : subgroup H) [G'.normal] [H'.normal] (e : G ≃* H) (he : G' = H') :
G G' ≃* H H'

`quotient_group.congr` lifts the isomorphism `e : G ≃ H` to `G ⧸ G' ≃ H ⧸ H'`, given that `e` maps `G` to `H`.

Equations
@[simp]
theorem quotient_group.congr_mk {G : Type u} [group G] {H : Type v} [group H] (G' : subgroup G) (H' : subgroup H) [G'.normal] [H'.normal] (e : G ≃* H) (he : G' = H') (x : G) :
H' e he) = (e x)
theorem quotient_group.congr_mk' {G : Type u} [group G] {H : Type v} [group H] (G' : subgroup G) (H' : subgroup H) [G'.normal] [H'.normal] (e : G ≃* H) (he : G' = H') (x : G) :
H' e he) ( x) = (e x)
@[simp]
theorem quotient_group.congr_apply {G : Type u} [group G] {H : Type v} [group H] (G' : subgroup G) (H' : subgroup H) [G'.normal] [H'.normal] (e : G ≃* H) (he : G' = H') (x : G) :
H' e he) x = (e x)
@[simp]
theorem quotient_group.congr_refl {G : Type u} [group G] (G' : subgroup G) [G'.normal] (he : G' = G' := _) :
G' he = mul_equiv.refl (G G')
@[simp]
theorem quotient_group.congr_symm {G : Type u} [group G] {H : Type v} [group H] (G' : subgroup G) (H' : subgroup H) [G'.normal] [H'.normal] (e : G ≃* H) (he : G' = H') :
H' e he).symm = G' e.symm _
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

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

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

Equations
def quotient_group.quotient_mul_equiv_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
@[simp]
theorem quotient_add_group.quotient_add_equiv_of_eq_mk {G : Type u} [add_group G] {M N : add_subgroup G} [M.normal] [N.normal] (h : M = N) (x : G) :
@[simp]
theorem quotient_group.quotient_mul_equiv_of_eq_mk {G : Type u} [group G] {M N : 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

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

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

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.

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