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 ⊤