SpecIso

Mathlib.AlgebraicGeometry.AffineSpace

URI: https://scilib.ai/kg/mathlib#AlgebraicGeometry.AffineSpace.SpecIso

Lean4

/-- The affine space over an affine base is isomorphic to the spectrum of the polynomial ring. -/
def SpecIso (R : CommRingCat.{max u v}) : 𝔸(n; Spec R) ≅ Spec <| .of <| MvPolynomial n R :=
  isoOfIsAffine _ _ ≪≫
    Scheme.Spec.mapIso (MvPolynomial.mapEquiv _ (Scheme.ΓSpecIso R).symm.commRingCatIsoToRingEquiv).toCommRingCatIso.op

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

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

Разделы

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

Аффилиация

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