English
There is an instance that coherently composes sheaves: coherentTopology C HasSheafCompose s given preregular C, finitaryExtensive C, and appropriate preservation assumptions.
Русский
Существует экземпляр, обеспечивающий композицию для когерентной топологии: coherentTopology C HasSheafCompose s при preregular C, finitaryExtensive C и соответствующих условиях сохранения.
LaTeX
$$IsSheaf(coherentTopology C) F → IsSheaf(coherentTopology C) (F ⋙ s)$$
Lean4
instance [Preregular C] [FinitaryExtensive C] [∀ (X : C), Projective X] [PreservesFiniteProducts s] :
(coherentTopology C).HasSheafCompose s where isSheaf F hF := isSheaf_coherent_of_projective_comp F s hF
