instRespectsIsoSchemeTopologicallyIsClosedMap

Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap

URI: https://scilib.ai/kg/mathlib#AlgebraicGeometry.instRespectsIsoSchemeTopologicallyIsClosedMap

English

The property of being a topologically open embedding is Zariski-local on the source.

Русский

Свойство быть открытым вложением по топологии локально на источнике.

LaTeX

$$$IsZariskiLocalAtSource(\text{topologically IsOpenEmbedding})$$$

Lean4

instance : (topologically IsClosedMap).RespectsIso :=
  topologically_respectsIso _ (fun e ↦ e.isClosedMap) (fun _ _ hf hg ↦ hg.comp hf)

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

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

Разделы

Аффилиация

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