toPushforwardStalkAlgHom — Mathlib

English

There is a canonical algebra homomorphism from S to the stalk of the pushforward structure sheaf, describing the algebra structure on the pushforward stalk.

Русский

Существует канонический алгебра-гомоморфизм из S в stalk пушфорвардной структуры оболочки, описывающий алгебраическую структуру stalk.

LaTeX

$$$S \to_{\text{AlgHom}} (\Spec.topMap \cdot).stalk p$$$

Lean4

/-- This is the `AlgHom` version of `toPushforwardStalk`, which is the map `S ⟶ (f∗ 𝒪ₛ)ₚ` for some
algebra `R ⟶ S` and some `p : Spec R`.
-/
@[simps!]
def toPushforwardStalkAlgHom :
    S →ₐ[R] (Spec.topMap (CommRingCat.ofHom (algebraMap R S)) _* (structureSheaf S).1).stalk p :=
  { (StructureSheaf.toPushforwardStalk (CommRingCat.ofHom (algebraMap R S)) p).hom with commutes' := fun _ => rfl }

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