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

Instances For

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

Instances For

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
@[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 `MonoidHom`s 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 `AddMonoidHom`s 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 := have 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 := have 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' := ⋯ }

Instances For

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

Instances For

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.

Instances For

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.

Instances For

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. `lift`s) to a group homomorphism `G/N →* M`.

Equations

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

Instances For

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. `lift`s) to a group homomorphism `G/N →* M`.

Equations

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

Instances For

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

Instances For

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

Instances For

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