English
If F preserves the limit of (S.index P).multicospan for all X,S,P, then hasSheafCompose F holds, i.e., there is a sheaf composition along F.
Русский
Если F сохраняет предел multicospan по всем X,S,P, тогда существует композиция Шейфа вдоль F.
LaTeX
$$$\forall X,S,P\; PreservesLimit( (S.index P).multicospan\ F) \Rightarrow J.HasSheafCompose F$$$
Lean4
/-- Composing a sheaf with a functor preserving the limit of `(S.index P).multicospan` yields a functor
between sheaf categories.
-/
instance hasSheafCompose_of_preservesMulticospan (F : A ⥤ B)
[∀ (X : C) (S : J.Cover X) (P : Cᵒᵖ ⥤ A), PreservesLimit (S.index P).multicospan F] : J.HasSheafCompose F where
isSheaf P
hP := by
rw [Presheaf.isSheaf_iff_multifork] at hP ⊢
intro X S
obtain ⟨h⟩ := hP X S
replace h := isLimitOfPreserves F h
replace h := Limits.IsLimit.ofIsoLimit h (S.mapMultifork F P)
exact ⟨Limits.IsLimit.postcomposeHomEquiv (S.multicospanComp F P) _ h⟩
