# mathlibdocumentation

topology.sheaves.sheaf_condition.pairwise_intersections

# 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
def Top.presheaf.is_sheaf_pairwise_intersections {C : Type u} {X : Top} (F : X) :
Prop

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

Equations
def Top.presheaf.is_sheaf_preserves_limit_pairwise_intersections {C : Type u} {X : Top} (F : X) :
Prop

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

Equations

The remainder of this file shows that these conditions are equivalent to the usual 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]
theorem Top.presheaf.sheaf_condition_pairwise_intersections.cone_equiv_functor_obj_2 {C : Type u} {X : Top} (F : X) ⦃ι : Type v⦄ (U : ι → )  :
@[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]
theorem Top.presheaf.sheaf_condition_pairwise_intersections.cone_equiv_unit_iso_app_hom_hom {C : Type u} {X : Top} (F : X) ⦃ι : Type v⦄ (U : ι → )  :
@[simp]
theorem Top.presheaf.sheaf_condition_pairwise_intersections.cone_equiv_unit_iso_inv_app_hom {C : Type u} {X : Top} (F : X) ⦃ι : Type v⦄ (U : ι → ) (X_1 : category_theory.limits.cone ) :
@[simp]
theorem Top.presheaf.sheaf_condition_pairwise_intersections.cone_equiv_unit_iso_hom_app_hom {C : Type u} {X : Top} (F : X) ⦃ι : Type v⦄ (U : ι → ) (X_1 : category_theory.limits.cone ) :
noncomputable def Top.presheaf.sheaf_condition_pairwise_intersections.cone_equiv_unit_iso {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_counit_iso_inv_app_hom {C : Type u} {X : Top} (F : X) ⦃ι : Type v⦄ (U : ι → )  :
noncomputable def Top.presheaf.sheaf_condition_pairwise_intersections.cone_equiv_counit_iso {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_counit_iso_hom_app_hom {C : Type u} {X : Top} (F : X) ⦃ι : Type v⦄ (U : ι → )  :
@[simp]
theorem Top.presheaf.sheaf_condition_pairwise_intersections.cone_equiv_counit_iso_2 {C : Type u} {X : Top} (F : X) ⦃ι : Type v⦄ (U : ι → ) :
@[simp]
theorem Top.presheaf.sheaf_condition_pairwise_intersections.cone_equiv_functor_2 {C : Type u} {X : Top} (F : X) ⦃ι : Type v⦄ (U : ι → ) :
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]
theorem Top.presheaf.sheaf_condition_pairwise_intersections.cone_equiv_unit_iso_2 {C : Type u} {X : Top} (F : X) ⦃ι : Type v⦄ (U : ι → ) :
@[simp]
theorem Top.presheaf.sheaf_condition_pairwise_intersections.cone_equiv_inverse_2 {C : Type u} {X : Top} (F : X) ⦃ι : Type v⦄ (U : ι → ) :
noncomputable def Top.presheaf.sheaf_condition_pairwise_intersections.is_limit_map_cone_of_is_limit_sheaf_condition_fork {C : Type u} {X : Top} (F : X) ⦃ι : Type v⦄ (U : ι → )  :

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

Equations
noncomputable def Top.presheaf.sheaf_condition_pairwise_intersections.is_limit_sheaf_condition_fork_of_is_limit_map_cone {C : Type u} {X : Top} (F : X) ⦃ι : Type v⦄ (U : ι → )  :

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

Equations
theorem Top.presheaf.is_sheaf_iff_is_sheaf_pairwise_intersections {C : Type u} {X : Top} (F : X) :

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 Top.sheaf.inter_union_pullback_cone {X : Top} {C : Type u} (F : X) (U V : topological_space.opens X) :

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.

Equations
@[simp]
theorem Top.sheaf.inter_union_pullback_cone_X {X : Top} {C : Type u} (F : X) (U V : topological_space.opens X) :
V).X = F.val.obj (opposite.op (U V))
@[simp]
theorem Top.sheaf.inter_union_pullback_cone_fst {X : Top} {C : Type u} (F : X) (U V : topological_space.opens X) :
@[simp]
theorem Top.sheaf.inter_union_pullback_cone_snd {X : Top} {C : Type u} (F : X) (U V : topological_space.opens X) :
noncomputable def Top.sheaf.inter_union_pullback_cone_lift {X : Top} {C : Type u} (F : X) (U V : topological_space.opens X) (s : (F.val.map )  :
s.X 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). TODO: generalize to C without products.

Equations
theorem Top.sheaf.inter_union_pullback_cone_lift_left {X : Top} {C : Type u} (F : X) (U V : topological_space.opens X)  :
= s.fst
theorem Top.sheaf.inter_union_pullback_cone_lift_right {X : Top} {C : Type u} (F : X) (U V : topological_space.opens X)  :
= s.snd
noncomputable def Top.sheaf.is_limit_pullback_cone {X : Top} {C : Type u} (F : X) (U V : topological_space.opens X)  :

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

Equations
• = let ι : := λ (_x : , Top.sheaf.is_limit_pullback_cone._match_1 U V _x in (λ (s : , Top.sheaf.is_limit_pullback_cone._proof_1, _⟩)
• Top.sheaf.is_limit_pullback_cone._match_1 U V {down := j} = j.cases_on U V
noncomputable def Top.sheaf.is_product_of_disjoint {X : Top} {C : Type u} (F : X) (U V : topological_space.opens X) (h : U V = ) :

If U, V are disjoint, then F(U ∪ V) = F(U) × F(V).

Equations