isoSpec — Mathlib

English

Let X be a scheme and U an affine open subset of X. Then there exists a canonical isomorphism of schemes U ≅ Spec Γ(X, U).

Русский

Пусть X — схема, U — аффинное открытое подмножество X. Существует канонический изоморфизм схем U ≅ Spec Γ(X, U).

LaTeX

$$$U \\cong \\operatorname{Spec} \\Gamma(X, U)$$$

Lean4

/-- The isomorphism `U ≅ Spec Γ(X, U)` for an affine `U`. -/
@[simps! -isSimp inv]
def isoSpec : ↑U ≅ Spec Γ(X, U) :=
  haveI : IsAffine U := hU
  U.toScheme.isoSpec ≪≫ Scheme.Spec.mapIso U.topIso.symm.op

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