toSchemeHom_isOpenImmersion

Mathlib.AlgebraicGeometry.OpenImmersion

URI: https://scilib.ai/kg/mathlib#AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toSchemeHom_isOpenImmersion

English

If two schemes X and Y have identical underlyingLocallyRingedSpaces, then X = Y.

Русский

Если две схемы X и Y имеют одинаковые сопоставления локально кольцевых пространств, то X = Y.

LaTeX

$$$$ X.toLocallyRingedSpace = Y.toLocallyRingedSpace \Rightarrow X = Y $$$$

Lean4

instance toSchemeHom_isOpenImmersion : AlgebraicGeometry.IsOpenImmersion (toSchemeHom Y f) :=
  H

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

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

Разделы

Аффилиация

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