Flasque Sheaves

We define and prove basic properties about flasque sheaves on topological spaces.

Main definition

• TopCat.Sheaf.IsFlasque: A sheaf is flasque if all of the restriction morphisms are epimorphisms.

Main results

• TopCat.Sheaf.IsFlasque.epi_of_shortExact: Given a short exact sequence of sheaves, 0 ⟶ 𝓕 ⟶ 𝓖 ⟶ 𝓗 ⟶ 0, if 𝓕 is flasque then 𝓖(U) ⟶ 𝓗(U) is surjective, for any open U.

• TopCat.Sheaf.IsFlasque.of_shortExact_of_isFlasque₁₂ : Given a short exact sequence of sheaves, 0 ⟶ 𝓕 ⟶ 𝓖 ⟶ 𝓗 ⟶ 0, if 𝓕 and 𝓖 are flasque, then 𝓗 is flasque.

class TopCat.Presheaf.IsFlasque {X : TopCat} {C : Type v} [CategoryTheory.Category.{w, v} C] (F : Presheaf C X) : Prop

A sheaf is flasque if all of the restriction morphisms are epimorphisms.

• epi {U V : (TopologicalSpace.Opens ↑X)ᵒᵖ} (i : U ⟶ V) : CategoryTheory.Epi (F.map i)

instance TopCat.Presheaf.IsFlasque.pushforward_isFlasque {X : TopCat} {C : Type v} [CategoryTheory.Category.{w, v} C] (F : Presheaf C X) {Y : TopCat} [F.IsFlasque] (f : X ⟶ Y) : ((pushforward C f).obj F).IsFlasque

@[reducible, inline]

abbrev TopCat.Sheaf.IsFlasque {X : TopCat} {C : Type v} [CategoryTheory.Category.{w, v} C] (F : Sheaf C X) : Prop

A sheaf is flasque if it is flasque as a presheaf

Equations

• F.IsFlasque = TopCat.Presheaf.IsFlasque F.obj

instance TopCat.Sheaf.IsFlasque.pushforward_isFlasque {X : TopCat} {C : Type v} [CategoryTheory.Category.{w, v} C] {Y : TopCat} (F : Sheaf C X) [F.IsFlasque] (f : X ⟶ Y) : ((pushforward C f).obj F).IsFlasque

@[reducible, inline]

abbrev TopCat.Sheaf.IsFlasque.Under {X : TopCat} {U : TopologicalSpace.Opens ↑X} {F G : Sheaf AddCommGrpCat X} (g : F ⟶ G) (s : ↑(G.obj.obj (Opposite.op U))) : Type u

Given a morphism of sheaves g: F ⟶ G and a section s of G(U), Under g s is comprised of an open V and a section of F(V) that maps to s |_ V via g.

Equations

• One or more equations did not get rendered due to their size.

theorem TopCat.Sheaf.IsFlasque.structured_arrows_elements_sheaf_chains_bounded {X : TopCat} {U : TopologicalSpace.Opens ↑X} {F G : Sheaf AddCommGrpCat X} (g : F ⟶ G) (s : ↑(G.obj.obj (Opposite.op U))) (c : Set (Under g s)) (h : IsChain (fun (x y : Under g s) => Nonempty (y ⟶ x)) c) : ∃ (ub : Under g s), ∀ a ∈ c, Nonempty (ub ⟶ a)

theorem TopCat.Sheaf.IsFlasque.epi_of_shortExact {X : TopCat} {U : TopologicalSpace.Opens ↑X} {S : CategoryTheory.ShortComplex (Sheaf AddCommGrpCat X)} (hS : S.ShortExact) [S.X₁.IsFlasque] : CategoryTheory.Epi (S.g.hom.app (Opposite.op U))

Given a short exact sequence of sheaves, 0 ⟶ 𝓕 ⟶ 𝓖 ⟶ 𝓗 ⟶ 0, if 𝓕 is flasque then 𝓖(U) ⟶ 𝓗(U) is surjective, for any open U.

theorem TopCat.Sheaf.IsFlasque.of_shortExact_of_isFlasque₁₂ {X : TopCat} {S : CategoryTheory.ShortComplex (Sheaf AddCommGrpCat X)} (hS : S.ShortExact) [S.X₁.IsFlasque] [S.X₂.IsFlasque] : S.X₃.IsFlasque

Given a short exact sequence of sheaves, 0 ⟶ 𝓕 ⟶ 𝓖 ⟶ 𝓗 ⟶ 0, if 𝓕 and 𝓖 are flasque, then 𝓗 is flasque.