English
Similarly, the counit at Y in Sheaf J D satisfies a canonical equality after applying sheafification and whiskering.
Русский
Аналогично, соподзаконная карта counit на Y в Sheaf J D удовлетворяет каноническому равенству после применения шейфицирования и whiskering.
LaTeX
$$$((\\mathrm{adjunction}\\ J\\ adj).\\mathrm{counit}.\\mathrm{app}\\ Y).{\\mathrm{val}} = \\text{sheafifyLift}(J,...)\\, Y.\\mathrm{cond}$$$
Lean4
@[simp]
theorem adjunction_counit_app_val [HasWeakSheafify J D] [HasSheafCompose J F] (adj : G ⊣ F) (Y : Sheaf J D) :
((adjunction J adj).counit.app Y).val = sheafifyLift J (((adj.whiskerRight Cᵒᵖ).counit.app Y.val)) Y.cond :=
by
change ((𝟭 (Sheaf _ _)).map ((adjunction J adj).counit.app Y)).val = _
simp only [Functor.comp_obj, sheafToPresheaf_obj, sheafCompose_obj_val, whiskeringRight_obj_obj, adjunction,
Adjunction.map_restrictFullyFaithful_counit_app, Iso.refl_inv, NatTrans.id_app, Functor.comp_map,
whiskeringRight_obj_map, Adjunction.comp_counit_app, comp_val, sheafificationAdjunction_counit_app_val,
sheafifyMap_sheafifyLift, Functor.id_obj, whiskerRight_id', Category.comp_id, Category.id_comp]
