inr_ι — Mathlib

English

In PushoutObjObj, the canonical left and right injections satisfy expected compatibility with the structure maps; specifically inl and inr compose with ι to give the functorial maps.

Русский

У PushoutObjObj канонические инъекции слева и справа совместимы с картами структуры; в частности inl и inr образуют композиции с ι в нужные отображения функторов.

LaTeX

$$$\\text{sq.inl} \\;\\text{and} \\; \\text{sq.inr}$ совместимы с $\\text{sq.ι}$ по определению pushoutObjObj.$$$

Lean4

@[reassoc (attr := simp)]
theorem inr_ι : sq.inr ≫ sq.ι = (F.map f₁).app Y₂ := by simp [ι]

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