instIsAffineHomOfIsIsoScheme

Mathlib.AlgebraicGeometry.Morphisms.Affine

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

English

If f is an isomorphism of schemes, then f is affine.

Русский

Если morphism f — изоморфизм схем, то f — аффинная морфизм.

LaTeX

$$$IsIso(f) \\Rightarrow IsAffineHom f$$$

Lean4

instance (priority := 900) [IsIso f] : IsAffineHom f :=
  ⟨fun _ hU ↦ hU.preimage_of_isIso f⟩

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

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

Разделы

Аффилиация

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