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 isup 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

• isLimit (F.mapCone (cone U)), or
• preservesLimit (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.

def TopCat.Presheaf.IsSheafPairwiseIntersections {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X : TopCat} (F : 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.)

Equations

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

def TopCat.Presheaf.IsSheafPreservesLimitPairwiseIntersections {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X : TopCat} (F : Presheaf C X) : Prop

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

Equations

• F.IsSheafPreservesLimitPairwiseIntersections = ∀ ⦃ι : Type ?u.26⦄ (U : ι → TopologicalSpace.Opens ↑X), CategoryTheory.Limits.PreservesLimit (CategoryTheory.Pairwise.diagram U).op F

def TopCat.Presheaf.SheafCondition.pairwiseToOpensLeCoverObj {X : TopCat} {ι : Type u_2} (U : ι → TopologicalSpace.Opens ↑X) : CategoryTheory.Pairwise ι → OpensLeCover U

Implementation detail: the object level of pairwiseToOpensLeCover : Pairwise ι ⥤ OpensLeCover U

Equations

• TopCat.Presheaf.SheafCondition.pairwiseToOpensLeCoverObj U (CategoryTheory.Pairwise.single i) = { obj := U i, property := ⋯ }
• TopCat.Presheaf.SheafCondition.pairwiseToOpensLeCoverObj U (CategoryTheory.Pairwise.pair i j) = { obj := U i ⊓ U j, property := ⋯ }

def TopCat.Presheaf.SheafCondition.pairwiseToOpensLeCoverMap {X : TopCat} {ι : Type u_2} (U : ι → TopologicalSpace.Opens ↑X) {V W : CategoryTheory.Pairwise ι} : (V ⟶ W) → (pairwiseToOpensLeCoverObj U V ⟶ pairwiseToOpensLeCoverObj U W)

Implementation detail: the morphism level of pairwiseToOpensLeCover : Pairwise ι ⥤ OpensLeCover U

Equations

• One or more equations did not get rendered due to their size.
• TopCat.Presheaf.SheafCondition.pairwiseToOpensLeCoverMap U (CategoryTheory.Pairwise.Hom.left i j) = CategoryTheory.homOfLE ⋯
• TopCat.Presheaf.SheafCondition.pairwiseToOpensLeCoverMap U (CategoryTheory.Pairwise.Hom.right i j) = CategoryTheory.homOfLE ⋯

def TopCat.Presheaf.SheafCondition.pairwiseToOpensLeCover {X : TopCat} {ι : Type u_2} (U : ι → TopologicalSpace.Opens ↑X) : CategoryTheory.Functor (CategoryTheory.Pairwise ι) (OpensLeCover U)

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.

@[simp]

theorem TopCat.Presheaf.SheafCondition.pairwiseToOpensLeCover_obj {X : TopCat} {ι : Type u_2} (U : ι → TopologicalSpace.Opens ↑X) (a✝ : CategoryTheory.Pairwise ι) : (pairwiseToOpensLeCover U).obj a✝ = pairwiseToOpensLeCoverObj U a✝

@[simp]

theorem TopCat.Presheaf.SheafCondition.pairwiseToOpensLeCover_map {X : TopCat} {ι : Type u_2} (U : ι → TopologicalSpace.Opens ↑X) {x✝ x✝¹ : CategoryTheory.Pairwise ι} (i : x✝ ⟶ x✝¹) : (pairwiseToOpensLeCover U).map i = pairwiseToOpensLeCoverMap U i

instance TopCat.Presheaf.SheafCondition.instNonemptyStructuredArrowPairwiseOpensLeCoverPairwiseToOpensLeCover {X : TopCat} {ι : Type u_2} (U : ι → TopologicalSpace.Opens ↑X) (V : OpensLeCover U) : Nonempty (CategoryTheory.StructuredArrow V (pairwiseToOpensLeCover U))

instance TopCat.Presheaf.SheafCondition.instFinalPairwiseOpensLeCoverPairwiseToOpensLeCover {X : TopCat} {ι : Type u_2} (U : ι → TopologicalSpace.Opens ↑X) : (pairwiseToOpensLeCover U).Final

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.

def TopCat.Presheaf.SheafCondition.pairwiseDiagramIso {X : TopCat} {ι : Type u_2} (U : ι → TopologicalSpace.Opens ↑X) : CategoryTheory.Pairwise.diagram U ≅ (pairwiseToOpensLeCover U).comp (CategoryTheory.ObjectProperty.ι fun (V : TopologicalSpace.Opens ↑X) => ∃ (i : ι), V ≤ U i)

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.

def TopCat.Presheaf.SheafCondition.pairwiseCoconeIso {X : TopCat} {ι : Type u_2} (U : ι → TopologicalSpace.Opens ↑X) : (CategoryTheory.Pairwise.cocone U).op ≅ (CategoryTheory.Limits.Cones.postcomposeEquivalence (CategoryTheory.NatIso.op (pairwiseDiagramIso U))).functor.obj (CategoryTheory.Limits.Cone.whisker (pairwiseToOpensLeCover U).op (opensLeCoverCocone U).op)

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

Equations

• TopCat.Presheaf.SheafCondition.pairwiseCoconeIso U = CategoryTheory.Limits.Cones.ext (CategoryTheory.Iso.refl (CategoryTheory.Pairwise.cocone U).op.pt) ⋯

def TopCat.Presheaf.isLimitOpensLeCoverEquivPairwise {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {X : TopCat} (F : Presheaf C X) {ι : Type u_2} (U : ι → TopologicalSpace.Opens ↑X) : CategoryTheory.Limits.IsLimit (CategoryTheory.Functor.mapCone F (SheafCondition.opensLeCoverCocone U).op) ≃ CategoryTheory.Limits.IsLimit (CategoryTheory.Functor.mapCone F (CategoryTheory.Pairwise.cocone U).op)

The diagram over all { V : Opens X // ∃ i, V ≤ U i } is a limit iff the diagram over U i and U i ⊓ U j is a limit.

Equations

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

theorem TopCat.Presheaf.isSheafOpensLeCover_iff_isSheafPairwiseIntersections {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {X : TopCat} (F : Presheaf C X) : 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.isSheafPairwiseIntersections {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {X : TopCat} {F : Presheaf C X} {ι : Type u_2} (U : ι → TopologicalSpace.Opens ↑X) (h : F.IsSheaf) : Nonempty (CategoryTheory.Limits.IsLimit (CategoryTheory.Functor.mapCone F (CategoryTheory.Pairwise.cocone U).op))

theorem TopCat.Presheaf.isSheaf_iff_isSheafPairwiseIntersections {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {X : TopCat} (F : Presheaf C X) : 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.isSheafPreservesLimitPairwiseIntersections {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {X : TopCat} {F : Presheaf C X} {ι : Type u_2} (U : ι → TopologicalSpace.Opens ↑X) (h : F.IsSheaf) : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Pairwise.diagram U).op F

theorem TopCat.Presheaf.isSheaf_iff_isSheafPreservesLimitPairwiseIntersections {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {X : TopCat} (F : Presheaf C X) : 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_1} [CategoryTheory.Category.{u_2, u_1} C] {X : TopCat} (F : Sheaf C X) (U V : TopologicalSpace.Opens ↑X) : CategoryTheory.Limits.PullbackCone (F.val.map (CategoryTheory.homOfLE ⋯).op) (F.val.map (CategoryTheory.homOfLE ⋯).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

• F.interUnionPullbackCone U V = CategoryTheory.Limits.PullbackCone.mk (F.val.map (CategoryTheory.homOfLE ⋯).op) (F.val.map (CategoryTheory.homOfLE ⋯).op) ⋯

@[simp]

theorem TopCat.Sheaf.interUnionPullbackCone_pt {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X : TopCat} (F : Sheaf C X) (U V : TopologicalSpace.Opens ↑X) : (F.interUnionPullbackCone U V).pt = F.val.obj (Opposite.op (U ⊔ V))

@[simp]

theorem TopCat.Sheaf.interUnionPullbackCone_fst {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X : TopCat} (F : Sheaf C X) (U V : TopologicalSpace.Opens ↑X) : (F.interUnionPullbackCone U V).fst = F.val.map (CategoryTheory.homOfLE ⋯).op

@[simp]

theorem TopCat.Sheaf.interUnionPullbackCone_snd {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X : TopCat} (F : Sheaf C X) (U V : TopologicalSpace.Opens ↑X) : (F.interUnionPullbackCone U V).snd = F.val.map (CategoryTheory.homOfLE ⋯).op

def TopCat.Sheaf.interUnionPullbackConeLift {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X : TopCat} (F : Sheaf C X) (U V : TopologicalSpace.Opens ↑X) (s : CategoryTheory.Limits.PullbackCone (F.val.map (CategoryTheory.homOfLE ⋯).op) (F.val.map (CategoryTheory.homOfLE ⋯).op)) : s.pt ⟶ F.val.obj (Opposite.op (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.

theorem TopCat.Sheaf.interUnionPullbackConeLift_left {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X : TopCat} (F : Sheaf C X) (U V : TopologicalSpace.Opens ↑X) (s : CategoryTheory.Limits.PullbackCone (F.val.map (CategoryTheory.homOfLE ⋯).op) (F.val.map (CategoryTheory.homOfLE ⋯).op)) : CategoryTheory.CategoryStruct.comp (F.interUnionPullbackConeLift U V s) (F.val.map (CategoryTheory.homOfLE ⋯).op) = s.fst

theorem TopCat.Sheaf.interUnionPullbackConeLift_right {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X : TopCat} (F : Sheaf C X) (U V : TopologicalSpace.Opens ↑X) (s : CategoryTheory.Limits.PullbackCone (F.val.map (CategoryTheory.homOfLE ⋯).op) (F.val.map (CategoryTheory.homOfLE ⋯).op)) : CategoryTheory.CategoryStruct.comp (F.interUnionPullbackConeLift U V s) (F.val.map (CategoryTheory.homOfLE ⋯).op) = s.snd

def TopCat.Sheaf.isLimitPullbackCone {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X : TopCat} (F : Sheaf C X) (U V : TopologicalSpace.Opens ↑X) : 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.

def TopCat.Sheaf.isProductOfDisjoint {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X : TopCat} (F : Sheaf C X) (U V : TopologicalSpace.Opens ↑X) (h : U ⊓ V = ⊥) : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.BinaryFan.mk (F.val.map (CategoryTheory.homOfLE ⋯).op) (F.val.map (CategoryTheory.homOfLE ⋯).op))

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.