Group extensions from surjective homomorphisms

A surjective homomorphism determines an extension by its kernel. An equivalence with that kernel can be used to choose a different group as the extension's left term.

Main definitions and results

• GroupExtension.ofSurjective: the canonical extension by the kernel of a surjective homomorphism.
• GroupExtension.ofMulEquivKer: ofSurjective with its kernel relabelled by relabelKer.
• GroupExtension.ofMulEquivKer_inl: its inclusion is the given kernel equivalence followed by the kernel subtype.
• GroupExtension.ofMulEquivKer_rightHom: its projection is the original homomorphism.

The constructions are mirrored for additive groups by to_additive.

def GroupExtension.ofSurjective {E : Type v} {G : Type w} [Group E] [Group G] {f : E →* G} (hf : Function.Surjective ⇑f) : GroupExtension (↥f.ker) E G

A surjective homomorphism f : E →* G determines an extension of G by f.ker.

Equations

• GroupExtension.ofSurjective hf = { inl := f.ker.subtype, rightHom := f, inl_injective := ⋯, range_inl_eq_ker_rightHom := ⋯, rightHom_surjective := hf }

def AddGroupExtension.ofSurjective {E : Type v} {G : Type w} [AddGroup E] [AddGroup G] {f : E →+ G} (hf : Function.Surjective ⇑f) : AddGroupExtension (↥f.ker) E G

A surjective homomorphism f : E →+ G determines an extension of G by f.ker.

Equations

• AddGroupExtension.ofSurjective hf = { inl := f.ker.subtype, rightHom := f, inl_injective := ⋯, range_inl_eq_ker_rightHom := ⋯, rightHom_surjective := hf }

@[simp]

theorem GroupExtension.ofSurjective_inl {E : Type v} {G : Type w} [Group E] [Group G] {f : E →* G} (hf : Function.Surjective ⇑f) : (ofSurjective hf).inl = f.ker.subtype

The inclusion in GroupExtension.ofSurjective hf is the kernel subtype.

@[simp]

theorem AddGroupExtension.ofSurjective_inl {E : Type v} {G : Type w} [AddGroup E] [AddGroup G] {f : E →+ G} (hf : Function.Surjective ⇑f) : (ofSurjective hf).inl = f.ker.subtype

The inclusion in AddGroupExtension.ofSurjective hf is the kernel subtype.

@[simp]

theorem GroupExtension.ofSurjective_rightHom {E : Type v} {G : Type w} [Group E] [Group G] {f : E →* G} (hf : Function.Surjective ⇑f) : (ofSurjective hf).rightHom = f

The projection in GroupExtension.ofSurjective hf is the original homomorphism.

@[simp]

theorem AddGroupExtension.ofSurjective_rightHom {E : Type v} {G : Type w} [AddGroup E] [AddGroup G] {f : E →+ G} (hf : Function.Surjective ⇑f) : (ofSurjective hf).rightHom = f

The projection in AddGroupExtension.ofSurjective hf is the original homomorphism.

def GroupExtension.ofMulEquivKer {N : Type u} {E : Type v} {G : Type w} [Group N] [Group E] [Group G] {f : E →* G} (hf : Function.Surjective ⇑f) (e : N ≃* ↥f.ker) : GroupExtension N E G

A surjective homomorphism f : E →* G, together with an equivalence N ≃* f.ker, determines a group extension of G by N.

Equations

• GroupExtension.ofMulEquivKer hf e = (GroupExtension.ofSurjective hf).relabelKer e

def AddGroupExtension.ofAddEquivKer {N : Type u} {E : Type v} {G : Type w} [AddGroup N] [AddGroup E] [AddGroup G] {f : E →+ G} (hf : Function.Surjective ⇑f) (e : N ≃+ ↥f.ker) : AddGroupExtension N E G

A surjective homomorphism f : E →+ G, together with an equivalence N ≃+ f.ker, determines an additive group extension of G by N.

Equations

• AddGroupExtension.ofAddEquivKer hf e = (AddGroupExtension.ofSurjective hf).relabelKer e

@[simp]

theorem GroupExtension.ofMulEquivKer_inl {N : Type u} {E : Type v} {G : Type w} [Group N] [Group E] [Group G] {f : E →* G} (hf : Function.Surjective ⇑f) (e : N ≃* ↥f.ker) : (ofMulEquivKer hf e).inl = f.ker.subtype.comp e.toMonoidHom

The inclusion of GroupExtension.ofMulEquivKer hf e is the given kernel equivalence followed by the kernel subtype.

@[simp]

theorem AddGroupExtension.ofAddEquivKer_inl {N : Type u} {E : Type v} {G : Type w} [AddGroup N] [AddGroup E] [AddGroup G] {f : E →+ G} (hf : Function.Surjective ⇑f) (e : N ≃+ ↥f.ker) : (ofAddEquivKer hf e).inl = f.ker.subtype.comp e.toAddMonoidHom

The inclusion of AddGroupExtension.ofAddEquivKer hf e is the given kernel equivalence followed by the kernel subtype.

@[simp]

theorem GroupExtension.ofMulEquivKer_rightHom {N : Type u} {E : Type v} {G : Type w} [Group N] [Group E] [Group G] {f : E →* G} (hf : Function.Surjective ⇑f) (e : N ≃* ↥f.ker) : (ofMulEquivKer hf e).rightHom = f

The projection of GroupExtension.ofMulEquivKer hf e is the original homomorphism.

@[simp]

theorem AddGroupExtension.ofAddEquivKer_rightHom {N : Type u} {E : Type v} {G : Type w} [AddGroup N] [AddGroup E] [AddGroup G] {f : E →+ G} (hf : Function.Surjective ⇑f) (e : N ≃+ ↥f.ker) : (ofAddEquivKer hf e).rightHom = f

The projection of AddGroupExtension.ofAddEquivKer hf e is the original homomorphism.