# mathlib3documentation

topology.sheaves.sheaf_condition.equalizer_products

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

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.

noncomputable 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
noncomputable 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
noncomputable 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
noncomputable 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
noncomputable 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
@[simp]
theorem Top.presheaf.sheaf_condition_equalizer_products.res_π_apply {C : Type u} {X : Top} (F : X) {ι : Type v'} (U : ι ) (i : ι) (x : (F.obj (opposite.op (supr U)))) :
@[simp]
theorem Top.presheaf.sheaf_condition_equalizer_products.res_π {C : Type u} {X : Top} (F : X) {ι : Type v'} (U : ι ) (i : ι) :
theorem Top.presheaf.sheaf_condition_equalizer_products.w_apply {C : Type u} {X : Top} (F : X) {ι : Type v'} (U : ι ) (x : (F.obj (opposite.op (supr U)))) :
@[reducible]
noncomputable 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
noncomputable 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]
noncomputable 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]
noncomputable 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
noncomputable 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
noncomputable 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
def Top.presheaf.is_sheaf_equalizer_products {C : Type u} {X : Top} (F : X) :
Prop

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

The remainder of this file shows that the equalizer_products sheaf condition is equivalent to the pariwise_intersections sheaf condition.

@[simp]
theorem Top.presheaf.sheaf_condition_pairwise_intersections.cone_equiv_functor_obj_X {C : Type u} {X : Top} (F : X) {ι : Type v'} (U : ι )  :
@[simp]
theorem Top.presheaf.sheaf_condition_pairwise_intersections.cone_equiv_functor_obj_π_app {C : Type u} {X : Top} (F : X) {ι : Type v'} (U : ι )  :
= Z.cases_on (category_theory.limits.pi.lift (λ (i : ι), c.π.app (category_theory.limits.pi.lift (λ (b : ι × ι), c.π.app (opposite.op b.snd))))
noncomputable def Top.presheaf.sheaf_condition_pairwise_intersections.cone_equiv_functor_obj {C : Type u} {X : Top} (F : X) {ι : Type v'} (U : ι )  :

Implementation of sheaf_condition_pairwise_intersections.cone_equiv.

Equations
noncomputable def Top.presheaf.sheaf_condition_pairwise_intersections.cone_equiv_functor {C : Type u} {X : Top} (F : X) {ι : Type v'} (U : ι ) :

Implementation of sheaf_condition_pairwise_intersections.cone_equiv.

Equations
@[simp]
@[simp]
theorem Top.presheaf.sheaf_condition_pairwise_intersections.cone_equiv_functor_map_hom {C : Type u} {X : Top} (F : X) {ι : Type v'} (U : ι ) (c c' : category_theory.limits.cone ) (f : c c') :
@[simp]
theorem Top.presheaf.sheaf_condition_pairwise_intersections.cone_equiv_inverse_obj_X {C : Type u} {X : Top} (F : X) {ι : Type v'} (U : ι )  :
@[simp]
theorem Top.presheaf.sheaf_condition_pairwise_intersections.cone_equiv_inverse_obj_π_app {C : Type u} {X : Top} (F : X) {ι : Type v'} (U : ι ) (x : ᵒᵖ) :
= opposite.rec (λ (x : , x.cases_on (λ (i : ι), category_theory.limits.pi.π (λ (i : ι), F.obj (opposite.op (U i))) i) (λ (i j : ι), category_theory.limits.pi.π (λ (p : ι × ι), F.obj (opposite.op (U p.fst U p.snd))) (i, j))) x
noncomputable def Top.presheaf.sheaf_condition_pairwise_intersections.cone_equiv_inverse_obj {C : Type u} {X : Top} (F : X) {ι : Type v'} (U : ι )  :

Implementation of sheaf_condition_pairwise_intersections.cone_equiv.

Equations
noncomputable def Top.presheaf.sheaf_condition_pairwise_intersections.cone_equiv_inverse {C : Type u} {X : Top} (F : X) {ι : Type v'} (U : ι ) :

Implementation of sheaf_condition_pairwise_intersections.cone_equiv.

Equations
@[simp]
theorem Top.presheaf.sheaf_condition_pairwise_intersections.cone_equiv_inverse_map_hom {C : Type u} {X : Top} (F : X) {ι : Type v'} (U : ι ) (f : c c') :
@[simp]
noncomputable def Top.presheaf.sheaf_condition_pairwise_intersections.cone_equiv_unit_iso_app {C : Type u} {X : Top} (F : X) {ι : Type v'} (U : ι )  :

Implementation of sheaf_condition_pairwise_intersections.cone_equiv.

Equations
@[simp]
@[simp]

Implementation of sheaf_condition_pairwise_intersections.cone_equiv.

Equations

Implementation of sheaf_condition_pairwise_intersections.cone_equiv.

Equations
@[simp]
@[simp]
noncomputable def Top.presheaf.sheaf_condition_pairwise_intersections.cone_equiv {C : Type u} {X : Top} (F : X) {ι : Type v'} (U : ι ) :

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

Equations
@[simp]
@[simp]

If sheaf_condition_equalizer_products.fork is an equalizer, then F.map_cone (cone U) is a limit cone.

Equations

If F.map_cone (cone U) is a limit cone, then sheaf_condition_equalizer_products.fork is an equalizer.

Equations

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