English
A split group extension is equivalent to the extension associated to the semidirect product with the action conjAct; there is a natural equivalence between the two extensions.
Русский
Разложенное расширение группы эквивалентно расширению, полученному из полусоединённого произведения по действию коньюгации; существует естественная эквивалентность между двумя расширениями.
LaTeX
$$$ (\\text{SemidirectProduct}(N,G, s.conjAct) \\toGroupExtension s.conjAct) \\Equiv S $$$
Lean4
/-- A split group extension is equivalent to the extension associated to a semidirect product. -/
noncomputable def semidirectProductToGroupExtensionEquiv : (SemidirectProduct.toGroupExtension s.conjAct).Equiv S
where
toFun := fun ⟨n, g⟩ ↦ S.inl n * s g
invFun := fun e ↦ ⟨Function.invFun S.inl (e * (s (S.rightHom e))⁻¹), S.rightHom e⟩
left_inv := fun ⟨n, g⟩ ↦ by
simp only [map_mul, rightHom_inl, rightHom_splitting, one_mul, mul_inv_cancel_right,
Function.leftInverse_invFun S.inl_injective n]
right_inv := fun e ↦ by
simp only [← eq_mul_inv_iff_mul_eq]
apply Function.invFun_eq
rw [← MonoidHom.mem_range, S.range_inl_eq_ker_rightHom, MonoidHom.mem_ker, map_mul, map_inv, rightHom_splitting,
mul_inv_cancel]
map_mul' := fun ⟨n₁, g₁⟩ ⟨n₂, g₂⟩ ↦
by
simp only [conjAct, MonoidHom.comp_apply, map_mul, inl_conjAct_comm, MonoidHom.coe_coe]
group
inl_comm := by
ext n
simp only [SemidirectProduct.toGroupExtension, Function.comp_apply, MulEquiv.coe_mk, Equiv.coe_fn_mk,
SemidirectProduct.left_inl, SemidirectProduct.right_inl, map_one, mul_one]
rightHom_comm := by
ext ⟨n, g⟩
simp only [SemidirectProduct.toGroupExtension, Function.comp_apply, MulEquiv.coe_mk, Equiv.coe_fn_mk, map_mul,
rightHom_inl, one_mul, rightHom_splitting, SemidirectProduct.rightHom_eq_right]
