isIso_base

Mathlib.AlgebraicGeometry.Scheme

URI: https://scilib.ai/kg/mathlib#AlgebraicGeometry.Scheme.isIso_base

English

If f: X ⟶ Y is an isomorphism of schemes, then its base map f.base is an isomorphism of topological spaces.

Русский

Если f: X ⟶ Y — изоморфизм схем, то базовое отображение f.base является изоморфизмом верхних пространств.

LaTeX

$$$\\text{IsIso}(f.base)$$$

Lean4

instance isIso_base {X Y : Scheme.{u}} (f : X ⟶ Y) [IsIso f] : IsIso f.base :=
  Scheme.forgetToTop.map_isIso f

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

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

Разделы

Аффилиация

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