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

@[simp]

theorem QuotientGroup.leftRel_eq_top {G : Type u_1} [Group G] {N : Subgroup G} : leftRel N = ⊤ ↔ N = ⊤

@[simp]

theorem QuotientAddGroup.leftRel_eq_top {G : Type u_1} [AddGroup G] {N : AddSubgroup G} : leftRel N = ⊤ ↔ N = ⊤

@[simp]

theorem QuotientGroup.rightRel_eq_top {G : Type u_1} [Group G] {N : Subgroup G} : rightRel N = ⊤ ↔ N = ⊤

@[simp]

theorem QuotientAddGroup.rightRel_eq_top {G : Type u_1} [AddGroup G] {N : AddSubgroup G} : rightRel N = ⊤ ↔ N = ⊤

@[simp]

theorem QuotientGroup.subsingleton_iff {G : Type u_1} [Group G] {N : Subgroup G} : Subsingleton (G ⧸ N) ↔ N = ⊤

@[simp]

theorem QuotientAddGroup.subsingleton_iff {G : Type u_1} [AddGroup G] {N : AddSubgroup G} : Subsingleton (G ⧸ N) ↔ N = ⊤

@[simp]

theorem QuotientGroup.nontrivial_iff {G : Type u_1} [Group G] {N : Subgroup G} : Nontrivial (G ⧸ N) ↔ N ≠ ⊤

@[simp]

theorem QuotientAddGroup.nontrivial_iff {G : Type u_1} [AddGroup G] {N : AddSubgroup G} : Nontrivial (G ⧸ N) ↔ N ≠ ⊤

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

The congruence relation generated by a normal subgroup.

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

The additive congruence relation generated by a normal additive subgroup.

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

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

theorem QuotientGroup.con_ker_eq_conKer {G : Type u_1} {M : Type u_4} [Group G] [Monoid M] (f : G →* M) : QuotientGroup.con f.ker = Con.ker f

The congruence relation defined by the kernel of a group homomorphism is equal to its kernel as a congruence relation.

theorem QuotientAddGroup.con_ker_eq_addConKer {G : Type u_1} {M : Type u_4} [AddGroup G] [AddMonoid M] (f : G →+ M) : QuotientAddGroup.con f.ker = AddCon.ker f

The additive congruence relation defined by the kernel of an additive group homomorphism is equal to its kernel as an additive congruence relation.

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

The group homomorphism from G to G/N.

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

The additive group homomorphism from G to G/N.

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

theorem QuotientGroup.mk'_eq_mk' {G : Type u_1} [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_1} [AddGroup G] (N : AddSubgroup G) [nN : N.Normal] {x y : G} : (mk' N) x = (mk' N) y ↔ ∃ z ∈ N, x + z = y

theorem QuotientGroup.monoidHom_ext {G : Type u_1} {M : Type u_4} [Group G] [Monoid M] (N : Subgroup G) [nN : N.Normal] ⦃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].

theorem QuotientAddGroup.addMonoidHom_ext {G : Type u_1} {M : Type u_4} [AddGroup G] [AddMonoid M] (N : AddSubgroup G) [nN : N.Normal] ⦃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_iff {G : Type u_1} {M : Type u_4} [Group G] [Monoid M] {N : Subgroup G} [nN : N.Normal] {f g : G ⧸ N →* M} : f = g ↔ f.comp (mk' N) = g.comp (mk' N)

theorem QuotientAddGroup.addMonoidHom_ext_iff {G : Type u_1} {M : Type u_4} [AddGroup G] [AddMonoid M] {N : AddSubgroup G} [nN : N.Normal] {f g : G ⧸ N →+ M} : f = g ↔ f.comp (mk' N) = g.comp (mk' N)

@[simp]

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

@[simp]

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

@[simp]

theorem QuotientGroup.mk'_comp_subtype {G : Type u_1} [Group G] (N : Subgroup G) [nN : N.Normal] : (mk' N).comp N.subtype = 1

@[simp]

theorem QuotientAddGroup.mk'_comp_subtype {G : Type u_1} [AddGroup G] (N : AddSubgroup G) [nN : N.Normal] : (mk' N).comp N.subtype = 0

@[simp]

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

@[simp]

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

