lift_unique — Mathlib

English

If fg ∘ inl = f and fg ∘ inr = g for fg : M ∗ N →* P, then fg = lift f g.

Русский

Если для fg : M ∗ N →* P выполнено fg ∘ inl = f и fg ∘ inr = g, тогда fg = lift f g.

LaTeX

$$$ fg \circ \mathrm{inl} = f \quad\text{and}\quad fg \circ \mathrm{inr} = g \Rightarrow fg = \mathrm{lift}(f,g) $$$

Lean4

@[to_additive]
theorem lift_unique {f : M →* P} {g : N →* P} {fg : M ∗ N →* P} (h₁ : fg.comp inl = f) (h₂ : fg.comp inr = g) :
    fg = lift f g :=
  hom_ext h₁ h₂

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