instRespectsIsoSchemeTopologicallyIsClosedEmbedding

Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap

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

English

The open-embedding property respects isomorphisms of schemes.

Русский

Свойство открытого вложения уважает изоморфизма схем.

LaTeX

$$$\text{IsOpenEmbedding}$-RespectsIso$$

Lean4

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

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

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

Разделы

Аффилиация

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