English
For an adjunction G ⊣ F between functors, the unit at X in Sheaf J E yields a canonical equality between certain component maps after whiskering and sheafification.
Русский
При наличии сопряжения G ⊣ F между функторaми, единица на X в Sheaf J E удовлетворяет каноническому равенству между компонентами после whiskering и шейфицирования.
LaTeX
$$$((\\mathrm{adjunction}\\ J\\ adj).\\mathrm{unit}.\\mathrm{app}\\ X).{\\mathrm{val}} = \\dots$$$
Lean4
@[simp]
theorem adjunction_unit_app_val [HasWeakSheafify J D] [HasSheafCompose J F] (adj : G ⊣ F) (X : Sheaf J E) :
((adjunction J adj).unit.app X).val =
(adj.whiskerRight Cᵒᵖ).unit.app _ ≫ whiskerRight (toSheafify J (X.val ⋙ G)) F :=
by
change (sheafToPresheaf _ _).map ((adjunction J adj).unit.app X) = _
simp only [Functor.id_obj, Functor.comp_obj, whiskeringRight_obj_obj, adjunction,
Adjunction.map_restrictFullyFaithful_unit_app, Adjunction.comp_unit_app, sheafificationAdjunction_unit_app,
whiskeringRight_obj_map, Iso.refl_hom, NatTrans.id_app, Functor.comp_map, Functor.map_id, whiskerRight_id',
Category.comp_id]
rfl
