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.Section S: structure for right inverses to rightHom of a group extension S of G by N
• (Add?)GroupExtension.Splitting S: structure for section homomorphisms of a group extension S of G by N
• 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.

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.

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) extends E →+ E' : Type (max u_2 u_4)

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

• toFun : E → E'
• map_zero' : (↑self.toAddMonoidHom).toFun 0 = 0
• map_add' (x y : E) : (↑self.toAddMonoidHom).toFun (x + y) = (↑self.toAddMonoidHom).toFun x + (↑self.toAddMonoidHom).toFun y
• inl_comm : self.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.

structure AddGroupExtension.Section {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)

Section of an additive group extension is a right inverse to S.rightHom.

• toFun : G → E

  The underlying function

• rightInverse_rightHom : Function.RightInverse self.toFun ⇑S.rightHom

  Section is a right inverse to S.rightHom

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) extends G →+ E, S.Section : Type (max u_2 u_3)

Splitting of an additive group extension is a section homomorphism.

• toFun : G → E
• map_zero' : (↑self.toAddMonoidHom).toFun 0 = 0
• map_add' (x y : G) : (↑self.toAddMonoidHom).toFun (x + y) = (↑self.toAddMonoidHom).toFun x + (↑self.toAddMonoidHom).toFun y
• rightInverse_rightHom : Function.RightInverse (↑self.toAddMonoidHom).toFun ⇑S.rightHom

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.

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.

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

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

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) extends E →* E' : Type (max u_2 u_4)

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

• toFun : E → E'
• map_one' : (↑self.toMonoidHom).toFun 1 = 1
• map_mul' (x y : E) : (↑self.toMonoidHom).toFun (x * y) = (↑self.toMonoidHom).toFun x * (↑self.toMonoidHom).toFun y
• inl_comm : self.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.

structure GroupExtension.Section {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)

Section of a group extension is a right inverse to S.rightHom.

• toFun : G → E

  The underlying function

• rightInverse_rightHom : Function.RightInverse self.toFun ⇑S.rightHom

  Section is a right inverse to S.rightHom

