English
For a category that is finitary extensive, a presheaf of sets is a sheaf precisely when it preserves finite products.
Русский
Для категории с конечной экстендированностью, Presheaf множество шар тогда и только тогда, когда сохраняет конечные произведения.
LaTeX
$$$\mathrm{IsSheaf}(\mathrm{extensiveTopology}(C), F) \iff \mathrm{PreservesFiniteProducts}(F)$$$
Lean4
/-- A presheaf of sets on a category which is `FinitaryExtensive` is a sheaf iff it preserves finite
products.
-/
theorem isSheaf_iff_preservesFiniteProducts (F : Cᵒᵖ ⥤ Type w) :
Presieve.IsSheaf (extensiveTopology C) F ↔ PreservesFiniteProducts F :=
by
refine ⟨fun hF ↦ ⟨fun n ↦ ⟨fun {K} ↦ ?_⟩⟩, fun hF ↦ ?_⟩
· rw [extensiveTopology, isSheaf_coverage] at hF
let Z : Fin n → C := fun i ↦ unop (K.obj ⟨i⟩)
have : (ofArrows Z (Cofan.mk (∐ Z) (Sigma.ι Z)).inj).HasPairwisePullbacks :=
inferInstanceAs (ofArrows Z (Sigma.ι Z)).HasPairwisePullbacks
have : ∀ (i : Fin n), Mono (Cofan.inj (Cofan.mk (∐ Z) (Sigma.ι Z)) i) :=
inferInstanceAs <| ∀ (i : Fin n), Mono (Sigma.ι Z i)
let i : K ≅ Discrete.functor (fun i ↦ op (Z i)) := Discrete.natIsoFunctor
let _ : PreservesLimit (Discrete.functor (fun i ↦ op (Z i))) F :=
Presieve.preservesProduct_of_isSheafFor F ?_ initialIsInitial _ (coproductIsCoproduct Z)
(FinitaryExtensive.isPullback_initial_to_sigma_ι Z) (hF (Presieve.ofArrows Z (fun i ↦ Sigma.ι Z i)) ?_)
· exact preservesLimit_of_iso_diagram F i.symm
· apply hF
refine ⟨Empty, inferInstance, Empty.elim, IsEmpty.elim inferInstance, rfl, ⟨default, ?_, ?_⟩⟩
· ext b
cases b
· simp only [eq_iff_true_of_subsingleton]
· refine ⟨Fin n, inferInstance, Z, (fun i ↦ Sigma.ι Z i), rfl, ?_⟩
suffices Sigma.desc (fun i ↦ Sigma.ι Z i) = 𝟙 _ by rw [this]; infer_instance
ext
simp
· rw [extensiveTopology, Presieve.isSheaf_coverage]
intro X R ⟨Y, α, Z, π, hR, hi⟩
have : IsIso (Sigma.desc (Cofan.inj (Cofan.mk X π))) := hi
have : R.Extensive := ⟨Y, α, Z, π, hR, ⟨Cofan.isColimitOfIsIsoSigmaDesc (Cofan.mk X π)⟩⟩
exact isSheafFor_extensive_of_preservesFiniteProducts R F
