op_comp_isSheaf — Mathlib

English

If F is continuous, then IsSheaf for the op-constructed composition holds for any G: a sheaf-presheaf composition preserves sheafness.

Русский

Если F непрерывна, то IsSheaf для композиции через op сохраняется, для любого G.

LaTeX

$$$Presheaf.IsSheaf J (F.op.comp G.val)$$$

Lean4

theorem op_comp_isSheaf [Functor.IsContinuous.{t} F J K] (G : Sheaf K A) : Presheaf.IsSheaf J (F.op ⋙ G.val) := fun T =>
  F.op_comp_isSheaf_of_types J K ⟨_, (isSheaf_iff_isSheaf_of_type _ _).2 (G.cond T)⟩

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