theorem QuotientGroup.ker_le_range_iff {G : Type u_1} {H : Type u_2} {I : Type u_3} [Group G] [Group H] [MulOneClass 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_1} {H : Type u_2} {I : Type u_3} [AddGroup G] [AddGroup H] [AddZeroClass 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_1} [Group G] (N : Subgroup G) [nN : N.Normal] : (mk' N).ker = N

@[simp]

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

theorem QuotientGroup.eq_iff_div_mem {G : Type u_1} [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_1} [AddGroup G] {N : AddSubgroup G} [nN : N.Normal] {x y : G} : ↑x = ↑y ↔ x - y ∈ N

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

def Con.subgroup {G : Type u_1} [Group G] (c : Con G) : Subgroup G

The subgroup defined by the class of 1 for a congruence relation on a group.

def AddCon.addSubgroup {G : Type u_1} [AddGroup G] (c : AddCon G) : AddSubgroup G

The AddSubgroup defined by the class of 0 for an additive congruence relation on an AddGroup.

@[simp]

theorem Con.mem_subgroup_iff {G : Type u_1} [Group G] {c : Con G} {x : G} : x ∈ c.subgroup ↔ c x 1

@[simp]

theorem AddCon.mem_addSubgroup_iff {G : Type u_1} [AddGroup G] {c : AddCon G} {x : G} : x ∈ c.addSubgroup ↔ c x 0

instance QuotientGroup.instNormalSubgroup {G : Type u_1} [Group G] (c : Con G) : c.subgroup.Normal

instance QuotientAddGroup.instNormalAddSubgroup {G : Type u_1} [AddGroup G] (c : AddCon G) : c.addSubgroup.Normal

@[simp]

theorem Con.subgroup_quotientGroupCon {G : Type u_1} [Group G] (H : Subgroup G) [H.Normal] : (QuotientGroup.con H).subgroup = H

@[simp]

theorem AddCon.addSubgroup_quotientAddGroupCon {G : Type u_1} [AddGroup G] (H : AddSubgroup G) [H.Normal] : (QuotientAddGroup.con H).addSubgroup = H

@[simp]

theorem QuotientGroup.con_subgroup {G : Type u_1} [Group G] (c : Con G) : QuotientGroup.con c.subgroup = c

@[simp]

theorem QuotientAddGroup.con_addSubgroup {G : Type u_1} [AddGroup G] (c : AddCon G) : QuotientAddGroup.con c.addSubgroup = c

def Subgroup.orderIsoCon {G : Type u_1} [Group G] : { N : Subgroup G // N.Normal } ≃o Con G

The normal subgroups correspond to the congruence relations on a group.

def AddSubgroup.orderIsoAddCon {G : Type u_1} [AddGroup G] : { N : AddSubgroup G // N.Normal } ≃o AddCon G

The normal subgroups correspond to the additive congruence relations on an AddGroup.

@[simp]

theorem Subgroup.orderIsoCon_apply {G : Type u_1} [Group G] (N : { N : Subgroup G // N.Normal }) : orderIsoCon N = QuotientGroup.con ↑N

@[simp]

theorem AddSubgroup.orderIsoAddCon_apply {G : Type u_1} [AddGroup G] (N : { N : AddSubgroup G // N.Normal }) : orderIsoAddCon N = QuotientAddGroup.con ↑N

@[simp]

theorem Subgroup.orderIsoCon_symm_apply_coe {G : Type u_1} [Group G] (c : Con G) : ↑((RelIso.symm orderIsoCon) c) = c.subgroup

@[simp]

theorem AddSubgroup.orderIsoAddCon_symm_apply_coe {G : Type u_1} [AddGroup G] (c : AddCon G) : ↑((RelIso.symm orderIsoAddCon) c) = c.addSubgroup

@[simp]

theorem QuotientGroup.con_le_iff {G : Type u_1} [Group G] {N M : Subgroup G} [N.Normal] [M.Normal] : QuotientGroup.con N ≤ QuotientGroup.con M ↔ N ≤ M

@[simp]

theorem QuotientAddGroup.con_le_iff {G : Type u_1} [AddGroup G] {N M : AddSubgroup G} [N.Normal] [M.Normal] : QuotientAddGroup.con N ≤ QuotientAddGroup.con M ↔ N ≤ M

theorem QuotientGroup.con_mono {G : Type u_1} [Group G] {N M : Subgroup G} [hN : N.Normal] [hM : M.Normal] (h : N ≤ M) : QuotientGroup.con N ≤ QuotientGroup.con M

theorem QuotientAddGroup.con_mono {G : Type u_1} [AddGroup G] {N M : AddSubgroup G} [hN : N.Normal] [hM : M.Normal] (h : N ≤ M) : QuotientAddGroup.con N ≤ QuotientAddGroup.con M

def QuotientGroup.lift {G : Type u_1} {M : Type u_4} [Group G] [Monoid M] (N : Subgroup G) [nN : N.Normal] (φ : 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.

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem QuotientGroup.lift_comp_mk' {G : Type u_1} {M : Type u_4} [Group G] [Monoid M] (N : Subgroup G) [nN : N.Normal] (φ : G →* M) (HN : N ≤ φ.ker) : (lift N φ HN).comp (mk' N) = φ

@[simp]

theorem QuotientAddGroup.lift_comp_mk' {G : Type u_1} {M : Type u_4} [AddGroup G] [AddMonoid M] (N : AddSubgroup G) [nN : N.Normal] (φ : G →+ M) (HN : N ≤ φ.ker) : (lift N φ HN).comp (mk' N) = φ

@[simp]

theorem QuotientGroup.lift_quot_mk {G : Type u_1} {M : Type u_4} [Group G] [Monoid M] (N : Subgroup G) [nN : N.Normal] {φ : 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_1} {M : Type u_4} [AddGroup G] [AddMonoid M] (N : AddSubgroup G) [nN : N.Normal] {φ : G →+ M} (HN : N ≤ φ.ker) (g : G) : (lift N φ HN) (Quot.mk (⇑(leftRel N)) g) = φ g

theorem QuotientGroup.lift_surjective_of_surjective {G : Type u_1} {M : Type u_4} [Group G] [Monoid M] (N : Subgroup G) [nN : N.Normal] (φ : G →* M) (hφ : Function.Surjective ⇑φ) (HN : N ≤ φ.ker) : Function.Surjective ⇑(lift N φ HN)

theorem QuotientAddGroup.lift_surjective_of_surjective {G : Type u_1} {M : Type u_4} [AddGroup G] [AddMonoid M] (N : AddSubgroup G) [nN : N.Normal] (φ : G →+ M) (hφ : Function.Surjective ⇑φ) (HN : N ≤ φ.ker) : Function.Surjective ⇑(lift N φ HN)

theorem QuotientGroup.ker_lift {G : Type u_1} {M : Type u_4} [Group G] [Monoid M] (N : Subgroup G) [nN : N.Normal] (φ : G →* M) (HN : N ≤ φ.ker) : (lift N φ HN).ker = Subgroup.map (mk' N) φ.ker

theorem QuotientAddGroup.ker_lift {G : Type u_1} {M : Type u_4} [AddGroup G] [AddMonoid M] (N : AddSubgroup G) [nN : N.Normal] (φ : G →+ M) (HN : N ≤ φ.ker) : (lift N φ HN).ker = AddSubgroup.map (mk' N) φ.ker

noncomputable def QuotientGroup.liftEquiv {G : Type u_1} {H : Type u_2} [Group G] [Group H] (N : Subgroup G) [nN : N.Normal] {φ : G →* H} (hφ : Function.Surjective ⇑φ) (HN : N = φ.ker) : G ⧸ N ≃* H

A surjective group homomorphism φ : G →* H with N = ker(φ) descends (i.e. lifts) to a group isomorphism G/N ≃* H.

noncomputable def QuotientAddGroup.liftEquiv {G : Type u_1} {H : Type u_2} [AddGroup G] [AddGroup H] (N : AddSubgroup G) [nN : N.Normal] {φ : G →+ H} (hφ : Function.Surjective ⇑φ) (HN : N = φ.ker) : G ⧸ N ≃+ H

A surjective AddGroup homomorphism φ : G →+ H with N = ker(φ) descends (i.e. lifts) to an AddGroup isomorphism G/N ≃+ H.

@[simp]

theorem QuotientGroup.liftEquiv_coe {G : Type u_1} {H : Type u_2} [Group G] [Group H] (N : Subgroup G) [nN : N.Normal] {φ : G →* H} (hφ : Function.Surjective ⇑φ) (HN : N = φ.ker) (g : G) : (liftEquiv N hφ HN) ↑g = φ g

@[simp]

theorem QuotientAddGroup.liftEquiv_coe {G : Type u_1} {H : Type u_2} [AddGroup G] [AddGroup H] (N : AddSubgroup G) [nN : N.Normal] {φ : G →+ H} (hφ : Function.Surjective ⇑φ) (HN : N = φ.ker) (g : G) : (liftEquiv N hφ HN) ↑g = φ g

@[simp]

theorem QuotientGroup.liftEquiv_mk {G : Type u_1} {H : Type u_2} [Group G] [Group H] (N : Subgroup G) [nN : N.Normal] {φ : G →* H} (hφ : Function.Surjective ⇑φ) (HN : N = φ.ker) (g : G) : (liftEquiv N hφ HN) ↑g = φ g

@[simp]

theorem QuotientAddGroup.liftEquiv_mk {G : Type u_1} {H : Type u_2} [AddGroup G] [AddGroup H] (N : AddSubgroup G) [nN : N.Normal] {φ : G →+ H} (hφ : Function.Surjective ⇑φ) (HN : N = φ.ker) (g : G) : (liftEquiv N hφ HN) ↑g = φ g

def QuotientGroup.map {G : Type u_1} {H : Type u_2} [Group G] [Group H] (N : Subgroup G) [nN : N.Normal] (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).

def QuotientAddGroup.map {G : Type u_1} {H : Type u_2} [AddGroup G] [AddGroup H] (N : AddSubgroup G) [nN : N.Normal] (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).

@[simp]

theorem QuotientGroup.map_mk {G : Type u_1} {H : Type u_2} [Group G] [Group H] (N : Subgroup G) [nN : N.Normal] (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_1} {H : Type u_2} [AddGroup G] [AddGroup H] (N : AddSubgroup G) [nN : N.Normal] (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_1} {H : Type u_2} [Group G] [Group H] (N : Subgroup G) [nN : N.Normal] (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_1} {H : Type u_2} [AddGroup G] [AddGroup H] (N : AddSubgroup G) [nN : N.Normal] (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_surjective_of_surjective {G : Type u_1} {H : Type u_2} [Group G] [Group H] (N : Subgroup G) [nN : N.Normal] (M : Subgroup H) [M.Normal] (f : G →* H) (hf : Function.Surjective (mk ∘ ⇑f)) (h : N ≤ Subgroup.comap f M) : Function.Surjective ⇑(map N M f h)

theorem QuotientAddGroup.map_surjective_of_surjective {G : Type u_1} {H : Type u_2} [AddGroup G] [AddGroup H] (N : AddSubgroup G) [nN : N.Normal] (M : AddSubgroup H) [M.Normal] (f : G →+ H) (hf : Function.Surjective (mk ∘ ⇑f)) (h : N ≤ AddSubgroup.comap f M) : Function.Surjective ⇑(map N M f h)

theorem QuotientGroup.ker_map {G : Type u_1} {H : Type u_2} [Group G] [Group H] (N : Subgroup G) [nN : N.Normal] (M : Subgroup H) [M.Normal] (f : G →* H) (h : N ≤ Subgroup.comap f M) : (map N M f h).ker = Subgroup.map (mk' N) (Subgroup.comap f M)

theorem QuotientAddGroup.ker_map {G : Type u_1} {H : Type u_2} [AddGroup G] [AddGroup H] (N : AddSubgroup G) [nN : N.Normal] (M : AddSubgroup H) [M.Normal] (f : G →+ H) (h : N ≤ AddSubgroup.comap f M) : (map N M f h).ker = AddSubgroup.map (mk' N) (AddSubgroup.comap f M)

theorem QuotientGroup.map_id_apply {G : Type u_1} [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_1} [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_1} [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_1} [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_1} {H : Type u_2} [Group G] [Group H] (N : Subgroup G) [nN : N.Normal] {I : Type u_5} [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_1} {H : Type u_2} [AddGroup G] [AddGroup H] (N : AddSubgroup G) [nN : N.Normal] {I : Type u_5} [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_1} {H : Type u_2} [Group G] [Group H] (N : Subgroup G) [nN : N.Normal] {I : Type u_5} [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_1} {H : Type u_2} [AddGroup G] [AddGroup H] (N : AddSubgroup G) [nN : N.Normal] {I : Type u_5} [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_1} [Group G] (N : Subgroup G) [nN : N.Normal] : mk '' ↑N = 1

@[simp]

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

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

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

theorem QuotientGroup.image_coe_inj {G : Type u_1} [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_1} [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_1} {H : Type u_2} [Group G] [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.

def QuotientAddGroup.congr {G : Type u_1} {H : Type u_2} [AddGroup G] [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.

@[simp]

theorem QuotientGroup.congr_mk {G : Type u_1} {H : Type u_2} [Group G] [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_1} {H : Type u_2} [Group G] [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_1} {H : Type u_2} [Group G] [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_1} [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_1} {H : Type u_2} [Group G] [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 ⋯