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 an isomorphism making a commuting diagram. Use AddGroupExtension.Equiv.ofMonoidHom in Mathlib/GroupTheory/GroupExtension/Basic.lean to construct an equivalence without providing the inverse map.

• toFun : E → E'
• invFun : E' → E
• left_inv : Function.LeftInverse self.invFun self.toFun
• right_inv : Function.RightInverse self.invFun self.toFun
• map_add' (x y : E) : self.toFun (x + y) = self.toFun x + self.toFun y
• inl_comm : ⇑self.toAddEquiv ∘ ⇑S.inl = ⇑S'.inl

  The left-hand side of the diagram commutes.

• rightHom_comm : ⇑S'.rightHom ∘ ⇑self.toAddEquiv = ⇑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 an isomorphism making a commuting diagram. Use GroupExtension.Equiv.ofMonoidHom in Mathlib/GroupTheory/GroupExtension/Basic.lean to construct an equivalence without providing the inverse map.

• toFun : E → E'
• invFun : E' → E
• left_inv : Function.LeftInverse self.invFun self.toFun
• right_inv : Function.RightInverse self.invFun self.toFun
• map_mul' (x y : E) : self.toFun (x * y) = self.toFun x * self.toFun y
• inl_comm : ⇑self.toMulEquiv ∘ ⇑S.inl = ⇑S'.inl

  The left-hand side of the diagram commutes.

• rightHom_comm : ⇑S'.rightHom ∘ ⇑self.toMulEquiv = ⇑S.rightHom

  The right-hand side of the diagram commutes.

