hasSheafCompose_of_preservesLimitsOfSize

English

If F preserves limits of a given size, then hasSheafCompose F holds.

Русский

Если F сохраняет пределы заданного размера, то имеет место hasSheafCompose F.

LaTeX

$$$\text{PreservesLimitsOfSize}\;F \Rightarrow J.HasSheafCompose F$$$

Lean4

/-- Composing a sheaf with a functor preserving limits of the same size as the hom sets in `C` yields a
functor between sheaf categories.

Note: the size of the limit that `F` is required to preserve in
`hasSheafCompose_of_preservesMulticospan` is in general larger than this.
-/
instance hasSheafCompose_of_preservesLimitsOfSize [PreservesLimitsOfSize.{v₁, max u₁ v₁} F] : J.HasSheafCompose F where
  isSheaf _ hP := Presheaf.isSheaf_comp_of_isSheaf J _ F hP

Похожие утверждения