smul_section_apply — Mathlib

English

The germ map from a tilde-localized module to a stalk-to-fiber linear map composes with the stalk maps to give the open-to-localization map. This expresses natural compatibility of germs with stalk-to-fiber identifications.

Русский

Герма-гомоморфизм из модуля tilde к локальной связке совместим с линейным отображением стэков через раскрывающуюся карту открытости, выражая естественную совместимость герма с идентификациями стэков.

LaTeX

$$$\text{germ} \circ \text{stalkToFiberLinearMap} = \text{openToLocalization}$$$

Lean4

theorem smul_section_apply (r : R) (U : Opens (PrimeSpectrum.Top R)) (s : (tildeInModuleCat M).obj (op U)) (x : U) :
    (r • s).1 x = r • (s.1 x) :=
  rfl

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