English
Forgetful preservation of pullbacks on the right: forgetToPresheafedSpace preserves pullback on the right.
Русский
Сохранение пуллбэка справа через forgetToPresheafedSpace.
LaTeX
$$$ \mathrm{forgetToPresheafedSpace}\text{ preserves pullback on right}$$$
Lean4
instance forgetToPresheafedSpace_preservesPullback_of_left :
PreservesLimit (cospan f g) (LocallyRingedSpace.forgetToSheafedSpace ⋙ SheafedSpace.forgetToPresheafedSpace) :=
preservesLimit_of_preserves_limit_cone (pullbackConeOfLeftIsLimit f g) <|
by
apply (isLimitMapConePullbackConeEquiv _ _).symm.toFun
exact PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftIsLimit f.1 g.1
