noncomputable def AlgebraicGeometry.algebraOfHomSpec {R : Type u} [CommRing R] {X : Scheme} (s : X ⟶ Spec (CommRingCat.of R)) (U : X.Opens) : Algebra R ↑(X.presheaf.obj (Opposite.op U))

Every morphism X ⟶ Spec (.of R) induces an R-algebra structure on Γ(X, U) for every U.

Equations

• One or more equations did not get rendered due to their size.