forget_preservesLimitsOfRight — Mathlib

English

The forgetful functor from the open immersion setting to the base category preserves limits arising from the right hand side of a pullback diagram.

Русский

Обратная к открытому вложению функция забывания сохраняет пределы справа от диаграммы pullback.

LaTeX

$$$\text{PreservesLimit}(\mathrm{cospan}\ g\ f,\ \mathrm{forget})$$$

Lean4

instance forget_preservesLimitsOfRight : PreservesLimit (cospan g f) (forget C) :=
  preservesPullback_symmetry (forget C) f g

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