Quotients of groups by normal subgroups #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
This files develops the basic theory of quotients of groups by normal subgroups. In particular it proves Noether's first and second isomorphism theorems.
Main definitions #
mk': the canonical group homomorphismG →* G/Ngiven a normal subgroupNofG.lift φ: the group homomorphismG/N →* Hgiven a group homomorphismφ : G →* Hsuch thatN ⊆ ker φ.map f: the group homomorphismG/N →* H/Mgiven a group homomorphismf : G →* Hsuch thatN ⊆ f⁻¹(M).
Main statements #
quotient_ker_equiv_range: Noether's first isomorphism theorem, an explicit isomorphismG/ker φ → range φfor every group homomorphismφ : G →* H.quotient_inf_equiv_prod_normal_quotient: Noether's second isomorphism theorem, an explicit isomorphism betweenH/(H ∩ N)and(HN)/Ngiven a subgroupHand a normal subgroupNof a groupG.quotient_group.quotient_quotient_equiv_quotient: Noether's third isomorphism theorem, the canonical isomorphism between(G / N) / (M / N)andG / M, whereN ≤ M.
Tags #
isomorphism theorems, quotient groups
@[protected]
The congruence relation generated by a normal subgroup.
Equations
- quotient_group.con N = {to_setoid := quotient_group.left_rel N, mul' := _}
@[protected]
def
quotient_add_group.con
{G : Type u}
[add_group G]
(N : add_subgroup G)
[nN : N.normal] :
add_con G
The additive congruence relation generated by a normal additive subgroup.
Equations
- quotient_add_group.con N = {to_setoid := quotient_add_group.left_rel N, add' := _}
@[protected, instance]
Equations
@[protected, instance]
def
quotient_add_group.quotient.add_group
{G : Type u}
[add_group G]
(N : add_subgroup G)
[nN : N.normal] :
Equations
The group homomorphism from G to G/N.
Equations
The additive group homomorphism from G to G/N.
Equations
@[simp]
theorem
quotient_group.coe_mk'
{G : Type u}
[group G]
(N : subgroup G)
[nN : N.normal] :
⇑(quotient_group.mk' N) = coe
@[simp]
theorem
quotient_add_group.coe_mk'
{G : Type u}
[add_group G]
(N : add_subgroup G)
[nN : N.normal] :
@[simp]
theorem
quotient_group.mk'_apply
{G : Type u}
[group G]
(N : subgroup G)
[nN : N.normal]
(x : G) :
⇑(quotient_group.mk' N) x = ↑x
@[simp]
theorem
quotient_add_group.mk'_apply
{G : Type u}
[add_group G]
(N : add_subgroup G)
[nN : N.normal]
(x : G) :
⇑(quotient_add_group.mk' N) x = ↑x
theorem
quotient_add_group.mk'_surjective
{G : Type u}
[add_group G]
(N : add_subgroup G)
[nN : N.normal] :
theorem
quotient_add_group.mk'_eq_mk'
{G : Type u}
[add_group G]
(N : add_subgroup G)
[nN : N.normal]
{x y : G} :
@[ext]
theorem
quotient_add_group.add_monoid_hom_ext
{G : Type u}
[add_group G]
(N : add_subgroup G)
[nN : N.normal]
{H : Type v}
[add_group H]
⦃f g : G ⧸ N →+ H⦄
(h : f.comp (quotient_add_group.mk' N) = g.comp (quotient_add_group.mk' N)) :
f = g
Two add_monoid_homs from an additive quotient group are equal if their
compositions with add_quotient_group.mk' are equal.
@[ext]
theorem
quotient_group.monoid_hom_ext
{G : Type u}
[group G]
(N : subgroup G)
[nN : N.normal]
{H : Type v}
[group H]
⦃f g : G ⧸ N →* H⦄
(h : f.comp (quotient_group.mk' N) = g.comp (quotient_group.mk' N)) :
f = g
Two monoid_homs from a quotient group are equal if their compositions with
quotient_group.mk' are equal.
@[simp]
theorem
quotient_add_group.eq_zero_iff
{G : Type u}
[add_group G]
{N : add_subgroup G}
[nN : N.normal]
(x : G) :
@[simp]
theorem
quotient_add_group.ker_mk
{G : Type u}
[add_group G]
(N : add_subgroup G)
[nN : N.normal] :
(quotient_add_group.mk' N).ker = N
@[simp]
theorem
quotient_group.ker_mk
{G : Type u}
[group G]
(N : subgroup G)
[nN : N.normal] :
(quotient_group.mk' N).ker = N
@[protected, instance]
def
quotient_add_group.quotient.add_comm_group
{G : Type u_1}
[add_comm_group G]
(N : add_subgroup G) :
add_comm_group (G ⧸ N)
Equations
- quotient_add_group.quotient.add_comm_group N = {add := add_group.add (quotient_add_group.quotient.add_group N), add_assoc := _, zero := add_group.zero (quotient_add_group.quotient.add_group N), zero_add := _, add_zero := _, nsmul := add_group.nsmul (quotient_add_group.quotient.add_group N), nsmul_zero' := _, nsmul_succ' := _, neg := add_group.neg (quotient_add_group.quotient.add_group N), sub := add_group.sub (quotient_add_group.quotient.add_group N), sub_eq_add_neg := _, zsmul := add_group.zsmul (quotient_add_group.quotient.add_group N), zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _}
@[protected, instance]
def
quotient_group.quotient.comm_group
{G : Type u_1}
[comm_group G]
(N : subgroup G) :
comm_group (G ⧸ N)
Equations
- quotient_group.quotient.comm_group N = {mul := group.mul (quotient_group.quotient.group N), mul_assoc := _, one := group.one (quotient_group.quotient.group N), one_mul := _, mul_one := _, npow := group.npow (quotient_group.quotient.group N), npow_zero' := _, npow_succ' := _, inv := group.inv (quotient_group.quotient.group N), div := group.div (quotient_group.quotient.group N), div_eq_mul_inv := _, zpow := group.zpow (quotient_group.quotient.group N), zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, mul_left_inv := _, mul_comm := _}
@[simp]
theorem
quotient_add_group.coe_zero
{G : Type u}
[add_group G]
(N : add_subgroup G)
[nN : N.normal] :
def
quotient_group.lift
{G : Type u}
[group G]
(N : subgroup G)
[nN : N.normal]
{H : Type v}
[group H]
(φ : G →* H)
(HN : ∀ (x : G), x ∈ N → ⇑φ x = 1) :
A group homomorphism φ : G →* H with N ⊆ ker(φ) descends (i.e. lifts) to a
group homomorphism G/N →* H.
Equations
- quotient_group.lift N φ HN = (quotient_group.con N).lift φ _
def
quotient_add_group.lift
{G : Type u}
[add_group G]
(N : add_subgroup G)
[nN : N.normal]
{H : Type v}
[add_group H]
(φ : G →+ H)
(HN : ∀ (x : G), x ∈ N → ⇑φ x = 0) :
An add_group homomorphism φ : G →+ H with N ⊆ ker(φ) descends (i.e. lifts)
to a group homomorphism G/N →* H.
Equations
- quotient_add_group.lift N φ HN = (quotient_add_group.con N).lift φ _
@[simp]
theorem
quotient_add_group.lift_mk'
{G : Type u}
[add_group G]
(N : add_subgroup G)
[nN : N.normal]
{H : Type v}
[add_group H]
{φ : G →+ H}
(HN : ∀ (x : G), x ∈ N → ⇑φ x = 0)
(g : G) :
⇑(quotient_add_group.lift N φ HN) (quotient_add_group.mk g) = ⇑φ g
def
quotient_add_group.map
{G : Type u}
[add_group G]
(N : add_subgroup G)
[nN : N.normal]
{H : Type v}
[add_group H]
(M : add_subgroup H)
[M.normal]
(f : G →+ H)
(h : N ≤ add_subgroup.comap f M) :
An add_group homomorphism f : G →+ H induces a map G/N →+ H/M if
N ⊆ f⁻¹(M).
Equations
- quotient_add_group.map N M f h = quotient_add_group.lift N ((quotient_add_group.mk' M).comp f) _
def
quotient_group.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) :
A group homomorphism f : G →* H induces a map G/N →* H/M if N ⊆ f⁻¹(M).
Equations
- quotient_group.map N M f h = quotient_group.lift N ((quotient_group.mk' M).comp f) _
@[simp]
theorem
quotient_add_group.map_coe
{G : Type u}
[add_group G]
(N : add_subgroup G)
[nN : N.normal]
{H : Type v}
[add_group H]
(M : add_subgroup H)
[M.normal]
(f : G →+ H)
(h : N ≤ add_subgroup.comap f M)
(x : G) :
theorem
quotient_group.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) :
⇑(quotient_group.map N M f h) (⇑(quotient_group.mk' N) x) = ↑(⇑f x)
theorem
quotient_add_group.map_mk'
{G : Type u}
[add_group G]
(N : add_subgroup G)
[nN : N.normal]
{H : Type v}
[add_group H]
(M : add_subgroup H)
[M.normal]
(f : G →+ H)
(h : N ≤ add_subgroup.comap f M)
(x : G) :
⇑(quotient_add_group.map N M f h) (⇑(quotient_add_group.mk' N) x) = ↑(⇑f x)
theorem
quotient_add_group.map_id_apply
{G : Type u}
[add_group G]
(N : add_subgroup G)
[nN : N.normal]
(h : N ≤ add_subgroup.comap (add_monoid_hom.id G) N := _)
(x : G ⧸ N) :
⇑(quotient_add_group.map N N (add_monoid_hom.id G) h) x = x
theorem
quotient_group.map_id_apply
{G : Type u}
[group G]
(N : subgroup G)
[nN : N.normal]
(h : N ≤ subgroup.comap (monoid_hom.id G) N := _)
(x : G ⧸ N) :
⇑(quotient_group.map N N (monoid_hom.id G) h) x = x
@[simp]
theorem
quotient_add_group.map_id
{G : Type u}
[add_group G]
(N : add_subgroup G)
[nN : N.normal]
(h : N ≤ add_subgroup.comap (add_monoid_hom.id G) N := _) :
quotient_add_group.map N N (add_monoid_hom.id G) h = add_monoid_hom.id (G ⧸ N)
@[simp]
theorem
quotient_group.map_id
{G : Type u}
[group G]
(N : subgroup G)
[nN : N.normal]
(h : N ≤ subgroup.comap (monoid_hom.id G) N := _) :
quotient_group.map N N (monoid_hom.id G) h = monoid_hom.id (G ⧸ N)
@[simp]
theorem
quotient_add_group.map_map
{G : Type u}
[add_group G]
(N : add_subgroup G)
[nN : N.normal]
{H : Type v}
[add_group H]
{I : Type u_1}
[add_group I]
(M : add_subgroup H)
(O : add_subgroup I)
[M.normal]
[O.normal]
(f : G →+ H)
(g : H →+ I)
(hf : N ≤ add_subgroup.comap f M)
(hg : M ≤ add_subgroup.comap g O)
(hgf : N ≤ add_subgroup.comap (g.comp f) O := _)
(x : G ⧸ N) :
⇑(quotient_add_group.map M O g hg) (⇑(quotient_add_group.map N M f hf) x) = ⇑(quotient_add_group.map N O (g.comp f) hgf) x
@[simp]
theorem
quotient_group.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) :
⇑(quotient_group.map M O g hg) (⇑(quotient_group.map N M f hf) x) = ⇑(quotient_group.map N O (g.comp f) hgf) x
@[simp]
theorem
quotient_add_group.map_comp_map
{G : Type u}
[add_group G]
(N : add_subgroup G)
[nN : N.normal]
{H : Type v}
[add_group H]
{I : Type u_1}
[add_group I]
(M : add_subgroup H)
(O : add_subgroup I)
[M.normal]
[O.normal]
(f : G →+ H)
(g : H →+ I)
(hf : N ≤ add_subgroup.comap f M)
(hg : M ≤ add_subgroup.comap g O)
(hgf : N ≤ add_subgroup.comap (g.comp f) O := _) :
(quotient_add_group.map M O g hg).comp (quotient_add_group.map N M f hf) = quotient_add_group.map N O (g.comp f) hgf
@[simp]
theorem
quotient_group.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 := _) :
(quotient_group.map M O g hg).comp (quotient_group.map N M f hf) = quotient_group.map N O (g.comp f) hgf
def
quotient_add_group.congr
{G : Type u}
[add_group G]
{H : Type v}
[add_group H]
(G' : add_subgroup G)
(H' : add_subgroup H)
[G'.normal]
[H'.normal]
(e : G ≃+ H)
(he : add_subgroup.map ↑e G' = H') :
quotient_add_group.congr lifts the isomorphism e : G ≃ H to G ⧸ G' ≃ H ⧸ H',
given that e maps G to H.
Equations
- quotient_add_group.congr G' H' e he = {to_fun := ⇑(quotient_add_group.map G' H' ↑e _), inv_fun := ⇑(quotient_add_group.map H' G' ↑(e.symm) _), left_inv := _, right_inv := _, map_add' := _}
def
quotient_group.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') :
quotient_group.congr lifts the isomorphism e : G ≃ H to G ⧸ G' ≃ H ⧸ H',
given that e maps G to H.
Equations
- quotient_group.congr G' H' e he = {to_fun := ⇑(quotient_group.map G' H' ↑e _), inv_fun := ⇑(quotient_group.map H' G' ↑(e.symm) _), left_inv := _, right_inv := _, map_mul' := _}
@[simp]
theorem
quotient_group.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) :
⇑(quotient_group.congr G' H' e he) (quotient_group.mk x) = ↑(⇑e x)
theorem
quotient_group.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) :
⇑(quotient_group.congr G' H' e he) (⇑(quotient_group.mk' G') x) = ⇑(quotient_group.mk' H') (⇑e x)
@[simp]
theorem
quotient_group.congr_refl
{G : Type u}
[group G]
(G' : subgroup G)
[G'.normal]
(he : subgroup.map ↑(mul_equiv.refl G) G' = G' := _) :
quotient_group.congr G' G' (mul_equiv.refl G) he = mul_equiv.refl (G ⧸ G')
@[simp]
theorem
quotient_group.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') :
(quotient_group.congr G' H' e he).symm = quotient_group.congr H' G' e.symm _
@[simp]
theorem
quotient_group.ker_lift_mk'
{G : Type u}
[group G]
{H : Type v}
[group H]
(φ : G →* H)
(g : G) :
⇑(quotient_group.ker_lift φ) (quotient_group.mk g) = ⇑φ g
@[simp]
theorem
quotient_add_group.ker_lift_mk'
{G : Type u}
[add_group G]
{H : Type v}
[add_group H]
(φ : G →+ H)
(g : G) :
⇑(quotient_add_group.ker_lift φ) (quotient_add_group.mk g) = ⇑φ g
def
quotient_group.quotient_ker_equiv_of_right_inverse
{G : Type u}
[group G]
{H : Type v}
[group H]
(φ : G →* H)
(ψ : H → G)
(hφ : function.right_inverse ψ ⇑φ) :
The canonical isomorphism G/(ker φ) ≃* H induced by a homomorphism φ : G →* H
with a right inverse ψ : H → G.
Equations
- quotient_group.quotient_ker_equiv_of_right_inverse φ ψ hφ = {to_fun := ⇑(quotient_group.ker_lift φ), inv_fun := quotient_group.mk ∘ ψ, left_inv := _, right_inv := hφ, map_mul' := _}
def
quotient_add_group.quotient_ker_equiv_of_right_inverse
{G : Type u}
[add_group G]
{H : Type v}
[add_group H]
(φ : G →+ H)
(ψ : H → G)
(hφ : function.right_inverse ψ ⇑φ) :
The canonical isomorphism G/(ker φ) ≃+ H induced by a homomorphism φ : G →+ H
with a right inverse ψ : H → G.
Equations
- quotient_add_group.quotient_ker_equiv_of_right_inverse φ ψ hφ = {to_fun := ⇑(quotient_add_group.ker_lift φ), inv_fun := quotient_add_group.mk ∘ ψ, left_inv := _, right_inv := hφ, map_add' := _}
@[simp]
theorem
quotient_group.quotient_ker_equiv_of_right_inverse_apply
{G : Type u}
[group G]
{H : Type v}
[group H]
(φ : G →* H)
(ψ : H → G)
(hφ : function.right_inverse ψ ⇑φ)
(ᾰ : G ⧸ φ.ker) :
⇑(quotient_group.quotient_ker_equiv_of_right_inverse φ ψ hφ) ᾰ = ⇑(quotient_group.ker_lift φ) ᾰ
@[simp]
theorem
quotient_add_group.quotient_ker_equiv_of_right_inverse_symm_apply
{G : Type u}
[add_group G]
{H : Type v}
[add_group H]
(φ : G →+ H)
(ψ : H → G)
(hφ : function.right_inverse ψ ⇑φ)
(ᾰ : H) :
⇑((quotient_add_group.quotient_ker_equiv_of_right_inverse φ ψ hφ).symm) ᾰ = (quotient_add_group.mk ∘ ψ) ᾰ
@[simp]
theorem
quotient_group.quotient_ker_equiv_of_right_inverse_symm_apply
{G : Type u}
[group G]
{H : Type v}
[group H]
(φ : G →* H)
(ψ : H → G)
(hφ : function.right_inverse ψ ⇑φ)
(ᾰ : H) :
⇑((quotient_group.quotient_ker_equiv_of_right_inverse φ ψ hφ).symm) ᾰ = (quotient_group.mk ∘ ψ) ᾰ
@[simp]
The canonical isomorphism G/⊥ ≃+ G.
Equations
- quotient_add_group.quotient_bot = quotient_add_group.quotient_ker_equiv_of_right_inverse (add_monoid_hom.id G) id quotient_add_group.quotient_bot._proof_2
The canonical isomorphism G/⊥ ≃* G.
Equations
- quotient_group.quotient_bot = quotient_group.quotient_ker_equiv_of_right_inverse (monoid_hom.id G) id quotient_group.quotient_bot._proof_2
@[simp]
@[simp]
@[simp]
theorem
quotient_add_group.quotient_bot_apply
{G : Type u}
[add_group G]
(ᾰ : G ⧸ (add_monoid_hom.id G).ker) :
noncomputable
def
quotient_add_group.quotient_ker_equiv_of_surjective
{G : Type u}
[add_group G]
{H : Type v}
[add_group H]
(φ : G →+ H)
(hφ : function.surjective ⇑φ) :
The canonical isomorphism G/(ker φ) ≃+ H induced by a surjection φ : G →+ H.
For a computable version, see quotient_add_group.quotient_ker_equiv_of_right_inverse.
noncomputable
def
quotient_group.quotient_ker_equiv_of_surjective
{G : Type u}
[group G]
{H : Type v}
[group H]
(φ : G →* H)
(hφ : function.surjective ⇑φ) :
The canonical isomorphism G/(ker φ) ≃* H induced by a surjection φ : G →* H.
For a computable version, see quotient_group.quotient_ker_equiv_of_right_inverse.
def
quotient_add_group.quotient_add_equiv_of_eq
{G : Type u}
[add_group G]
{M N : add_subgroup G}
[M.normal]
[N.normal]
(h : M = N) :
If two normal subgroups M and N of G are the same, their quotient groups are
isomorphic.
Equations
- quotient_add_group.quotient_add_equiv_of_eq h = {to_fun := (add_subgroup.quotient_equiv_of_eq h).to_fun, inv_fun := (add_subgroup.quotient_equiv_of_eq h).inv_fun, left_inv := _, right_inv := _, map_add' := _}
def
quotient_group.quotient_mul_equiv_of_eq
{G : Type u}
[group G]
{M N : subgroup G}
[M.normal]
[N.normal]
(h : M = N) :
If two normal subgroups M and N of G are the same, their quotient groups are
isomorphic.
Equations
- quotient_group.quotient_mul_equiv_of_eq h = {to_fun := (subgroup.quotient_equiv_of_eq h).to_fun, inv_fun := (subgroup.quotient_equiv_of_eq h).inv_fun, left_inv := _, right_inv := _, map_mul' := _}
@[simp]
theorem
quotient_add_group.quotient_add_equiv_of_eq_mk
{G : Type u}
[add_group G]
{M N : add_subgroup G}
[M.normal]
[N.normal]
(h : M = N)
(x : G) :
def
quotient_add_group.quotient_map_add_subgroup_of_of_le
{G : Type u}
[add_group G]
{A' A B' B : add_subgroup G}
[hAN : (A'.add_subgroup_of A).normal]
[hBN : (B'.add_subgroup_of B).normal]
(h' : A' ≤ B')
(h : A ≤ B) :
↥A ⧸ A'.add_subgroup_of A →+ ↥B ⧸ B'.add_subgroup_of B
Let A', A, B', B be subgroups of G. If A' ≤ B' and A ≤ B,
then there is a map A / (A' ⊓ A) →+ B / (B' ⊓ B) induced by the inclusions.
Equations
def
quotient_group.quotient_map_subgroup_of_of_le
{G : Type u}
[group G]
{A' A B' B : subgroup G}
[hAN : (A'.subgroup_of A).normal]
[hBN : (B'.subgroup_of B).normal]
(h' : A' ≤ B')
(h : A ≤ B) :
↥A ⧸ A'.subgroup_of A →* ↥B ⧸ B'.subgroup_of B
Let A', A, B', B be subgroups of G. If A' ≤ B' and A ≤ B,
then there is a map A / (A' ⊓ A) →* B / (B' ⊓ B) induced by the inclusions.
Equations
- quotient_group.quotient_map_subgroup_of_of_le h' h = quotient_group.map (A'.subgroup_of A) (B'.subgroup_of B) (subgroup.inclusion h) _
@[simp]
theorem
quotient_add_group.quotient_map_add_subgroup_of_of_le_coe
{G : Type u}
[add_group G]
{A' A B' B : add_subgroup G}
[hAN : (A'.add_subgroup_of A).normal]
[hBN : (B'.add_subgroup_of B).normal]
(h' : A' ≤ B')
(h : A ≤ B)
(x : ↥A) :
@[simp]
theorem
quotient_group.quotient_map_subgroup_of_of_le_coe
{G : Type u}
[group G]
{A' A B' B : subgroup G}
[hAN : (A'.subgroup_of A).normal]
[hBN : (B'.subgroup_of B).normal]
(h' : A' ≤ B')
(h : A ≤ B)
(x : ↥A) :
⇑(quotient_group.quotient_map_subgroup_of_of_le h' h) ↑x = ↑(⇑(subgroup.inclusion h) x)
def
quotient_group.equiv_quotient_subgroup_of_of_eq
{G : Type u}
[group G]
{A' A B' B : subgroup G}
[hAN : (A'.subgroup_of A).normal]
[hBN : (B'.subgroup_of B).normal]
(h' : A' = B')
(h : A = B) :
↥A ⧸ A'.subgroup_of A ≃* ↥B ⧸ B'.subgroup_of B
Let A', A, B', B be subgroups of G.
If A' = B' and A = B, then the quotients A / (A' ⊓ A) and B / (B' ⊓ B) are isomorphic.
Applying this equiv is nicer than rewriting along the equalities, since the type of
(A'.subgroup_of A : subgroup A) depends on on A.
def
quotient_add_group.equiv_quotient_add_subgroup_of_of_eq
{G : Type u}
[add_group G]
{A' A B' B : add_subgroup G}
[hAN : (A'.add_subgroup_of A).normal]
[hBN : (B'.add_subgroup_of B).normal]
(h' : A' = B')
(h : A = B) :
↥A ⧸ A'.add_subgroup_of A ≃+ ↥B ⧸ B'.add_subgroup_of B
Let A', A, B', B be subgroups of G.
If A' = B' and A = B, then the quotients A / (A' ⊓ A) and B / (B' ⊓ B) are isomorphic.
Applying this equiv is nicer than rewriting along the equalities, since the type of
(A'.add_subgroup_of A : add_subgroup A) depends on on A.
def
quotient_group.hom_quotient_zpow_of_hom
{A B : Type u}
[comm_group A]
[comm_group B]
(f : A →* B)
(n : ℤ) :
A ⧸ (zpow_group_hom n).range →* B ⧸ (zpow_group_hom n).range
The map of quotients by powers of an integer induced by a group homomorphism.
Equations
def
quotient_add_group.hom_quotient_zsmul_of_hom
{A B : Type u}
[add_comm_group A]
[add_comm_group B]
(f : A →+ B)
(n : ℤ) :
A ⧸ (zsmul_add_group_hom n).range →+ B ⧸ (zsmul_add_group_hom n).range
The map of quotients by multiples of an integer induced by an additive group homomorphism.
Equations
@[simp]
@[simp]
@[simp]
theorem
quotient_group.hom_quotient_zpow_of_hom_comp
{A B : Type u}
[comm_group A]
[comm_group B]
(f : A →* B)
(g : B →* A)
(n : ℤ) :
@[simp]
theorem
quotient_add_group.hom_quotient_zsmul_of_hom_comp
{A B : Type u}
[add_comm_group A]
[add_comm_group B]
(f : A →+ B)
(g : B →+ A)
(n : ℤ) :
@[simp]
theorem
quotient_group.hom_quotient_zpow_of_hom_comp_of_right_inverse
{A B : Type u}
[comm_group A]
[comm_group B]
(f : A →* B)
(g : B →* A)
(n : ℤ)
(i : function.right_inverse ⇑g ⇑f) :
@[simp]
theorem
quotient_add_group.hom_quotient_zsmul_of_hom_comp_of_right_inverse
{A B : Type u}
[add_comm_group A]
[add_comm_group B]
(f : A →+ B)
(g : B →+ A)
(n : ℤ)
(i : function.right_inverse ⇑g ⇑f) :
def
quotient_group.equiv_quotient_zpow_of_equiv
{A B : Type u}
[comm_group A]
[comm_group B]
(e : A ≃* B)
(n : ℤ) :
A ⧸ (zpow_group_hom n).range ≃* B ⧸ (zpow_group_hom n).range
The equivalence of quotients by powers of an integer induced by a group isomorphism.
Equations
def
quotient_add_group.equiv_quotient_zsmul_of_equiv
{A B : Type u}
[add_comm_group A]
[add_comm_group B]
(e : A ≃+ B)
(n : ℤ) :
A ⧸ (zsmul_add_group_hom n).range ≃+ B ⧸ (zsmul_add_group_hom n).range
The equivalence of quotients by multiples of an integer induced by an additive group isomorphism.
@[simp]
@[simp]
theorem
quotient_add_group.equiv_quotient_zsmul_of_equiv_refl
{A : Type u}
[add_comm_group A]
(n : ℤ) :
@[simp]
theorem
quotient_group.equiv_quotient_zpow_of_equiv_symm
{A B : Type u}
[comm_group A]
[comm_group B]
(e : A ≃* B)
(n : ℤ) :
@[simp]
theorem
quotient_add_group.equiv_quotient_zsmul_of_equiv_symm
{A B : Type u}
[add_comm_group A]
[add_comm_group B]
(e : A ≃+ B)
(n : ℤ) :
@[simp]
theorem
quotient_group.equiv_quotient_zpow_of_equiv_trans
{A B C : Type u}
[comm_group A]
[comm_group B]
[comm_group C]
(e : A ≃* B)
(d : B ≃* C)
(n : ℤ) :
@[simp]
theorem
quotient_add_group.equiv_quotient_zsmul_of_equiv_trans
{A B C : Type u}
[add_comm_group A]
[add_comm_group B]
[add_comm_group C]
(e : A ≃+ B)
(d : B ≃+ C)
(n : ℤ) :
noncomputable
def
quotient_group.quotient_inf_equiv_prod_normal_quotient
{G : Type u}
[group G]
(H N : subgroup G)
[N.normal] :
↥H ⧸ N.subgroup_of H ≃* ↥(H ⊔ N) ⧸ N.subgroup_of (H ⊔ N)
Noether's second isomorphism theorem: given two subgroups H and N of a group G, where
N is normal, defines an isomorphism between H/(H ∩ N) and (HN)/N.
Equations
- quotient_group.quotient_inf_equiv_prod_normal_quotient H N = let φ : ↥H →* ↥(H ⊔ N) ⧸ N.subgroup_of (H ⊔ N) := (quotient_group.mk' (N.subgroup_of (H ⊔ N))).comp (subgroup.inclusion _) in have φ_surjective : function.surjective ⇑φ, from _, (quotient_group.quotient_mul_equiv_of_eq _).trans (quotient_group.quotient_ker_equiv_of_surjective φ φ_surjective)
noncomputable
def
quotient_add_group.quotient_inf_equiv_sum_normal_quotient
{G : Type u}
[add_group G]
(H N : add_subgroup G)
[N.normal] :
↥H ⧸ N.add_subgroup_of H ≃+ ↥(H ⊔ N) ⧸ N.add_subgroup_of (H ⊔ N)
The second isomorphism theorem: given two subgroups H and N of a group G,
where N is normal, defines an isomorphism between H/(H ∩ N) and (H + N)/N
Equations
- quotient_add_group.quotient_inf_equiv_sum_normal_quotient H N = let φ : ↥H →+ ↥(H ⊔ N) ⧸ N.add_subgroup_of (H ⊔ N) := (quotient_add_group.mk' (N.add_subgroup_of (H ⊔ N))).comp (add_subgroup.inclusion _) in have φ_surjective : function.surjective ⇑φ, from _, (quotient_add_group.quotient_add_equiv_of_eq _).trans (quotient_add_group.quotient_ker_equiv_of_surjective φ φ_surjective)
@[protected, instance]
def
quotient_group.map_normal
{G : Type u}
[group G]
(N : subgroup G)
[nN : N.normal]
(M : subgroup G)
[nM : M.normal] :
(subgroup.map (quotient_group.mk' N) M).normal
@[protected, instance]
def
quotient_add_group.map_normal
{G : Type u}
[add_group G]
(N : add_subgroup G)
[nN : N.normal]
(M : add_subgroup G)
[nM : M.normal] :
def
quotient_add_group.quotient_quotient_equiv_quotient_aux
{G : Type u}
[add_group G]
(N : add_subgroup G)
[nN : N.normal]
(M : add_subgroup G)
[nM : M.normal]
(h : N ≤ M) :
(G ⧸ N) ⧸ add_subgroup.map (quotient_add_group.mk' N) M →+ G ⧸ M
The map from the third isomorphism theorem for additive groups:
(A / N) / (M / N) → A / M.
Equations
def
quotient_group.quotient_quotient_equiv_quotient_aux
{G : Type u}
[group G]
(N : subgroup G)
[nN : N.normal]
(M : subgroup G)
[nM : M.normal]
(h : N ≤ M) :
(G ⧸ N) ⧸ subgroup.map (quotient_group.mk' N) M →* G ⧸ M
The map from the third isomorphism theorem for groups: (G / N) / (M / N) → G / M.
Equations
- quotient_group.quotient_quotient_equiv_quotient_aux N M h = quotient_group.lift (subgroup.map (quotient_group.mk' N) M) (quotient_group.map N M (monoid_hom.id G) h) _
@[simp]
theorem
quotient_add_group.quotient_quotient_equiv_quotient_aux_coe
{G : Type u}
[add_group G]
(N : add_subgroup G)
[nN : N.normal]
(M : add_subgroup G)
[nM : M.normal]
(h : N ≤ M)
(x : G ⧸ N) :
⇑(quotient_add_group.quotient_quotient_equiv_quotient_aux N M h) ↑x = ⇑(quotient_add_group.map N M (add_monoid_hom.id G) h) x
@[simp]
theorem
quotient_group.quotient_quotient_equiv_quotient_aux_coe
{G : Type u}
[group G]
(N : subgroup G)
[nN : N.normal]
(M : subgroup G)
[nM : M.normal]
(h : N ≤ M)
(x : G ⧸ N) :
⇑(quotient_group.quotient_quotient_equiv_quotient_aux N M h) ↑x = ⇑(quotient_group.map N M (monoid_hom.id G) h) x
theorem
quotient_add_group.quotient_quotient_equiv_quotient_aux_coe_coe
{G : Type u}
[add_group G]
(N : add_subgroup G)
[nN : N.normal]
(M : add_subgroup G)
[nM : M.normal]
(h : N ≤ M)
(x : G) :
def
quotient_group.quotient_quotient_equiv_quotient
{G : Type u}
[group G]
(N : subgroup G)
[nN : N.normal]
(M : subgroup G)
[nM : M.normal]
(h : N ≤ M) :
(G ⧸ N) ⧸ subgroup.map (quotient_group.mk' N) M ≃* G ⧸ M
Noether's third isomorphism theorem for groups: (G / N) / (M / N) ≃* G / M.
Equations
def
quotient_add_group.quotient_quotient_equiv_quotient
{G : Type u}
[add_group G]
(N : add_subgroup G)
[nN : N.normal]
(M : add_subgroup G)
[nM : M.normal]
(h : N ≤ M) :
(G ⧸ N) ⧸ add_subgroup.map (quotient_add_group.mk' N) M ≃+ G ⧸ M
Noether's third isomorphism theorem for additive groups:
(A / N) / (M / N) ≃+ A / M.
Equations
theorem
quotient_add_group.subsingleton_quotient_top
{G : Type u}
[add_group G] :
subsingleton (G ⧸ ⊤)
theorem
quotient_add_group.add_subgroup_eq_top_of_subsingleton
{G : Type u}
[add_group G]
(H : add_subgroup G)
(h : subsingleton (G ⧸ H)) :
If the quotient by an additive subgroup gives a singleton then the additive subgroup is the whole additive group.
theorem
quotient_group.subgroup_eq_top_of_subsingleton
{G : Type u}
[group G]
(H : subgroup G)
(h : subsingleton (G ⧸ H)) :
If the quotient by a subgroup gives a singleton then the subgroup is the whole group.
theorem
quotient_group.comap_comap_center
{G : Type u}
[group G]
{H₁ : subgroup G}
[H₁.normal]
{H₂ : subgroup (G ⧸ H₁)}
[H₂.normal] :
subgroup.comap (quotient_group.mk' H₁) (subgroup.comap (quotient_group.mk' H₂) (subgroup.center ((G ⧸ H₁) ⧸ H₂))) = subgroup.comap (quotient_group.mk' (subgroup.comap (quotient_group.mk' H₁) H₂)) (subgroup.center (G ⧸ subgroup.comap (quotient_group.mk' H₁) H₂))
theorem
quotient_add_group.comap_comap_center
{G : Type u}
[add_group G]
{H₁ : add_subgroup G}
[H₁.normal]
{H₂ : add_subgroup (G ⧸ H₁)}
[H₂.normal] :
add_subgroup.comap (quotient_add_group.mk' H₁) (add_subgroup.comap (quotient_add_group.mk' H₂) (add_subgroup.center ((G ⧸ H₁) ⧸ H₂))) = add_subgroup.comap (quotient_add_group.mk' (add_subgroup.comap (quotient_add_group.mk' H₁) H₂)) (add_subgroup.center (G ⧸ add_subgroup.comap (quotient_add_group.mk' H₁) H₂))
noncomputable
def
group.fintype_of_ker_le_range
{F G H : Type u}
[group F]
[group G]
[group H]
[fintype F]
[fintype H]
(f : F →* G)
(g : G →* H)
(h : g.ker ≤ f.range) :
fintype G
If F and H are finite such that ker(G →* H) ≤ im(F →* G), then G is finite.
Equations
- group.fintype_of_ker_le_range f g h = fintype.of_equiv ((G ⧸ g.ker) × ↥(g.ker)) subgroup.group_equiv_quotient_times_subgroup.symm