English
The counit of the constant-sheaf adjunction factors through the isomorphism constantCommuteCompose, expressing a compatibility of the composition of functors.
Русский
Коунит константного сопоставления факторизуется через изоморфизм constantCommuteCompose, отражая совместимость композиции функторов.
LaTeX
$$ ((constantCommuteCompose J U).hom.app (F.val.obj ⟨T⟩)) ≫ ((constantSheafAdj J B hT).counit.app ((sheafCompose J U).obj F)) = ((sheafCompose J U).map ((constantSheafAdj J D hT).counit.app F))$$
Lean4
/-- The counit of `constantSheafAdj` factors through the isomorphism `constantCommuteCompose`. -/
theorem constantSheafAdj_counit_w {T : C} (hT : IsTerminal T) :
((constantCommuteCompose J U).hom.app (F.val.obj ⟨T⟩)) ≫
((constantSheafAdj J B hT).counit.app ((sheafCompose J U).obj F)) =
((sheafCompose J U).map ((constantSheafAdj J D hT).counit.app F)) :=
by
apply Sheaf.hom_ext
rw [comp_val, constantCommuteCompose_hom_app_val, assoc, Iso.inv_comp_eq]
apply sheafify_hom_ext _ _ _ ((sheafCompose J U).obj F).cond
ext x
simp [NatTrans.comp_app] -- simp [NatTrans.comp_app] to unfold some definitions
simp [← map_comp, ← NatTrans.comp_app] -- simp [← NatTrans.comp_app] to simplify some compositions
