toSpecΓ — Mathlib

English

For every commutative ring R, the counit morphism from R to the global sections of the structure sheaf on Spec R is an isomorphism.

Русский

Для каждой коммутативной кольцевой группы R сопутствующая каунт-морфизма от R к Γ(Spec R, O) является изоморфизмом.

LaTeX

$$$\operatorname{IsIso}(\mathrm{toSpec}\Gamma(R)).$$$

Lean4

/-- The counit morphism `R ⟶ Γ(Spec R)` given by `AlgebraicGeometry.StructureSheaf.toOpen`. -/
def toSpecΓ (R : CommRingCat.{u}) : R ⟶ Γ.obj (op (Spec.toLocallyRingedSpace.obj (op R))) :=
  StructureSheaf.toOpen R ⊤

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