English
If f: X → Z is open immersion and g: Y → Z is open immersion, then the base change of f along g is an open immersion; equivalently, the projection from the pullback is open immersion.
Русский
Если f: X → Z и g: Y → Z — открытые вложения, то базисное изменение вдоль g сохраняет открытое вложение, то есть проекция из петли открыта.
LaTeX
$$$IsOpenImmersion( pullback.fst\, g\, f )$$$
Lean4
instance forgetToTop_preserves_of_left : PreservesLimit (cospan f g) Scheme.forgetToTop :=
by
delta Scheme.forgetToTop
refine
@Limits.comp_preservesLimit _ _ _ _ _ _ (K := cospan f g) _ _ (F := forget) (G := LocallyRingedSpace.forgetToTop) ?_
?_
· infer_instance
refine @preservesLimit_of_iso_diagram _ _ _ _ _ _ _ _ _ (diagramIsoCospan.{u} _).symm ?_
dsimp [LocallyRingedSpace.forgetToTop]
infer_instance