# Equivalent formulations of the sheaf condition #

We give an equivalent formulation of the sheaf condition.

Given any indexed type ι, we define overlap ι, a category with objects corresponding to

• individual open sets, single i, and
• intersections of pairs of open sets, pair i j, with morphisms from pair i j to both single i and single j.

Any open cover U : ι → opens X provides a functor diagram U : overlap ι ⥤ (opens X)ᵒᵖ.

There is a canonical cone over this functor, cone U, whose cone point is supr U, and in fact this is a limit cone.

A presheaf F : presheaf C X is a sheaf precisely if it preserves this limit. We express this in two equivalent ways, as

• is_limit (F.map_cone (cone U)), or
• preserves_limit (diagram U) F

We show that this sheaf condition is equivalent to the OpensLeCover sheaf condition, and thereby also equivalent to the default sheaf condition.

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 supr U, mapping down to the U i and the U i ⊓ U j.)

Equations
• One or more equations did not get rendered due to their size.
Instances For

An alternative formulation of the sheaf condition (which we prove equivalent to the usual one below as isSheaf_iff_isSheafPreservesLimitPairwiseIntersections).

A presheaf is a sheaf if F preserves the limit of Pairwise.diagram U. (Recall Pairwise.diagram U is the diagram consisting of the pairwise intersections U i ⊓ U j mapping into the open sets U i. This diagram has limit supr U.)

Equations
• F.IsSheafPreservesLimitPairwiseIntersections = ∀ ⦃ι : Type w⦄ (U : ),
Instances For

Implementation detail: the object level of pairwise_to_opens_le_cover : pairwise ι ⥤ opens_le_cover U

Equations
• One or more equations did not get rendered due to their size.
Instances For
def TopCat.Presheaf.SheafCondition.pairwiseToOpensLeCoverMap {X : TopCat} {ι : Type w} (U : ) {V : } {W : } :

Implementation detail: the morphism level of pairwise_to_opens_le_cover : pairwise ι ⥤ opens_le_cover U

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem TopCat.Presheaf.SheafCondition.pairwiseToOpensLeCover_map {X : TopCat} {ι : Type w} (U : ) {V : } {W : } (i : V W) :

The category of single and double intersections of the U i maps into the category of open sets below some U i.

Equations
• One or more equations did not get rendered due to their size.
Instances For
Equations
• =

The diagram consisting of the U i and U i ⊓ U j is cofinal in the diagram of all opens contained in some U i.

Equations
• =

The diagram in opens X indexed by pairwise intersections from U is isomorphic (in fact, equal) to the diagram factored through OpensLeCover U.

Equations
• One or more equations did not get rendered due to their size.
Instances For

The cocone Pairwise.cocone U with cocone point supr U over Pairwise.diagram U is isomorphic to the cocone opensLeCoverCocone U (with the same cocone point) after appropriate whiskering and postcomposition.

Equations
Instances For
theorem TopCat.Presheaf.isSheafOpensLeCover_iff_isSheafPairwiseIntersections {C : Type u} {X : TopCat} (F : ) :
F.IsSheafOpensLeCover F.IsSheafPairwiseIntersections

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 TopCat.Presheaf.isSheaf_iff_isSheafPairwiseIntersections {C : Type u} {X : TopCat} (F : ) :
F.IsSheaf F.IsSheafPairwiseIntersections

The sheaf condition in terms of an equalizer diagram is equivalent to the reformulation in terms of a limit diagram over U i and U i ⊓ U j.

theorem TopCat.Presheaf.isSheaf_iff_isSheafPreservesLimitPairwiseIntersections {C : Type u} {X : TopCat} (F : ) :
F.IsSheaf F.IsSheafPreservesLimitPairwiseIntersections

The sheaf condition in terms of an equalizer diagram is equivalent to the reformulation in terms of the presheaf preserving the limit of the diagram consisting of the U i and U i ⊓ U j.

def TopCat.Sheaf.interUnionPullbackCone {C : Type u} {X : TopCat} (F : ) (U : ) (V : ) :
CategoryTheory.Limits.PullbackCone (F.val.map .op) (F.val.map .op)

For a sheaf F, F(U ⊔ V) is the pullback of F(U) ⟶ F(U ⊓ V) and F(V) ⟶ F(U ⊓ V). This is the pullback cone.

