algebra_section_stalk — Mathlib

English

For a presheaf of rings, each stalk carries an algebra structure over the ring of sections on the open set.

Русский

Для прешейфа колец каждый stalk имеет структуру алгебры над кольцом секций на открытом множестве.

LaTeX

$$$\\text{Algebra}(F_{|U}, F_{stalk}(x))$$$

Lean4

instance algebra_section_stalk (F : X.Presheaf CommRingCat) {U : Opens X} (x : U) :
    Algebra (F.obj <| op U) (F.stalk x) :=
  (F.germ U x.1 x.2).hom.toAlgebra

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