isAffine_Spec — Mathlib

English

There is a canonical isomorphism between Spec R and Spec of R, via the ΓSpecIso.

Русский

Существует канонический изоморфизм между Spec R и Spec Γ( R ), через ΓSpecIso.

LaTeX

$$$(\\mathrm{Spec}(R)).isoSpec = \\mathrm{Scheme.Spec.mapIso}(\\mathrm{ΓSpecIso}(R)).op$$$

Lean4

instance isAffine_Spec (R : CommRingCat) : IsAffine (Spec R) :=
  AlgebraicGeometry.isAffine_affineScheme ⟨_, Scheme.Spec.obj_mem_essImage (op R)⟩

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