arrowMap_refl — Mathlib

English

Let C be a category and F a functor from the downward-closed set up to j into C. For any i with i ≤ j, the endomorphism arrowMap F i i given by the canonical witness is the identity on F.obj ⟨i, hi⟩.

Русский

Пусть C — категория, F — функтор из области Set.Iic j в C. Для любого i с i ≤ j эндоморфизм arrowMap F i i, заданный каноническим witnesses, является тождественным отображением на F.obj ⟨i, hi⟩.

LaTeX

$$$ \\operatorname{arrowMap}(F,i,i,\\text{proof},hi) = \\operatorname{Arrow.mk}(\\operatorname{Id}_{F(\\langle i, hi\\rangle)}) $$$

Lean4

@[simp]
theorem arrowMap_refl {j : J} (F : Set.Iic j ⥤ C) (i : J) (hi : i ≤ j) :
    arrowMap F i i (by simp) hi = Arrow.mk (𝟙 (F.obj ⟨i, hi⟩)) := by simp [arrowMap]

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