Quotients of groups by normal subgroups

This file defines the group structure on the quotient by a normal subgroup.

Main definitions

• QuotientGroup.Quotient.Group: the group structure on G/N given a normal subgroup N of G.
• 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).

Tags

quotient groups

def QuotientGroup.con {G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] : Con G

The congruence relation generated by a normal subgroup.

Equations

• QuotientGroup.con N = { toSetoid := QuotientGroup.leftRel N, mul' := ⋯ }

def QuotientAddGroup.con {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : N.Normal] : AddCon G

The additive congruence relation generated by a normal additive subgroup.

Equations

• QuotientAddGroup.con N = { toSetoid := QuotientAddGroup.leftRel N, add' := ⋯ }

instance QuotientGroup.Quotient.group {G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] : Group (G ⧸ N)

Equations

• QuotientGroup.Quotient.group N = (QuotientGroup.con N).group

instance QuotientAddGroup.Quotient.addGroup {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : N.Normal] : AddGroup (G ⧸ N)

Equations

• QuotientAddGroup.Quotient.addGroup N = (QuotientAddGroup.con N).addGroup

def QuotientGroup.mk' {G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] : G →* G ⧸ N

The group homomorphism from G to G/N.

Equations

• QuotientGroup.mk' N = MonoidHom.mk' QuotientGroup.mk ⋯

def QuotientAddGroup.mk' {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : N.Normal] : G →+ G ⧸ N

The additive group homomorphism from G to G/N.

Equations

• QuotientAddGroup.mk' N = AddMonoidHom.mk' QuotientAddGroup.mk ⋯

@[simp]

theorem QuotientGroup.coe_mk' {G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] : ⇑(mk' N) = mk

@[simp]

theorem QuotientAddGroup.coe_mk' {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : N.Normal] : ⇑(mk' N) = mk

@[simp]

theorem QuotientGroup.mk'_apply {G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] (x : G) : (mk' N) x = ↑x

@[simp]

theorem QuotientAddGroup.mk'_apply {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : N.Normal] (x : G) : (mk' N) x = ↑x

theorem QuotientGroup.mk'_surjective {G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] : Function.Surjective ⇑(mk' N)

theorem QuotientAddGroup.mk'_surjective {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : N.Normal] : Function.Surjective ⇑(mk' N)

theorem QuotientGroup.mk'_eq_mk' {G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] {x y : G} : (mk' N) x = (mk' N) y ↔ ∃ z ∈ N, x * z = y

theorem QuotientAddGroup.mk'_eq_mk' {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : N.Normal] {x y : G} : (mk' N) x = (mk' N) y ↔ ∃ z ∈ N, x + z = y

theorem QuotientAddGroup.addMonoidHom_ext {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : N.Normal] {M : Type x} [AddMonoid M] ⦃f g : G ⧸ N →+ M⦄ (h : f.comp (mk' N) = g.comp (mk' N)) : f = g

Two AddMonoidHoms from an additive quotient group are equal if their compositions with AddQuotientGroup.mk' are equal.

See note [partially-applied ext lemmas].

theorem QuotientGroup.monoidHom_ext {G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] {M : Type x} [Monoid M] ⦃f g : G ⧸ N →* M⦄ (h : f.comp (mk' N) = g.comp (mk' N)) : f = g

Two MonoidHoms from a quotient group are equal if their compositions with QuotientGroup.mk' are equal.

See note [partially-applied ext lemmas].

@[simp]

theorem QuotientGroup.eq_one_iff {G : Type u} [Group G] {N : Subgroup G} [N.Normal] (x : G) : ↑x = 1 ↔ x ∈ N

@[simp]

theorem QuotientAddGroup.eq_zero_iff {G : Type u} [AddGroup G] {N : AddSubgroup G} [N.Normal] (x : G) : ↑x = 0 ↔ x ∈ N

@[simp]

theorem QuotientGroup.range_mk' {G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] : (mk' N).range = ⊤

@[simp]

theorem QuotientAddGroup.range_mk' {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : N.Normal] : (mk' N).range = ⊤

