monoidHomSubgroup — Mathlib

English

There is a group isomorphism between a semidirect product of complementary subgroups and the ambient group.

Русский

Существует изоморфизм групп между полупрямым произведением комплементарных подгрупп и окружающей группой.

LaTeX

$$$ H \rtimes[(H.normalizerMonoidHom)\circ (inclusion \; h)] K \cong G $$$

Lean4

/-- The homomorphism from a semidirect product of subgroups to the ambient group. -/
@[simps!]
def monoidHomSubgroup {H K : Subgroup G} (h : K ≤ H.normalizer) :
    H ⋊[(H.normalizerMonoidHom).comp (inclusion h)] K →* G :=
  lift H.subtype K.subtype (by simp [DFunLike.ext_iff])

Похожие утверждения