stalk_open_algebraMap — Mathlib

English

The algebra map from the section ring on U to the stalk at x is given by the germ homomorphism.

Русский

Алгебраическая карта от колец секций на U к stalk в x задаётся гёрмом.

LaTeX

$$$\\alpha: F(U) \\to F_{stalk}(x)$ with \\alpha = (germ U x).hom$$$

Lean4

@[simp]
theorem stalk_open_algebraMap {X : TopCat} (F : X.Presheaf CommRingCat) {U : Opens X} (x : U) :
    algebraMap (F.obj <| op U) (F.stalk x) = (F.germ U x.1 x.2).hom :=
  rfl

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