English
There is a canonical PreservesColimits instance for forgetToSheafedSpace, ensuring that forgetful functor preserves colimits.
Русский
Существует канонический инстанс PreservesColimits для forgetToSheafedSpace, гарантирующий сохранение колимитов забывающим функтором.
LaTeX
$$PreservesColimits forgetToSheafedSpace$$
Lean4
noncomputable instance preservesCoequalizer : PreservesColimitsOfShape WalkingParallelPair forgetToSheafedSpace.{v} :=
⟨fun {F} => by
-- Porting note: was `apply preservesColimitOfIsoDiagram ...` and the proof that preservation
-- of colimit is provided later
suffices
PreservesColimit (parallelPair (F.map WalkingParallelPairHom.left) (F.map WalkingParallelPairHom.right))
forgetToSheafedSpace
from preservesColimit_of_iso_diagram _ (diagramIsoParallelPair F).symm
apply preservesColimit_of_preserves_colimit_cocone (coequalizerCoforkIsColimit _ _)
apply (isColimitMapCoconeCoforkEquiv _ _).symm _
dsimp only [forgetToSheafedSpace]
exact coequalizerIsCoequalizer _ _⟩
