inr_of_isLimit — Mathlib

English

The right inclusion map into a binary biproduct X ⊞ Y is the unique morphism consistent with the colimit-like universal property when evaluated at zero on X and identity on Y.

Русский

Правое включение в бинарный бипродукт описывается как уникальный морфизм, согласованный с аналогичной унитарной структурой для 0_X и id_Y.

LaTeX

$$$t.inr = \mathrm{ht}.lift (\mathrm BinaryFan.mk 0 (id_Y))$$$

Lean4

theorem inr_of_isLimit {X Y : C} {t : BinaryBicone X Y} (ht : IsLimit t.toCone) :
    t.inr = ht.lift (BinaryFan.mk 0 (𝟙 Y)) := by apply ht.uniq (BinaryFan.mk 0 (𝟙 Y)); rintro ⟨⟨⟩⟩ <;> simp

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