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

theorem QuotientAddGroup.con.proof_1 {G : Type u_1} [AddGroup G] (N : AddSubgroup G) [nN : N.Normal] {a : G} {b : G} {c : G} {d : G} (hab : (QuotientAddGroup.leftRel N) a b) (hcd : (QuotientAddGroup.leftRel N) c d) :

(QuotientAddGroup.leftRel N) (a + c) (b + d)

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

Instances For

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

Instances For

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

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

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 ⋯

Instances For

source

theorem QuotientAddGroup.mk'.proof_1 {G : Type u_1} [AddGroup G] (N : AddSubgroup G) :

∀ (x x_1 : G), ↑(x + x_1) = ↑(x + x_1)

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 ⋯

Instances For

source

@[simp]

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

⇑(QuotientAddGroup.mk' N) = QuotientAddGroup.mk

source

@[simp]

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

⇑(QuotientGroup.mk' N) = QuotientGroup.mk

source

@[simp]

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

(QuotientAddGroup.mk' N) x = ↑x

source

@[simp]

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

(QuotientGroup.mk' N) x = ↑x

source

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

Function.Surjective ⇑(QuotientAddGroup.mk' N)

source

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

Function.Surjective ⇑(QuotientGroup.mk' N)

source

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

(QuotientAddGroup.mk' N) x = (QuotientAddGroup.mk' N) y ↔ ∃ z ∈ N, x + z = y

source

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

(QuotientGroup.mk' N) x = (QuotientGroup.mk' N) y ↔ ∃ z ∈ N, x * z = y

source

theorem QuotientAddGroup.addMonoidHom_ext {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : N.Normal] {M : Type x} [AddMonoid M] ⦃f : G ⧸ N →+ M⦄ ⦃g : G ⧸ N →+ M⦄ (h : f.comp (QuotientAddGroup.mk' N) = g.comp (QuotientAddGroup.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 QuotientAddGroup.addMonoidHom_ext_iff {G : Type u} [AddGroup G] {N : AddSubgroup G} [nN : N.Normal] {M : Type x} [AddMonoid M] {f : G ⧸ N →+ M} {g : G ⧸ N →+ M} :

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

source

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

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

source

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

@[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.eq_one_iff {G : Type u} [Group G] {N : Subgroup G} [N.Normal] (x : G) :

↑x = 1 ↔ x ∈ N

source

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 ↔ (QuotientAddGroup.mk' f.range).comp g.ker.subtype = 0

source

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 ↔ (QuotientGroup.mk' f.range).comp g.ker.subtype = 1

source

@[simp]

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

(QuotientAddGroup.mk' N).ker = N

source

@[simp]

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

(QuotientGroup.mk' N).ker = N

source

theorem QuotientAddGroup.eq_iff_sub_mem {G : Type u} [AddGroup G] {N : AddSubgroup G} [nN : N.Normal] {x : G} {y : G} :

↑x = ↑y ↔ x - y ∈ N

source

theorem QuotientGroup.eq_iff_div_mem {G : Type u} [Group G] {N : Subgroup G} [nN : N.Normal] {x : G} {y : G} :

↑x = ↑y ↔ x / y ∈ N

source

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

AddCommGroup (G ⧸ N)

Equations

QuotientAddGroup.Quotient.addCommGroup N = AddCommGroup.mk ⋯

source

theorem QuotientAddGroup.Quotient.addCommGroup.proof_1 {G : Type u_1} [AddCommGroup G] (N : AddSubgroup G) (a : G ⧸ N) (b : G ⧸ N) :

a + b = b + a

source

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

CommGroup (G ⧸ N)

Equations

QuotientGroup.Quotient.commGroup N = CommGroup.mk ⋯

source

@[simp]

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

↑0 = 0

source

@[simp]

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

↑1 = 1

source

@[simp]

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

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

source

@[simp]

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

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

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_inv {G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] (a : G) :

↑a⁻¹ = (↑a)⁻¹

source

@[simp]

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

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

source

@[simp]

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

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

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_pow {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.mk_zpow {G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] (a : G) (n : ℤ) :

↑(a ^ n) = ↑a ^ n

source

@[simp]

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

AddSubgroup.map (QuotientAddGroup.mk' N) N = ⊥

source

@[simp]

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

Subgroup.map (QuotientGroup.mk' N) N = ⊥

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

Instances For

source

theorem QuotientAddGroup.lift.proof_1 {G : Type u_1} [AddGroup G] (N : AddSubgroup G) [nN : N.Normal] {M : Type u_2} [AddMonoid M] (φ : G →+ M) (HN : N ≤ φ.ker) (x : G) (y : G) (h : (QuotientAddGroup.con N) x y) :

(AddCon.ker φ) x y

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

Instances For

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

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

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

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

(QuotientGroup.lift N φ HN) ↑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) :

(QuotientAddGroup.lift N φ HN) (Quot.mk (⇑(QuotientAddGroup.leftRel N)) g) = φ g

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

(QuotientGroup.lift N φ HN) (Quot.mk (⇑(QuotientGroup.leftRel N)) g) = φ g

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

Instances For

source

theorem QuotientAddGroup.map.proof_1 {G : Type u_1} [AddGroup G] (N : AddSubgroup G) {H : Type u_2} [AddGroup H] (M : AddSubgroup H) (f : G →+ H) (h : N ≤ AddSubgroup.comap f M) ⦃x : G⦄ (hx : x ∈ N) :

↑(f x) = ↑0

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

Instances For

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

(QuotientAddGroup.map N M f h) ↑x = ↑(f x)

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

(QuotientGroup.map N M f h) ↑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) :

(QuotientAddGroup.map N M f h) ((QuotientAddGroup.mk' N) 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) :

(QuotientGroup.map N M f h) ((QuotientGroup.mk' N) x) = ↑(f x)

source

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

(QuotientAddGroup.map N N (AddMonoidHom.id G) h) x = x

source

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

(QuotientGroup.map N N (MonoidHom.id G) h) x = x

source

@[simp]

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

QuotientAddGroup.map N N (AddMonoidHom.id G) h = AddMonoidHom.id (G ⧸ N)

source

@[simp]

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

QuotientGroup.map N N (MonoidHom.id G) h = MonoidHom.id (G ⧸ N)

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 : optParam (N ≤ AddSubgroup.comap (g.comp f) O) ⋯) (x : G ⧸ N) :

(QuotientAddGroup.map M O g hg) ((QuotientAddGroup.map N M f hf) x) = (QuotientAddGroup.map N O (g.comp f) hgf) x

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 : optParam (N ≤ Subgroup.comap (g.comp f) O) ⋯) (x : G ⧸ N) :

(QuotientGroup.map M O g hg) ((QuotientGroup.map N M f hf) x) = (QuotientGroup.map N O (g.comp f) hgf) x

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 : optParam (N ≤ AddSubgroup.comap (g.comp f) O) ⋯) :

(QuotientAddGroup.map M O g hg).comp (QuotientAddGroup.map N M f hf) = QuotientAddGroup.map N O (g.comp f) hgf

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 : optParam (N ≤ Subgroup.comap (g.comp f) O) ⋯) :

(QuotientGroup.map M O g hg).comp (QuotientGroup.map N M f hf) = QuotientGroup.map N O (g.comp f) hgf

source

@[simp]

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

QuotientAddGroup.mk '' ↑N = 0

source

@[simp]

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

QuotientGroup.mk '' ↑N = 1

source

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

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

source

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

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

source

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

QuotientAddGroup.mk '' s = QuotientAddGroup.mk '' t ↔ ↑N + s = ↑N + t

source

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

QuotientGroup.mk '' s = QuotientGroup.mk '' t ↔ ↑N * s = ↑N * t

source

theorem QuotientAddGroup.congr.proof_5 {G : Type u_2} [AddGroup G] {H : Type u_1} [AddGroup H] (G' : AddSubgroup G) (H' : AddSubgroup H) (e : G ≃+ H) (he : AddSubgroup.map (↑e) G' = H') :

H' ≤ AddSubgroup.comap (↑e.symm) G'

source

theorem QuotientAddGroup.congr.proof_6 {G : Type u_1} [AddGroup G] {H : Type u_2} [AddGroup H] (G' : AddSubgroup G) (H' : AddSubgroup H) [G'.Normal] [H'.Normal] (e : G ≃+ H) (he : AddSubgroup.map (↑e) G' = H') (x : G ⧸ G') :

(QuotientAddGroup.map H' G' ↑e.symm ⋯) ((QuotientAddGroup.map G' H' ↑e ⋯) x) = x

source

theorem QuotientAddGroup.congr.proof_3 {G : Type u_1} [AddGroup G] {H : Type u_2} [AddGroup H] (G' : AddSubgroup G) (H' : AddSubgroup H) (e : G ≃+ H) (he : AddSubgroup.map (↑e) G' = H') :

G' ≤ AddSubgroup.comap (↑e) H'

source

theorem QuotientAddGroup.congr.proof_1 {G : Type u_1} [AddGroup G] {H : Type u_2} [AddGroup H] :

AddMonoidHomClass (G ≃+ H) G H

source

theorem QuotientAddGroup.congr.proof_2 {G : Type u_1} [AddGroup G] {H : Type u_2} [AddGroup H] (G' : AddSubgroup G) (H' : AddSubgroup H) (e : G ≃+ H) (he : AddSubgroup.map (↑e) G' = H') :

G' ≤ AddSubgroup.comap (↑e) H'

source

theorem QuotientAddGroup.congr.proof_7 {G : Type u_2} [AddGroup G] {H : Type u_1} [AddGroup H] (G' : AddSubgroup G) (H' : AddSubgroup H) [G'.Normal] [H'.Normal] (e : G ≃+ H) (he : AddSubgroup.map (↑e) G' = H') (x : H ⧸ H') :

(QuotientAddGroup.map G' H' ↑e ⋯) ((QuotientAddGroup.map H' G' ↑e.symm ⋯) x) = x

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

Instances For

source

theorem QuotientAddGroup.congr.proof_4 {G : Type u_1} [AddGroup G] {H : Type u_2} [AddGroup H] :

AddMonoidHomClass (H ≃+ G) H G

source

theorem QuotientAddGroup.congr.proof_8 {G : Type u_1} [AddGroup G] {H : Type u_2} [AddGroup H] (G' : AddSubgroup G) (H' : AddSubgroup H) [G'.Normal] [H'.Normal] (e : G ≃+ H) (he : AddSubgroup.map (↑e) G' = H') (x : G ⧸ G') (y : G ⧸ G') :

(↑(QuotientAddGroup.map G' H' ↑e ⋯)).toFun (x + y) = (↑(QuotientAddGroup.map G' H' ↑e ⋯)).toFun x + (↑(QuotientAddGroup.map G' H' ↑e ⋯)).toFun y

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

Instances For

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

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

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

(QuotientGroup.congr G' H' e he) ↑x = (QuotientGroup.mk' H') (e x)

source

@[simp]

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

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

(QuotientGroup.congr G' H' e he).symm = QuotientGroup.congr H' G' e.symm ⋯

HepLean Documentation

Mathlib.GroupTheory.QuotientGroup.Defs

Quotients of groups by normal subgroups #

Main definitions #

Tags #