theorem QuotientGroup.ker_le_range_iff {G : Type u} [Group G] {H : Type v} [Group H] {I : Type w} [Group I] (f : G →* H) [f.range.Normal] (g : H →* I) : g.ker ≤ f.range ↔ (mk' f.range).comp g.ker.subtype = 1

theorem QuotientAddGroup.ker_le_range_iff {G : Type u} [AddGroup G] {H : Type v} [AddGroup H] {I : Type w} [AddGroup I] (f : G →+ H) [f.range.Normal] (g : H →+ I) : g.ker ≤ f.range ↔ (mk' f.range).comp g.ker.subtype = 0

@[simp]

theorem QuotientGroup.ker_mk' {G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] : (mk' N).ker = N

@[simp]

theorem QuotientAddGroup.ker_mk' {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : N.Normal] : (mk' N).ker = N

theorem QuotientGroup.eq_iff_div_mem {G : Type u} [Group G] {N : Subgroup G} [nN : N.Normal] {x y : G} : ↑x = ↑y ↔ x / y ∈ N

theorem QuotientAddGroup.eq_iff_sub_mem {G : Type u} [AddGroup G] {N : AddSubgroup G} [nN : N.Normal] {x y : G} : ↑x = ↑y ↔ x - y ∈ N

instance QuotientGroup.Quotient.commGroup {G : Type u_1} [CommGroup G] (N : Subgroup G) : CommGroup (G ⧸ N)

Equations

• QuotientGroup.Quotient.commGroup N = CommGroup.mk ⋯

instance QuotientAddGroup.Quotient.addCommGroup {G : Type u_1} [AddCommGroup G] (N : AddSubgroup G) : AddCommGroup (G ⧸ N)

Equations

• QuotientAddGroup.Quotient.addCommGroup N = AddCommGroup.mk ⋯

@[simp]

theorem QuotientGroup.mk_one {G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] : ↑1 = 1

@[simp]

theorem QuotientAddGroup.mk_zero {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : N.Normal] : ↑0 = 0

@[simp]

theorem QuotientGroup.mk_mul {G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] (a b : G) : ↑(a * b) = ↑a * ↑b

@[simp]

theorem QuotientAddGroup.mk_add {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : N.Normal] (a b : G) : ↑(a + b) = ↑a + ↑b

@[simp]

theorem QuotientGroup.mk_inv {G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] (a : G) : ↑a⁻¹ = (↑a)⁻¹

@[simp]

theorem QuotientAddGroup.mk_neg {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : N.Normal] (a : G) : ↑(-a) = -↑a

@[simp]

theorem QuotientGroup.mk_div {G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] (a b : G) : ↑(a / b) = ↑a / ↑b

@[simp]

theorem QuotientAddGroup.mk_sub {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : N.Normal] (a b : G) : ↑(a - b) = ↑a - ↑b

@[simp]

theorem QuotientGroup.mk_pow {G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] (a : G) (n : ℕ) : ↑(a ^ n) = ↑a ^ n

@[simp]

theorem QuotientAddGroup.mk_nsmul {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : N.Normal] (a : G) (n : ℕ) : ↑(n • a) = n • ↑a

@[simp]

theorem QuotientGroup.mk_zpow {G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] (a : G) (n : ℤ) : ↑(a ^ n) = ↑a ^ n

@[simp]

theorem QuotientAddGroup.mk_zsmul {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : N.Normal] (a : G) (n : ℤ) : ↑(n • a) = n • ↑a

@[simp]

theorem QuotientGroup.map_mk'_self {G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] : Subgroup.map (mk' N) N = ⊥

@[simp]

theorem QuotientAddGroup.map_mk'_self {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : N.Normal] : AddSubgroup.map (mk' N) N = ⊥

def QuotientGroup.lift {G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] {M : Type x} [Monoid M] (φ : G →* M) (HN : N ≤ φ.ker) : G ⧸ N →* M

A group homomorphism φ : G →* M with N ⊆ ker(φ) descends (i.e. lifts) to a group homomorphism G/N →* M.

Equations

• QuotientGroup.lift N φ HN = (QuotientGroup.con N).lift φ ⋯

def QuotientAddGroup.lift {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : N.Normal] {M : Type x} [AddMonoid M] (φ : G →+ M) (HN : N ≤ φ.ker) : G ⧸ N →+ M

An AddGroup homomorphism φ : G →+ M with N ⊆ ker(φ) descends (i.e. lifts) to a group homomorphism G/N →* M.

Equations

• QuotientAddGroup.lift N φ HN = (QuotientAddGroup.con N).lift φ ⋯

@[simp]

theorem QuotientGroup.lift_mk {G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] {M : Type x} [Monoid M] {φ : G →* M} (HN : N ≤ φ.ker) (g : G) : (lift N φ HN) ↑g = φ g

