# Documentation

Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts

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

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.

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.

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.

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.

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]
def TopCat.Presheaf.SheafConditionEqualizerProducts.diagram {C : Type u} {X : TopCat} (F : ) {ι : Type v'} (U : ) :

The equalizer diagram for the sheaf condition.

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.

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.

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.

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.

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.

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

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.

Instances For
@[simp]
theorem TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivFunctor_map_hom {C : Type u} {X : TopCat} (F : ) {ι : Type v'} (U : ) (f : c c') :
().hom = f.hom
@[simp]
theorem TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivFunctor_obj_pt {C : Type u} {X : TopCat} (F : ) {ι : Type v'} (U : ) :
().pt = c.pt

Implementation of SheafConditionPairwiseIntersections.coneEquiv.

Instances For
@[simp]

Implementation of SheafConditionPairwiseIntersections.coneEquiv.

Instances For
@[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.

Instances For

Implementation of SheafConditionPairwiseIntersections.coneEquiv.

Instances For

Implementation of SheafConditionPairwiseIntersections.coneEquiv.

Instances For

Implementation of SheafConditionPairwiseIntersections.coneEquiv.

Instances For

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

Instances For

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

Instances For

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

Instances For

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