lift_unique — Mathlib

English

Any homomorphism F : N ⋊[φ] G →* H is determined by its restrictions to N and G; F = lift (F ∘ inl) (F ∘ inr) h.

Русский

Любое гомоморфизм F: N ⋊[φ] G →* H задаётся своими ограничениями на N и G; F = lift (F ∘ inl) (F ∘ inr) h.

LaTeX

$$$ F = \text{lift} (F \circ inl) (F \circ inr) h $$$

Lean4

theorem lift_unique (F : N ⋊[φ] G →* H) : F = lift (F.comp inl) (F.comp inr) fun _ ↦ by ext; simp [inl_aut] :=
  by
  rw [DFunLike.ext_iff]
  simp only [lift, MonoidHom.comp_apply, MonoidHom.coe_mk, OneHom.coe_mk, ← map_mul, inl_left_mul_inr_right,
    forall_const]

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