Flasqueness of the constant sheaf on an irreducible space

On an irreducible topological space, the constant sheaf with values in any object of AddCommGrpCat is flasque. The proof descends from the explicit +-construction: the presheaf-level surjectivity lemmas toPlus_surjective_of_const and toPlus_surjective_of_firstPlus combine via a section-by-section gluing argument that relies crucially on nonempty_preirreducible_inter for irreducible spaces.

Main results

• sheafify_const_flasque_of_irreducible
• presheafToSheaf_const_flasque_of_irreducible
• constantSheaf_flasque_of_irreducible
• isFlasqueSheaf_zeroOutsideInt_top

theorem toPlus_injective_of_const {X : Type u} [TopologicalSpace X] {A : AddCommGrpCat} (U : TopologicalSpace.Opens X) (hU : (↑U).Nonempty) (a b : ↑(((CategoryTheory.Functor.const (TopologicalSpace.Opens X)ᵒᵖ).obj A).obj (Opposite.op U))) (h : (CategoryTheory.ConcreteCategory.hom (((Opens.grothendieckTopology X).toPlus ((CategoryTheory.Functor.const (TopologicalSpace.Opens X)ᵒᵖ).obj A)).app (Opposite.op U))) a = (CategoryTheory.ConcreteCategory.hom (((Opens.grothendieckTopology X).toPlus ((CategoryTheory.Functor.const (TopologicalSpace.Opens X)ᵒᵖ).obj A)).app (Opposite.op U))) b) : a = b

theorem toPlus_surjective_of_const {X : Type u} [TopologicalSpace X] {A : AddCommGrpCat} (U : TopologicalSpace.Opens X) (hU : (↑U).Nonempty) : Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom (((Opens.grothendieckTopology X).toPlus ((CategoryTheory.Functor.const (TopologicalSpace.Opens X)ᵒᵖ).obj A)).app (Opposite.op U)))

theorem toPlus_naturality_const {X : Type u} [TopologicalSpace X] {A : AddCommGrpCat} {U V : TopologicalSpace.Opens X} (i : U ⟶ V) (a : ↑(((CategoryTheory.Functor.const (TopologicalSpace.Opens X)ᵒᵖ).obj A).obj (Opposite.op V))) : (CategoryTheory.ConcreteCategory.hom (((Opens.grothendieckTopology X).toPlus ((CategoryTheory.Functor.const (TopologicalSpace.Opens X)ᵒᵖ).obj A)).app (Opposite.op U))) a = (CategoryTheory.ConcreteCategory.hom (((Opens.grothendieckTopology X).plusObj ((CategoryTheory.Functor.const (TopologicalSpace.Opens X)ᵒᵖ).obj A)).map i.op)) ((CategoryTheory.ConcreteCategory.hom (((Opens.grothendieckTopology X).toPlus ((CategoryTheory.Functor.const (TopologicalSpace.Opens X)ᵒᵖ).obj A)).app (Opposite.op V))) a)

theorem toPlus_surjective_of_firstPlus {X : Type u} [TopologicalSpace X] [IrreducibleSpace X] {A : AddCommGrpCat} (U : TopologicalSpace.Opens X) (hU : (↑U).Nonempty) : Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom (((Opens.grothendieckTopology X).toPlus ((Opens.grothendieckTopology X).plusObj ((CategoryTheory.Functor.const (TopologicalSpace.Opens X)ᵒᵖ).obj A))).app (Opposite.op U)))

theorem sheafify_const_flasque_of_irreducible (X : TopCat) [IrreducibleSpace ↑X] (A : AddCommGrpCat) : IsFlasqueSheaf { obj := (Opens.grothendieckTopology ↑X).sheafify ((CategoryTheory.Functor.const (TopologicalSpace.Opens ↑X)ᵒᵖ).obj A), property := ⋯ }

On an irreducible space, the sheafification of the constant presheaf is flasque.

theorem presheafToSheaf_const_flasque_of_irreducible (X : TopCat) [IrreducibleSpace ↑X] (A : AddCommGrpCat) : IsFlasqueSheaf ((CategoryTheory.presheafToSheaf (Opens.grothendieckTopology ↑X) AddCommGrpCat).obj ((CategoryTheory.Functor.const (TopologicalSpace.Opens ↑X)ᵒᵖ).obj A))

On an irreducible space, the presheaf-to-sheaf image of the constant presheaf is flasque.

theorem constantSheaf_flasque_of_irreducible (X : TopCat) [IrreducibleSpace ↑X] (A : AddCommGrpCat) : IsFlasqueSheaf ((CategoryTheory.constantSheaf (Opens.grothendieckTopology ↑X) AddCommGrpCat).obj A)

theorem isFlasqueSheaf_zeroOutsideInt_top (X : TopCat) [IrreducibleSpace ↑X] : IsFlasqueSheaf (TopCat.Sheaf.zeroOutsideInt ⊤)

zeroOutsideInt ⊤ is flasque on an irreducible space: it is the sheafification of constZ.zeroOutside ⊤ ≅ constZ (via zeroOutsideTopIso), and the constant sheaf on an irreducible space is flasque (constantSheaf_flasque_of_irreducible).