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 j
to bothsingle i
andsingle 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
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
- F.is_sheaf_pairwise_intersections = ∀ ⦃ι : Type w⦄ (U : ι → topological_space.opens ↥X), nonempty (category_theory.limits.is_limit (category_theory.functor.map_cone F (category_theory.pairwise.cocone U).op))
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
- F.is_sheaf_preserves_limit_pairwise_intersections = ∀ ⦃ι : Type w⦄ (U : ι → topological_space.opens ↥X), nonempty (category_theory.limits.preserves_limit (category_theory.pairwise.diagram U).op F)
The remainder of this file shows that these conditions are equivalent to the usual sheaf condition.
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 (opposite.op (category_theory.pairwise.single i)))) (category_theory.limits.pi.lift (λ (b : ι × ι), c.π.app (opposite.op (category_theory.pairwise.pair b.fst b.snd)))), naturality' := _}}
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).op ⋙ 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).op ⋙ F)) (f : c ⟶ c'), {hom := f.hom, w' := _}, map_id' := _, map_comp' := _}
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 : (category_theory.pairwise ι)ᵒᵖ), opposite.rec (λ (x : category_theory.pairwise ι), x.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))) x, naturality' := _}}
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' := _}
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).op ⋙ 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' := _}
Implementation of sheaf_condition_pairwise_intersections.cone_equiv
.
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' := _}) _
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' := _}
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.cocone U).op).X, w' := _}, hom_inv_id' := _, inv_hom_id' := _}
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.cocone U).op)).X, w' := _}, inv := {hom := 𝟙 (Top.presheaf.sheaf_condition_equalizer_products.fork F U).X, w' := _}, hom_inv_id' := _, inv_hom_id' := _}
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
.
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
- F.inter_union_pullback_cone U V = category_theory.limits.pullback_cone.mk (F.val.map (category_theory.hom_of_le _).op) (F.val.map (category_theory.hom_of_le _).op) _
(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
- F.inter_union_pullback_cone_lift U V s = let ι : ulift category_theory.limits.walking_pair → topological_space.opens ↥X := λ (j : ulift category_theory.limits.walking_pair), j.down.cases_on U V in _.some.lift {X := s.X, π := {app := opposite.rec (λ (X_1 : category_theory.pairwise (ulift category_theory.limits.walking_pair)), X_1.cases_on (λ (X_1 : ulift category_theory.limits.walking_pair), X_1.cases_on (λ (X_1 : category_theory.limits.walking_pair), X_1.cases_on s.fst s.snd)) (λ (X_1_ᾰ X_1_ᾰ_1 : ulift category_theory.limits.walking_pair), X_1_ᾰ.cases_on (λ (X_1_ᾰ : category_theory.limits.walking_pair), X_1_ᾰ.cases_on (s.fst ≫ F.val.map (category_theory.hom_of_le _).op) (s.snd ≫ F.val.map (category_theory.hom_of_le _).op)))), naturality' := _}} ≫ F.val.map (category_theory.eq_to_hom _).op
For a sheaf F
, F(U ∪ V)
is the pullback of F(U) ⟶ F(U ∩ V)
and F(V) ⟶ F(U ∩ V)
.
Equations
- F.is_limit_pullback_cone U V = let ι : ulift category_theory.limits.walking_pair → topological_space.opens ↥X := λ (_x : ulift category_theory.limits.walking_pair), Top.sheaf.is_limit_pullback_cone._match_1 U V _x in (F.inter_union_pullback_cone U V).is_limit_aux' (λ (s : category_theory.limits.pullback_cone (F.val.map (category_theory.hom_of_le _).op) (F.val.map (category_theory.hom_of_le _).op)), ⟨F.inter_union_pullback_cone_lift U V 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
If U, V
are disjoint, then F(U ∪ V) = F(U) × F(V)
.
Equations
- F.is_product_of_disjoint U V h = is_product_of_is_terminal_is_pullback (F.val.map (category_theory.hom_of_le _).op) (F.val.map (category_theory.hom_of_le _).op) (F.val.map (category_theory.hom_of_le _).op) (F.val.map (category_theory.hom_of_le _).op) (F.is_terminal_of_eq_empty h) (F.is_limit_pullback_cone U V)