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)
.
The product of the sections of a presheaf over a family of open sets.
Equations
- Top.presheaf.sheaf_condition_equalizer_products.pi_opens F U = ∏ λ (i : ι), F.obj (opposite.op (U i))
The product of the sections of a presheaf over the pairwise intersections of a family of open sets.
Equations
- Top.presheaf.sheaf_condition_equalizer_products.pi_inters F U = ∏ λ (p : ι × ι), F.obj (opposite.op (U p.fst ⊓ U p.snd))
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
- Top.presheaf.sheaf_condition_equalizer_products.left_res F U = category_theory.limits.pi.lift (λ (p : ι × ι), category_theory.limits.pi.π (λ (i : ι), F.obj (opposite.op (U i))) p.fst ≫ F.map ((U p.fst).inf_le_left (U p.snd)).op)
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
- Top.presheaf.sheaf_condition_equalizer_products.right_res F U = category_theory.limits.pi.lift (λ (p : ι × ι), category_theory.limits.pi.π (λ (i : ι), F.obj (opposite.op (U i))) p.snd ≫ F.map ((U p.fst).inf_le_right (U p.snd)).op)
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
- Top.presheaf.sheaf_condition_equalizer_products.res F U = category_theory.limits.pi.lift (λ (i : ι), F.map (topological_space.opens.le_supr U i).op)
The equalizer diagram for the sheaf condition.
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.
Isomorphic presheaves have isomorphic pi_opens
for any cover U
.
Equations
- Top.presheaf.sheaf_condition_equalizer_products.pi_opens.iso_of_iso U α = category_theory.limits.pi.map_iso (λ (X_1 : ι), α.app (opposite.op (U X_1)))
Isomorphic presheaves have isomorphic pi_inters
for any cover U
.
Equations
- Top.presheaf.sheaf_condition_equalizer_products.pi_inters.iso_of_iso U α = category_theory.limits.pi.map_iso (λ (X_1 : ι × ι), α.app (opposite.op (U X_1.fst ⊓ U X_1.snd)))
Isomorphic presheaves have isomorphic sheaf condition diagrams.
Equations
- Top.presheaf.sheaf_condition_equalizer_products.diagram.iso_of_iso U α = category_theory.nat_iso.of_components (λ (X_1 : category_theory.limits.walking_parallel_pair), X_1.cases_on (Top.presheaf.sheaf_condition_equalizer_products.pi_opens.iso_of_iso U α) (Top.presheaf.sheaf_condition_equalizer_products.pi_inters.iso_of_iso U α)) _
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
Push forward a cover along an open embedding.
Equations
- Top.presheaf.sheaf_condition_equalizer_products.cover.of_open_embedding oe 𝒰 = λ (i : ι), _.functor.obj (𝒰 i)
The isomorphism between pi_opens
corresponding to an open embedding.
Equations
The isomorphism between pi_inters
corresponding to an open embedding.
Equations
- Top.presheaf.sheaf_condition_equalizer_products.pi_inters.iso_of_open_embedding oe 𝒰 = category_theory.limits.pi.map_iso (λ (X_1 : ι × ι), category_theory.functor.map_iso F (id {hom := category_theory.hom_of_le _, inv := category_theory.hom_of_le _, hom_inv_id' := _, inv_hom_id' := _}.op))
The isomorphism of sheaf condition diagrams corresponding to an open embedding.
Equations
- Top.presheaf.sheaf_condition_equalizer_products.diagram.iso_of_open_embedding oe 𝒰 = category_theory.nat_iso.of_components (λ (X_1 : category_theory.limits.walking_parallel_pair), X_1.cases_on (Top.presheaf.sheaf_condition_equalizer_products.pi_opens.iso_of_open_embedding oe 𝒰) (Top.presheaf.sheaf_condition_equalizer_products.pi_inters.iso_of_open_embedding oe 𝒰)) _
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
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
- F.is_sheaf_equalizer_products = ∀ ⦃ι : Type v⦄ (U : ι → topological_space.opens ↥X), nonempty (category_theory.limits.is_limit (Top.presheaf.sheaf_condition_equalizer_products.fork F U))