instance GroupExtension.Section.instFunLike {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.Section G E

Equations

• GroupExtension.Section.instFunLike S = { coe := GroupExtension.Section.toFun, coe_injective' := ⋯ }

instance AddGroupExtension.Section.instFunLike {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.Section G E

Equations

• AddGroupExtension.Section.instFunLike S = { coe := AddGroupExtension.Section.toFun, coe_injective' := ⋯ }

@[simp]

theorem GroupExtension.Section.coe_mk {N : Type u_1} {E : Type u_2} {G : Type u_3} [Group N] [Group E] [Group G] {S : GroupExtension N E G} (σ : G → E) (hσ : Function.RightInverse σ ⇑S.rightHom) : ⇑{ toFun := σ, rightInverse_rightHom := hσ } = σ

@[simp]

theorem AddGroupExtension.Section.coe_mk {N : Type u_1} {E : Type u_2} {G : Type u_3} [AddGroup N] [AddGroup E] [AddGroup G] {S : AddGroupExtension N E G} (σ : G → E) (hσ : Function.RightInverse σ ⇑S.rightHom) : ⇑{ toFun := σ, rightInverse_rightHom := hσ } = σ

@[simp]

theorem GroupExtension.Section.rightHom_section {N : Type u_1} {E : Type u_2} {G : Type u_3} [Group N] [Group E] [Group G] {S : GroupExtension N E G} (σ : S.Section) (g : G) : S.rightHom (σ g) = g

@[simp]

theorem AddGroupExtension.Section.rightHom_section {N : Type u_1} {E : Type u_2} {G : Type u_3} [AddGroup N] [AddGroup E] [AddGroup G] {S : AddGroupExtension N E G} (σ : S.Section) (g : G) : S.rightHom (σ g) = g

@[simp]

theorem GroupExtension.Section.rightHom_comp_section {N : Type u_1} {E : Type u_2} {G : Type u_3} [Group N] [Group E] [Group G] {S : GroupExtension N E G} (σ : S.Section) : ⇑S.rightHom ∘ ⇑σ = id

@[simp]

theorem AddGroupExtension.Section.rightHom_comp_section {N : Type u_1} {E : Type u_2} {G : Type u_3} [AddGroup N] [AddGroup E] [AddGroup G] {S : AddGroupExtension N E G} (σ : S.Section) : ⇑S.rightHom ∘ ⇑σ = id

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) extends G →* E, S.Section : Type (max u_2 u_3)

Splitting of a group extension is a section homomorphism.

• toFun : G → E
• map_one' : (↑self.toMonoidHom).toFun 1 = 1
• map_mul' (x y : G) : (↑self.toMonoidHom).toFun (x * y) = (↑self.toMonoidHom).toFun x * (↑self.toMonoidHom).toFun y
• rightInverse_rightHom : Function.RightInverse (↑self.toMonoidHom).toFun ⇑S.rightHom

instance GroupExtension.Splitting.instFunLike {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

• GroupExtension.Splitting.instFunLike S = { coe := fun (s : S.Splitting) => (↑s.toMonoidHom).toFun, coe_injective' := ⋯ }

instance AddGroupExtension.Splitting.instFunLike {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

• AddGroupExtension.Splitting.instFunLike S = { coe := fun (s : S.Splitting) => (↑s.toAddMonoidHom).toFun, coe_injective' := ⋯ }

instance GroupExtension.Splitting.instMonoidHomClass {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

instance AddGroupExtension.Splitting.instAddMonoidHomClass {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

@[simp]

theorem GroupExtension.Splitting.coe_mk {N : Type u_1} {E : Type u_2} {G : Type u_3} [Group N] [Group E] [Group G] {S : GroupExtension N E G} (s : G →* E) (hs : Function.RightInverse ⇑s ⇑S.rightHom) : ⇑{ toMonoidHom := s, rightInverse_rightHom := hs } = ⇑s

@[simp]

theorem AddGroupExtension.Splitting.coe_mk {N : Type u_1} {E : Type u_2} {G : Type u_3} [AddGroup N] [AddGroup E] [AddGroup G] {S : AddGroupExtension N E G} (s : G →+ E) (hs : Function.RightInverse ⇑s ⇑S.rightHom) : ⇑{ toAddMonoidHom := s, rightInverse_rightHom := hs } = ⇑s

@[simp]

theorem GroupExtension.Splitting.coe_monoidHom_mk {N : Type u_1} {E : Type u_2} {G : Type u_3} [Group N] [Group E] [Group G] {S : GroupExtension N E G} (s : G →* E) (hs : Function.RightInverse ⇑s ⇑S.rightHom) : ↑{ toMonoidHom := s, rightInverse_rightHom := hs } = s

@[simp]

theorem AddGroupExtension.Splitting.coe_addMonoidHom_mk {N : Type u_1} {E : Type u_2} {G : Type u_3} [AddGroup N] [AddGroup E] [AddGroup G] {S : AddGroupExtension N E G} (s : G →+ E) (hs : Function.RightInverse ⇑s ⇑S.rightHom) : ↑{ toAddMonoidHom := s, rightInverse_rightHom := hs } = s

@[simp]

theorem GroupExtension.Splitting.rightHom_splitting {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) (g : G) : S.rightHom (s g) = g

@[simp]

theorem AddGroupExtension.Splitting.rightHom_splitting {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) (g : G) : S.rightHom (s g) = g

@[simp]

theorem GroupExtension.Splitting.rightHom_comp_splitting {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.rightHom.comp ↑s = MonoidHom.id G

@[simp]

theorem AddGroupExtension.Splitting.rightHom_comp_splitting {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.rightHom.comp ↑s = AddMonoidHom.id G

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' : 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 = fun (g : G) => S.inl n * s' g * (S.inl n)⁻¹

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' : 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 = fun (g : G) => S.inl n + s' 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) : (toGroupExtension φ).inl = inl

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

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

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

Equations

• SemidirectProduct.inr_splitting φ = { toMonoidHom := SemidirectProduct.inr, rightInverse_rightHom := ⋯ }