stalkFunctor_map_germ — Mathlib

English

Naturality of germ with respect to a morphism of presheaves.

Русский

Натуральность зародка по отношению к морфизму между пресшефами.

LaTeX

$$$F.germ\ U\ x\ hx\; ≫\ (stalkFunctor\ C\ x).map\ f =\ f.app\ (op\ U)\; ≫\ G.germ\ U\ x\ hx$$$

Lean4

@[reassoc (attr := simp)]
theorem stalkFunctor_map_germ {F G : X.Presheaf C} (U : Opens X) (x : X) (hx : x ∈ U) (f : F ⟶ G) :
    F.germ U x hx ≫ (stalkFunctor C x).map f = f.app (op U) ≫ G.germ U x hx :=
  colimit.ι_map (whiskerLeft (OpenNhds.inclusion x).op f) (op ⟨U, hx⟩)

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