instance GroupExtension.Equiv.instEquivLike {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} : EquivLike (S.Equiv S') E E'

Equations

• GroupExtension.Equiv.instEquivLike = { coe := fun (equiv : S.Equiv S') => ⇑equiv.toMulEquiv, inv := fun (equiv : S.Equiv S') => ⇑equiv.symm, left_inv := ⋯, right_inv := ⋯, coe_injective' := ⋯ }

instance AddGroupExtension.Equiv.instEquivLike {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} : EquivLike (S.Equiv S') E E'

Equations

• One or more equations did not get rendered due to their size.

instance GroupExtension.Equiv.instMulEquivClass {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} : MulEquivClass (S.Equiv S') E E'

instance AddGroupExtension.Equiv.instAddEquivClass {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} : AddEquivClass (S.Equiv S') E E'

@[simp]

theorem GroupExtension.Equiv.toMulEquiv_eq_coe {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} (equiv : S.Equiv S') : equiv.toMulEquiv = ↑equiv

@[simp]

theorem AddGroupExtension.Equiv.toAddEquiv_eq_coe {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} (equiv : S.Equiv S') : equiv.toAddEquiv = ↑equiv

@[simp]

theorem GroupExtension.Equiv.coe_toMulEquiv {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} (equiv : S.Equiv S') : ⇑↑equiv = ⇑equiv

@[simp]

theorem AddGroupExtension.Equiv.coe_toAddEquiv {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} (equiv : S.Equiv S') : ⇑↑equiv = ⇑equiv

@[simp]

theorem GroupExtension.Equiv.map_inl {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} (equiv : S.Equiv S') (n : N) : equiv (S.inl n) = S'.inl n

@[simp]

theorem AddGroupExtension.Equiv.map_inl {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} (equiv : S.Equiv S') (n : N) : equiv (S.inl n) = S'.inl n

@[simp]

theorem GroupExtension.Equiv.rightHom_map {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} (equiv : S.Equiv S') (e : E) : S'.rightHom (equiv e) = S.rightHom e

@[simp]

theorem AddGroupExtension.Equiv.rightHom_map {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} (equiv : S.Equiv S') (e : E) : S'.rightHom (equiv e) = S.rightHom e

def GroupExtension.Equiv.symm {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} (equiv : S.Equiv S') : S'.Equiv S

The inverse of an equivalence of group extensions is an equivalence.

Equations

• equiv.symm = { toMulEquiv := equiv.symm, inl_comm := ⋯, rightHom_comm := ⋯ }

def AddGroupExtension.Equiv.symm {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} (equiv : S.Equiv S') : S'.Equiv S

The inverse of an equivalence of additive group extensions is an equivalence.

Equations

• equiv.symm = { toAddEquiv := equiv.symm, inl_comm := ⋯, rightHom_comm := ⋯ }

def GroupExtension.Equiv.Simps.symm_apply {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} (equiv : S.Equiv S') : E' → E

See Note [custom simps projection].

Equations

• GroupExtension.Equiv.Simps.symm_apply equiv = ⇑equiv.symm

def AddGroupExtension.Equiv.Simps.symm_apply {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} (equiv : S.Equiv S') : E' → E

See Note [custom simps projection].

Equations

• AddGroupExtension.Equiv.Simps.symm_apply equiv = ⇑equiv.symm

@[simp]

theorem GroupExtension.Equiv.coe_symm {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} (equiv : S.Equiv S') : (↑equiv).symm = ↑equiv.symm

@[simp]

theorem AddGroupExtension.Equiv.coe_symm {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} (equiv : S.Equiv S') : (↑equiv).symm = ↑equiv.symm

@[simp]

theorem AddGroupExtension.Equiv.symm_symm_apply {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} (equiv : S.Equiv S') (a✝ : E) : equiv.symm.symm a✝ = equiv a✝

@[simp]

theorem GroupExtension.Equiv.symm_symm_apply {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} (equiv : S.Equiv S') (a✝ : E) : equiv.symm.symm a✝ = equiv a✝

def GroupExtension.Equiv.trans {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} (equiv : S.Equiv S') {E'' : Type u_5} [Group E''] {S'' : GroupExtension N E'' G} (equiv' : S'.Equiv S'') : S.Equiv S''

The composition of monoid isomorphisms associated to equivalences of group extensions gives another equivalence.

Equations

• equiv.trans equiv' = { toMulEquiv := equiv.trans equiv'.toMulEquiv, inl_comm := ⋯, rightHom_comm := ⋯ }

def AddGroupExtension.Equiv.trans {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} (equiv : S.Equiv S') {E'' : Type u_5} [AddGroup E''] {S'' : AddGroupExtension N E'' G} (equiv' : S'.Equiv S'') : S.Equiv S''

The composition of monoid isomorphisms associated to equivalences of additive group extensions gives another equivalence.

Equations

• equiv.trans equiv' = { toAddEquiv := equiv.trans equiv'.toAddEquiv, inl_comm := ⋯, rightHom_comm := ⋯ }

@[simp]

theorem GroupExtension.Equiv.trans_symm_apply {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} (equiv : S.Equiv S') {E'' : Type u_5} [Group E''] {S'' : GroupExtension N E'' G} (equiv' : S'.Equiv S'') (a✝ : E'') : (equiv.trans equiv').symm a✝ = equiv.symm (equiv'.symm a✝)

@[simp]

theorem AddGroupExtension.Equiv.trans_symm_apply {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} (equiv : S.Equiv S') {E'' : Type u_5} [AddGroup E''] {S'' : AddGroupExtension N E'' G} (equiv' : S'.Equiv S'') (a✝ : E'') : (equiv.trans equiv').symm a✝ = equiv.symm (equiv'.symm a✝)

@[simp]

theorem GroupExtension.Equiv.trans_apply {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} (equiv : S.Equiv S') {E'' : Type u_5} [Group E''] {S'' : GroupExtension N E'' G} (equiv' : S'.Equiv S'') (a✝ : E) : (equiv.trans equiv') a✝ = equiv' (equiv a✝)

@[simp]

theorem AddGroupExtension.Equiv.trans_apply {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} (equiv : S.Equiv S') {E'' : Type u_5} [AddGroup E''] {S'' : AddGroupExtension N E'' G} (equiv' : S'.Equiv S'') (a✝ : E) : (equiv.trans equiv') a✝ = equiv' (equiv a✝)

def GroupExtension.Equiv.refl {N : Type u_1} {E : Type u_2} {G : Type u_3} [Group N] [Group E] [Group G] (S : GroupExtension N E G) : S.Equiv S

A group extension is equivalent to itself.

Equations

• GroupExtension.Equiv.refl S = { toMulEquiv := MulEquiv.refl E, inl_comm := ⋯, rightHom_comm := ⋯ }

def AddGroupExtension.Equiv.refl {N : Type u_1} {E : Type u_2} {G : Type u_3} [AddGroup N] [AddGroup E] [AddGroup G] (S : AddGroupExtension N E G) : S.Equiv S

An additive group extension is equivalent to itself.

Equations

• AddGroupExtension.Equiv.refl S = { toAddEquiv := AddEquiv.refl E, inl_comm := ⋯, rightHom_comm := ⋯ }

@[simp]

theorem GroupExtension.Equiv.refl_symm_apply {N : Type u_1} {E : Type u_2} {G : Type u_3} [Group N] [Group E] [Group G] (S : GroupExtension N E G) (a : E) : (refl S).symm a = a

@[simp]

theorem AddGroupExtension.Equiv.refl_symm_apply {N : Type u_1} {E : Type u_2} {G : Type u_3} [AddGroup N] [AddGroup E] [AddGroup G] (S : AddGroupExtension N E G) (a : E) : (refl S).symm a = a

@[simp]

theorem AddGroupExtension.Equiv.refl_apply {N : Type u_1} {E : Type u_2} {G : Type u_3} [AddGroup N] [AddGroup E] [AddGroup G] (S : AddGroupExtension N E G) (a : E) : (refl S) a = a

@[simp]

theorem GroupExtension.Equiv.refl_apply {N : Type u_1} {E : Type u_2} {G : Type u_3} [Group N] [Group E] [Group G] (S : GroupExtension N E G) (a : E) : (refl S) a = a

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 := ⋯ }