isSheaf_of_isOpenEmbedding — Mathlib

English

If f is an open embedding and F is a sheaf on Y, then the pullback along f is a sheaf on X.

Русский

Если f — открытое вложение и F — шейф на Y, то вытягивание вдоль f даёт шейф на X.

LaTeX

$$$\text{IsOpenEmbedding}(f) \Rightarrow \text{IsSheaf}(F) \Rightarrow \text{IsSheaf}(h^{*}F)$$$

Lean4

theorem isSheaf_of_isOpenEmbedding (h : IsOpenEmbedding f) (hF : F.IsSheaf) : IsSheaf (h.isOpenMap.functor.op ⋙ F) :=
  by
  have := h.functor_isContinuous
  exact Functor.op_comp_isSheaf _ _ _ ⟨_, hF⟩

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