forget_preservesPullbackOfLeft — Mathlib

English

Forgets to SheafedSpace preserve pullbacks on the left leg: forgetToSheafedSpace preserves the pullback of f,g on the left.

Русский

Забывающий функтор к SheafedSpace сохраняет обратную диаграмму слева: забывающий к SheafedSpace сохраняет пуллбэк слева.

LaTeX

$$$ \mathrm{forgetToSheafedSpace} \circ \text{pullback}(f,g) \text{ preserves left pullback }$$$

Lean4

instance forget_preservesPullbackOfLeft : PreservesLimit (cospan f g) LocallyRingedSpace.forgetToSheafedSpace :=
  preservesLimit_of_preserves_limit_cone (pullbackConeOfLeftIsLimit f g) <|
    by
    apply (isLimitMapConePullbackConeEquiv _ _).symm.toFun
    apply isLimitOfIsLimitPullbackConeMap SheafedSpace.forgetToPresheafedSpace
    exact PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftIsLimit f.1 g.1

Похожие утверждения