English
The adjunction between LocallyConstant.functor and the presheaf sections functor is established with the unit and counit specified, yielding an equivalence.
Русский
Установлена адъюнкция между LocallyConstant.functor и функцией секций предsheaf, задаются единица и каутиз, обеспечивающие эквивалентность.
LaTeX
$$Adjunction (LocallyConstant.functor P hs) and zero-cells$$
Lean4
theorem adjunction_left_triangle [HasExplicitFiniteCoproducts.{u} P] (X : Type max u w) :
functorToPresheaves.{u, w}.map ((unit P hs).app X) ≫ ((counit P hs).app ((functor P hs).obj X)).val =
𝟙 (functorToPresheaves.obj X) :=
by
ext ⟨S⟩ (f : LocallyConstant _ X)
simp only [Functor.id_obj, Functor.comp_obj, FunctorToTypes.comp, NatTrans.id_app, functorToPresheaves_obj_obj,
types_id_apply]
simp only [counit, counitApp_app]
have := CompHausLike.preregular hs
apply
presheaf_ext (X := ((functor P hs).obj X).val) (Y := ((functor.{u, w} P hs).obj X).val) (f.map ((unit P hs).app X))
intro a
erw [incl_of_counitAppApp]
simp only [functor_obj_val, functorToPresheaves_obj_obj, Functor.id_obj, counitAppAppImage, LocallyConstant.map_apply,
functorToPresheaves_obj_map, Quiver.Hom.unop_op]
ext x
erw [← map_eq_image _ a x]
rfl
