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 ofG
byN
as short exact sequences1 → N → E → G → 1
(0 → N → E → G → 0
for additive groups)(Add?)GroupExtension.Equiv S S'
: structure for equivalences of two group extensionsS
andS'
as specific homomorphismsE → 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 extensionS
ofG
byN
as section homomorphismsG → 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
andgroupCohomology.H1
(which will be available inGroupTheory/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 inRepresentationTheory/GroupCohomology/LowDegree.lean
).
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
The inclusion map is injective.
The range of the inclusion map is equal to the kernel of the projection map.
The projection map is surjective.
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
The inclusion map is injective.
The range of the inclusion map is equal to the kernel of the projection map.
The projection map is surjective.
AddGroupExtension
s 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.
Instances For
The left-hand side of the diagram commutes.
The right-hand side of the diagram commutes.
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.
Instances For
The section is a left inverse of the projection map.
The range of the inclusion map is a normal additive subgroup.
Equations
- ⋯ = ⋯
The range of the inclusion map is a normal subgroup.
Equations
- ⋯ = ⋯
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
GroupExtension
s 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.
Instances For
The left-hand side of the diagram commutes.
The right-hand side of the diagram commutes.
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.
Instances For
The section is a left inverse of the projection map.
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
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
Instances For
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
Instances For
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
A canonical splitting of the group extension associated to the semidirect product
Equations
- SemidirectProduct.inr_splitting φ = { sectionHom := SemidirectProduct.inr, rightHom_comp_sectionHom := ⋯ }