of_isOpenImmersion

Mathlib.AlgebraicGeometry.Morphisms.Basic

URI: https://scilib.ai/kg/mathlib#AlgebraicGeometry.IsZariskiLocalAtSource.of_isOpenImmersion

English

If P contains identities and f is an open immersion, then P f holds.

Русский

Если P содержит тождественные морфизмы и f является открытым вложением, тогда P f выполняется.

LaTeX

$$$[P. ContainsIdentities] \, [IsOpenImmersion f] \Rightarrow P f.$$$

Lean4

theorem of_isOpenImmersion [P.ContainsIdentities] [IsOpenImmersion f] : P f :=
  Category.comp_id f ▸ comp (P.id_mem Y) f

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

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

Разделы

Аффилиация

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