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

source

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

source

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

source

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

source

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

source

theorem QuotientGroup.con_ker_eq_conKer {G : Type u} [Group G] {M : Type x} [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.

source

theorem QuotientAddGroup.con_ker_eq_addConKer {G : Type u} [AddGroup G] {M : Type x} [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.

source

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 ⋯

source

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 ⋯

source

@[simp]

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

⇑(mk' N) = mk

source

@[simp]

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

⇑(mk' N) = mk

source

@[simp]

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

(mk' N) x = ↑x

source

@[simp]

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

(mk' N) x = ↑x

source

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

Function.Surjective ⇑(mk' N)

source

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

Function.Surjective ⇑(mk' N)

source

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

source

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

source

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

source

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

source

theorem QuotientGroup.monoidHom_ext_iff {G : Type u} [Group G] {N : Subgroup G} [nN : N.Normal] {M : Type x} [Monoid M] {f g : G ⧸ N →* M} :

f = g ↔ f.comp (mk' N) = g.comp (mk' N)

source

theorem QuotientAddGroup.addMonoidHom_ext_iff {G : Type u} [AddGroup G] {N : AddSubgroup G} [nN : N.Normal] {M : Type x} [AddMonoid M] {f g : G ⧸ N →+ M} :

f = g ↔ f.comp (mk' N) = g.comp (mk' N)

source

@[simp]

theorem QuotientGroup.eq_one_iff {G : Type u} [Group G] {N : Subgroup G} [N.Normal] (x : G) :

↑x = 1 ↔ x ∈ N

source

@[simp]

theorem QuotientAddGroup.eq_zero_iff {G : Type u} [AddGroup G] {N : AddSubgroup G} [N.Normal] (x : G) :

↑x = 0 ↔ x ∈ N

source

@[simp]

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

(mk' N).comp N.subtype = 1

source

@[simp]

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

(mk' N).comp N.subtype = 0

source

@[simp]

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

(mk' N).range = ⊤

source

@[simp]

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

(mk' N).range = ⊤

source

theorem QuotientGroup.ker_le_range_iff {G : Type u} [Group G] {H : Type v} [Group H] {I : Type w} [MulOneClass I] (f : G →* H) [f.range.Normal] (g : H →* I) :

g.ker ≤ f.range ↔ (mk' f.range).comp g.ker.subtype = 1

source

theorem QuotientAddGroup.ker_le_range_iff {G : Type u} [AddGroup G] {H : Type v} [AddGroup H] {I : Type w} [AddZeroClass I] (f : G →+ H) [f.range.Normal] (g : H →+ I) :

g.ker ≤ f.range ↔ (mk' f.range).comp g.ker.subtype = 0

source

@[simp]

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

(mk' N).ker = N

source

@[simp]

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

(mk' N).ker = N

source

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

source

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

source

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

CommGroup (G ⧸ N)

Equations

QuotientGroup.Quotient.commGroup N = { toGroup := let_fun this := ⋯; QuotientGroup.Quotient.group N, mul_comm := ⋯ }

source

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

AddCommGroup (G ⧸ N)

Equations

QuotientAddGroup.Quotient.addCommGroup N = { toAddGroup := let_fun this := ⋯; QuotientAddGroup.Quotient.addGroup N, add_comm := ⋯ }

source

@[simp]

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

↑1 = 1

source

@[simp]

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

↑0 = 0

source

@[simp]

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

↑(a * b) = ↑a * ↑b

source

@[simp]

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

↑(a + b) = ↑a + ↑b

source

@[simp]

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

↑a⁻¹ = (↑a)⁻¹

source

@[simp]

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

↑(-a) = -↑a

source

@[simp]

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

↑(a / b) = ↑a / ↑b

source

@[simp]

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

↑(a - b) = ↑a - ↑b

source

@[simp]

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

↑(a ^ n) = ↑a ^ n

source

@[simp]

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

↑(n • a) = n • ↑a

source

@[simp]

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

↑(a ^ n) = ↑a ^ n

source

@[simp]

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

↑(n • a) = n • ↑a

source

@[simp]

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

Subgroup.map (mk' N) N = ⊥

source

@[simp]

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

AddSubgroup.map (mk' N) N = ⊥

source

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

Subgroup G

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

Equations

c.subgroup = { carrier := {x : G | c x 1}, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }

source

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

AddSubgroup G

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

Equations

c.addSubgroup = { carrier := {x : G | c x 0}, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯ }

source

@[simp]

theorem Con.mem_subgroup_iff {G : Type u} [Group G] {c : Con G} {x : G} :

x ∈ c.subgroup ↔ c x 1

source

@[simp]

theorem AddCon.mem_addSubgroup_iff {G : Type u} [AddGroup G] {c : AddCon G} {x : G} :

x ∈ c.addSubgroup ↔ c x 0

source

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

c.subgroup.Normal

source

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

c.addSubgroup.Normal

source

@[simp]

theorem Con.subgroup_quotientGroupCon {G : Type u} [Group G] (H : Subgroup G) [H.Normal] :

(QuotientGroup.con H).subgroup = H

source

@[simp]

theorem AddCon.addSubgroup_quotientAddGroupCon {G : Type u} [AddGroup G] (H : AddSubgroup G) [H.Normal] :

(QuotientAddGroup.con H).addSubgroup = H

source

@[simp]

theorem QuotientGroup.con_subgroup {G : Type u} [Group G] (c : Con G) :

QuotientGroup.con c.subgroup = c

source

@[simp]

theorem QuotientAddGroup.con_addSubgroup {G : Type u} [AddGroup G] (c : AddCon G) :

QuotientAddGroup.con c.addSubgroup = c

source

def Subgroup.orderIsoCon {G : Type u} [Group G] :

{ N : Subgroup G // N.Normal } ≃o Con G

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

Equations

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

source

def AddSubgroup.orderIsoAddCon {G : Type u} [AddGroup G] :

{ N : AddSubgroup G // N.Normal } ≃o AddCon G

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

Equations

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

source

@[simp]

theorem Subgroup.orderIsoCon_symm_apply_coe {G : Type u} [Group G] (c : Con G) :

↑((RelIso.symm orderIsoCon) c) = c.subgroup

source

@[simp]

theorem AddSubgroup.orderIsoAddCon_symm_apply_coe {G : Type u} [AddGroup G] (c : AddCon G) :

↑((RelIso.symm orderIsoAddCon) c) = c.addSubgroup

source

@[simp]

theorem Subgroup.orderIsoCon_apply {G : Type u} [Group G] (N : { N : Subgroup G // N.Normal }) :

orderIsoCon N = QuotientGroup.con ↑N

source

@[simp]

theorem AddSubgroup.orderIsoAddCon_apply {G : Type u} [AddGroup G] (N : { N : AddSubgroup G // N.Normal }) :

orderIsoAddCon N = QuotientAddGroup.con ↑N

source

@[simp]

theorem QuotientGroup.con_le_iff {G : Type u} [Group G] {N M : Subgroup G} [N.Normal] [M.Normal] :

QuotientGroup.con N ≤ QuotientGroup.con M ↔ N ≤ M

source

@[simp]

theorem QuotientAddGroup.con_le_iff {G : Type u} [AddGroup G] {N M : AddSubgroup G} [N.Normal] [M.Normal] :

QuotientAddGroup.con N ≤ QuotientAddGroup.con M ↔ N ≤ M

source

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

QuotientGroup.con N ≤ QuotientGroup.con M

source

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

QuotientAddGroup.con N ≤ QuotientAddGroup.con M

source

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

source

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

source

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

source

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

source

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

source

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

source

@[simp]

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

(lift N φ HN).comp (mk' N) = φ

source

@[simp]

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

(lift N φ HN).comp (mk' N) = φ

source

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

source

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

source

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

Function.Surjective ⇑(lift N φ HN)

source

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

Function.Surjective ⇑(lift N φ HN)

source

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

(lift N φ HN).ker = Subgroup.map (mk' N) φ.ker

source

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

(lift N φ HN).ker = AddSubgroup.map (mk' N) φ.ker

source

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

source

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

source

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

source

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

source

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)

source

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)

source

theorem QuotientGroup.map_surjective_of_surjective {G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] {H : Type v} [Group H] (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)

source

theorem QuotientAddGroup.map_surjective_of_surjective {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : N.Normal] {H : Type v} [AddGroup H] (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)

source

theorem QuotientGroup.ker_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) :

(map N M f h).ker = Subgroup.map (mk' N) (Subgroup.comap f M)

source

theorem QuotientAddGroup.ker_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) :

(map N M f h).ker = AddSubgroup.map (mk' N) (AddSubgroup.comap f M)

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

@[simp]

theorem QuotientGroup.image_coe {G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] :

mk '' ↑N = 1

source

@[simp]

theorem QuotientAddGroup.image_coe {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : N.Normal] :

mk '' ↑N = 0

source

theorem QuotientGroup.preimage_image_coe {G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] (s : Set G) :

mk ⁻¹' (mk '' s) = ↑N * s

source

theorem QuotientAddGroup.preimage_image_coe {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : N.Normal] (s : Set G) :

mk ⁻¹' (mk '' s) = ↑N + s

source

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

source

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

source

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

source

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

source

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

source

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)

source

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

source

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

source

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

Documentation

Mathlib.GroupTheory.QuotientGroup.Defs

Quotients of groups by normal subgroups #

Main definitions #

Tags #