Sheaves
We define sheaves on a topological space, with values in an arbitrary category.
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).
We provide the instance category (sheaf C X) as the full subcategory of presheaves,
and the fully faithful functor sheaf.forget : sheaf C X ⥤ presheaf C X.
The product of the sections of a presheaf over a family of open sets.
Equations
- Top.sheaf_condition.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.sheaf_condition.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.sheaf_condition.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.sheaf_condition.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.sheaf_condition.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.
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
- Top.sheaf_condition F = Π ⦃ι : Type v⦄ (U : ι → topological_space.opens ↥X), category_theory.limits.is_limit (Top.sheaf_condition.fork F U)
The presheaf valued in punit over any topological space is a sheaf.
Equations
- Top.sheaf_condition_punit F = λ (ι : Type v) (U : ι → topological_space.opens ↥X), category_theory.limits.punit_cone_is_limit
Equations
- presheaf : Top.presheaf C X
- sheaf_condition : Top.sheaf_condition c.presheaf
A sheaf C X is a presheaf of objects from C over a (bundled) topological space X,
satisfying the sheaf condition.
Equations
- X.sheaf_inhabited = {default := {presheaf := category_theory.functor.star (topological_space.opens ↥X)ᵒᵖ category_theory.category.opposite, sheaf_condition := inhabited.default (Top.sheaf_condition (category_theory.functor.star (topological_space.opens ↥X)ᵒᵖ)) (Top.sheaf_condition_inhabited (category_theory.functor.star (topological_space.opens ↥X)ᵒᵖ))}}
The forgetful functor from sheaves to presheaves.