English
For a forgetful functor s from a concrete category A' to Type_max, J-topology on C, and presheaf P' valued in A', IsSheaf J P' is equivalent to IsSheaf J (P' ∘ s).
Русский
Для функторa забывания s:A' → Type_max и топологии J на C, предшаблон P' ценен в A', то IsSheaf J P' эквивалентно IsSheaf J (P' ∘ s).
LaTeX
$$$IsSheaf(J, P') \iff IsSheaf(J, P'\circ s)$$$
Lean4
/-- For a concrete category `(A, s)` where the forgetful functor `s : A ⥤ Type v` preserves limits and
reflects isomorphisms, and `A` has limits, an `A`-valued presheaf `P : Cᵒᵖ ⥤ A` is a sheaf iff its
underlying `Type`-valued presheaf `P ⋙ s : Cᵒᵖ ⥤ Type` is a sheaf.
Note this lemma applies for "algebraic" categories, e.g. groups, abelian groups and rings, but not
for the category of topological spaces, topological rings, etc. since reflecting isomorphisms does
not hold.
-/
theorem isSheaf_iff_isSheaf_forget (s : A' ⥤ Type max v₁ u₁) [HasLimits A'] [PreservesLimits s]
[s.ReflectsIsomorphisms] : IsSheaf J P' ↔ IsSheaf J (P' ⋙ s) :=
by
have : HasLimitsOfSize.{v₁, max v₁ u₁} A' := hasLimitsOfSizeShrink.{_, _, u₁, 0} A'
have : PreservesLimitsOfSize.{v₁, max v₁ u₁} s := preservesLimitsOfSize_shrink.{_, 0, _, u₁} s
apply isSheaf_iff_isSheaf_comp
