# The sheaf condition in terms of an equalizer of products #

Here we set up the machinery for the "usual" definition of the sheaf condition, e.g. as in https://stacks.math.columbia.edu/tag/0072 in terms of an equalizer diagram where the two objects are ∏ᶜ F.obj (U i) and ∏ᶜ F.obj (U i) ⊓ (U j).

We show that this sheaf condition is equivalent to the "pairwise intersections" sheaf condition when the presheaf is valued in a category with products, and thereby equivalent to the default sheaf condition.

def TopCat.Presheaf.SheafConditionEqualizerProducts.piOpens {C : Type u} {X : TopCat} (F : ) {ι : Type v'} (U : ) :
C

The product of the sections of a presheaf over a family of open sets.

Equations
Instances For
def TopCat.Presheaf.SheafConditionEqualizerProducts.piInters {C : Type u} {X : TopCat} (F : ) {ι : Type v'} (U : ) :
C

The product of the sections of a presheaf over the pairwise intersections of a family of open sets.

Equations
Instances For
def TopCat.Presheaf.SheafConditionEqualizerProducts.leftRes {C : Type u} {X : TopCat} (F : ) {ι : Type v'} (U : ) :

The morphism Π F.obj (U i) ⟶ Π F.obj (U i) ⊓ (U j) whose components are given by the restriction maps from U i to U i ⊓ U j.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def TopCat.Presheaf.SheafConditionEqualizerProducts.rightRes {C : Type u} {X : TopCat} (F : ) {ι : Type v'} (U : ) :

The morphism Π F.obj (U i) ⟶ Π F.obj (U i) ⊓ (U j) whose components are given by the restriction maps from U j to U i ⊓ U j.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def TopCat.Presheaf.SheafConditionEqualizerProducts.res {C : Type u} {X : TopCat} (F : ) {ι : Type v'} (U : ) :

The morphism F.obj U ⟶ Π F.obj (U i) whose components are given by the restriction maps from U j to U i ⊓ U j.

Equations
Instances For
theorem TopCat.Presheaf.SheafConditionEqualizerProducts.res_π_apply {C : Type u} {X : TopCat} (F : ) {ι : Type v'} (U : ) (i : ι) [inst : ] (x : .obj (F.obj (Opposite.op (iSup U)))) :
(CategoryTheory.Limits.limit.π (CategoryTheory.Discrete.functor fun (i : ι) => F.obj (Opposite.op (U i))) { as := i }) = (F.map .op) x
@[simp]
theorem TopCat.Presheaf.SheafConditionEqualizerProducts.res_π {C : Type u} {X : TopCat} (F : ) {ι : Type v'} (U : ) (i : ι) :
theorem TopCat.Presheaf.SheafConditionEqualizerProducts.w_apply {C : Type u} {X : TopCat} (F : ) {ι : Type v'} (U : ) [inst : ] (x : .obj (F.obj (Opposite.op (iSup U)))) :
@[reducible, inline]
abbrev TopCat.Presheaf.SheafConditionEqualizerProducts.diagram {C : Type u} {X : TopCat} (F : ) {ι : Type v'} (U : ) :

The equalizer diagram for the sheaf condition.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def TopCat.Presheaf.SheafConditionEqualizerProducts.fork {C : Type u} {X : TopCat} (F : ) {ι : Type v'} (U : ) :

The restriction map F.obj U ⟶ Π F.obj (U i) gives a cone over the equalizer diagram for the sheaf condition. The sheaf condition asserts this cone is a limit cone.

Equations
Instances For
@[simp]
theorem TopCat.Presheaf.SheafConditionEqualizerProducts.fork_pt {C : Type u} {X : TopCat} (F : ) {ι : Type v'} (U : ) :
= F.obj (Opposite.op (iSup U))
@[simp]
theorem TopCat.Presheaf.SheafConditionEqualizerProducts.fork_ι {C : Type u} {X : TopCat} (F : ) {ι : Type v'} (U : ) :
@[simp]
@[simp]
def TopCat.Presheaf.SheafConditionEqualizerProducts.piOpens.isoOfIso {C : Type u} {X : TopCat} {F : } {ι : Type v'} (U : ) {G : } (α : F G) :

Isomorphic presheaves have isomorphic piOpens for any cover U.

Equations
Instances For
def TopCat.Presheaf.SheafConditionEqualizerProducts.piInters.isoOfIso {C : Type u} {X : TopCat} {F : } {ι : Type v'} (U : ) {G : } (α : F G) :

Isomorphic presheaves have isomorphic piInters for any cover U.

Equations
Instances For
def TopCat.Presheaf.SheafConditionEqualizerProducts.diagram.isoOfIso {C : Type u} {X : TopCat} {F : } {ι : Type v'} (U : ) {G : } (α : F G) :

Isomorphic presheaves have isomorphic sheaf condition diagrams.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def TopCat.Presheaf.SheafConditionEqualizerProducts.fork.isoOfIso {C : Type u} {X : TopCat} {F : } {ι : Type v'} (U : ) {G : } (α : F G) :

If F G : presheaf C X are isomorphic presheaves, then the fork F U, the canonical cone of the sheaf condition diagram for F, is isomorphic to fork F G postcomposed with the corresponding isomorphism between sheaf condition diagrams.

Equations
Instances For

The sheaf condition for a F : presheaf C X requires that the morphism F.obj U ⟶ ∏ᶜ F.obj (U i) (where U is some open set which is the union of the U i) is the equalizer of the two morphisms ∏ᶜ F.obj (U i) ⟶ ∏ᶜ F.obj (U i) ⊓ (U j).

Equations
• F.IsSheafEqualizerProducts = ∀ ⦃ι : Type v'⦄ (U : ),
Instances For

The remainder of this file shows that the "equalizer products" sheaf condition is equivalent to the "pairwise intersections" sheaf condition.

Implementation of SheafConditionPairwiseIntersections.coneEquiv.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivFunctor_map_hom {C : Type u} {X : TopCat} (F : ) {ι : Type v'} (U : ) {c : CategoryTheory.Limits.Cone (.comp F)} {c' : CategoryTheory.Limits.Cone (.comp F)} (f : c c') :
.hom = f.hom
@[simp]

Implementation of SheafConditionPairwiseIntersections.coneEquiv.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivInverseObj_π_app {C : Type u} {X : TopCat} (F : ) {ι : Type v'} (U : ) (x : ) :
= Opposite.rec' (fun (x : ) => CategoryTheory.Pairwise.casesOn x (fun (i : ι) => CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π (fun (i : ι) => F.obj (Opposite.op (U i))) i)) fun (i j : ι) => CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π (fun (p : ι × ι) => F.obj (Opposite.op (U p.1 U p.2))) (i, j))) x

Implementation of SheafConditionPairwiseIntersections.coneEquiv.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivInverse_obj_π_app {C : Type u} {X : TopCat} (F : ) {ι : Type v'} (U : ) (x : ) :
.app x = CategoryTheory.Pairwise.rec (fun (a : ι) => CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π (fun (i : ι) => F.obj (Opposite.op (U i))) a)) (fun (a a_1 : ι) => CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π (fun (p : ι × ι) => F.obj (Opposite.op (U p.1 U p.2))) (a, a_1)))) ()
@[simp]
theorem TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivInverse_obj_pt {C : Type u} {X : TopCat} (F : ) {ι : Type v'} (U : ) :
.pt = c.pt
@[simp]
theorem TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivInverse_map_hom {C : Type u} {X : TopCat} (F : ) {ι : Type v'} (U : ) (f : c c') :
.hom = f.hom

Implementation of SheafConditionPairwiseIntersections.coneEquiv.

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

Implementation of SheafConditionPairwiseIntersections.coneEquiv.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivUnitIso_inv_app_hom {C : Type u} {X : TopCat} (F : ) {ι : Type v'} (U : ι) (X : CategoryTheory.Limits.Cone (.comp F)) :
().hom =
@[simp]
theorem TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivUnitIso_hom_app_hom {C : Type u} {X : TopCat} (F : ) {ι : Type v'} (U : ι) (X : CategoryTheory.Limits.Cone (.comp F)) :
().hom =

Implementation of SheafConditionPairwiseIntersections.coneEquiv.

Equations
Instances For
@[simp]
theorem TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivCounitIso_hom_app_hom {C : Type u} {X : TopCat} (F : ) {ι : Type v'} (U : ι) :
().hom =
@[simp]
theorem TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivCounitIso_inv_app_hom {C : Type u} {X : TopCat} (F : ) {ι : Type v'} (U : ι) :
().hom =

Implementation of SheafConditionPairwiseIntersections.coneEquiv.

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

Cones over diagram U ⋙ F are the same as a cones over the usual sheaf condition equalizer diagram.

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

If SheafConditionEqualizerProducts.fork is an equalizer, then F.mapCone (cone U) is a limit cone.

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

If F.mapCone (cone U) is a limit cone, then SheafConditionEqualizerProducts.fork is an equalizer.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem TopCat.Presheaf.isSheaf_iff_isSheafEqualizerProducts {C : Type u} {X : TopCat} (F : ) :
F.IsSheaf F.IsSheafEqualizerProducts

The sheaf condition in terms of an equalizer diagram is equivalent to the default sheaf condition.