unit_ext — Mathlib

English

In a monoidal category with finite products, any two morphisms from X to the tensor unit are equal if they coincide after composing with the terminal projection.

Русский

В моноидальной категории с конечными произведениями любые две морфизмы X ⟶ 1_C совпадают, если они совпадают после композиции с проекцией терминала.

LaTeX

$$$\forall f,g:\, X \to 1_C,\; f=g \iff f \circ t = g \circ t$$$

Lean4

@[ext]
theorem unit_ext {X : C} (f g : X ⟶ 𝟙_ C) : f = g :=
  terminal.hom_ext f g

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