stalkSpecializes_stalkPushforward

English

Germ equality propagates to stalk specialization.

Русский

Равенство зародков переходит к специализации на стэлах.

LaTeX

$$germ_stalkSpecializes ...$$

Lean4

@[reassoc (attr := simp), elementwise (attr := simp)]
theorem stalkSpecializes_stalkPushforward (f : X ⟶ Y) (F : X.Presheaf C) {x y : X} (h : x ⤳ y) :
    (f _* F).stalkSpecializes (f.hom.map_specializes h) ≫ F.stalkPushforward _ f x =
      F.stalkPushforward _ f y ≫ F.stalkSpecializes h :=
  by
  change (_ : colimit _ ⟶ _) = (_ : colimit _ ⟶ _)
  ext; delta stalkPushforward
  simp only [stalkSpecializes, colimit.ι_desc_assoc, colimit.ι_map_assoc, colimit.ι_pre, Category.assoc,
    colimit.pre_desc, colimit.ι_desc]
  rfl

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