forget_preservesOfRight

Mathlib.AlgebraicGeometry.OpenImmersion

URI: https://scilib.ai/kg/mathlib#AlgebraicGeometry.IsOpenImmersion.forget_preservesOfRight

English

If f is an open immersion, then HasPullback f g.

Русский

Если f — открытое погружение, тогда существует предельный объект pullback f g.

LaTeX

$$HasPullback f g$$

Lean4

instance forget_preservesOfRight : PreservesLimit (cospan g f) forget :=
  preservesPullback_symmetry _ _ _

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru