isSheaf_iff_preservesFiniteProducts_of_projective

English

In the same setup with projective objects, for F in opposite category, IsSheaf(coherentTopology C) F is equivalent to PreservesFiniteProducts F.

Русский

В той же конфигурации с проектными объектами для F в противоположной категории IsSheaf(coherentTopology C) F эквивалентно PreservesFiniteProducts F.

LaTeX

$$$IsSheaf(coherentTopology\, C) F \iff PreservesFiniteProducts F$$$

Lean4

theorem isSheaf_iff_preservesFiniteProducts_of_projective [Preregular C] [FinitaryExtensive C]
    [∀ (X : C), Projective X] : IsSheaf (coherentTopology C) F ↔ PreservesFiniteProducts F := by
  rw [isSheaf_coherent_iff_regular_and_extensive, and_iff_left (isSheaf_of_projective F),
    isSheaf_iff_preservesFiniteProducts]

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