sections_smul_localizations_def — Mathlib

English

In the tilde construction, the smultiplication by a section r of the base ring on a localization m equals the smultiplication by r evaluated at the base point on m.

Русский

В конструкции tilde умножение секции на локализацию соответствует умножению на ту же секцию, взятой в базовой точке, на элементе локализации.

LaTeX

$$$\forall (U)\; (x)\; r \cdot m = r\_{|x} \cdot m$$$

Lean4

@[simp]
theorem sections_smul_localizations_def {U : (Opens (PrimeSpectrum.Top R))ᵒᵖ} (x : U.unop)
    (r : (Spec.structureSheaf R).val.obj U) (m : Localizations M ↑x) : r • m = r.1 x • m :=
  rfl

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