openAlgebra — Mathlib

English

On an open set in Spec(R) opposite, the structure sheaf carries a natural algebra structure over R.

Русский

На открытом множестве в Speс(R) структура sheaf естественно переносит структуру алгебры над R.

LaTeX

$$$\\text{openAlgebra}(U) : Algebra_R((\\text{structureSheaf R}).val.obj U)$$$

Lean4

instance openAlgebra (U : (Opens (PrimeSpectrum R))ᵒᵖ) : Algebra R ((structureSheaf R).val.obj U) :=
  (toOpen R (unop U)).hom.toAlgebra

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