Group Extensions

This file defines extensions of multiplicative and additive groups and their associated structures such as splittings and equivalences.

Main definitions

• (Add?)GroupExtension N E G: structure for extensions of G by N as short exact sequences 1 → N → E → G → 1 (0 → N → E → G → 0 for additive groups)
• (Add?)GroupExtension.Equiv S S': structure for equivalences of two group extensions S and S' as specific homomorphisms E → E' such that each diagram below is commutative

For multiplicative groups:
      ↗︎ E  ↘
1 → N   ↓    G → 1
      ↘︎ E' ↗︎️

For additive groups:
      ↗︎ E  ↘
0 → N   ↓    G → 0
      ↘︎ E' ↗︎️

• (Add?)GroupExtension.Splitting S: structure for splittings of a group extension S of G by N as section homomorphisms G → E
• SemidirectProduct.toGroupExtension φ: the multiplicative group extension associated to the semidirect product coming from φ : G →* MulAut N, 1 → N → N ⋊[φ] G → G → 1

TODO

If N is abelian,

• there is a bijection between N-conjugacy classes of (SemidirectProduct.toGroupExtension φ).Splitting and groupCohomology.H1 (which will be available in GroupTheory/GroupExtension/Abelian.lean to be added in a later PR).
• there is a bijection between equivalence classes of group extensions and groupCohomology.H2 (which is also stated as a TODO in RepresentationTheory/GroupCohomology/LowDegree.lean).

structure AddGroupExtension (N : Type u_1) (E : Type u_2) (G : Type u_3) [AddGroup N] [AddGroup E] [AddGroup G] : Type (max (max u_1 u_2) u_3)

AddGroupExtension N E G is a short exact sequence of additive groups 0 → N → E → G → 0.

• inl : N →+ E

  The inclusion homomorphism N →+ E

• rightHom : E →+ G

  The projection homomorphism E →+ G

• inl_injective : Function.Injective ⇑self.inl

  The inclusion map is injective.

• range_inl_eq_ker_rightHom : self.inl.range = self.rightHom.ker

  The range of the inclusion map is equal to the kernel of the projection map.

• rightHom_surjective : Function.Surjective ⇑self.rightHom

  The projection map is surjective.

theorem AddGroupExtension.inl_injective {N : Type u_1} {E : Type u_2} {G : Type u_3} [AddGroup N] [AddGroup E] [AddGroup G] (self : AddGroupExtension N E G) : Function.Injective ⇑self.inl

The inclusion map is injective.

theorem AddGroupExtension.range_inl_eq_ker_rightHom {N : Type u_1} {E : Type u_2} {G : Type u_3} [AddGroup N] [AddGroup E] [AddGroup G] (self : AddGroupExtension N E G) : self.inl.range = self.rightHom.ker

The range of the inclusion map is equal to the kernel of the projection map.

theorem AddGroupExtension.rightHom_surjective {N : Type u_1} {E : Type u_2} {G : Type u_3} [AddGroup N] [AddGroup E] [AddGroup G] (self : AddGroupExtension N E G) : Function.Surjective ⇑self.rightHom

The projection map is surjective.

structure GroupExtension (N : Type u_1) (E : Type u_2) (G : Type u_3) [Group N] [Group E] [Group G] : Type (max (max u_1 u_2) u_3)

GroupExtension N E G is a short exact sequence of groups 1 → N → E → G → 1.

• inl : N →* E

  The inclusion homomorphism N →* E

• rightHom : E →* G

  The projection homomorphism E →* G

• inl_injective : Function.Injective ⇑self.inl

  The inclusion map is injective.

• range_inl_eq_ker_rightHom : self.inl.range = self.rightHom.ker

  The range of the inclusion map is equal to the kernel of the projection map.

• rightHom_surjective : Function.Surjective ⇑self.rightHom

  The projection map is surjective.

theorem GroupExtension.inl_injective {N : Type u_1} {E : Type u_2} {G : Type u_3} [Group N] [Group E] [Group G] (self : GroupExtension N E G) : Function.Injective ⇑self.inl

The inclusion map is injective.

