hom_ext — Mathlib

English

Two homomorphisms out of a semidirect product agree if they agree after composing with both inl and inr.

Русский

Два гомоморфизма из полупрямого произведения совпадают, если они совпадают после композиции с inl и with inr.

LaTeX

$$$ (f \circ inl) = (g \circ inl) \;\wedge\; (f \circ inr) = (g \circ inr) \Rightarrow f = g $$$

Lean4

/-- Two maps out of the semidirect product are equal if they're equal after composition
  with both `inl` and `inr` -/
theorem hom_ext {f g : N ⋊[φ] G →* H} (hl : f.comp inl = g.comp inl) (hr : f.comp inr = g.comp inr) : f = g :=
  by
  rw [lift_unique f, lift_unique g]
  simp only [*]

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