openToLocalization — Mathlib

English

There is a canonical morphism of modules from M (as a constant sheaf) to the localization module on an open U, given by evaluating sections and projecting to the localized fiber at each point.

Русский

Существует канонический морфизм модулей от M к локализации над открытым U, задаваемый оценкой секций и проекцией в локализованный волокна на каждой точке.

LaTeX

$$$\mathrm{openToLocalization}(U) : (M) \to (LocalizedModule\ x) ?$$$

Lean4

/-- The ring homomorphism that takes a section of the structure sheaf of `R` on the open set `U`,
implemented as a subtype of dependent functions to localizations at prime ideals, and evaluates
the section on the point corresponding to a given prime ideal. -/
noncomputable def openToLocalization (U : Opens (PrimeSpectrum R)) (x : PrimeSpectrum R) (hx : x ∈ U) :
    (tildeInModuleCat M).obj (op U) ⟶ ModuleCat.of R (LocalizedModule x.asIdeal.primeCompl M) :=
  -- TODO: after https://github.com/leanprover-community/mathlib4/pull/19511 we need to hint `(X := ...)` and `(Y := ...)`
    -- This suggests `restrictScalars` needs to be redesigned.

  ModuleCat.ofHom (X := (tildeInModuleCat M).obj (op U)) (Y := ModuleCat.of R (LocalizedModule x.asIdeal.primeCompl M))
    { toFun := fun s => (s.1 ⟨x, hx⟩ :)
      map_add' := fun _ _ => rfl
      map_smul' := fun _ _ => rfl }

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