instRespectsIsoSchemeTopologicallyIsEmbedding

Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap

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

English

The property of being a topologically embedding is preserved under isomorphisms of schemes.

Русский

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

LaTeX

$$$\mathrm{RespectsIso}(\text{topologically IsEmbedding})$$$

Lean4

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

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

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

Разделы

Аффилиация

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