inl_of_isLimit — Mathlib

English

The left inclusion map into a binary biproduct X ⊞ Y is the unique morphism consistent with the bilimit structure when evaluated at the identity on X and zero on Y.

Русский

Левое включение в бинарный бипроизводный объект X ⊞ Y определяется как уникальный морфизм, согласованный с bilimit-структурой для id_X и 0_{Y}.

LaTeX

$$$t.inl = \mathrm{ht}.lift (\mathrm BinaryFan.mk (id_X) 0)$$$

Lean4

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

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