isSheaf_coherent_of_projective_of_comp

English

Under preregular C, finitaryExtensive C, and all X projective, for F ∘ s the isSheaf equivalence holds with finite products: IsSheaf(coherentTopology C) F ⇔ PreservesFiniteProducts F.

Русский

При preregular C, finitaryExtensive C и всех X проектных, IsSheaf(coherentTopology C) F ⇔ PreservesFiniteProducts F.

LaTeX

$$IsSheaf(coherentTopology C) F ⇔ PreservesFiniteProducts F$$

Lean4

theorem isSheaf_coherent_of_projective_of_comp [Preregular C] [FinitaryExtensive C] [∀ (X : C), Projective X]
    [ReflectsFiniteProducts s] (hF : IsSheaf (coherentTopology C) (F ⋙ s)) : IsSheaf (coherentTopology C) F :=
  by
  rw [isSheaf_iff_preservesFiniteProducts_of_projective] at hF ⊢
  exact ⟨fun n ↦ ⟨fun {K} ↦ ⟨fun {c} hc ↦ ⟨isLimitOfReflects s (isLimitOfPreserves (F ⋙ s) hc)⟩⟩⟩⟩

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