Equations
Instances For
@[simp]
theorem TopCat.Sheaf.interUnionPullbackCone_pt {C : Type u} {X : TopCat} (F : ) (U : ) (V : ) :
(F.interUnionPullbackCone U V).pt = F.val.obj { unop := U V }
@[simp]
theorem TopCat.Sheaf.interUnionPullbackCone_fst {C : Type u} {X : TopCat} (F : ) (U : ) (V : ) :
(F.interUnionPullbackCone U V).fst = F.val.map .op
@[simp]
theorem TopCat.Sheaf.interUnionPullbackCone_snd {C : Type u} {X : TopCat} (F : ) (U : ) (V : ) :
(F.interUnionPullbackCone U V).snd = F.val.map .op
def TopCat.Sheaf.interUnionPullbackConeLift {C : Type u} {X : TopCat} (F : ) (U : ) (V : ) (s : CategoryTheory.Limits.PullbackCone (F.val.map .op) (F.val.map .op)) :
s.pt F.val.obj { unop := U V }

(Implementation). Every cone over F(U) ⟶ F(U ⊓ V) and F(V) ⟶ F(U ⊓ V) factors through F(U ⊔ V).

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem TopCat.Sheaf.interUnionPullbackConeLift_left {C : Type u} {X : TopCat} (F : ) (U : ) (V : ) (s : CategoryTheory.Limits.PullbackCone (F.val.map .op) (F.val.map .op)) :
CategoryTheory.CategoryStruct.comp (F.interUnionPullbackConeLift U V s) (F.val.map .op) = s.fst
theorem TopCat.Sheaf.interUnionPullbackConeLift_right {C : Type u} {X : TopCat} (F : ) (U : ) (V : ) (s : CategoryTheory.Limits.PullbackCone (F.val.map .op) (F.val.map .op)) :
CategoryTheory.CategoryStruct.comp (F.interUnionPullbackConeLift U V s) (F.val.map .op) = s.snd
def TopCat.Sheaf.isLimitPullbackCone {C : Type u} {X : TopCat} (F : ) (U : ) (V : ) :
CategoryTheory.Limits.IsLimit (F.interUnionPullbackCone U V)

For a sheaf F, F(U ⊔ V) is the pullback of F(U) ⟶ F(U ⊓ V) and F(V) ⟶ F(U ⊓ V).

Equations
• One or more equations did not get rendered due to their size.
Instances For
def TopCat.Sheaf.isProductOfDisjoint {C : Type u} {X : TopCat} (F : ) (U : ) (V : ) (h : U V = ) :

If U, V are disjoint, then F(U ⊔ V) = F(U) × F(V).

Equations
• One or more equations did not get rendered due to their size.
Instances For
def TopCat.Sheaf.objSupIsoProdEqLocus {X : TopCat} (F : ) (U : ) (V : ) :
F.val.obj { unop := U V } CommRingCat.of ((RingHom.comp (F.val.map .op) (RingHom.fst (F.val.obj { unop := U }) (F.val.obj { unop := V }))).eqLocus (RingHom.comp (F.val.map .op) (RingHom.snd (F.val.obj { unop := U }) (F.val.obj { unop := V }))))

F(U ⊔ V) is isomorphic to the eq_locus of the two maps F(U) × F(V) ⟶ F(U ⊓ V).

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem TopCat.Sheaf.objSupIsoProdEqLocus_hom_fst {X : TopCat} (F : ) (U : ) (V : ) (x : (F.val.obj { unop := U V })) :
(((F.objSupIsoProdEqLocus U V).hom x)).1 = (F.val.map .op) x
theorem TopCat.Sheaf.objSupIsoProdEqLocus_hom_snd {X : TopCat} (F : ) (U : ) (V : ) (x : (F.val.obj { unop := U V })) :
(((F.objSupIsoProdEqLocus U V).hom x)).2 = (F.val.map .op) x
theorem TopCat.Sheaf.objSupIsoProdEqLocus_inv_fst {X : TopCat} (F : ) (U : ) (V : ) (x : ((RingHom.comp (F.val.map .op) (RingHom.fst (F.val.obj { unop := U }) (F.val.obj { unop := V }))).eqLocus (RingHom.comp (F.val.map .op) (RingHom.snd (F.val.obj { unop := U }) (F.val.obj { unop := V }))))) :
(F.val.map .op) ((F.objSupIsoProdEqLocus U V).inv x) = (x).1
theorem TopCat.Sheaf.objSupIsoProdEqLocus_inv_snd {X : TopCat} (F : ) (U : ) (V : ) (x : ((RingHom.comp (F.val.map .op) (RingHom.fst (F.val.obj { unop := U }) (F.val.obj { unop := V }))).eqLocus (RingHom.comp (F.val.map .op) (RingHom.snd (F.val.obj { unop := U }) (F.val.obj { unop := V }))))) :
(F.val.map .op) ((F.objSupIsoProdEqLocus U V).inv x) = (x).2