stalkToFiberLinearMap_germ — Mathlib

English

The germ-to-stalk-to-fiber alignment is compatible with the tilde-open localization identifications, ensuring the germ in the stalk matches the corresponding fiber element after tilde and localization.

Русский

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

LaTeX

$$$(germ \circ stalkToFiberLinearMap) = openToLocalization$$$

Lean4

@[simp]
theorem stalkToFiberLinearMap_germ (U : Opens (PrimeSpectrum.Top R)) (x : PrimeSpectrum.Top R) (hx : x ∈ U)
    (s : (tildeInModuleCat M).obj (op U)) :
    (stalkToFiberLinearMap M x).hom (TopCat.Presheaf.germ (tildeInModuleCat M) U x hx s) = (s.1 ⟨x, hx⟩ :) :=
  DFunLike.ext_iff.1 (ModuleCat.hom_ext_iff.mp (germ_comp_stalkToFiberLinearMap M U x hx)) s

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