isSheafFor_extensive_of_preservesFiniteProducts

English

A finite-product-preserving presheaf is a sheaf for the extensive topology on a finitaryPreExtensive category.

Русский

Пресшебаф сохраняющий конечные произведения является шаром для экстенсивной топологии в финитарной предэкстензивной категории.

LaTeX

$$$S.\mathrm{IsSheafFor} F \iff F \text{ preserves finite products}$$$

Lean4

/-- A finite-product-preserving presheaf is a sheaf for the extensive topology on a category which is
`FinitaryPreExtensive`.
-/
theorem isSheafFor_extensive_of_preservesFiniteProducts {X : C} (S : Presieve X) [S.Extensive] (F : Cᵒᵖ ⥤ Type w)
    [PreservesFiniteProducts F] : S.IsSheafFor F :=
  by
  obtain ⟨α, _, Z, π, rfl, ⟨hc⟩⟩ := Extensive.arrows_nonempty_isColimit (R := S)
  have : (ofArrows Z (Cofan.mk X π).inj).HasPairwisePullbacks := (inferInstance : (ofArrows Z π).HasPairwisePullbacks)
  cases nonempty_fintype α
  exact isSheafFor_of_preservesProduct F _ hc

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