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 frompair i jto bothsingle iandsingle 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)), orpreserves_limit (diagram U) F
@[nolint]
def
Top.presheaf.sheaf_condition_pairwise_intersections
{X : Top}
{C : Type u}
[category_theory.category C]
(F : Top.presheaf C X) :
Type (max u (v+1))
An alternative formulation of the sheaf condition
(which we prove equivalent to the usual one below as
sheaf_condition_equiv_sheaf_condition_pairwise_intersections).
A presheaf is a sheaf if F sends the cone pairwise.cone U to a limit cone.
(Recall pairwise.cone U, has cone point supr U, mapping down to the U i and the U i ⊓ U j.)
Equations
- F.sheaf_condition_pairwise_intersections = Π ⦃ι : Type v⦄ (U : ι → topological_space.opens ↥X), category_theory.limits.is_limit (category_theory.functor.map_cone F (category_theory.pairwise.cone U))
@[instance]
def
Top.presheaf.sheaf_condition_pairwise_intersections.subsingleton
{X : Top}
{C : Type u}
[category_theory.category C]
(F : Top.presheaf C X) :
@[nolint]
def
Top.presheaf.sheaf_condition_preserves_limit_pairwise_intersections
{X : Top}
{C : Type u}
[category_theory.category C]
(F : Top.presheaf C X) :
Type (max u (v+1))
An alternative formulation of the sheaf condition
(which we prove equivalent to the usual one below as
sheaf_condition_equiv_sheaf_condition_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
- F.sheaf_condition_preserves_limit_pairwise_intersections = Π ⦃ι : Type v⦄ (U : ι → topological_space.opens ↥X), category_theory.limits.preserves_limit (category_theory.pairwise.diagram U) F
@[instance]
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
{X : Top}
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_products C]
(F : Top.presheaf C X)
⦃ι : Type v⦄
(U : ι → topological_space.opens ↥X)
(c : category_theory.limits.cone (category_theory.pairwise.diagram U ⋙ F)) :
@[simp]
theorem
Top.presheaf.sheaf_condition_pairwise_intersections.cone_equiv_functor_obj_π_app
{X : Top}
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_products C]
(F : Top.presheaf C X)
⦃ι : Type v⦄
(U : ι → topological_space.opens ↥X)
(c : category_theory.limits.cone (category_theory.pairwise.diagram U ⋙ F))
(Z : category_theory.limits.walking_parallel_pair) :
(Top.presheaf.sheaf_condition_pairwise_intersections.cone_equiv_functor_obj F U c).π.app Z = Z.cases_on (category_theory.limits.pi.lift (λ (i : ι), c.π.app (category_theory.pairwise.single i))) (category_theory.limits.pi.lift (λ (b : ι × ι), c.π.app (category_theory.pairwise.pair b.fst b.snd)))
def
Top.presheaf.sheaf_condition_pairwise_intersections.cone_equiv_functor_obj
{X : Top}
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_products C]
(F : Top.presheaf C X)
⦃ι : Type v⦄
(U : ι → topological_space.opens ↥X)
(c : category_theory.limits.cone (category_theory.pairwise.diagram U ⋙ F)) :
Implementation of sheaf_condition_pairwise_intersections.cone_equiv.
Equations
- Top.presheaf.sheaf_condition_pairwise_intersections.cone_equiv_functor_obj F U c = {X := c.X, π := {app := λ (Z : category_theory.limits.walking_parallel_pair), Z.cases_on (category_theory.limits.pi.lift (λ (i : ι), c.π.app (category_theory.pairwise.single i))) (category_theory.limits.pi.lift (λ (b : ι × ι), c.π.app (category_theory.pairwise.pair b.fst b.snd))), naturality' := _}}
def
Top.presheaf.sheaf_condition_pairwise_intersections.cone_equiv_functor
{X : Top}
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_products C]
(F : Top.presheaf C X)
⦃ι : Type v⦄
(U : ι → topological_space.opens ↥X) :
Implementation of sheaf_condition_pairwise_intersections.cone_equiv.
Equations
- Top.presheaf.sheaf_condition_pairwise_intersections.cone_equiv_functor F U = {obj := λ (c : category_theory.limits.cone (category_theory.pairwise.diagram U ⋙ F)), Top.presheaf.sheaf_condition_pairwise_intersections.cone_equiv_functor_obj F U c, map := λ (c c' : category_theory.limits.cone (category_theory.pairwise.diagram U ⋙ F)) (f : c ⟶ c'), {hom := f.hom, w' := _}, map_id' := _, map_comp' := _}
@[simp]
theorem
Top.presheaf.sheaf_condition_pairwise_intersections.cone_equiv_functor_obj_2
{X : Top}
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_products C]
(F : Top.presheaf C X)
⦃ι : Type v⦄
(U : ι → topological_space.opens ↥X)
(c : category_theory.limits.cone (category_theory.pairwise.diagram U ⋙ F)) :
@[simp]
theorem
Top.presheaf.sheaf_condition_pairwise_intersections.cone_equiv_functor_map_hom
{X : Top}
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_products C]
(F : Top.presheaf C X)
⦃ι : Type v⦄
(U : ι → topological_space.opens ↥X)
(c c' : category_theory.limits.cone (category_theory.pairwise.diagram U ⋙ F))
(f : c ⟶ c') :
@[simp]
theorem
Top.presheaf.sheaf_condition_pairwise_intersections.cone_equiv_inverse_obj_X
{X : Top}
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_products C]
(F : Top.presheaf C X)
⦃ι : Type v⦄
(U : ι → topological_space.opens ↥X)
(c : category_theory.limits.cone (Top.presheaf.sheaf_condition_equalizer_products.diagram F U)) :
@[simp]
theorem
Top.presheaf.sheaf_condition_pairwise_intersections.cone_equiv_inverse_obj_π_app
{X : Top}
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_products C]
(F : Top.presheaf C X)
⦃ι : Type v⦄
(U : ι → topological_space.opens ↥X)
(c : category_theory.limits.cone (Top.presheaf.sheaf_condition_equalizer_products.diagram F U))
(X_1 : category_theory.pairwise ι) :
(Top.presheaf.sheaf_condition_pairwise_intersections.cone_equiv_inverse_obj F U c).π.app X_1 = X_1.cases_on (λ (i : ι), c.π.app category_theory.limits.walking_parallel_pair.zero ≫ category_theory.limits.pi.π (λ (i : ι), F.obj (opposite.op (U i))) i) (λ (i j : ι), c.π.app category_theory.limits.walking_parallel_pair.one ≫ category_theory.limits.pi.π (λ (p : ι × ι), F.obj (opposite.op (U p.fst ⊓ U p.snd))) (i, j))
def
Top.presheaf.sheaf_condition_pairwise_intersections.cone_equiv_inverse_obj
{X : Top}
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_products C]
(F : Top.presheaf C X)
⦃ι : Type v⦄
(U : ι → topological_space.opens ↥X)
(c : category_theory.limits.cone (Top.presheaf.sheaf_condition_equalizer_products.diagram F U)) :
Implementation of sheaf_condition_pairwise_intersections.cone_equiv.
Equations
- Top.presheaf.sheaf_condition_pairwise_intersections.cone_equiv_inverse_obj F U c = {X := c.X, π := {app := λ (X_1 : category_theory.pairwise ι), X_1.cases_on (λ (i : ι), c.π.app category_theory.limits.walking_parallel_pair.zero ≫ category_theory.limits.pi.π (λ (i : ι), F.obj (opposite.op (U i))) i) (λ (i j : ι), c.π.app category_theory.limits.walking_parallel_pair.one ≫ category_theory.limits.pi.π (λ (p : ι × ι), F.obj (opposite.op (U p.fst ⊓ U p.snd))) (i, j)), naturality' := _}}
def
Top.presheaf.sheaf_condition_pairwise_intersections.cone_equiv_inverse
{X : Top}
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_products C]
(F : Top.presheaf C X)
⦃ι : Type v⦄
(U : ι → topological_space.opens ↥X) :
Implementation of sheaf_condition_pairwise_intersections.cone_equiv.
Equations
- Top.presheaf.sheaf_condition_pairwise_intersections.cone_equiv_inverse F U = {obj := λ (c : category_theory.limits.cone (Top.presheaf.sheaf_condition_equalizer_products.diagram F U)), Top.presheaf.sheaf_condition_pairwise_intersections.cone_equiv_inverse_obj F U c, map := λ (c c' : category_theory.limits.cone (Top.presheaf.sheaf_condition_equalizer_products.diagram F U)) (f : c ⟶ c'), {hom := f.hom, w' := _}, map_id' := _, map_comp' := _}
@[simp]
theorem
Top.presheaf.sheaf_condition_pairwise_intersections.cone_equiv_inverse_map_hom
{X : Top}
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_products C]
(F : Top.presheaf C X)
⦃ι : Type v⦄
(U : ι → topological_space.opens ↥X)
(c c' : category_theory.limits.cone (Top.presheaf.sheaf_condition_equalizer_products.diagram F U))
(f : c ⟶ c') :
@[simp]
theorem
Top.presheaf.sheaf_condition_pairwise_intersections.cone_equiv_inverse_obj_2
{X : Top}
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_products C]
(F : Top.presheaf C X)
⦃ι : Type v⦄
(U : ι → topological_space.opens ↥X)
(c : category_theory.limits.cone (Top.presheaf.sheaf_condition_equalizer_products.diagram F U)) :
def
Top.presheaf.sheaf_condition_pairwise_intersections.cone_equiv_unit_iso_app
{X : Top}
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_products C]
(F : Top.presheaf C X)
⦃ι : Type v⦄
(U : ι → topological_space.opens ↥X)
(c : category_theory.limits.cone (category_theory.pairwise.diagram U ⋙ F)) :
Implementation of sheaf_condition_pairwise_intersections.cone_equiv.
Equations
- Top.presheaf.sheaf_condition_pairwise_intersections.cone_equiv_unit_iso_app F U c = {hom := {hom := 𝟙 ((𝟭 (category_theory.limits.cone (category_theory.pairwise.diagram U ⋙ F))).obj c).X, w' := _}, inv := {hom := 𝟙 ((Top.presheaf.sheaf_condition_pairwise_intersections.cone_equiv_functor F U ⋙ Top.presheaf.sheaf_condition_pairwise_intersections.cone_equiv_inverse F U).obj c).X, w' := _}, hom_inv_id' := _, inv_hom_id' := _}
@[simp]
theorem
Top.presheaf.sheaf_condition_pairwise_intersections.cone_equiv_unit_iso_app_inv_hom
{X : Top}
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_products C]
(F : Top.presheaf C X)
⦃ι : Type v⦄
(U : ι → topological_space.opens ↥X)
(c : category_theory.limits.cone (category_theory.pairwise.diagram U ⋙ F)) :
@[simp]
theorem
Top.presheaf.sheaf_condition_pairwise_intersections.cone_equiv_unit_iso_app_hom_hom
{X : Top}
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_products C]
(F : Top.presheaf C X)
⦃ι : Type v⦄
(U : ι → topological_space.opens ↥X)
(c : category_theory.limits.cone (category_theory.pairwise.diagram U ⋙ F)) :
@[simp]
theorem
Top.presheaf.sheaf_condition_pairwise_intersections.cone_equiv_unit_iso_inv_app_hom
{X : Top}
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_products C]
(F : Top.presheaf C X)
⦃ι : Type v⦄
(U : ι → topological_space.opens ↥X)
(X_1 : category_theory.limits.cone (category_theory.pairwise.diagram U ⋙ F)) :
@[simp]
theorem
Top.presheaf.sheaf_condition_pairwise_intersections.cone_equiv_unit_iso_hom_app_hom
{X : Top}
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_products C]
(F : Top.presheaf C X)
⦃ι : Type v⦄
(U : ι → topological_space.opens ↥X)
(X_1 : category_theory.limits.cone (category_theory.pairwise.diagram U ⋙ F)) :
((Top.presheaf.sheaf_condition_pairwise_intersections.cone_equiv_unit_iso F U).hom.app X_1).hom = 𝟙 ((𝟭 (category_theory.limits.cone (category_theory.pairwise.diagram U ⋙ F))).obj X_1).X
def
Top.presheaf.sheaf_condition_pairwise_intersections.cone_equiv_unit_iso
{X : Top}
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_products C]
(F : Top.presheaf C X)
⦃ι : Type v⦄
(U : ι → topological_space.opens ↥X) :
Implementation of sheaf_condition_pairwise_intersections.cone_equiv.
@[simp]
theorem
Top.presheaf.sheaf_condition_pairwise_intersections.cone_equiv_counit_iso_inv_app_hom
{X : Top}
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_products C]
(F : Top.presheaf C X)
⦃ι : Type v⦄
(U : ι → topological_space.opens ↥X)
(X_1 : category_theory.limits.cone (Top.presheaf.sheaf_condition_equalizer_products.diagram F U)) :
def
Top.presheaf.sheaf_condition_pairwise_intersections.cone_equiv_counit_iso
{X : Top}
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_products C]
(F : Top.presheaf C X)
⦃ι : Type v⦄
(U : ι → topological_space.opens ↥X) :
Implementation of sheaf_condition_pairwise_intersections.cone_equiv.
Equations
- Top.presheaf.sheaf_condition_pairwise_intersections.cone_equiv_counit_iso F U = category_theory.nat_iso.of_components (λ (c : category_theory.limits.cone (Top.presheaf.sheaf_condition_equalizer_products.diagram F U)), {hom := {hom := 𝟙 ((Top.presheaf.sheaf_condition_pairwise_intersections.cone_equiv_inverse F U ⋙ Top.presheaf.sheaf_condition_pairwise_intersections.cone_equiv_functor F U).obj c).X, w' := _}, inv := {hom := 𝟙 ((𝟭 (category_theory.limits.cone (Top.presheaf.sheaf_condition_equalizer_products.diagram F U))).obj c).X, w' := _}, hom_inv_id' := _, inv_hom_id' := _}) _
@[simp]
theorem
Top.presheaf.sheaf_condition_pairwise_intersections.cone_equiv_counit_iso_hom_app_hom
{X : Top}
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_products C]
(F : Top.presheaf C X)
⦃ι : Type v⦄
(U : ι → topological_space.opens ↥X)
(X_1 : category_theory.limits.cone (Top.presheaf.sheaf_condition_equalizer_products.diagram F U)) :
@[simp]
theorem
Top.presheaf.sheaf_condition_pairwise_intersections.cone_equiv_counit_iso_2
{X : Top}
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_products C]
(F : Top.presheaf C X)
⦃ι : Type v⦄
(U : ι → topological_space.opens ↥X) :
@[simp]
theorem
Top.presheaf.sheaf_condition_pairwise_intersections.cone_equiv_functor_2
{X : Top}
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_products C]
(F : Top.presheaf C X)
⦃ι : Type v⦄
(U : ι → topological_space.opens ↥X) :
def
Top.presheaf.sheaf_condition_pairwise_intersections.cone_equiv
{X : Top}
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_products C]
(F : Top.presheaf C X)
⦃ι : Type v⦄
(U : ι → topological_space.opens ↥X) :
Cones over diagram U ⋙ F are the same as a cones over the usual sheaf condition equalizer diagram.
Equations
- Top.presheaf.sheaf_condition_pairwise_intersections.cone_equiv F U = {functor := Top.presheaf.sheaf_condition_pairwise_intersections.cone_equiv_functor F U, inverse := Top.presheaf.sheaf_condition_pairwise_intersections.cone_equiv_inverse F U, unit_iso := Top.presheaf.sheaf_condition_pairwise_intersections.cone_equiv_unit_iso F U, counit_iso := Top.presheaf.sheaf_condition_pairwise_intersections.cone_equiv_counit_iso F U, functor_unit_iso_comp' := _}
@[simp]
theorem
Top.presheaf.sheaf_condition_pairwise_intersections.cone_equiv_unit_iso_2
{X : Top}
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_products C]
(F : Top.presheaf C X)
⦃ι : Type v⦄
(U : ι → topological_space.opens ↥X) :
@[simp]
theorem
Top.presheaf.sheaf_condition_pairwise_intersections.cone_equiv_inverse_2
{X : Top}
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_products C]
(F : Top.presheaf C X)
⦃ι : Type v⦄
(U : ι → topological_space.opens ↥X) :
def
Top.presheaf.sheaf_condition_pairwise_intersections.is_limit_map_cone_of_is_limit_sheaf_condition_fork
{X : Top}
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_products C]
(F : Top.presheaf C X)
⦃ι : Type v⦄
(U : ι → topological_space.opens ↥X)
(P : category_theory.limits.is_limit (Top.presheaf.sheaf_condition_equalizer_products.fork F U)) :
If sheaf_condition_equalizer_products.fork is an equalizer,
then F.map_cone (cone U) is a limit cone.
Equations
- Top.presheaf.sheaf_condition_pairwise_intersections.is_limit_map_cone_of_is_limit_sheaf_condition_fork F U P = (⇑((category_theory.limits.is_limit.of_cone_equiv (Top.presheaf.sheaf_condition_pairwise_intersections.cone_equiv F U).symm).symm) P).of_iso_limit {hom := {hom := 𝟙 ((Top.presheaf.sheaf_condition_pairwise_intersections.cone_equiv F U).symm.functor.obj (Top.presheaf.sheaf_condition_equalizer_products.fork F U)).X, w' := _}, inv := {hom := 𝟙 (category_theory.functor.map_cone F (category_theory.pairwise.cone U)).X, w' := _}, hom_inv_id' := _, inv_hom_id' := _}
def
Top.presheaf.sheaf_condition_pairwise_intersections.is_limit_sheaf_condition_fork_of_is_limit_map_cone
{X : Top}
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_products C]
(F : Top.presheaf C X)
⦃ι : Type v⦄
(U : ι → topological_space.opens ↥X)
(Q : category_theory.limits.is_limit (category_theory.functor.map_cone F (category_theory.pairwise.cone U))) :
If F.map_cone (cone U) is a limit cone,
then sheaf_condition_equalizer_products.fork is an equalizer.
Equations
- Top.presheaf.sheaf_condition_pairwise_intersections.is_limit_sheaf_condition_fork_of_is_limit_map_cone F U Q = (⇑((category_theory.limits.is_limit.of_cone_equiv (Top.presheaf.sheaf_condition_pairwise_intersections.cone_equiv F U)).symm) Q).of_iso_limit {hom := {hom := 𝟙 ((Top.presheaf.sheaf_condition_pairwise_intersections.cone_equiv F U).functor.obj (category_theory.functor.map_cone F (category_theory.pairwise.cone U))).X, w' := _}, inv := {hom := 𝟙 (Top.presheaf.sheaf_condition_equalizer_products.fork F U).X, w' := _}, hom_inv_id' := _, inv_hom_id' := _}
def
Top.presheaf.sheaf_condition_equiv_sheaf_condition_pairwise_intersections
{X : Top}
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_products C]
(F : Top.presheaf C 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.
Equations
- F.sheaf_condition_equiv_sheaf_condition_pairwise_intersections = equiv.Pi_congr_right (λ (i : Type v), equiv.Pi_congr_right (λ (U : i → topological_space.opens ↥X), equiv_of_subsingleton_of_subsingleton (Top.presheaf.sheaf_condition_pairwise_intersections.is_limit_map_cone_of_is_limit_sheaf_condition_fork F U) (Top.presheaf.sheaf_condition_pairwise_intersections.is_limit_sheaf_condition_fork_of_is_limit_map_cone F U)))
def
Top.presheaf.sheaf_condition_equiv_sheaf_condition_preserves_limit_pairwise_intersections
{X : Top}
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_products C]
(F : Top.presheaf C X) :
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.
Equations
- F.sheaf_condition_equiv_sheaf_condition_preserves_limit_pairwise_intersections = F.sheaf_condition_equiv_sheaf_condition_pairwise_intersections.trans (equiv.Pi_congr_right (λ (i : Type v), equiv.Pi_congr_right (λ (U : i → topological_space.opens ↥X), equiv_of_subsingleton_of_subsingleton (λ (P : category_theory.limits.is_limit (category_theory.functor.map_cone F (category_theory.pairwise.cone U))), category_theory.limits.preserves_limit_of_preserves_limit_cone (category_theory.pairwise.cone_is_limit U) P) (λ (a : category_theory.limits.preserves_limit (category_theory.pairwise.diagram U) F), category_theory.limits.preserves_limit.preserves (category_theory.pairwise.cone_is_limit U)))))