range_inl_eq_ker_rightHom — Mathlib

English

Let N, G be groups and φ : G →* MulAut N. The range of the left inclusion equals the kernel of the rightHom map.

Русский

Пусть N и G — группы, φ: G →* MulAut N. Область значений inl равна ядру rightHom.

LaTeX

$$$\mathrm{range}((\mathrm{inl} : N \to N \rtimes_{\varphi} G)) = \mathrm{ker}(\mathrm{rightHom}).$$$

Lean4

theorem range_inl_eq_ker_rightHom : (inl : N →* N ⋊[φ] G).range = rightHom.ker :=
  le_antisymm (fun _ ↦ by simp +contextual [MonoidHom.mem_ker, eq_comm]) fun x hx ↦
    ⟨x.left, by ext <;> simp_all [MonoidHom.mem_ker]⟩

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