pushforward_sheaf_of_sheaf — Mathlib

English

The object part of the pushforward along f agrees with the pushforward of the object part.

Русский

Часть объекта переноса вдоль f совпадает с переносом объекта.

LaTeX

$$$((pushforward C f).obj F).\\text{val} = (f _* F).$$$

Lean4

/-- The pushforward of a sheaf (by a continuous map) is a sheaf.
-/
theorem pushforward_sheaf_of_sheaf {F : X.Presheaf C} (h : F.IsSheaf) : (f _* F).IsSheaf :=
  (Opens.map f).op_comp_isSheaf _ _ ⟨_, h⟩

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