@[simp]

theorem QuotientAddGroup.lift_mk {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : N.Normal] {M : Type x} [AddMonoid M] {φ : G →+ M} (HN : N ≤ φ.ker) (g : G) : (lift N φ HN) ↑g = φ g

@[simp]

theorem QuotientGroup.lift_mk' {G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] {M : Type x} [Monoid M] {φ : G →* M} (HN : N ≤ φ.ker) (g : G) : (lift N φ HN) ↑g = φ g

@[simp]

theorem QuotientAddGroup.lift_mk' {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : N.Normal] {M : Type x} [AddMonoid M] {φ : G →+ M} (HN : N ≤ φ.ker) (g : G) : (lift N φ HN) ↑g = φ g

@[simp]

theorem QuotientGroup.lift_quot_mk {G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] {M : Type x} [Monoid M] {φ : G →* M} (HN : N ≤ φ.ker) (g : G) : (lift N φ HN) (Quot.mk (⇑(leftRel N)) g) = φ g

@[simp]

theorem QuotientAddGroup.lift_quot_mk {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : N.Normal] {M : Type x} [AddMonoid M] {φ : G →+ M} (HN : N ≤ φ.ker) (g : G) : (lift N φ HN) (Quot.mk (⇑(leftRel N)) g) = φ g

def QuotientGroup.map {G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] {H : Type v} [Group H] (M : Subgroup H) [M.Normal] (f : G →* H) (h : N ≤ Subgroup.comap f M) : G ⧸ N →* H ⧸ M

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

Equations

• QuotientGroup.map N M f h = QuotientGroup.lift N ((QuotientGroup.mk' M).comp f) ⋯

def QuotientAddGroup.map {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : N.Normal] {H : Type v} [AddGroup H] (M : AddSubgroup H) [M.Normal] (f : G →+ H) (h : N ≤ AddSubgroup.comap f M) : G ⧸ N →+ H ⧸ M

An AddGroup homomorphism f : G →+ H induces a map G/N →+ H/M if N ⊆ f⁻¹(M).

Equations

• QuotientAddGroup.map N M f h = QuotientAddGroup.lift N ((QuotientAddGroup.mk' M).comp f) ⋯

@[simp]

theorem QuotientGroup.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 ≤ Subgroup.comap f M) (x : G) : (map N M f h) ↑x = ↑(f x)

@[simp]

theorem QuotientAddGroup.map_mk {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : N.Normal] {H : Type v} [AddGroup H] (M : AddSubgroup H) [M.Normal] (f : G →+ H) (h : N ≤ AddSubgroup.comap f M) (x : G) : (map N M f h) ↑x = ↑(f x)

theorem QuotientGroup.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 ≤ Subgroup.comap f M) (x : G) : (map N M f h) ((mk' N) x) = ↑(f x)

theorem QuotientAddGroup.map_mk' {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : N.Normal] {H : Type v} [AddGroup H] (M : AddSubgroup H) [M.Normal] (f : G →+ H) (h : N ≤ AddSubgroup.comap f M) (x : G) : (map N M f h) ((mk' N) x) = ↑(f x)

theorem QuotientGroup.map_id_apply {G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] (h : N ≤ Subgroup.comap (MonoidHom.id G) N := ⋯) (x : G ⧸ N) : (map N N (MonoidHom.id G) h) x = x

theorem QuotientAddGroup.map_id_apply {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : N.Normal] (h : N ≤ AddSubgroup.comap (AddMonoidHom.id G) N := ⋯) (x : G ⧸ N) : (map N N (AddMonoidHom.id G) h) x = x

@[simp]

theorem QuotientGroup.map_id {G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] (h : N ≤ Subgroup.comap (MonoidHom.id G) N := ⋯) : map N N (MonoidHom.id G) h = MonoidHom.id (G ⧸ N)

@[simp]

theorem QuotientAddGroup.map_id {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : N.Normal] (h : N ≤ AddSubgroup.comap (AddMonoidHom.id G) N := ⋯) : map N N (AddMonoidHom.id G) h = AddMonoidHom.id (G ⧸ N)

@[simp]

theorem QuotientGroup.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 ≤ Subgroup.comap f M) (hg : M ≤ Subgroup.comap g O) (hgf : N ≤ Subgroup.comap (g.comp f) O := ⋯) (x : G ⧸ N) : (map M O g hg) ((map N M f hf) x) = (map N O (g.comp f) hgf) x

@[simp]

theorem QuotientAddGroup.map_map {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : N.Normal] {H : Type v} [AddGroup H] {I : Type u_1} [AddGroup I] (M : AddSubgroup H) (O : AddSubgroup I) [M.Normal] [O.Normal] (f : G →+ H) (g : H →+ I) (hf : N ≤ AddSubgroup.comap f M) (hg : M ≤ AddSubgroup.comap g O) (hgf : N ≤ AddSubgroup.comap (g.comp f) O := ⋯) (x : G ⧸ N) : (map M O g hg) ((map N M f hf) x) = (map N O (g.comp f) hgf) x

@[simp]

theorem QuotientGroup.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 ≤ Subgroup.comap f M) (hg : M ≤ Subgroup.comap g O) (hgf : N ≤ Subgroup.comap (g.comp f) O := ⋯) : (map M O g hg).comp (map N M f hf) = map N O (g.comp f) hgf

