instAlgebraCarrierFunctionFieldSpec

English

For a domain R, the function field of Spec R is naturally an algebra over R, i.e., Spec R has a canonical R-algebra structure on its function field.

Русский

Для области R функция поле поля Spec R естественным образом является R-алгеброй; то есть на функции поля Spec R задается каноническая структура R-алгебры.

LaTeX

$$$R\text{-algebra on } (\operatorname{Spec} R).\mathrm{functionField}$ whenever $R$ is a domain.$$

Lean4

noncomputable instance (R : CommRingCat.{u}) [IsDomain R] : Algebra R (Spec R).functionField :=
  -- TODO: can we write this normally after the refactor finishes?

  RingHom.toAlgebra <| by apply CommRingCat.Hom.hom; apply StructureSheaf.toStalk

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