English
A second proof that the unit of the LocallyConstant adjunction is an isomorphism in the coherent topology setting.
Русский
Вторая запись того, что единица адъюнкции LocallyConstant является изоморфизмом в когерентной топологии.
LaTeX
$$unitIso isomorphism in coherent topology context$$
Lean4
/-- `CompHausLike.LocallyConstant.functor` is left adjoint to the forgetful functor.
-/
@[simps]
noncomputable def adjunction [HasExplicitFiniteCoproducts.{u} P] :
functor.{u, w} P hs ⊣ (sheafSections _ _).obj ⟨CompHausLike.of P PUnit.{u + 1}⟩
where
unit := unit P hs
counit := counit P hs
left_triangle_components := by
intro X
simp only [Functor.comp_obj, Functor.id_obj, Functor.flip_obj_obj, sheafToPresheaf_obj, functor_obj_val,
functorToPresheaves_obj_obj]
apply Sheaf.hom_ext
rw [Sheaf.comp_val, Sheaf.id_val]
exact adjunction_left_triangle P hs X
right_triangle_components := by
intro X
ext (x : X.val.obj _)
simp only [Functor.comp_obj, Functor.id_obj, Functor.flip_obj_obj, sheafToPresheaf_obj, functor_obj_val,
functorToPresheaves_obj_obj, types_id_apply, Functor.flip_obj_map, sheafToPresheaf_map, counit_app_val]
have := CompHausLike.preregular hs
letI : PreservesFiniteProducts ((sheafToPresheaf (coherentTopology _) _).obj X) :=
inferInstanceAs (PreservesFiniteProducts (Sheaf.val _))
apply presheaf_ext ((unit P hs).app _ x)
intro a
erw [incl_of_counitAppApp]
simp only [unit_app, counitAppAppImage, coe_const]
erw [← map_eq_image _ a ⟨PUnit.unit, by simp [mem_iff_eq_image, ← map_preimage_eq_image]⟩]
rfl
