algebraMap_pushforward_stalk — Mathlib

English

The algebra structure on the stalk of pushforward carries over to the carrier ring of the stalk via the pushforward map.

Русский

Алгебраическая структура на стоке пушфорварда переносится в носитель стока через pushforward.

LaTeX

$$$\text{algebraCarrierStalk} = (\text{StructureSheaf}.toPushforwardStalk)\,\text{hom}$$$

Lean4

theorem algebraMap_pushforward_stalk :
    algebraMap R ((Spec.topMap f _* (structureSheaf S).1).stalk p) = (f ≫ StructureSheaf.toPushforwardStalk f p).hom :=
  rfl

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