isIso_toLRSHom

Mathlib.AlgebraicGeometry.Scheme

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

English

If f is an isomorphism, then its associated LRSHom is also an isomorphism.

Русский

Если f является изоморфизмом, то соответствующий LRSHom тоже является изоморфизмом.

LaTeX

$$$\\text{IsIso}(f.\\mathrm{toLRSHom})$$$

Lean4

instance isIso_toLRSHom {X Y : Scheme} (f : X ⟶ Y) [IsIso f] : IsIso f.toLRSHom :=
  forgetToLocallyRingedSpace.map_isIso f

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

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

Разделы

Аффилиация

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