Theorems · Definition · category theory

TopCat.Presheaf.IsSheafPairwiseIntersections

{C : Type u_1} → [inst : CategoryTheory.Category.{v_1, u_1} C] → {X : TopCat} → TopCat.Presheaf C X → Prop

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.)

Defined in

Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections

Cited by

3 results in Mathlib

Foundations

Depth 71 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.Category