English
The extensive topology functor preserves shape-J colimits; namely, the sheaf-to-presheaf construction preserves colimits of shape J.
Русский
Функтор экстензивной топологии сохраняет колимиты формы J; конструкция from sheaf to presheaf сохраняет колимиты формы J.
LaTeX
$$$\mathrm{PreservesColimitsOfShape} J\,(\mathrm{sheafToPresheaf}(\mathrm{extensiveTopology}(C) , A))$$$
Lean4
instance [PreservesFiniteProducts (colim (J := J) (C := A))] :
PreservesColimitsOfShape J (sheafToPresheaf (extensiveTopology C) A) where
preservesColimit
{G} := by
suffices CreatesColimit G (sheafToPresheaf (extensiveTopology C) A) from inferInstance
refine createsColimitOfIsSheaf _ (fun c hc ↦ ?_)
let i : c.pt ≅ (G ⋙ sheafToPresheaf _ _).flip ⋙ colim := hc.coconePointUniqueUpToIso (pointwiseIsColimit _)
rw [Presheaf.isSheaf_of_iso_iff i]
exact isSheaf_pointwiseColimit _
