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).

source

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.

Instances For

source

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.

Instances For

source

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.

Instances For

source

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

Instances For

source

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

Instances For

source

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.

source

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.

source

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

source

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

source

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

source

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

source

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

Instances For

source

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.

source

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.

Instances For

source

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

source

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.

source

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'

source

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'

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

Instances For

source

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

Instances For

source

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

Instances For

source

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

Instances For

source

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

source

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

source

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

source

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

source

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

Instances For

source

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

Instances For

source

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

source

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

source

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

source

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

source

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

Instances For

source

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

Instances For

source

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

source

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

source

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

source

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

source

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

Instances For

source

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

source

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

source

@[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σ } = σ

source

@[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σ } = σ

source

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

source

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

source

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

source

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

source

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

Instances For

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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)⁻¹

Instances For

source

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

Instances For

source

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

Instances For

source

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

(toGroupExtension φ).inl = inl

source

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

(toGroupExtension φ).rightHom = rightHom

source

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

Instances For

Documentation

Mathlib.GroupTheory.GroupExtension.Defs

Group Extensions #

Main definitions #

TODO #