Quotients of groups by normal subgroups

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 statements

• QuotientGroup.quotientKerEquivRange: Noether's first isomorphism theorem, an explicit isomorphism G/ker φ → range φ for every group homomorphism φ : G →* H.

Tags

isomorphism theorems, quotient groups

def QuotientGroup.rangeKerLift {G : Type u} [Group G] {H : Type v} [Group H] (φ : G →* H) : G ⧸ φ.ker →* ↥φ.range

The induced map from the quotient by the kernel to the range.

Equations

• QuotientGroup.rangeKerLift φ = QuotientGroup.lift φ.ker φ.rangeRestrict ⋯

def QuotientAddGroup.rangeKerLift {G : Type u} [AddGroup G] {H : Type v} [AddGroup H] (φ : G →+ H) : G ⧸ φ.ker →+ ↥φ.range

The induced map from the quotient by the kernel to the range.

Equations

• QuotientAddGroup.rangeKerLift φ = QuotientAddGroup.lift φ.ker φ.rangeRestrict ⋯

theorem QuotientGroup.rangeKerLift_injective {G : Type u} [Group G] {H : Type v} [Group H] (φ : G →* H) : Function.Injective ⇑(rangeKerLift φ)

theorem QuotientAddGroup.rangeKerLift_injective {G : Type u} [AddGroup G] {H : Type v} [AddGroup H] (φ : G →+ H) : Function.Injective ⇑(rangeKerLift φ)

theorem QuotientGroup.rangeKerLift_surjective {G : Type u} [Group G] {H : Type v} [Group H] (φ : G →* H) : Function.Surjective ⇑(rangeKerLift φ)

theorem QuotientAddGroup.rangeKerLift_surjective {G : Type u} [AddGroup G] {H : Type v} [AddGroup H] (φ : G →+ H) : Function.Surjective ⇑(rangeKerLift φ)

noncomputable def QuotientGroup.quotientKerEquivRange {G : Type u} [Group G] {H : Type v} [Group H] (φ : G →* H) : G ⧸ φ.ker ≃* ↥φ.range

Noether's first isomorphism theorem (a definition): the canonical isomorphism between G/(ker φ) to range φ.

Equations

• QuotientGroup.quotientKerEquivRange φ = MulEquiv.ofBijective (QuotientGroup.rangeKerLift φ) ⋯

noncomputable def QuotientAddGroup.quotientKerEquivRange {G : Type u} [AddGroup G] {H : Type v} [AddGroup H] (φ : G →+ H) : G ⧸ φ.ker ≃+ ↥φ.range

The first isomorphism theorem (a definition): the canonical isomorphism between G/(ker φ) to range φ.

Equations

• QuotientAddGroup.quotientKerEquivRange φ = AddEquiv.ofBijective (QuotientAddGroup.rangeKerLift φ) ⋯