Quotients of groups by normal subgroups

This file develops the basic theory of quotients of groups by normal subgroups. In particular, it proves Noether's first and second isomorphism theorems.

Main statements

• QuotientGroup.quotientKerEquivRange: Noether's first isomorphism theorem, an explicit isomorphism G/ker φ → range φ for every group homomorphism φ : G →* H.
• QuotientGroup.quotientInfEquivProdNormalizerQuotient: Noether's second isomorphism theorem, an explicit isomorphism between H/(H ∩ N) and (HN)/N given a subgroup H that lies in the normalizer N_G(N) of a subgroup N of a group G.
• QuotientGroup.quotientQuotientEquivQuotient: Noether's third isomorphism theorem, the canonical isomorphism between (G / N) / (M / N) and G / M, where N ≤ M.
• QuotientGroup.comapMk'OrderIso: The correspondence theorem, a lattice isomorphism between the lattice of subgroups of G ⧸ N and the sublattice of subgroups of G containing N.

Tags

isomorphism theorems, quotient groups

theorem QuotientGroup.sound {G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] (U : Set (G ⧸ N)) (g : ↥N.op) : g • ⇑(mk' N) ⁻¹' U = ⇑(mk' N) ⁻¹' U

theorem QuotientAddGroup.sound {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : N.Normal] (U : Set (G ⧸ N)) (g : ↥N.op) : g +ᵥ ⇑(mk' N) ⁻¹' U = ⇑(mk' N) ⁻¹' U

@[simp]

theorem QuotientGroup.mk_prod {G : Type u_1} {ι : Type u_2} [CommGroup G] (N : Subgroup G) (s : Finset ι) {f : ι → G} : ↑(s.prod f) = ∏ i ∈ s, ↑(f i)

@[simp]

theorem QuotientAddGroup.mk_sum {G : Type u_1} {ι : Type u_2} [AddCommGroup G] (N : AddSubgroup G) (s : Finset ι) {f : ι → G} : ↑(s.sum f) = ∑ i ∈ s, ↑(f i)

theorem QuotientGroup.strictMono_comap_prod_map {G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] : StrictMono fun (H : Subgroup G) => (Subgroup.comap N.subtype H, Subgroup.map (mk' N) H)

theorem QuotientAddGroup.strictMono_comap_prod_map {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : N.Normal] : StrictMono fun (H : AddSubgroup G) => (AddSubgroup.comap N.subtype H, AddSubgroup.map (mk' N) H)

def QuotientGroup.kerLift {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.

def QuotientAddGroup.kerLift {G : Type u} [AddGroup G] {H : Type v} [AddGroup H] (φ : G →+ H) : G ⧸ φ.ker →+ H

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

@[simp]

theorem QuotientGroup.kerLift_mk {G : Type u} [Group G] {H : Type v} [Group H] (φ : G →* H) (g : G) : (kerLift φ) ↑g = φ g

@[simp]

theorem QuotientAddGroup.kerLift_mk {G : Type u} [AddGroup G] {H : Type v} [AddGroup H] (φ : G →+ H) (g : G) : (kerLift φ) ↑g = φ g

@[deprecated QuotientAddGroup.kerLift_mk (since := "2025-10-28")]

theorem QuotientAddGroup.kerLift_mk' {G : Type u} [AddGroup G] {H : Type v} [AddGroup H] (φ : G →+ H) (g : G) : (kerLift φ) ↑g = φ g

Alias of QuotientAddGroup.kerLift_mk.

@[deprecated QuotientGroup.kerLift_mk (since := "2025-10-28")]

theorem QuotientGroup.kerLift_mk' {G : Type u} [Group G] {H : Type v} [Group H] (φ : G →* H) (g : G) : (kerLift φ) ↑g = φ g

Alias of QuotientGroup.kerLift_mk.

theorem QuotientGroup.kerLift_injective {G : Type u} [Group G] {H : Type v} [Group H] (φ : G →* H) : Function.Injective ⇑(kerLift φ)

theorem QuotientAddGroup.kerLift_injective {G : Type u} [AddGroup G] {H : Type v} [AddGroup H] (φ : G →+ H) : Function.Injective ⇑(kerLift φ)

def QuotientGroup.rangeKerLift {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.

def QuotientAddGroup.rangeKerLift {G : Type u} [AddGroup G] {H : Type v} [AddGroup H] (φ : G →+ H) : G ⧸ φ.ker →+ ↥φ.range

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

theorem QuotientGroup.rangeKerLift_injective {G : Type u} [Group G] {H : Type v} [Group H] (φ : G →* H) : Function.Injective ⇑(rangeKerLift φ)

theorem QuotientAddGroup.rangeKerLift_injective {G : Type u} [AddGroup G] {H : Type v} [AddGroup H] (φ : G →+ H) : Function.Injective ⇑(rangeKerLift φ)

theorem QuotientGroup.rangeKerLift_surjective {G : Type u} [Group G] {H : Type v} [Group H] (φ : G →* H) : Function.Surjective ⇑(rangeKerLift φ)

theorem QuotientAddGroup.rangeKerLift_surjective {G : Type u} [AddGroup G] {H : Type v} [AddGroup H] (φ : G →+ H) : Function.Surjective ⇑(rangeKerLift φ)

noncomputable def QuotientGroup.quotientKerEquivRange {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 φ.

noncomputable def QuotientAddGroup.quotientKerEquivRange {G : Type u} [AddGroup G] {H : Type v} [AddGroup H] (φ : G →+ H) : G ⧸ φ.ker ≃+ ↥φ.range

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

def QuotientGroup.quotientKerEquivOfRightInverse {G : Type u} [Group G] {H : Type v} [Group H] (φ : G →* H) (ψ : H → G) (hφ : Function.RightInverse ψ ⇑φ) : G ⧸ φ.ker ≃* H

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

def QuotientAddGroup.quotientKerEquivOfRightInverse {G : Type u} [AddGroup G] {H : Type v} [AddGroup H] (φ : G →+ H) (ψ : H → G) (hφ : Function.RightInverse ψ ⇑φ) : G ⧸ φ.ker ≃+ H

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

@[simp]

theorem QuotientAddGroup.quotientKerEquivOfRightInverse_symm_apply {G : Type u} [AddGroup G] {H : Type v} [AddGroup H] (φ : G →+ H) (ψ : H → G) (hφ : Function.RightInverse ψ ⇑φ) (a✝ : H) : (quotientKerEquivOfRightInverse φ ψ hφ).symm a✝ = (mk ∘ ψ) a✝

@[simp]

theorem QuotientGroup.quotientKerEquivOfRightInverse_apply {G : Type u} [Group G] {H : Type v} [Group H] (φ : G →* H) (ψ : H → G) (hφ : Function.RightInverse ψ ⇑φ) (a : G ⧸ φ.ker) : (quotientKerEquivOfRightInverse φ ψ hφ) a = (kerLift φ) a

@[simp]

theorem QuotientAddGroup.quotientKerEquivOfRightInverse_apply {G : Type u} [AddGroup G] {H : Type v} [AddGroup H] (φ : G →+ H) (ψ : H → G) (hφ : Function.RightInverse ψ ⇑φ) (a : G ⧸ φ.ker) : (quotientKerEquivOfRightInverse φ ψ hφ) a = (kerLift φ) a

@[simp]

theorem QuotientGroup.quotientKerEquivOfRightInverse_symm_apply {G : Type u} [Group G] {H : Type v} [Group H] (φ : G →* H) (ψ : H → G) (hφ : Function.RightInverse ψ ⇑φ) (a✝ : H) : (quotientKerEquivOfRightInverse φ ψ hφ).symm a✝ = (mk ∘ ψ) a✝

def QuotientGroup.quotientBot {G : Type u} [Group G] : G ⧸ ⊥ ≃* G

The canonical isomorphism G/⊥ ≃* G.

def QuotientAddGroup.quotientBot {G : Type u} [AddGroup G] : G ⧸ ⊥ ≃+ G

The canonical isomorphism G/⊥ ≃+ G.

@[simp]

theorem QuotientGroup.quotientBot_symm_apply {G : Type u} [Group G] (a✝ : G) : quotientBot.symm a✝ = ↑a✝

@[simp]

theorem QuotientAddGroup.quotientBot_apply {G : Type u} [AddGroup G] (a : G ⧸ (AddMonoidHom.id G).ker) : quotientBot a = (kerLift (AddMonoidHom.id G)) a

@[simp]

theorem QuotientGroup.quotientBot_apply {G : Type u} [Group G] (a : G ⧸ (MonoidHom.id G).ker) : quotientBot a = (kerLift (MonoidHom.id G)) a

@[simp]

theorem QuotientAddGroup.quotientBot_symm_apply {G : Type u} [AddGroup G] (a✝ : G) : quotientBot.symm a✝ = ↑a✝

noncomputable def QuotientGroup.quotientKerEquivOfSurjective {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 QuotientGroup.quotientKerEquivOfRightInverse.

noncomputable def QuotientAddGroup.quotientKerEquivOfSurjective {G : Type u} [AddGroup G] {H : Type v} [AddGroup 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 QuotientAddGroup.quotientKerEquivOfRightInverse.

def QuotientGroup.quotientMulEquivOfEq {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.

def QuotientAddGroup.quotientAddEquivOfEq {G : Type u} [AddGroup G] {M N : AddSubgroup 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.

@[simp]

theorem QuotientGroup.quotientMulEquivOfEq_mk {G : Type u} [Group G] {M N : Subgroup G} [M.Normal] [N.Normal] (h : M = N) (x : G) : (quotientMulEquivOfEq h) ↑x = ↑x

@[simp]

theorem QuotientAddGroup.quotientAddEquivOfEq_mk {G : Type u} [AddGroup G] {M N : AddSubgroup G} [M.Normal] [N.Normal] (h : M = N) (x : G) : (quotientAddEquivOfEq h) ↑x = ↑x

def QuotientGroup.quotientMapSubgroupOfOfLe {G : Type u} [Group G] {A' A B' B : Subgroup G} [_hAN : (A'.subgroupOf A).Normal] [_hBN : (B'.subgroupOf B).Normal] (h' : A' ≤ B') (h : A ≤ B) : ↥A ⧸ A'.subgroupOf A →* ↥B ⧸ B'.subgroupOf 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.

def QuotientAddGroup.quotientMapAddSubgroupOfOfLe {G : Type u} [AddGroup G] {A' A B' B : AddSubgroup G} [_hAN : (A'.addSubgroupOf A).Normal] [_hBN : (B'.addSubgroupOf B).Normal] (h' : A' ≤ B') (h : A ≤ B) : ↥A ⧸ A'.addSubgroupOf A →+ ↥B ⧸ B'.addSubgroupOf 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.

@[simp]

theorem QuotientGroup.quotientMapSubgroupOfOfLe_mk {G : Type u} [Group G] {A' A B' B : Subgroup G} [_hAN : (A'.subgroupOf A).Normal] [_hBN : (B'.subgroupOf B).Normal] (h' : A' ≤ B') (h : A ≤ B) (x : ↥A) : (quotientMapSubgroupOfOfLe h' h) ↑x = ↑((Subgroup.inclusion h) x)

@[simp]

theorem QuotientAddGroup.quotientMapAddSubgroupOfOfLe_mk {G : Type u} [AddGroup G] {A' A B' B : AddSubgroup G} [_hAN : (A'.addSubgroupOf A).Normal] [_hBN : (B'.addSubgroupOf B).Normal] (h' : A' ≤ B') (h : A ≤ B) (x : ↥A) : (quotientMapAddSubgroupOfOfLe h' h) ↑x = ↑((AddSubgroup.inclusion h) x)

def QuotientGroup.equivQuotientSubgroupOfOfEq {G : Type u} [Group G] {A' A B' B : Subgroup G} [hAN : (A'.subgroupOf A).Normal] [hBN : (B'.subgroupOf B).Normal] (h' : A' = B') (h : A = B) : ↥A ⧸ A'.subgroupOf A ≃* ↥B ⧸ B'.subgroupOf 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'.subgroupOf A : Subgroup A) depends on A.

def QuotientAddGroup.equivQuotientAddSubgroupOfOfEq {G : Type u} [AddGroup G] {A' A B' B : AddSubgroup G} [hAN : (A'.addSubgroupOf A).Normal] [hBN : (B'.addSubgroupOf B).Normal] (h' : A' = B') (h : A = B) : ↥A ⧸ A'.addSubgroupOf A ≃+ ↥B ⧸ B'.addSubgroupOf 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'.addSubgroupOf A : AddSubgroup A) depends on A.

def QuotientGroup.homQuotientZPowOfHom {A B : Type u} [CommGroup A] [CommGroup B] (f : A →* B) (n : ℤ) : A ⧸ (zpowGroupHom n).range →* B ⧸ (zpowGroupHom n).range

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

def QuotientAddGroup.homQuotientZSMulOfHom {A B : Type u} [AddCommGroup A] [AddCommGroup B] (f : A →+ B) (n : ℤ) : A ⧸ (zsmulAddGroupHom n).range →+ B ⧸ (zsmulAddGroupHom n).range

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

@[simp]

theorem QuotientGroup.homQuotientZPowOfHom_id {A : Type u} [CommGroup A] (n : ℤ) : homQuotientZPowOfHom (MonoidHom.id A) n = MonoidHom.id (A ⧸ (zpowGroupHom n).range)

@[simp]

theorem QuotientAddGroup.homQuotientZSMulOfHom_id {A : Type u} [AddCommGroup A] (n : ℤ) : homQuotientZSMulOfHom (AddMonoidHom.id A) n = AddMonoidHom.id (A ⧸ (zsmulAddGroupHom n).range)

@[simp]

theorem QuotientGroup.homQuotientZPowOfHom_comp {A B : Type u} [CommGroup A] [CommGroup B] (f : A →* B) (g : B →* A) (n : ℤ) : homQuotientZPowOfHom (f.comp g) n = (homQuotientZPowOfHom f n).comp (homQuotientZPowOfHom g n)

@[simp]

theorem QuotientAddGroup.homQuotientZSMulOfHom_comp {A B : Type u} [AddCommGroup A] [AddCommGroup B] (f : A →+ B) (g : B →+ A) (n : ℤ) : homQuotientZSMulOfHom (f.comp g) n = (homQuotientZSMulOfHom f n).comp (homQuotientZSMulOfHom g n)

@[simp]

theorem QuotientGroup.homQuotientZPowOfHom_comp_of_rightInverse {A B : Type u} [CommGroup A] [CommGroup B] (f : A →* B) (g : B →* A) (n : ℤ) (i : Function.RightInverse ⇑g ⇑f) : (homQuotientZPowOfHom f n).comp (homQuotientZPowOfHom g n) = MonoidHom.id (B ⧸ (zpowGroupHom n).range)

@[simp]

theorem QuotientAddGroup.homQuotientZSMulOfHom_comp_of_rightInverse {A B : Type u} [AddCommGroup A] [AddCommGroup B] (f : A →+ B) (g : B →+ A) (n : ℤ) (i : Function.RightInverse ⇑g ⇑f) : (homQuotientZSMulOfHom f n).comp (homQuotientZSMulOfHom g n) = AddMonoidHom.id (B ⧸ (zsmulAddGroupHom n).range)

def QuotientGroup.equivQuotientZPowOfEquiv {A B : Type u} [CommGroup A] [CommGroup B] (e : A ≃* B) (n : ℤ) : A ⧸ (zpowGroupHom n).range ≃* B ⧸ (zpowGroupHom n).range

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

def QuotientAddGroup.equivQuotientZSMulOfEquiv {A B : Type u} [AddCommGroup A] [AddCommGroup B] (e : A ≃+ B) (n : ℤ) : A ⧸ (zsmulAddGroupHom n).range ≃+ B ⧸ (zsmulAddGroupHom n).range

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

@[simp]

theorem QuotientGroup.equivQuotientZPowOfEquiv_refl {A : Type u} [CommGroup A] (n : ℤ) : MulEquiv.refl (A ⧸ (zpowGroupHom n).range) = equivQuotientZPowOfEquiv (MulEquiv.refl A) n

@[simp]

theorem QuotientAddGroup.equivQuotientZSMulOfEquiv_refl {A : Type u} [AddCommGroup A] (n : ℤ) : AddEquiv.refl (A ⧸ (zsmulAddGroupHom n).range) = equivQuotientZSMulOfEquiv (AddEquiv.refl A) n

@[simp]

theorem QuotientGroup.equivQuotientZPowOfEquiv_symm {A B : Type u} [CommGroup A] [CommGroup B] (e : A ≃* B) (n : ℤ) : (equivQuotientZPowOfEquiv e n).symm = equivQuotientZPowOfEquiv e.symm n

@[simp]

theorem QuotientAddGroup.equivQuotientZSMulOfEquiv_symm {A B : Type u} [AddCommGroup A] [AddCommGroup B] (e : A ≃+ B) (n : ℤ) : (equivQuotientZSMulOfEquiv e n).symm = equivQuotientZSMulOfEquiv e.symm n

@[simp]

theorem QuotientGroup.equivQuotientZPowOfEquiv_trans {A B C : Type u} [CommGroup A] [CommGroup B] [CommGroup C] (e : A ≃* B) (d : B ≃* C) (n : ℤ) : (equivQuotientZPowOfEquiv e n).trans (equivQuotientZPowOfEquiv d n) = equivQuotientZPowOfEquiv (e.trans d) n

@[simp]

theorem QuotientAddGroup.equivQuotientZSMulOfEquiv_trans {A B C : Type u} [AddCommGroup A] [AddCommGroup B] [AddCommGroup C] (e : A ≃+ B) (d : B ≃+ C) (n : ℤ) : (equivQuotientZSMulOfEquiv e n).trans (equivQuotientZSMulOfEquiv d n) = equivQuotientZSMulOfEquiv (e.trans d) n

noncomputable def QuotientGroup.quotientInfEquivProdNormalizerQuotient {G : Type u} [Group G] (H N : Subgroup G) (hLE : H ≤ N.normalizer) : ↥H ⧸ N.subgroupOf H ≃* ↥(H ⊔ N) ⧸ N.subgroupOf (H ⊔ N)

Noether's second isomorphism theorem: given a subgroup N of G and a subgroup H of the normalizer of N in G, defines an isomorphism between H/(H ∩ N) and (HN)/N.

noncomputable def QuotientAddGroup.quotientInfEquivSumNormalizerQuotient {G : Type u} [AddGroup G] (H N : AddSubgroup G) (hLE : H ≤ N.normalizer) : ↥H ⧸ N.addSubgroupOf H ≃+ ↥(H ⊔ N) ⧸ N.addSubgroupOf (H ⊔ N)

Noether's second isomorphism theorem: given a subgroup N of G and a subgroup H of the normalizer of N in G, defines an isomorphism between H/(H ∩ N) and (H + N)/N

noncomputable def QuotientGroup.quotientInfEquivProdNormalQuotient {G : Type u} [Group G] (H N : Subgroup G) [hN : N.Normal] : ↥H ⧸ N.subgroupOf H ≃* ↥(H ⊔ N) ⧸ N.subgroupOf (H ⊔ 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.

noncomputable def QuotientAddGroup.quotientInfEquivSumNormalQuotient {G : Type u} [AddGroup G] (H N : AddSubgroup G) [hN : N.Normal] : ↥H ⧸ N.addSubgroupOf H ≃+ ↥(H ⊔ N) ⧸ N.addSubgroupOf (H ⊔ 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 (H + N)/N.

instance QuotientGroup.map_normal {G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] (M : Subgroup G) [nM : M.Normal] : (Subgroup.map (mk' N) M).Normal

instance QuotientAddGroup.map_normal {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : N.Normal] (M : AddSubgroup G) [nM : M.Normal] : (AddSubgroup.map (mk' N) M).Normal

def QuotientGroup.quotientQuotientEquivQuotientAux {G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] (M : Subgroup G) [nM : M.Normal] (h : N ≤ M) : (G ⧸ N) ⧸ Subgroup.map (mk' N) M →* G ⧸ M

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

def QuotientAddGroup.quotientQuotientEquivQuotientAux {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : N.Normal] (M : AddSubgroup G) [nM : M.Normal] (h : N ≤ M) : (G ⧸ N) ⧸ AddSubgroup.map (mk' N) M →+ G ⧸ M

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

@[simp]

theorem QuotientGroup.quotientQuotientEquivQuotientAux_mk {G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] (M : Subgroup G) [nM : M.Normal] (h : N ≤ M) (x : G ⧸ N) : (quotientQuotientEquivQuotientAux N M h) ↑x = (map N M (MonoidHom.id G) h) x

@[simp]

theorem QuotientAddGroup.quotientQuotientEquivQuotientAux_mk {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : N.Normal] (M : AddSubgroup G) [nM : M.Normal] (h : N ≤ M) (x : G ⧸ N) : (quotientQuotientEquivQuotientAux N M h) ↑x = (map N M (AddMonoidHom.id G) h) x

theorem QuotientGroup.quotientQuotientEquivQuotientAux_mk_mk {G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] (M : Subgroup G) [nM : M.Normal] (h : N ≤ M) (x : G) : (quotientQuotientEquivQuotientAux N M h) ↑↑x = ↑x

theorem QuotientAddGroup.quotientQuotientEquivQuotientAux_mk_mk {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : N.Normal] (M : AddSubgroup G) [nM : M.Normal] (h : N ≤ M) (x : G) : (quotientQuotientEquivQuotientAux N M h) ↑↑x = ↑x

def QuotientGroup.quotientQuotientEquivQuotient {G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] (M : Subgroup G) [nM : M.Normal] (h : N ≤ M) : (G ⧸ N) ⧸ Subgroup.map (mk' N) M ≃* G ⧸ M

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

def QuotientAddGroup.quotientQuotientEquivQuotient {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : N.Normal] (M : AddSubgroup G) [nM : M.Normal] (h : N ≤ M) : (G ⧸ N) ⧸ AddSubgroup.map (mk' N) M ≃+ G ⧸ M

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

theorem QuotientGroup.le_comap_mk' {G : Type u} [Group G] (N : Subgroup G) [N.Normal] (H : Subgroup (G ⧸ N)) : N ≤ Subgroup.comap (mk' N) H

theorem QuotientAddGroup.le_comap_mk' {G : Type u} [AddGroup G] (N : AddSubgroup G) [N.Normal] (H : AddSubgroup (G ⧸ N)) : N ≤ AddSubgroup.comap (mk' N) H

@[simp]

theorem QuotientGroup.comap_map_mk' {G : Type u} [Group G] (N H : Subgroup G) [N.Normal] : Subgroup.comap (mk' N) (Subgroup.map (mk' N) H) = N ⊔ H

@[simp]

theorem QuotientAddGroup.comap_map_mk' {G : Type u} [AddGroup G] (N H : AddSubgroup G) [N.Normal] : AddSubgroup.comap (mk' N) (AddSubgroup.map (mk' N) H) = N ⊔ H

def QuotientGroup.comapMk'OrderIso {G : Type u} [Group G] (N : Subgroup G) [hn : N.Normal] : Subgroup (G ⧸ N) ≃o { H : Subgroup G // N ≤ H }

The correspondence theorem, or lattice theorem, or fourth isomorphism theorem for multiplicative groups

def QuotientAddGroup.comapMk'OrderIso {G : Type u} [AddGroup G] (N : AddSubgroup G) [hn : N.Normal] : AddSubgroup (G ⧸ N) ≃o { H : AddSubgroup G // N ≤ H }

The correspondence theorem, or lattice theorem, or fourth isomorphism theorem for additive groups

theorem QuotientGroup.subsingleton_quotient_top {G : Type u} [Group G] : Subsingleton (G ⧸ ⊤)

theorem QuotientAddGroup.subsingleton_quotient_top {G : Type u} [AddGroup G] : Subsingleton (G ⧸ ⊤)

theorem QuotientGroup.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 QuotientAddGroup.addSubgroup_eq_top_of_subsingleton {G : Type u} [AddGroup G] (H : AddSubgroup G) (h : Subsingleton (G ⧸ H)) : H = ⊤

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

theorem QuotientGroup.comap_comap_center {G : Type u} [Group G] {H₁ : Subgroup G} [H₁.Normal] {H₂ : Subgroup (G ⧸ H₁)} [H₂.Normal] : Subgroup.comap (mk' H₁) (Subgroup.comap (mk' H₂) (Subgroup.center ((G ⧸ H₁) ⧸ H₂))) = Subgroup.comap (mk' (Subgroup.comap (mk' H₁) H₂)) (Subgroup.center (G ⧸ Subgroup.comap (mk' H₁) H₂))

theorem QuotientAddGroup.comap_comap_center {G : Type u} [AddGroup G] {H₁ : AddSubgroup G} [H₁.Normal] {H₂ : AddSubgroup (G ⧸ H₁)} [H₂.Normal] : AddSubgroup.comap (mk' H₁) (AddSubgroup.comap (mk' H₂) (AddSubgroup.center ((G ⧸ H₁) ⧸ H₂))) = AddSubgroup.comap (mk' (AddSubgroup.comap (mk' H₁) H₂)) (AddSubgroup.center (G ⧸ AddSubgroup.comap (mk' H₁) H₂))

theorem Subgroup.Characteristic.comap_quotient_mk {G : Type u} [Group G] {H : Subgroup G} [hH : H.Characteristic] {K : Subgroup (G ⧸ H)} (hK : K.Characteristic) : (comap (QuotientGroup.mk' H) K).Characteristic

theorem AddSubgroup.Characteristic.comap_quotient_mk {G : Type u} [AddGroup G] {H : AddSubgroup G} [hH : H.Characteristic] {K : AddSubgroup (G ⧸ H)} (hK : K.Characteristic) : (comap (QuotientAddGroup.mk' H) K).Characteristic

def MonoidHom.restrictHomKerEquiv {G : Type u} [Group G] (A : Type u_1) [CommGroup A] (H : Subgroup G) [H.Normal] : ↥(restrictHom H A).ker ≃* (G ⧸ H →* A)

The MulEquiv between the kernel of the restriction map to a normal subgroup H of homomorphisms of type G →* A and the group of homomorphisms G ⧸ H →* A.

def AddMonoidHom.restrictHomKerEquiv {G : Type u} [AddGroup G] (A : Type u_1) [AddCommGroup A] (H : AddSubgroup G) [H.Normal] : ↥(restrictHom H A).ker ≃+ (G ⧸ H →+ A)

The AddEquiv between the kernel of the restriction map to a normal subgroup H of homomorphisms of type G →+ A and the group of homomorphisms G ⧸ H →+ A.

@[simp]

theorem MonoidHom.restrictHomKerEquiv_apply_coe {G : Type u} [Group G] (A : Type u_1) [CommGroup A] (H : Subgroup G) [H.Normal] (f : ↥(restrictHom H A).ker) (g : G) : ((restrictHomKerEquiv A H) f) ↑g = ↑f g

@[simp]

theorem MonoidHom.restrictHomKerEquiv_symm_coe_apply {G : Type u} [Group G] (A : Type u_1) [CommGroup A] (H : Subgroup G) [H.Normal] (f : G ⧸ H →* A) (g : G) : ↑((restrictHomKerEquiv A H).symm f) g = f ↑g

@[simp]

theorem QuotientAddGroup.mk_nat_mul {R : Type u_1} [NonAssocRing R] (N : AddSubgroup R) [N.Normal] (n : ℕ) (a : R) : ↑(↑n * a) = n • ↑a

@[simp]

theorem QuotientAddGroup.mk_int_mul {R : Type u_1} [NonAssocRing R] (N : AddSubgroup R) [N.Normal] (n : ℤ) (a : R) : ↑(↑n * a) = n • ↑a