forgetToTop_preserves_of_right — Mathlib

English

For a morphism f: X → Z open immersion and any g: Y → Z, the forgetful functor from the fibered diagram preserves the limit of the cospan; in particular, the induced limit in schemes is preserved by forgetful functor to Top.

Русский

Для морфизма f: X → Z открытое вложение и любого g: Y → Z сохранение пределов в диаграмме типа "сополан" сохраняется фунторский забыватель.

LaTeX

$$$\text{PreservesLimit}(\text{cospan }f\ g)\; Scheme. forgetToTop$$$

Lean4

instance forgetToTop_preserves_of_right : PreservesLimit (cospan g f) Scheme.forgetToTop :=
  preservesPullback_symmetry _ _ _

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