id_pre — Mathlib

English

The pre of the identity on J is the image under lim of the inverse left unitor: limit.pre F (id_J) = lim.map (Functor.leftUnitor F).inv.

Русский

Предел pre для единицы на J равен образу под lim от обратного левого унитора: limit.pre F (id_J) = lim.map (Functor.leftUnitor F).inv.

LaTeX

$$$\\operatorname{limit.pre} F (\\mathrm{id}_J) = \\operatorname{lim.map} (\\mathrm{Functor.leftUnitor} F)^{-1}$$$

Lean4

theorem id_pre (F : J ⥤ C) : limit.pre F (𝟭 _) = lim.map (Functor.leftUnitor F).inv := by cat_disch

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