isSheaf_coherent_of_projective_comp

English

If preregular C, finitaryExtensive C, and every X is projective, and s preserves finite products, then IsSheaf(coherentTopology C) (F ⋙ s) implies IsSheaf(coherentTopology C) F.

Русский

Если C — preregular, finitaryExtensive, и все X проектны, и s сохраняет конечные произведения, то IsSheaf(coherentTopology C) (F ⋙ s) ⇒ IsSheaf(coherentTopology C) F.

LaTeX

$$IsSheaf(coherentTopology C) (F ⋙ s) ⇒ IsSheaf(coherentTopology C) F$$

Lean4

theorem isSheaf_coherent_of_projective_comp [Preregular C] [FinitaryExtensive C] [∀ (X : C), Projective X]
    [PreservesFiniteProducts s] (hF : IsSheaf (coherentTopology C) F) : IsSheaf (coherentTopology C) (F ⋙ s) :=
  by
  rw [isSheaf_iff_preservesFiniteProducts_of_projective] at hF ⊢
  infer_instance

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