# mathlibdocumentation

topology.sheaves.sheaf_condition.equalizer_products

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

def Top.presheaf.sheaf_condition_equalizer_products.pi_opens {C : Type u} {X : Top} (F : X) {ι : Type v} (U : ι → ) :
C

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

Equations
def Top.presheaf.sheaf_condition_equalizer_products.pi_inters {C : Type u} {X : Top} (F : X) {ι : Type v} (U : ι → ) :
C

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

Equations
def Top.presheaf.sheaf_condition_equalizer_products.left_res {C : Type u} {X : Top} (F : X) {ι : 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
def Top.presheaf.sheaf_condition_equalizer_products.right_res {C : Type u} {X : Top} (F : X) {ι : 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
def Top.presheaf.sheaf_condition_equalizer_products.res {C : Type u} {X : Top} (F : X) {ι : 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
def Top.presheaf.sheaf_condition_equalizer_products.diagram {C : Type u} {X : Top} (F : X) {ι : Type v} (U : ι → ) :

The equalizer diagram for the sheaf condition.

Equations
def Top.presheaf.sheaf_condition_equalizer_products.fork {C : Type u} {X : Top} (F : X) {ι : 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
@[simp]
theorem Top.presheaf.sheaf_condition_equalizer_products.fork_X {C : Type u} {X : Top} (F : X) {ι : Type v} (U : ι → ) :

@[simp]
theorem Top.presheaf.sheaf_condition_equalizer_products.fork_ι {C : Type u} {X : Top} (F : X) {ι : Type v} (U : ι → ) :

@[simp]

@[simp]

@[simp]
def Top.presheaf.sheaf_condition_equalizer_products.pi_opens.iso_of_iso {C : Type u} {X : Top} {F : X} {ι : Type v} (U : ι → ) {G : X} (α : F G) :

Isomorphic presheaves have isomorphic pi_opens for any cover U.

Equations
@[simp]
def Top.presheaf.sheaf_condition_equalizer_products.pi_inters.iso_of_iso {C : Type u} {X : Top} {F : X} {ι : Type v} (U : ι → ) {G : X} (α : F G) :

Isomorphic presheaves have isomorphic pi_inters for any cover U.

Equations
def Top.presheaf.sheaf_condition_equalizer_products.diagram.iso_of_iso {C : Type u} {X : Top} {F : X} {ι : Type v} (U : ι → ) {G : X} (α : F G) :

Isomorphic presheaves have isomorphic sheaf condition diagrams.

Equations
def Top.presheaf.sheaf_condition_equalizer_products.fork.iso_of_iso {C : Type u} {X : Top} {F : X} {ι : Type v} (U : ι → ) {G : X} (α : 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
@[simp]
def Top.presheaf.sheaf_condition_equalizer_products.cover.of_open_embedding {X : Top} {ι : Type v} {V : Top} {j : V X} (oe : open_embedding j) (𝒰 : ι → ) :

Push forward a cover along an open embedding.

Equations
@[simp]
def Top.presheaf.sheaf_condition_equalizer_products.pi_opens.iso_of_open_embedding {C : Type u} {X : Top} {F : X} {ι : Type v} {V : Top} {j : V X} (oe : open_embedding j) (𝒰 : ι → ) :

The isomorphism between pi_opens corresponding to an open embedding.

Equations
@[simp]
def Top.presheaf.sheaf_condition_equalizer_products.pi_inters.iso_of_open_embedding {C : Type u} {X : Top} {F : X} {ι : Type v} {V : Top} {j : V X} (oe : open_embedding j) (𝒰 : ι → ) :

The isomorphism between pi_inters corresponding to an open embedding.

Equations
def Top.presheaf.sheaf_condition_equalizer_products.diagram.iso_of_open_embedding {C : Type u} {X : Top} {F : X} {ι : Type v} {V : Top} {j : V X} (oe : open_embedding j) (𝒰 : ι → ) :

The isomorphism of sheaf condition diagrams corresponding to an open embedding.

Equations
def Top.presheaf.sheaf_condition_equalizer_products.fork.iso_of_open_embedding {C : Type u} {X : Top} {F : X} {ι : Type v} {V : Top} {j : V X} (oe : open_embedding j) (𝒰 : ι → ) :

If F : presheaf C X is a presheaf, and oe : U ⟶ X is an open embedding, then the sheaf condition fork for a cover 𝒰 in U for the composition of oe and F is isomorphic to sheaf condition fork for oe '' 𝒰, precomposed with the isomorphism of indexing diagrams diagram.iso_of_open_embedding.

We use this to show that the restriction of sheaf along an open embedding is still a sheaf.

Equations