English
If the forgetful functors from the constants are faithful and full, and the composition with the forgetful functor preserves constants, then F is constant whenever the composition is constant.
Русский
Если забывающие функторы для константные полны и верны, и композиция с забывающим функтором сохраняет константное, тогда F константен.
LaTeX
$$$((-\text{sheafCompose } J U).obj F).IsConstant(J) \Rightarrow F.IsConstant(J)$$$
Lean4
theorem isConstant_of_forget [constantSheaf J D |>.Faithful] [constantSheaf J D |>.Full] [constantSheaf J B |>.Faithful]
[constantSheaf J B |>.Full] [(sheafCompose J U).ReflectsIsomorphisms] [((sheafCompose J U).obj F).IsConstant J]
{T : C} (hT : IsTerminal T) : F.IsConstant J :=
by
have : IsIso ((sheafCompose J U).map ((constantSheafAdj J D hT).counit.app F)) :=
by
rw [← constantSheafAdj_counit_w]
infer_instance
rw [F.isConstant_iff_isIso_counit_app (hT := hT)]
exact isIso_of_reflects_iso _ (sheafCompose J U)