theorem GroupExtension.range_inl_eq_ker_rightHom {N : Type u_1} {E : Type u_2} {G : Type u_3} [Group N] [Group E] [Group G] (self : GroupExtension N E G) : self.inl.range = self.rightHom.ker

The range of the inclusion map is equal to the kernel of the projection map.

theorem GroupExtension.rightHom_surjective {N : Type u_1} {E : Type u_2} {G : Type u_3} [Group N] [Group E] [Group G] (self : GroupExtension N E G) : Function.Surjective ⇑self.rightHom

The projection map is surjective.

structure AddGroupExtension.Equiv {N : Type u_1} {E : Type u_2} {G : Type u_3} [AddGroup N] [AddGroup E] [AddGroup G] (S : AddGroupExtension N E G) {E' : Type u_4} [AddGroup E'] (S' : AddGroupExtension N E' G) : Type (max u_2 u_4)

AddGroupExtensions are equivalent iff there is a homomorphism making a commuting diagram.

• toAddMonoidHom : E →+ E'

  The homomorphism

• inl_comm : self.toAddMonoidHom.comp S.inl = S'.inl

  The left-hand side of the diagram commutes.

• rightHom_comm : S'.rightHom.comp self.toAddMonoidHom = S.rightHom

  The right-hand side of the diagram commutes.

