# Documentation

Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections

# 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 opens_le_cover 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 is_sheaf_iff_is_sheaf_pairwise_intersections).

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

Instances For

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

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

Instances For

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

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

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.

Instances For

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.

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

Instances For

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

Instances For

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.

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.

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 (CategoryTheory.homOfLE (_ : U V U)).op) (F.val.map (CategoryTheory.homOfLE (_ : U V V)).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.

Instances For
@[simp]
theorem TopCat.Sheaf.interUnionPullbackCone_pt {C : Type u} {X : TopCat} (F : ) (U : ) (V : ) :
().pt = F.val.obj (Opposite.op (U V))
@[simp]
theorem TopCat.Sheaf.interUnionPullbackCone_fst {C : Type u} {X : TopCat} (F : ) (U : ) (V : ) :
= F.val.map (CategoryTheory.homOfLE (_ : U U V)).op
@[simp]
theorem TopCat.Sheaf.interUnionPullbackCone_snd {C : Type u} {X : TopCat} (F : ) (U : ) (V : ) :
= F.val.map (CategoryTheory.homOfLE (_ : V U V)).op
def TopCat.Sheaf.interUnionPullbackConeLift {C : Type u} {X : TopCat} (F : ) (U : ) (V : ) (s : CategoryTheory.Limits.PullbackCone (F.val.map (CategoryTheory.homOfLE (_ : U V U)).op) (F.val.map (CategoryTheory.homOfLE (_ : U V V)).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).

Instances For
theorem TopCat.Sheaf.interUnionPullbackConeLift_left {C : Type u} {X : TopCat} (F : ) (U : ) (V : ) (s : CategoryTheory.Limits.PullbackCone (F.val.map (CategoryTheory.homOfLE (_ : U V U)).op) (F.val.map (CategoryTheory.homOfLE (_ : U V V)).op)) :
theorem TopCat.Sheaf.interUnionPullbackConeLift_right {C : Type u} {X : TopCat} (F : ) (U : ) (V : ) (s : CategoryTheory.Limits.PullbackCone (F.val.map (CategoryTheory.homOfLE (_ : U V U)).op) (F.val.map (CategoryTheory.homOfLE (_ : U V V)).op)) :
def TopCat.Sheaf.isLimitPullbackCone {C : Type u} {X : TopCat} (F : ) (U : ) (V : ) :

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

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

Instances For
def TopCat.Sheaf.objSupIsoProdEqLocus {X : TopCat} (F : ) (U : ) (V : ) :
F.val.obj (Opposite.op (U V)) CommRingCat.of { x // x RingHom.eqLocus (RingHom.comp (F.val.map (CategoryTheory.homOfLE (_ : U V U)).op) (RingHom.fst ↑(F.val.obj ()) ↑(F.val.obj ()))) (RingHom.comp (F.val.map (CategoryTheory.homOfLE (_ : U V V)).op) (RingHom.snd ↑(F.val.obj ()) ↑(F.val.obj ()))) }

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

Instances For
theorem TopCat.Sheaf.objSupIsoProdEqLocus_hom_fst {X : TopCat} (F : ) (U : ) (V : ) (x : ().obj (F.val.obj (Opposite.op (U V)))) :
(↑(().hom x)).fst = ↑(F.val.map (CategoryTheory.homOfLE (_ : U U V)).op) x
theorem TopCat.Sheaf.objSupIsoProdEqLocus_hom_snd {X : TopCat} (F : ) (U : ) (V : ) (x : ().obj (F.val.obj (Opposite.op (U V)))) :
(↑(().hom x)).snd = ↑(F.val.map (CategoryTheory.homOfLE (_ : V U V)).op) x
theorem TopCat.Sheaf.objSupIsoProdEqLocus_inv_fst {X : TopCat} (F : ) (U : ) (V : ) (x : ().obj (CommRingCat.of { x // x RingHom.eqLocus (RingHom.comp (F.val.map (CategoryTheory.homOfLE (_ : U V U)).op) (RingHom.fst ↑(F.val.obj ()) ↑(F.val.obj ()))) (RingHom.comp (F.val.map (CategoryTheory.homOfLE (_ : U V V)).op) (RingHom.snd ↑(F.val.obj ()) ↑(F.val.obj ()))) })) :
↑(F.val.map (CategoryTheory.homOfLE (_ : U U V)).op) (().inv x) = (x).fst
theorem TopCat.Sheaf.objSupIsoProdEqLocus_inv_snd {X : TopCat} (F : ) (U : ) (V : ) (x : ().obj (CommRingCat.of { x // x RingHom.eqLocus (RingHom.comp (F.val.map (CategoryTheory.homOfLE (_ : U V U)).op) (RingHom.fst ↑(F.val.obj ()) ↑(F.val.obj ()))) (RingHom.comp (F.val.map (CategoryTheory.homOfLE (_ : U V V)).op) (RingHom.snd ↑(F.val.obj ()) ↑(F.val.obj ()))) })) :
↑(F.val.map (CategoryTheory.homOfLE (_ : V U V)).op) (().inv x) = (x).snd