Basic operations on group extensions #
This file provides operations on an existing group extension.
Main definitions and results #
GroupExtension.relabelKer: relabels the kernel term of a group extension.
The construction is mirrored for additive groups by to_additive.
def
GroupExtension.relabelKer
{N : Type u}
{E : Type v}
{G : Type w}
[Group N]
[Group E]
[Group G]
(S : GroupExtension N E G)
{N' : Type u_1}
[Group N']
(e : N' ≃* N)
:
GroupExtension N' E G
Relabel the kernel term of a group extension along a multiplicative equivalence.
Equations
- S.relabelKer e = { inl := S.inl.comp e.toMonoidHom, rightHom := S.rightHom, inl_injective := ⋯, range_inl_eq_ker_rightHom := ⋯, rightHom_surjective := ⋯ }
Instances For
def
AddGroupExtension.relabelKer
{N : Type u}
{E : Type v}
{G : Type w}
[AddGroup N]
[AddGroup E]
[AddGroup G]
(S : AddGroupExtension N E G)
{N' : Type u_1}
[AddGroup N']
(e : N' ≃+ N)
:
AddGroupExtension N' E G
Relabel the kernel term of an additive group extension along an additive equivalence.
Equations
- S.relabelKer e = { inl := S.inl.comp e.toAddMonoidHom, rightHom := S.rightHom, inl_injective := ⋯, range_inl_eq_ker_rightHom := ⋯, rightHom_surjective := ⋯ }
Instances For
@[simp]
theorem
GroupExtension.relabelKer_inl
{N : Type u}
{E : Type v}
{G : Type w}
[Group N]
[Group E]
[Group G]
(S : GroupExtension N E G)
{N' : Type u_1}
[Group N']
(e : N' ≃* N)
:
The inclusion of S.relabelKer e is the original inclusion after e.
@[simp]
theorem
AddGroupExtension.relabelKer_inl
{N : Type u}
{E : Type v}
{G : Type w}
[AddGroup N]
[AddGroup E]
[AddGroup G]
(S : AddGroupExtension N E G)
{N' : Type u_1}
[AddGroup N']
(e : N' ≃+ N)
:
The inclusion of S.relabelKer e is the original inclusion after e.