English
For a diagram G of sheaves on the extensive topology, the presheaf obtained by taking the pointwise cocone is itself a sheaf.
Русский
Для диаграммы G шаров относительно экстенсивной топологии существование точечного когорта даёт шаровую пред-поверхность.
LaTeX
$$$\mathrm{IsSheaf}(\mathrm{extensiveTopology}(C), \mathrm{pointwiseCocone}(G \circ \mathrm{sheafToPresheaf}(A))).\mathrm{pt}$$$
Lean4
theorem isSheaf_pointwiseColimit [PreservesFiniteProducts (colim (J := J) (C := A))]
(G : J ⥤ Sheaf (extensiveTopology C) A) :
Presheaf.IsSheaf (extensiveTopology C) (pointwiseCocone (G ⋙ sheafToPresheaf _ A)).pt :=
by
rw [Presheaf.isSheaf_iff_preservesFiniteProducts]
dsimp only [pointwiseCocone_pt]
apply (config := { allowSynthFailures := true }) comp_preservesFiniteProducts
have : ∀ (i : J), PreservesFiniteProducts ((G ⋙ sheafToPresheaf _ A).obj i) := fun i ↦
by
rw [← Presheaf.isSheaf_iff_preservesFiniteProducts]
exact Sheaf.cond _
exact
⟨fun _ ↦
preservesLimitsOfShape_of_evaluation _ _ fun d ↦
inferInstanceAs (PreservesLimitsOfShape _ ((G ⋙ sheafToPresheaf _ _).obj d))⟩
