IsSheaf — Mathlib

English

If a presheaf P is a sheaf, so is P ⋙ s for any limit-preserving functor s under suitable hypotheses.

Русский

Если предшаблон P является шейфом, то P ⋙ s тоже шейф под соответствующими допущениями.

LaTeX

$$$IsSheaf(J, P) \Rightarrow IsSheaf(J, P\circ s)$$$

Lean4

/-- A presheaf is a sheaf for a topology if it is a sheaf for every sieve in the topology.

If the given topology is given by a pretopology, `isSheaf_pretopology` shows it suffices to
check the sheaf condition at presieves in the pretopology.
-/
def IsSheaf (P : Cᵒᵖ ⥤ Type w) : Prop :=
  ∀ ⦃X⦄ (S : Sieve X), S ∈ J X → IsSheafFor P (S : Presieve X)

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