stalkSpecializes_stalkFunctor_map

English

Extensional equivalence of two germs yields equality of their corresponding sections.

Русский

Расширенная эквивалентность двух зародков приводит к равенству соответствующих секций.

LaTeX

$$germ_ext ...$$

Lean4

@[reassoc (attr := simp), elementwise (attr := simp)]
theorem stalkSpecializes_stalkFunctor_map {F G : X.Presheaf C} (f : F ⟶ G) {x y : X} (h : x ⤳ y) :
    F.stalkSpecializes h ≫ (stalkFunctor C x).map f = (stalkFunctor C y).map f ≫ G.stalkSpecializes h :=
  by
  change (_ : colimit _ ⟶ _) = (_ : colimit _ ⟶ _)
  ext; delta stalkFunctor; simpa [stalkSpecializes] using by rfl

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