English
Define an isomorphism between two semidirect products given isomorphisms on the components with a commutativity condition.
Русский
Определить изоморфизм между двумя полупрямыми произведениями, заданный изоморфизмами на компонентах и условием равности слагаемых.
LaTeX
$$$ N_1 \rtimes_{\varphi_1} G_1 \cong N_2 \rtimes_{\varphi_2} G_2 $ under compatible fn, fg, h $$
Lean4
/-- Define a map from `N₁ ⋊[φ₁] G₁` to `N₂ ⋊[φ₂] G₂` given maps `N₁ →* N₂` and `G₁ →* G₂` that
satisfy a commutativity condition `∀ n g, fn (φ₁ g n) = φ₂ (fg g) (fn n)`. -/
def map : N₁ ⋊[φ₁] G₁ →* N₂ ⋊[φ₂] G₂ where
toFun x := ⟨fn x.1, fg x.2⟩
map_one' := by simp
map_mul' x
y := by
replace h := DFunLike.ext_iff.1 (h x.right) y.left
ext <;> simp_all
