IsSheafPairwiseIntersections — Mathlib

English

The cofinality of the pairwise diagram in OpensLeCover U ensures limit transfer along equivalences.

Русский

Кофинальность диаграммы pairwise в OpensLeCover U обеспечивает перенос предела через эквивалентности.

LaTeX

$$$\text{Final }(pairwiseToOpensLeCover U) \implies \text{IsLimit maps} $$$

Lean4

/-- An alternative formulation of the sheaf condition
(which we prove equivalent to the usual one below as
`isSheaf_iff_isSheafPairwiseIntersections`).

A presheaf is a sheaf if `F` sends the cone `(Pairwise.cocone U).op` to a limit cone.
(Recall `Pairwise.cocone U` has cone point `iSup U`, mapping down to the `U i` and the `U i ⊓ U j`.)
-/
def IsSheafPairwiseIntersections (F : Presheaf C X) : Prop :=
  ∀ ⦃ι : Type w⦄ (U : ι → Opens X), Nonempty (IsLimit (F.mapCone (Pairwise.cocone U).op))

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