isSheafOpensLeCover_iff_isSheafPairwiseIntersections

English

There is an equivalence between the IsLimit of opensLeCover-cone and the IsLimit of Pairwise diagram-cone.

Русский

Существует эквивалентность между IsLimit кокона OpensLeCover и IsLimit кокона диаграммы Pairwise.

LaTeX

$$$\text{isLimitOpensLeEquivPairwise} : IsLimit( F.mapCone opensLeCoverCocone ) \cong IsLimit( F.mapCone (Pairwise.cocone U).op )$$$

Lean4

/-- The sheaf condition
in terms of a limit diagram over all `{ V : Opens X // ∃ i, V ≤ U i }`
is equivalent to the reformulation
in terms of a limit diagram over `U i` and `U i ⊓ U j`.
-/
theorem isSheafOpensLeCover_iff_isSheafPairwiseIntersections : F.IsSheafOpensLeCover ↔ F.IsSheafPairwiseIntersections :=
  forall₂_congr fun _ U ↦ (F.isLimitOpensLeCoverEquivPairwise U).nonempty_congr

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