English
Given φ : G →* MulAut N, fn : N →* H, fg : G →* H and a compatibility h : ∀ g, fn ∘ (φ g).toMonoidHom = (MulAut.conj (fg g)).toMonoidHom ∘ fn, there exists a unique group homomorphism lift : N ⋊[φ] G →* H defined by lift(n,g) = fn(n) · fg(g).
Русский
Пусть задано φ : G →* MulAut N, fn : N →* H, fg : G →* H и совместимость h: ∀ g, fn ∘ φ(g) = conj_{fg(g)} ∘ fn. Тогда существует единственный гомоморфизм lift: N ⋊[φ] G →* H, заданный на элементе (n,g) как lift(n,g) = fn(n) · fg(g).
LaTeX
$$$ Lift : (N \to H) \times (G \to H) \to (N \rtimes_{\varphi} G \to^* H) \\to (n,g) \mapsto fn(n) \cdot fg(g) \,\wedge\, h$$
Lean4
/-- Define a group hom `N ⋊[φ] G →* H`, by defining maps `N →* H` and `G →* H` -/
def lift : N ⋊[φ] G →* H where
toFun a := fn a.1 * fg a.2
map_one' := by simp
map_mul' a
b := by
have := fun n g ↦ DFunLike.ext_iff.1 (h n) g
simp only [MulAut.conj_apply, MonoidHom.comp_apply, MulEquiv.coe_toMonoidHom] at this
simp only [mul_left, mul_right, map_mul, this, mul_assoc, inv_mul_cancel_left]