theorem AddGroupExtension.Equiv.inl_comm {N : Type u_1} {E : Type u_2} {G : Type u_3} [AddGroup N] [AddGroup E] [AddGroup G] {S : AddGroupExtension N E G} {E' : Type u_4} [AddGroup E'] {S' : AddGroupExtension N E' G} (self : S.Equiv S') : self.toAddMonoidHom.comp S.inl = S'.inl

The left-hand side of the diagram commutes.

theorem AddGroupExtension.Equiv.rightHom_comm {N : Type u_1} {E : Type u_2} {G : Type u_3} [AddGroup N] [AddGroup E] [AddGroup G] {S : AddGroupExtension N E G} {E' : Type u_4} [AddGroup E'] {S' : AddGroupExtension N E' G} (self : S.Equiv S') : S'.rightHom.comp self.toAddMonoidHom = S.rightHom

The right-hand side of the diagram commutes.

structure AddGroupExtension.Splitting {N : Type u_1} {E : Type u_2} {G : Type u_3} [AddGroup N] [AddGroup E] [AddGroup G] (S : AddGroupExtension N E G) : Type (max u_2 u_3)

Splitting of an additive group extension is a section homomorphism.

• sectionHom : G →+ E

  A section homomorphism

• rightHom_comp_sectionHom : S.rightHom.comp self.sectionHom = AddMonoidHom.id G

  The section is a left inverse of the projection map.

theorem AddGroupExtension.Splitting.rightHom_comp_sectionHom {N : Type u_1} {E : Type u_2} {G : Type u_3} [AddGroup N] [AddGroup E] [AddGroup G] {S : AddGroupExtension N E G} (self : S.Splitting) : S.rightHom.comp self.sectionHom = AddMonoidHom.id G

The section is a left inverse of the projection map.

instance AddGroupExtension.normal_inl_range {N : Type u_1} {E : Type u_2} {G : Type u_3} [AddGroup N] [AddGroup E] [AddGroup G] (S : AddGroupExtension N E G) : S.inl.range.Normal

The range of the inclusion map is a normal additive subgroup.

Equations

• ⋯ = ⋯

instance GroupExtension.normal_inl_range {N : Type u_1} {E : Type u_2} {G : Type u_3} [Group N] [Group E] [Group G] (S : GroupExtension N E G) : S.inl.range.Normal

The range of the inclusion map is a normal subgroup.

Equations

• ⋯ = ⋯

@[simp]

theorem AddGroupExtension.rightHom_inl {N : Type u_1} {E : Type u_2} {G : Type u_3} [AddGroup N] [AddGroup E] [AddGroup G] (S : AddGroupExtension N E G) (n : N) : S.rightHom (S.inl n) = 0

@[simp]

theorem GroupExtension.rightHom_inl {N : Type u_1} {E : Type u_2} {G : Type u_3} [Group N] [Group E] [Group G] (S : GroupExtension N E G) (n : N) : S.rightHom (S.inl n) = 1

@[simp]

theorem AddGroupExtension.rightHom_comp_inl {N : Type u_1} {E : Type u_2} {G : Type u_3} [AddGroup N] [AddGroup E] [AddGroup G] (S : AddGroupExtension N E G) : S.rightHom.comp S.inl = 0

@[simp]

theorem GroupExtension.rightHom_comp_inl {N : Type u_1} {E : Type u_2} {G : Type u_3} [Group N] [Group E] [Group G] (S : GroupExtension N E G) : S.rightHom.comp S.inl = 1

noncomputable def GroupExtension.conjAct {N : Type u_1} {E : Type u_2} {G : Type u_3} [Group N] [Group E] [Group G] (S : GroupExtension N E G) : E →* MulAut N

E acts on N by conjugation.

Equations

• S.conjAct = { toFun := fun (e : E) => (MonoidHom.ofInjective ⋯).trans (MulEquiv.trans (MulAut.conjNormal e) (MonoidHom.ofInjective ⋯).symm), map_one' := ⋯, map_mul' := ⋯ }

theorem GroupExtension.inl_conjAct_comm {N : Type u_1} {E : Type u_2} {G : Type u_3} [Group N] [Group E] [Group G] (S : GroupExtension N E G) {e : E} {n : N} : S.inl ((S.conjAct e) n) = e * S.inl n * e⁻¹

The inclusion and a conjugation commute.

structure GroupExtension.Equiv {N : Type u_1} {E : Type u_2} {G : Type u_3} [Group N] [Group E] [Group G] (S : GroupExtension N E G) {E' : Type u_4} [Group E'] (S' : GroupExtension N E' G) : Type (max u_2 u_4)

GroupExtensions are equivalent iff there is a homomorphism making a commuting diagram.

• toMonoidHom : E →* E'

  The homomorphism

• inl_comm : self.toMonoidHom.comp S.inl = S'.inl

  The left-hand side of the diagram commutes.

• rightHom_comm : S'.rightHom.comp self.toMonoidHom = S.rightHom

  The right-hand side of the diagram commutes.

theorem GroupExtension.Equiv.inl_comm {N : Type u_1} {E : Type u_2} {G : Type u_3} [Group N] [Group E] [Group G] {S : GroupExtension N E G} {E' : Type u_4} [Group E'] {S' : GroupExtension N E' G} (self : S.Equiv S') : self.toMonoidHom.comp S.inl = S'.inl

The left-hand side of the diagram commutes.

theorem GroupExtension.Equiv.rightHom_comm {N : Type u_1} {E : Type u_2} {G : Type u_3} [Group N] [Group E] [Group G] {S : GroupExtension N E G} {E' : Type u_4} [Group E'] {S' : GroupExtension N E' G} (self : S.Equiv S') : S'.rightHom.comp self.toMonoidHom = S.rightHom

The right-hand side of the diagram commutes.

structure GroupExtension.Splitting {N : Type u_1} {E : Type u_2} {G : Type u_3} [Group N] [Group E] [Group G] (S : GroupExtension N E G) : Type (max u_2 u_3)

Splitting of a group extension is a section homomorphism.

• sectionHom : G →* E

  A section homomorphism

• rightHom_comp_sectionHom : S.rightHom.comp self.sectionHom = MonoidHom.id G

  The section is a left inverse of the projection map.

theorem GroupExtension.Splitting.rightHom_comp_sectionHom {N : Type u_1} {E : Type u_2} {G : Type u_3} [Group N] [Group E] [Group G] {S : GroupExtension N E G} (self : S.Splitting) : S.rightHom.comp self.sectionHom = MonoidHom.id G

The section is a left inverse of the projection map.

instance AddGroupExtension.instFunLikeSplitting {N : Type u_1} {E : Type u_2} {G : Type u_3} [AddGroup N] [AddGroup E] [AddGroup G] (S : AddGroupExtension N E G) : FunLike S.Splitting G E

Equations

• S.instFunLikeSplitting = { coe := fun (s : S.Splitting) => ⇑s.sectionHom, coe_injective' := ⋯ }

theorem AddGroupExtension.instFunLikeSplitting.proof_1 {N : Type u_1} {E : Type u_2} {G : Type u_3} [AddGroup N] [AddGroup E] [AddGroup G] (S : AddGroupExtension N E G) : ∀ ⦃h : S.Splitting⦄ ⦃a₂ : S.Splitting⦄, (fun (s : S.Splitting) => ⇑s.sectionHom) h = (fun (s : S.Splitting) => ⇑s.sectionHom) a₂ → h = a₂

instance GroupExtension.instFunLikeSplitting {N : Type u_1} {E : Type u_2} {G : Type u_3} [Group N] [Group E] [Group G] (S : GroupExtension N E G) : FunLike S.Splitting G E

Equations

• S.instFunLikeSplitting = { coe := fun (s : S.Splitting) => ⇑s.sectionHom, coe_injective' := ⋯ }

instance AddGroupExtension.instAddMonoidHomClassSplitting {N : Type u_1} {E : Type u_2} {G : Type u_3} [AddGroup N] [AddGroup E] [AddGroup G] (S : AddGroupExtension N E G) : AddMonoidHomClass S.Splitting G E

Equations

• ⋯ = ⋯

instance GroupExtension.instMonoidHomClassSplitting {N : Type u_1} {E : Type u_2} {G : Type u_3} [Group N] [Group E] [Group G] (S : GroupExtension N E G) : MonoidHomClass S.Splitting G E

Equations

• ⋯ = ⋯

def AddGroupExtension.IsConj {N : Type u_1} {E : Type u_2} {G : Type u_3} [AddGroup N] [AddGroup E] [AddGroup G] (S : AddGroupExtension N E G) (s : S.Splitting) (s' : S.Splitting) : Prop

A splitting of an extension S is N-conjugate to another iff there exists n : N such that the section homomorphism is a conjugate of the other section homomorphism by S.inl n.

Equations

• S.IsConj s s' = ∃ (n : N), ⇑s.sectionHom = fun (g : G) => S.inl n + s'.sectionHom g + -S.inl n

def GroupExtension.IsConj {N : Type u_1} {E : Type u_2} {G : Type u_3} [Group N] [Group E] [Group G] (S : GroupExtension N E G) (s : S.Splitting) (s' : S.Splitting) : Prop

A splitting of an extension S is N-conjugate to another iff there exists n : N such that the section homomorphism is a conjugate of the other section homomorphism by S.inl n.

Equations

• S.IsConj s s' = ∃ (n : N), ⇑s.sectionHom = fun (g : G) => S.inl n * s'.sectionHom g * (S.inl n)⁻¹

def SemidirectProduct.toGroupExtension {N : Type u_1} {G : Type u_3} [Group G] [Group N] (φ : G →* MulAut N) : GroupExtension N (N ⋊[φ] G) G

The group extension associated to the semidirect product

Equations

• SemidirectProduct.toGroupExtension φ = { inl := SemidirectProduct.inl, rightHom := SemidirectProduct.rightHom, inl_injective := ⋯, range_inl_eq_ker_rightHom := ⋯, rightHom_surjective := ⋯ }

theorem SemidirectProduct.toGroupExtension_inl {N : Type u_1} {G : Type u_3} [Group G] [Group N] (φ : G →* MulAut N) : (SemidirectProduct.toGroupExtension φ).inl = SemidirectProduct.inl

theorem SemidirectProduct.toGroupExtension_rightHom {N : Type u_1} {G : Type u_3} [Group G] [Group N] (φ : G →* MulAut N) : (SemidirectProduct.toGroupExtension φ).rightHom = SemidirectProduct.rightHom

def SemidirectProduct.inr_splitting {N : Type u_1} {G : Type u_3} [Group G] [Group N] (φ : G →* MulAut N) : (SemidirectProduct.toGroupExtension φ).Splitting

A canonical splitting of the group extension associated to the semidirect product

Equations

• SemidirectProduct.inr_splitting φ = { sectionHom := SemidirectProduct.inr, rightHom_comp_sectionHom := ⋯ }