English
The base of the lift map has image equal to the preimage of the range of g.base under f.base.
Русский
Образ основания отображения-отклонения равен предобразу диапазона g.base по отношению к f.base.
LaTeX
$$$ \mathrm{range}(\mathrm{lift}(f,g,H')) = f_{base}^{-1}(\mathrm{range}(g_{base}))$$$
Lean4
instance forgetToTop_preservesPullback_of_left :
PreservesLimit (cospan f g) (LocallyRingedSpace.forgetToSheafedSpace ⋙ SheafedSpace.forget _) :=
by
change
PreservesLimit _ <|
(LocallyRingedSpace.forgetToSheafedSpace ⋙ SheafedSpace.forgetToPresheafedSpace) ⋙
PresheafedSpace.forget
_
-- Porting note: was `apply (config := { instances := False }) ...`
-- See https://github.com/leanprover/lean4/issues/2273
have :
PreservesLimit
(cospan ((cospan f g ⋙ forgetToSheafedSpace ⋙ SheafedSpace.forgetToPresheafedSpace).map WalkingCospan.Hom.inl)
((cospan f g ⋙ forgetToSheafedSpace ⋙ SheafedSpace.forgetToPresheafedSpace).map WalkingCospan.Hom.inr))
(PresheafedSpace.forget CommRingCat) :=
by dsimp; infer_instance
have :
PreservesLimit (cospan f g ⋙ forgetToSheafedSpace ⋙ SheafedSpace.forgetToPresheafedSpace)
(PresheafedSpace.forget CommRingCat) :=
by apply preservesLimit_of_iso_diagram _ (diagramIsoCospan _).symm
apply Limits.comp_preservesLimit
