isLocalHom_stalkMap_congr — Mathlib

English

If two morphisms f and g are equal (H: f = g), then for any x the stalk map of f at x being local implies the stalk map of g at x is local as well.

Русский

Если две стрелки f и g равны (H: f = g), то для любой точки x локальный гомоморфизм стэку стрелки f в x влечет за собой локальный гомоморфизм стэку стрелки g в x.

LaTeX

$$Eq f g → ∀ x, IsLocalHom (f.stalkMap x).hom → IsLocalHom (g.stalkMap x).hom$$

Lean4

theorem isLocalHom_stalkMap_congr {X Y : RingedSpace} (f g : X ⟶ Y) (H : f = g) (x)
    (h : IsLocalHom (f.stalkMap x).hom) : IsLocalHom (g.stalkMap x).hom := by
  rw [PresheafedSpace.stalkMap.congr_hom _ _ H.symm x]; infer_instance

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