@[simp]

theorem QuotientAddGroup.map_comp_map {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : N.Normal] {H : Type v} [AddGroup H] {I : Type u_1} [AddGroup I] (M : AddSubgroup H) (O : AddSubgroup I) [M.Normal] [O.Normal] (f : G →+ H) (g : H →+ I) (hf : N ≤ AddSubgroup.comap f M) (hg : M ≤ AddSubgroup.comap g O) (hgf : N ≤ AddSubgroup.comap (g.comp f) O := ⋯) : (map M O g hg).comp (map N M f hf) = map N O (g.comp f) hgf

@[simp]

theorem QuotientGroup.image_coe {G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] : mk '' ↑N = 1

@[simp]

theorem QuotientAddGroup.image_coe {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : N.Normal] : mk '' ↑N = 0

theorem QuotientGroup.preimage_image_coe {G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] (s : Set G) : mk ⁻¹' (mk '' s) = ↑N * s

theorem QuotientAddGroup.preimage_image_coe {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : N.Normal] (s : Set G) : mk ⁻¹' (mk '' s) = ↑N + s

theorem QuotientGroup.image_coe_inj {G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] {s t : Set G} : mk '' s = mk '' t ↔ ↑N * s = ↑N * t

theorem QuotientAddGroup.image_coe_inj {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : N.Normal] {s t : Set G} : mk '' s = mk '' t ↔ ↑N + s = ↑N + t

def QuotientGroup.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 : Subgroup.map (↑e) G' = H') : G ⧸ G' ≃* H ⧸ H'

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

Equations

• QuotientGroup.congr G' H' e he = { toFun := ⇑(QuotientGroup.map G' H' ↑e ⋯), invFun := ⇑(QuotientGroup.map H' G' ↑e.symm ⋯), left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ }

def QuotientAddGroup.congr {G : Type u} [AddGroup G] {H : Type v} [AddGroup H] (G' : AddSubgroup G) (H' : AddSubgroup H) [G'.Normal] [H'.Normal] (e : G ≃+ H) (he : AddSubgroup.map (↑e) G' = H') : G ⧸ G' ≃+ H ⧸ H'

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

Equations

• QuotientAddGroup.congr G' H' e he = { toFun := ⇑(QuotientAddGroup.map G' H' ↑e ⋯), invFun := ⇑(QuotientAddGroup.map H' G' ↑e.symm ⋯), left_inv := ⋯, right_inv := ⋯, map_add' := ⋯ }

@[simp]

theorem QuotientGroup.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 : Subgroup.map (↑e) G' = H') (x : G) : (congr G' H' e he) ↑x = ↑(e x)

theorem QuotientGroup.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 : Subgroup.map (↑e) G' = H') (x : G) : (congr G' H' e he) ((mk' G') x) = (mk' H') (e x)

@[simp]

theorem QuotientGroup.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 : Subgroup.map (↑e) G' = H') (x : G) : (congr G' H' e he) ↑x = (mk' H') (e x)

@[simp]

theorem QuotientGroup.congr_refl {G : Type u} [Group G] (G' : Subgroup G) [G'.Normal] (he : Subgroup.map (↑(MulEquiv.refl G)) G' = G' := ⋯) : congr G' G' (MulEquiv.refl G) he = MulEquiv.refl (G ⧸ G')

@[simp]

theorem QuotientGroup.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 : Subgroup.map (↑e) G' = H') : (congr G' H' e he).symm = congr H' G' e.symm ⋯