# 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

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

Equations

- QuotientGroup.kerLift φ = QuotientGroup.lift φ.ker φ ⋯

Instances For

source
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.

Equations

- QuotientAddGroup.kerLift φ = QuotientAddGroup.lift φ.ker φ ⋯

Instances For

source
@[simp]
theorem QuotientGroup.kerLift_mk {G : Type u} [Group G] {H : Type v} [Group H] (φ : G →* H) (g : G) :
(kerLift φ) ↑g = φ g
source
@[simp]
theorem QuotientAddGroup.kerLift_mk {G : Type u} [AddGroup G] {H : Type v} [AddGroup H] (φ : G →+ H) (g : G) :
(kerLift φ) ↑g = φ g
source
@[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`.

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

source
theorem QuotientGroup.kerLift_injective {G : Type u} [Group G] {H : Type v} [Group H] (φ : G →* H) :
Function.Injective ⇑(kerLift φ)
source
theorem QuotientAddGroup.kerLift_injective {G : Type u} [AddGroup G] {H : Type v} [AddGroup H] (φ : G →+ H) :
Function.Injective ⇑(kerLift φ)
source
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.

Equations

- QuotientGroup.rangeKerLift φ = QuotientGroup.lift φ.ker φ.rangeRestrict ⋯

Instances For

source
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.

Equations

- QuotientAddGroup.rangeKerLift φ = QuotientAddGroup.lift φ.ker φ.rangeRestrict ⋯

Instances For

source
theorem QuotientGroup.rangeKerLift_injective {G : Type u} [Group G] {H : Type v} [Group H] (φ : G →* H) :
Function.Injective ⇑(rangeKerLift φ)
source
theorem QuotientAddGroup.rangeKerLift_injective {G : Type u} [AddGroup G] {H : Type v} [AddGroup H] (φ : G →+ H) :
Function.Injective ⇑(rangeKerLift φ)
source
theorem QuotientGroup.rangeKerLift_surjective {G : Type u} [Group G] {H : Type v} [Group H] (φ : G →* H) :
Function.Surjective ⇑(rangeKerLift φ)
source
theorem QuotientAddGroup.rangeKerLift_surjective {G : Type u} [AddGroup G] {H : Type v} [AddGroup H] (φ : G →+ H) :
Function.Surjective ⇑(rangeKerLift φ)
source
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 φ`.

Equations

- QuotientGroup.quotientKerEquivRange φ = MulEquiv.ofBijective (QuotientGroup.rangeKerLift φ) ⋯

Instances For

source
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 φ`.

Equations

- QuotientAddGroup.quotientKerEquivRange φ = AddEquiv.ofBijective (QuotientAddGroup.rangeKerLift φ) ⋯

Instances For

source
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`.

Equations

- QuotientGroup.quotientKerEquivOfRightInverse φ ψ hφ = { toFun := ⇑(QuotientGroup.kerLift φ), invFun := QuotientGroup.mk ∘ ψ, left_inv := ⋯, right_inv := hφ, map_mul' := ⋯ }

Instances For

source
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`.

Equations

- QuotientAddGroup.quotientKerEquivOfRightInverse φ ψ hφ = { toFun := ⇑(QuotientAddGroup.kerLift φ), invFun := QuotientAddGroup.mk ∘ ψ, left_inv := ⋯, right_inv := hφ, map_add' := ⋯ }

Instances For

source
@[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✝
source
@[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
source
@[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
source
@[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✝
source
def QuotientGroup.quotientBot {G : Type u} [Group G] :
G ⧸ ⊥ ≃* G

The canonical isomorphism `G/⊥ ≃* G`.

Equations

- QuotientGroup.quotientBot = QuotientGroup.quotientKerEquivOfRightInverse (MonoidHom.id G) id ⋯

Instances For

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

The canonical isomorphism `G/⊥ ≃+ G`.

Equations

- QuotientAddGroup.quotientBot = QuotientAddGroup.quotientKerEquivOfRightInverse (AddMonoidHom.id G) id ⋯

Instances For

source
@[simp]
theorem QuotientAddGroup.quotientBot_symm_apply {G : Type u} [AddGroup G] (a✝ : G) :
quotientBot.symm a✝ = ↑a✝
source
@[simp]
theorem QuotientGroup.quotientBot_symm_apply {G : Type u} [Group G] (a✝ : G) :
quotientBot.symm a✝ = ↑a✝
source
@[simp]
theorem QuotientAddGroup.quotientBot_apply {G : Type u} [AddGroup G] (a : G ⧸ (AddMonoidHom.id G).ker) :
quotientBot a = (kerLift (AddMonoidHom.id G)) a
source
@[simp]
theorem QuotientGroup.quotientBot_apply {G : Type u} [Group G] (a : G ⧸ (MonoidHom.id G).ker) :
quotientBot a = (kerLift (MonoidHom.id G)) a
source
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`.

Equations

- QuotientGroup.quotientKerEquivOfSurjective φ hφ = QuotientGroup.quotientKerEquivOfRightInverse φ (Exists.choose ⋯) ⋯

Instances For

source
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`.

Equations

- QuotientAddGroup.quotientKerEquivOfSurjective φ hφ = QuotientAddGroup.quotientKerEquivOfRightInverse φ (Exists.choose ⋯) ⋯

Instances For

source
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.

Equations

- QuotientGroup.quotientMulEquivOfEq h = { toEquiv := Subgroup.quotientEquivOfEq h, map_mul' := ⋯ }

Instances For

source
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.

Equations

- QuotientAddGroup.quotientAddEquivOfEq h = { toEquiv := AddSubgroup.quotientEquivOfEq h, map_add' := ⋯ }

Instances For

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

Equations

- QuotientGroup.quotientMapSubgroupOfOfLe h' h = QuotientGroup.map (A'.subgroupOf A) (B'.subgroupOf B) (Subgroup.inclusion h) ⋯

Instances For

source
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.

Equations

- QuotientAddGroup.quotientMapAddSubgroupOfOfLe h' h = QuotientAddGroup.map (A'.addSubgroupOf A) (B'.addSubgroupOf B) (AddSubgroup.inclusion h) ⋯

Instances For

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

Equations

- QuotientGroup.equivQuotientSubgroupOfOfEq h' h = (QuotientGroup.quotientMapSubgroupOfOfLe ⋯ ⋯).toMulEquiv (QuotientGroup.quotientMapSubgroupOfOfLe ⋯ ⋯) ⋯ ⋯

Instances For

source
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`.

Equations

- QuotientAddGroup.equivQuotientAddSubgroupOfOfEq h' h = (QuotientAddGroup.quotientMapAddSubgroupOfOfLe ⋯ ⋯).toAddEquiv (QuotientAddGroup.quotientMapAddSubgroupOfOfLe ⋯ ⋯) ⋯ ⋯

Instances For

source
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.

Equations

- QuotientGroup.homQuotientZPowOfHom f n = QuotientGroup.lift (zpowGroupHom n).range ((QuotientGroup.mk' (zpowGroupHom n).range).comp f) ⋯

Instances For

source
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.

Equations

- QuotientAddGroup.homQuotientZSMulOfHom f n = QuotientAddGroup.lift (zsmulAddGroupHom n).range ((QuotientAddGroup.mk' (zsmulAddGroupHom n).range).comp f) ⋯

Instances For

source
@[simp]
theorem QuotientGroup.homQuotientZPowOfHom_id {A : Type u} [CommGroup A] (n : ℤ) :
homQuotientZPowOfHom (MonoidHom.id A) n = MonoidHom.id (A ⧸ (zpowGroupHom n).range)
source
@[simp]
theorem QuotientAddGroup.homQuotientZSMulOfHom_id {A : Type u} [AddCommGroup A] (n : ℤ) :
homQuotientZSMulOfHom (AddMonoidHom.id A) n = AddMonoidHom.id (A ⧸ (zsmulAddGroupHom n).range)
source
@[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)
source
@[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)
source
@[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)
source
@[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)
source
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.

Equations

- QuotientGroup.equivQuotientZPowOfEquiv e n = (QuotientGroup.homQuotientZPowOfHom (↑e) n).toMulEquiv (QuotientGroup.homQuotientZPowOfHom (↑e.symm) n) ⋯ ⋯

Instances For

source
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.

Equations

- QuotientAddGroup.equivQuotientZSMulOfEquiv e n = (QuotientAddGroup.homQuotientZSMulOfHom (↑e) n).toAddEquiv (QuotientAddGroup.homQuotientZSMulOfHom (↑e.symm) n) ⋯ ⋯

Instances For

source
@[simp]
theorem QuotientGroup.equivQuotientZPowOfEquiv_refl {A : Type u} [CommGroup A] (n : ℤ) :
MulEquiv.refl (A ⧸ (zpowGroupHom n).range) = equivQuotientZPowOfEquiv (MulEquiv.refl A) n
source
@[simp]
theorem QuotientAddGroup.equivQuotientZSMulOfEquiv_refl {A : Type u} [AddCommGroup A] (n : ℤ) :
AddEquiv.refl (A ⧸ (zsmulAddGroupHom n).range) = equivQuotientZSMulOfEquiv (AddEquiv.refl A) n
source
@[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
source
@[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
source
@[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
source
@[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
source
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`.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
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`

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
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`.

Equations

- QuotientGroup.quotientInfEquivProdNormalQuotient H N = QuotientGroup.quotientInfEquivProdNormalizerQuotient H N ⋯

Instances For

source
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`.

Equations

- QuotientAddGroup.quotientInfEquivSumNormalQuotient H N = QuotientAddGroup.quotientInfEquivSumNormalizerQuotient H N ⋯

Instances For

source
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
source
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
source
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`.

Equations

- QuotientGroup.quotientQuotientEquivQuotientAux N M h = QuotientGroup.lift (Subgroup.map (QuotientGroup.mk' N) M) (QuotientGroup.map N M (MonoidHom.id G) h) ⋯

Instances For

source
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`.

Equations

- QuotientAddGroup.quotientQuotientEquivQuotientAux N M h = QuotientAddGroup.lift (AddSubgroup.map (QuotientAddGroup.mk' N) M) (QuotientAddGroup.map N M (AddMonoidHom.id G) h) ⋯

Instances For

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

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
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`.

Equations

- One or more equations did not get rendered due to their size.

Instances For

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

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
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

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
theorem QuotientGroup.subsingleton_quotient_top {G : Type u} [Group G] :
Subsingleton (G ⧸ ⊤)
source
theorem QuotientAddGroup.subsingleton_quotient_top {G : Type u} [AddGroup G] :
Subsingleton (G ⧸ ⊤)
source
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.

source
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.

source
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₂))
source
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₂))
source
@[simp]
theorem QuotientAddGroup.mk_nat_mul {R : Type u_1} [NonAssocRing R] (N : AddSubgroup R) [N.Normal] (n : ℕ) (a : R) :
↑(↑n * a) = n • ↑a
source
@[simp]
theorem QuotientAddGroup.mk_int_mul {R : Type u_1} [NonAssocRing R] (N : AddSubgroup R) [N.Normal] (n : ℤ) (a : R) :
↑(↑n * a) = n • ↑a