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 statements

• QuotientGroup.quotientKerEquivRange: Noether's first isomorphism theorem, an explicit isomorphism G/ker φ → range φ for every group homomorphism φ : G →* H.
• QuotientGroup.quotientInfEquivProdNormalQuotient: 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.
• QuotientGroup.quotientQuotientEquivQuotient: Noether's third isomorphism theorem, the canonical isomorphism between (G / N) / (M / N) and G / M, where N ≤ M.

Tags

isomorphism theorems, quotient groups

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

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

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

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

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 (QuotientAddGroup.mk' N) H)

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 (QuotientGroup.mk' N) H)

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 φ ⋯

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 φ ⋯

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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 ⋯

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 ⋯

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

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

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

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

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 φ) ⋯

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 φ) ⋯

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' := ⋯ }

@[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), (QuotientGroup.quotientKerEquivOfRightInverse φ ψ hφ).symm a = (QuotientGroup.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) : (QuotientGroup.quotientKerEquivOfRightInverse φ ψ hφ) a = (QuotientGroup.kerLift φ) a

@[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), (QuotientAddGroup.quotientKerEquivOfRightInverse φ ψ hφ).symm a = (QuotientAddGroup.mk ∘ ψ) 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) : (QuotientAddGroup.quotientKerEquivOfRightInverse φ ψ hφ) a = (QuotientAddGroup.kerLift φ) a

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' := ⋯ }

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

The canonical isomorphism G/⊥ ≃+ G.

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

The canonical isomorphism G/⊥ ≃* G.

Equations

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

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 ⋯) ⋯

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 ⋯) ⋯

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

def QuotientGroup.quotientMulEquivOfEq {G : Type u} [Group G] {M : Subgroup G} {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' := ⋯ }

@[simp]

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

@[simp]

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

def QuotientAddGroup.quotientMapAddSubgroupOfOfLe {G : Type u} [AddGroup G] {A' : AddSubgroup G} {A : AddSubgroup G} {B' : AddSubgroup G} {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) ⋯

def QuotientGroup.quotientMapSubgroupOfOfLe {G : Type u} [Group G] {A' : Subgroup G} {A : Subgroup G} {B' : Subgroup G} {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) ⋯

@[simp]

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

@[simp]

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

def QuotientAddGroup.equivQuotientAddSubgroupOfOfEq {G : Type u} [AddGroup G] {A' : AddSubgroup G} {A : AddSubgroup G} {B' : AddSubgroup G} {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 ⋯ ⋯) ⋯ ⋯

def QuotientGroup.equivQuotientSubgroupOfOfEq {G : Type u} [Group G] {A' : Subgroup G} {A : Subgroup G} {B' : Subgroup G} {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 ⋯ ⋯) ⋯ ⋯

def QuotientAddGroup.homQuotientZSMulOfHom {A : Type u} {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) ⋯

def QuotientGroup.homQuotientZPowOfHom {A : Type u} {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) ⋯

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

def QuotientAddGroup.equivQuotientZSMulOfEquiv {A : Type u} {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) ⋯ ⋯

def QuotientGroup.equivQuotientZPowOfEquiv {A : Type u} {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) ⋯ ⋯

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

noncomputable def QuotientGroup.quotientInfEquivProdNormalQuotient {G : Type u} [Group G] (H : Subgroup G) (N : Subgroup G) [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

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

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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 (QuotientAddGroup.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) ⋯

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 (QuotientGroup.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) ⋯

@[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) : (QuotientAddGroup.quotientQuotientEquivQuotientAux N M h) ↑x = (QuotientAddGroup.map N M (AddMonoidHom.id G) h) x

@[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) : (QuotientGroup.quotientQuotientEquivQuotientAux N M h) ↑x = (QuotientGroup.map N M (MonoidHom.id G) h) 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) : (QuotientAddGroup.quotientQuotientEquivQuotientAux N M h) ↑↑x = ↑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) : (QuotientGroup.quotientQuotientEquivQuotientAux N M h) ↑↑x = ↑x

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

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

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

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

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.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.comap_comap_center {G : Type u} [AddGroup G] {H₁ : AddSubgroup G} [H₁.Normal] {H₂ : AddSubgroup (G ⧸ H₁)} [H₂.Normal] : AddSubgroup.comap (QuotientAddGroup.mk' H₁) (AddSubgroup.comap (QuotientAddGroup.mk' H₂) (AddSubgroup.center ((G ⧸ H₁) ⧸ H₂))) = AddSubgroup.comap (QuotientAddGroup.mk' (AddSubgroup.comap (QuotientAddGroup.mk' H₁) H₂)) (AddSubgroup.center (G ⧸ AddSubgroup.comap (QuotientAddGroup.mk' H₁) H₂))

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

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