mapPresheaf_obj_presheaf — Mathlib

English

The c-component of the map induced by a functor F between presheafed spaces corresponds to whiskering with F.

Русский

Компонента c отображения, полученного F между прешефдов пространствах, соответствует whiskerRight с F.

LaTeX

$$$(F.mapPresheaf.map f).c = whiskerRight f.c F$$$

Lean4

@[simp]
theorem mapPresheaf_obj_presheaf (F : C ⥤ D) (X : PresheafedSpace C) :
    (F.mapPresheaf.obj X).presheaf = X.presheaf ⋙ F :=
  rfl

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