isLocalHomValStalkMap — Mathlib

English

For a LocallyRingedSpace morphism f and x ∈ X, the stalk map at x is a local homomorphism.

Русский

Для гомоморфизма LocallyRingedSpace f и x ∈ X отображение stalkMap x является локальным гомоморфизмом.

LaTeX

$$$ \\text{IsLocalHom} (f.stalkMap x).hom $$$

Lean4

@[instance]
theorem isLocalHomValStalkMap {X Y : LocallyRingedSpace.{u}} (f : X ⟶ Y) (x : X) :
    IsLocalHom (f.toShHom.stalkMap x).hom :=
  f.2 x

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