isSheafFor — Mathlib

English

If P is a Type-valued presheaf and J is a Grothendieck topology with X, S a sieve in J X, then P satisfies the sheaf-for condition on S.arrows.

Русский

Если P — прешейф значений в Type и J — топология Гротендикета, то для X и S в J X выполняется условие IsSheafFor для стрел S.arrows.

LaTeX

$$$\\text{IsSheafFor } P\\; S.arrows$ при $S \\in J X$.$$

Lean4

theorem isSheafFor {P : Cᵒᵖ ⥤ Type w} (hP : Presheaf.IsSheaf J P) {X : C} (S : Sieve X) (hS : S ∈ J X) :
    Presieve.IsSheafFor P S.arrows := by
  rw [isSheaf_iff_isSheaf_of_type] at hP
  exact hP S hS

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