Basic lemmas about group extensions #
This file gives basic lemmas about group extensions.
For the main definitions, see Mathlib/GroupTheory/GroupExtension/Defs.lean
.
The isomorphism E ⧸ S.rightHom.ker ≃* G
induced by S.rightHom
The isomorphism E ⧸ S.rightHom.ker ≃+ G
induced by S.rightHom
The isomorphism E ⧸ S.inl.range ≃* G
induced by S.rightHom
The isomorphism E ⧸ S.inl.range ≃+ G
induced by S.rightHom
An arbitrarily chosen section
Equations
- S.surjInvRightHom = { toFun := Function.surjInv ⋯, rightInverse_rightHom := ⋯ }
An arbitrarily chosen section
Equations
- S.surjInvRightHom = { toFun := Function.surjInv ⋯, rightInverse_rightHom := ⋯ }
The composition of an isomorphism between equivalent group extensions and a section
The composition of an isomorphism between equivalent additive group extensions and a section
An equivalence of group extensions from a homomorphism making a commuting diagram. Such a homomorphism is necessarily an isomorphism.
Equations
- One or more equations did not get rendered due to their size.
An equivalence of additive group extensions from a homomorphism making a commuting diagram. Such a homomorphism is necessarily an isomorphism.
Equations
- One or more equations did not get rendered due to their size.
A split group extension is equivalent to the extension associated to a semidirect product.
Equations
- One or more equations did not get rendered due to their size.
The group associated to a split extension is isomorphic to a semidirect product.
The N
-conjugacy classes of splittings
Equations
The N
-conjugacy classes of splittings