Flasqueness is a local property #

A sheaf of sets is flasque when all of its restriction maps are surjective. This file proves that this can be checked locally: if every point of X has an open neighbourhood W such that every restriction map F(V) → F(U) with U ⊆ V ⊆ W is surjective, then every restriction map of F is surjective.

The proof is the classical Zorn argument. Fix U ⊆ V and a section s over U, and order the extensions of s to opens between U and V by extension of domain. A chain of extensions glues to an upper bound, so there is a maximal extension t over some O. Given a point x ∈ V, choose a neighbourhood W as above; the restriction of t to O ∩ V ∩ W extends to V ∩ W because restrictions inside W are surjective, and the two sections glue to an extension over O ∪ (V ∩ W). Maximality forces x ∈ O, hence O = V.

The argument is carried out for presheaves of types satisfying the sheaf condition, and is then transported to sheaves valued in a concrete category whose forgetful functor preserves limits, such as sheaves of modules or of abelian groups. For such sheaves Mathlib's TopCat.Sheaf.IsFlasque asks that all restriction maps be epimorphisms; surjective restrictions are epimorphisms, so the locality statement yields flasqueness. If the forgetful functor moreover preserves epimorphisms, flasqueness is shown to be equivalent to flasqueness of the restrictions to the members of some open cover; since flasqueness is invariant under isomorphism, a sheaf which is locally isomorphic to flasque sheaves is then flasque.

Main declarations #

TopCat.Presheaf.IsFlasque.of_iso: a presheaf isomorphic to a flasque presheaf is flasque;
TopCat.Presheaf.IsSheaf.map_surjective_of_locally_flasque: the locality statement for sheaves of types;
TopCat.Sheaf.map_surjective_of_locally_flasque: the same statement for sheaves valued in a concrete category;
TopCat.Sheaf.isFlasque_of_locally_flasque: local surjectivity of restrictions implies flasqueness;
TopCat.Sheaf.isFlasque_iff_locally_isFlasque: a sheaf is flasque if and only if every point has an open neighbourhood on which its restriction is flasque;
TopCat.Sheaf.isFlasque_of_locally_iso: a sheaf which is locally isomorphic to flasque sheaves is flasque.
CategoryTheory.Sheaf.isFlasque: flasque sheaves, as a class of objects closed under isomorphisms.

References #

R. Godement, Topologie algébrique et théorie des faisceaux, Chapitre II, §3.
G. E. Bredon, Sheaf Theory, Chapter II, §5.

source

theorem TopCat.Presheaf.IsFlasque.of_iso {X : TopCat} {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {F G : Presheaf C X} (e : F ≅ G) [F.IsFlasque] :

G.IsFlasque

A presheaf isomorphic to a flasque presheaf is flasque.

source

theorem TopCat.Presheaf.IsSheaf.map_surjective_of_locally_flasque {X : TopCat} {F : Presheaf (Type w) X} (hF : F.IsSheaf) (h : ∀ (x : ↑X), ∃ (W : TopologicalSpace.Opens ↑X), x ∈ W ∧ ∀ ⦃U V : TopologicalSpace.Opens ↑X⦄ (hUV : U ≤ V), V ≤ W → Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.homOfLE hUV).op))) {U V : TopologicalSpace.Opens ↑X} (hUV : U ≤ V) :

Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.homOfLE hUV).op))

If every restriction map of a sheaf of types inside some neighbourhood of each point is surjective, then every restriction map is surjective.

source

theorem TopCat.Sheaf.map_surjective_of_locally_flasque {X : TopCat} {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {FC : C → C → Type u_2} {CC : C → Type u_3} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [CategoryTheory.ConcreteCategory C FC] [CategoryTheory.Limits.PreservesLimitsOfSize.{u, u, v_1, u_3, u_1, u_3 + 1} (CategoryTheory.forget C)] (F : Sheaf C X) (h : ∀ (x : ↑X), ∃ (W : TopologicalSpace.Opens ↑X), x ∈ W ∧ ∀ ⦃U V : TopologicalSpace.Opens ↑X⦄ (hUV : U ≤ V), V ≤ W → Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom (F.obj.map (CategoryTheory.homOfLE hUV).op))) {U V : TopologicalSpace.Opens ↑X} (hUV : U ≤ V) :

Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom (F.obj.map (CategoryTheory.homOfLE hUV).op))

If every restriction map of a sheaf inside some neighbourhood of each point is surjective, then every restriction map is surjective.

source

theorem TopCat.Sheaf.isFlasque_of_locally_flasque {X : TopCat} {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {FC : C → C → Type u_2} {CC : C → Type u_3} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [CategoryTheory.ConcreteCategory C FC] [CategoryTheory.Limits.PreservesLimitsOfSize.{u, u, v_1, u_3, u_1, u_3 + 1} (CategoryTheory.forget C)] (F : Sheaf C X) (h : ∀ (x : ↑X), ∃ (W : TopologicalSpace.Opens ↑X), x ∈ W ∧ ∀ ⦃U V : TopologicalSpace.Opens ↑X⦄ (hUV : U ≤ V), V ≤ W → Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom (F.obj.map (CategoryTheory.homOfLE hUV).op))) :

F.IsFlasque

A sheaf is flasque as soon as every point has an open neighbourhood inside which all restriction maps are surjective.

source

instance TopCat.Sheaf.isFlasque_sheafPullback_obj {X : TopCat} {C : Type u_1} [CategoryTheory.Category.{u, u_1} C] {Y : TopCat} {f : Y ⟶ X} (hf : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) (F : Sheaf C X) [F.IsFlasque] :

((Topology.IsOpenEmbedding.sheafPullback C hf).obj F).IsFlasque

The restriction of a flasque sheaf along an open embedding is flasque.

source

theorem TopCat.Sheaf.isFlasque_iff_locally_isFlasque {X : TopCat} {C : Type u_1} [CategoryTheory.Category.{u, u_1} C] {FC : C → C → Type u_2} {CC : C → Type u_3} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [CategoryTheory.ConcreteCategory C FC] [CategoryTheory.Limits.PreservesLimitsOfSize.{u, u, u, u_3, u_1, u_3 + 1} (CategoryTheory.forget C)] [(CategoryTheory.forget C).PreservesEpimorphisms] (F : Sheaf C X) :

F.IsFlasque ↔ ∀ (x : ↑X), ∃ (W : TopologicalSpace.Opens ↑X), x ∈ W ∧ ((Topology.IsOpenEmbedding.sheafPullback C ⋯).obj F).IsFlasque

Flasqueness of a sheaf is local: a sheaf is flasque if and only if every point has an open neighbourhood W such that the restriction of the sheaf to W is flasque.

source