mathlib3 documentation

topology.sheaves.forget

Checking the sheaf condition on the underlying presheaf of types. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

If G : C ⥤ D is a functor which reflects isomorphisms and preserves limits (we assume all limits exist in both C and D), then checking the sheaf condition for a presheaf F : presheaf C X is equivalent to checking the sheaf condition for F ⋙ G.

The important special case is when C is a concrete category with a forgetful functor that preserves limits and reflects isomorphisms. Then to check the sheaf condition it suffices to check it on the underlying sheaf of types.

References #

source
noncomputable def Top.presheaf.sheaf_condition.diagram_comp_preserves_limits {C : Type u₁} [category_theory.category C] [category_theory.limits.has_limits C] {D : Type u₂} [category_theory.category D] [category_theory.limits.has_limits D] (G : C ⥤ D) [category_theory.limits.preserves_limits G] {X : Top} (F : Top.presheaf C X) {ι : Type v} (U : ι → topological_space.opens ↥X) :
Top.presheaf.sheaf_condition_equalizer_products.diagram F U ⋙ G ≅ Top.presheaf.sheaf_condition_equalizer_products.diagram (F ⋙ G) U

When G preserves limits, the sheaf condition diagram for F composed with G is naturally isomorphic to the sheaf condition diagram for F ⋙ G.

Equations
source
noncomputable def Top.presheaf.sheaf_condition.map_cone_fork {C : Type u₁} [category_theory.category C] [category_theory.limits.has_limits C] {D : Type u₂} [category_theory.category D] [category_theory.limits.has_limits D] (G : C ⥤ D) [category_theory.limits.preserves_limits G] {X : Top} (F : Top.presheaf C X) {ι : Type v} (U : ι → topological_space.opens ↥X) :
G.map_cone (Top.presheaf.sheaf_condition_equalizer_products.fork F U) ≅ (category_theory.limits.cones.postcompose (Top.presheaf.sheaf_condition.diagram_comp_preserves_limits G F U).inv).obj (Top.presheaf.sheaf_condition_equalizer_products.fork (F ⋙ G) U)

When G preserves limits, the image under G of the sheaf condition fork for F is the sheaf condition fork for F ⋙ G, postcomposed with the inverse of the natural isomorphism diagram_comp_preserves_limits.

Equations
source
theorem Top.presheaf.is_sheaf_iff_is_sheaf_comp {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (G : C ⥤ D) [category_theory.reflects_isomorphisms G] [category_theory.limits.has_limits C] [category_theory.limits.has_limits D] [category_theory.limits.preserves_limits G] {X : Top} (F : Top.presheaf C X) :
F.is_sheaf ↔ Top.presheaf.is_sheaf (F ⋙ G)

If G : C ⥤ D is a functor which reflects isomorphisms and preserves limits (we assume all limits exist in both C and D), then checking the sheaf condition for a presheaf F : presheaf C X is equivalent to checking the sheaf condition for F ⋙ G.

The important special case is when C is a concrete category with a forgetful functor that preserves limits and reflects isomorphisms. Then to check the sheaf condition it suffices to check it on the underlying sheaf of types.

Another useful example is the forgetful functor TopCommRing ⥤ Top.

See https://stacks.math.columbia.edu/tag/0073. In fact we prove a stronger version with arbitrary complete target category.

As an example, we now have everything we need to check the sheaf condition for a presheaf of commutative rings, merely by checking the sheaf condition for the underlying sheaf of types.

import algebra.category.Ring.limits
example (X : Top) (F : presheaf CommRing X) (h : presheaf.is_sheaf (F ⋙ (forget CommRing))) :
  F.is_sheaf :=
(is_sheaf_iff_is_sheaf_comp (forget CommRing) F).mpr h