English
If a sheaf F is isomorphic to a constant sheaf at some X, then F is constant.
Русский
Если шейф F изоморфен константному шейфу в некотором X, тогда F константен.
LaTeX
$$$\\text{isConstant\_of\_iso}: \\ F \\cong (\\text{constantSheaf } J D) .obj X \\Rightarrow \\text{IsConstant } J F$$$
Lean4
/-- The constant presheaf functor is left adjoint to evaluation at a terminal object. -/
@[simps! unit_app counit_app_app]
noncomputable def constantPresheafAdj {T : C} (hT : IsTerminal T) : Functor.const Cᵒᵖ ⊣ (evaluation Cᵒᵖ D).obj (op T)
where
unit := (Functor.constCompEvaluationObj D (op T)).hom
counit :=
{ app := fun F =>
{ app := fun ⟨X⟩ => F.map (IsTerminal.from hT X).op
naturality := fun _ _ _ =>
by
simp only [Functor.comp_obj, Functor.const_obj_obj, Functor.id_obj, Functor.const_obj_map, Category.id_comp,
← Functor.map_comp]
congr
simp }
naturality := by intros; ext; simp /- Note: `aesop` works but is kind of slow -/ }
