of_isIso

Mathlib.AlgebraicGeometry.AffineScheme

URI: https://scilib.ai/kg/mathlib#AlgebraicGeometry.IsAffine.of_isIso

← MathLib Explorer

English

The Spec functor is faithful.

Русский

Функтор Spec сохраняет различие морфизмов (Faithful).

LaTeX

$$$\\text{Spec}$ is faithful$$

Lean4

theorem of_isIso {X Y : Scheme} (f : X ⟶ Y) [IsIso f] [h : IsAffine Y] : IsAffine X := by rw [← essImage_Spec] at h ⊢;
  exact Functor.essImage.ofIso (asIso f).symm h

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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