English
Let F be a functor F: J^op → J → C with a end (i.e. a limit of the diagram given by F). The projections π_F(i) from End(F) to the component (F.obj(op i)).obj i are compatible with F along any morphism f: i → j in J; i.e. π_F(i) followed by the action of F.obj(op i) on f equals π_F(j) followed by the action (F.map f^op) at j.
Русский
Пусть F: J^op ⥤ J ⥤ C имеет предел конца. Отрезки π_F(i): End(F) → (F.obj(op i)).obj i совместимы с действием F по любому морфизму f: i → j: π_F(i) затем F.obj(op i).map(f) = π_F(j) затем (F.map f^op).app j.
LaTeX
$$$\forall i\,j:\,J\; (f:i\to j),\; \pi F i ≫ (F.obj (op i)).map f = \pi F j ≫ (F.map f.op).app j$$$
Lean4
@[reassoc]
theorem condition {i j : J} (f : i ⟶ j) : π F i ≫ (F.obj (op i)).map f = π F j ≫ (F.map f.op).app j := by
apply Wedge.condition
