instPreservesFiniteProductsOppositeVal

English

If C is preregular and finitaryExtensive and every object is projective, then IsSheaf(coherentTopology C) F iff PreservesFiniteProducts F, for F: Opposite C → A.

Русский

Если C — preregular и finitaryExtensive, и каждый объект проективен, то IsSheaf(coherentTopology C) F эквивално PreservesFiniteProducts F, где F: Opposite C → A.

LaTeX

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

Lean4

noncomputable instance [Preregular C] [FinitaryExtensive C] (F : Sheaf (coherentTopology C) A) :
    PreservesFiniteProducts F.val :=
  (Presheaf.isSheaf_iff_preservesFiniteProducts F.val).1
    ((Presheaf.isSheaf_coherent_iff_regular_and_extensive F.val).mp F.cond).1

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