Extension-by-zero presheaf and sheaf machinery

The "extension by zero" of a presheaf F along the inclusion of an open U. The construction zeroOutside U F agrees with F on opens W ≤ U and is the zero object elsewhere. Sheafified, with F = constZ (the constant presheaf with value ULift ℤ), this yields zeroOutsideInt U, which serves as the canonical generator family for the finitely-generated subsheaf reduction in the Grothendieck vanishing proof.

Main definitions

• TopCat.Presheaf.zeroOutside — the extension-by-zero presheaf.
• TopCat.Presheaf.constZ — the constant presheaf ULift ℤ.
• TopCat.Sheaf.zeroOutsideInt — sheafified extension-by-zero of constZ on U.
• TopCat.Sheaf.zeroOutsideInt.sHom — section-to-morphism construction.
• TopCat.Sheaf.zeroOutsideInt.generator — canonical generator of (constZ.zeroOutside U).obj (op U).

Main results

• zeroOutside_openHom_stalk_surj, sheafifyMap_zeroOutside_openHom_stalk_surj — stalk surjectivity for the open-inclusion morphisms (and their sheafifications) at points of the support.
• stalk_zeroOutsideInt_zero_outside — stalks of zeroOutsideInt U vanish off U.
• isZero_zeroOutsideInt_bot — zeroOutsideInt ⊥ is the zero sheaf.
• stalk_zeroOutsideInt_eq_zsmul_generator — stalks on U are integer multiples of the canonical germ.

noncomputable def TopCat.Presheaf.zeroOutside {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroObject C] {X : TopCat} (U : TopologicalSpace.Opens ↑X) (F : Presheaf C X) : Presheaf C X

Presheaf that agrees with F on opens contained in U and is zero outside U.

Equations

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

theorem TopCat.Presheaf.zeroOutside_isZero {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroObject C] {X : TopCat} {U : TopologicalSpace.Opens ↑X} {F : Presheaf C X} {W : TopologicalSpace.Opens ↑X} (h : ¬W ≤ U) : CategoryTheory.Limits.IsZero ((zeroOutside U F).obj (Opposite.op W))

theorem TopCat.Presheaf.zeroOutside_le {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroObject C] {X : TopCat} {U : TopologicalSpace.Opens ↑X} {F : Presheaf C X} {W : TopologicalSpace.Opens ↑X} (h : W ≤ U) : (zeroOutside U F).obj (Opposite.op W) = F.obj (Opposite.op W)

noncomputable def TopCat.Presheaf.zeroOutsideTopIso {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroObject C] {X : TopCat} {F : Presheaf C X} : zeroOutside ⊤ F ≅ F

zeroOutside ⊤ F ≅ F: zero-outside on the whole space is the identity.

Equations

• TopCat.Presheaf.zeroOutsideTopIso = CategoryTheory.NatIso.ofComponents (fun (W : (TopologicalSpace.Opens ↑X)ᵒᵖ) => CategoryTheory.eqToIso ⋯) ⋯

noncomputable def TopCat.Presheaf.zeroOutsideOpenHom {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroObject C] {X : TopCat} {U : TopologicalSpace.Opens ↑X} {F : Presheaf C X} {V : TopologicalSpace.Opens ↑X} (h : V ≤ U) : zeroOutside V F ⟶ zeroOutside U F

The canonical inclusion zeroOutside V F ⟶ zeroOutside U F for V ≤ U.

Equations

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

instance TopCat.Presheaf.zeroOutside_hom_mono {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroObject C] {X : TopCat} {U : TopologicalSpace.Opens ↑X} {F : Presheaf C X} {V : TopologicalSpace.Opens ↑X} (h : V ≤ U) [CategoryTheory.Limits.HasPullbacks C] : CategoryTheory.Mono (zeroOutsideOpenHom h)

The canonical inclusion of zero-outside presheaves is a monomorphism.

theorem zeroOutside_openHom_stalk_surj {X : TopCat} {F : TopCat.Presheaf AddCommGrpCat X} {V U : TopologicalSpace.Opens ↑X} (h : V ≤ U) (x : ↑X) (hx : x ∈ V) : Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom ((TopCat.Presheaf.stalkFunctor AddCommGrpCat x).map (TopCat.Presheaf.zeroOutsideOpenHom h)))

The presheaf stalk map of zeroOutsideOpenHom h at x ∈ V is surjective: any germ in the larger zero-outside presheaf can be lifted by restricting to W ∩ V ≤ V where the presheaf map is eqToHom (identity).

theorem sheafifyMap_zeroOutside_openHom_stalk_surj {X : TopCat} (F : TopCat.Presheaf AddCommGrpCat X) {V U : TopologicalSpace.Opens ↑X} (h : V ≤ U) (x : ↑X) (hx : x ∈ V) : Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom ((TopCat.Presheaf.stalkFunctor AddCommGrpCat x).map (CategoryTheory.sheafifyMap (Opens.grothendieckTopology ↑X) (TopCat.Presheaf.zeroOutsideOpenHom h))))

The sheaf stalk map of sheafifyMap (zeroOutsideOpenHom h) at x ∈ V is surjective. Transfers presheaf stalk surjectivity via toSheafify_naturality and the fact that stalk(toSheafify) is an isomorphism.

@[reducible, inline]

abbrev TopCat.Presheaf.constZ {X : TopCat} : Presheaf AddCommGrpCat X

The constant presheaf with value ULift ℤ.

Equations

• TopCat.Presheaf.constZ = (CategoryTheory.Functor.const (TopologicalSpace.Opens ↑X)ᵒᵖ).obj (AddCommGrpCat.of (ULift.{?u.1, 0} ℤ))

noncomputable def TopCat.Presheaf.zeroOutside.generator {X : TopCat} (U : TopologicalSpace.Opens ↑X) : ↑((zeroOutside U constZ).obj (Opposite.op U))

Distinguished integer generator of constZ.zeroOutside U over U.

Equations

• TopCat.Presheaf.zeroOutside.generator U = (CategoryTheory.ConcreteCategory.hom (CategoryTheory.eqToHom ⋯)) 1

noncomputable def TopCat.Presheaf.zeroOutside.sHom {X : TopCat} {U : TopologicalSpace.Opens ↑X} {F : Presheaf AddCommGrpCat X} (s : ↑(F.obj (Opposite.op U))) : zeroOutside U constZ ⟶ F

Morphism from constZ.zeroOutside U determined by a section over U.

Equations

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

theorem TopCat.Presheaf.zeroOutside.sHom_app_generator {X : TopCat} {U : TopologicalSpace.Opens ↑X} {F : Presheaf AddCommGrpCat X} (s : ↑(F.obj (Opposite.op U))) : (CategoryTheory.ConcreteCategory.hom ((sHom s).app (Opposite.op U))) (generator U) = s

theorem TopCat.Presheaf.zeroOutside.resGen_eqToHom_eq_one {X : TopCat} (V : TopologicalSpace.Opens ↑X) {W : TopologicalSpace.Opens ↑X} (hWV : W ≤ V) (hObjW : (zeroOutside V constZ).obj (Opposite.op W) = AddCommGrpCat.of (ULift.{u, 0} ℤ)) : (AddCommGrpCat.Hom.hom (CategoryTheory.eqToHom hObjW)) ((CategoryTheory.ConcreteCategory.hom ((zeroOutside V constZ).map (CategoryTheory.homOfLE hWV).op)) (generator V)) = 1

The restriction of the distinguished generator of constZ.zeroOutside V to a smaller open W ≤ V corresponds to 1 : ULift ℤ under the canonical identification with ULift ℤ.

theorem TopCat.Presheaf.zeroOutside.presheaf_stalk_zeroOutside_eq_zsmul_generator {X : TopCat} (V : TopologicalSpace.Opens ↑X) (x : ↑X) (hx : x ∈ V) (a : ↑((stalkFunctor AddCommGrpCat x).obj (zeroOutside V constZ))) : ∃ (n : ℤ), a = n • (CategoryTheory.ConcreteCategory.hom ((zeroOutside V constZ).germ V x hx)) (generator V)

At a point inside the support open, every stalk element of the presheaf constZ.zeroOutside V is an integer multiple of the germ of the distinguished generator over V.

noncomputable def TopCat.Sheaf.zeroOutsideInt {X : TopCat} (U : TopologicalSpace.Opens ↑X) : Sheaf AddCommGrpCat X

Sheafification of the integer-valued zero-outside presheaf.

Equations

• TopCat.Sheaf.zeroOutsideInt U = (CategoryTheory.presheafToSheaf (Opens.grothendieckTopology ↑X) AddCommGrpCat).obj (TopCat.Presheaf.zeroOutside U TopCat.Presheaf.constZ)

noncomputable def TopCat.Sheaf.zeroOutsideInt.generator {X : TopCat} (U : TopologicalSpace.Opens ↑X) : ↑((zeroOutsideInt U).presheaf.obj (Opposite.op U))

Distinguished generator section of zeroOutsideInt U over U.

Equations

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

noncomputable def TopCat.Sheaf.zeroOutsideInt.openHom {X : TopCat} {V U : TopologicalSpace.Opens ↑X} (h : V ≤ U) : zeroOutsideInt V ⟶ zeroOutsideInt U

The canonical morphism zeroOutsideInt V ⟶ zeroOutsideInt U for V ≤ U.

Equations

• TopCat.Sheaf.zeroOutsideInt.openHom h = { hom := CategoryTheory.sheafifyMap (Opens.grothendieckTopology ↑X) (TopCat.Presheaf.zeroOutsideOpenHom h) }

@[simp]

theorem TopCat.Sheaf.zeroOutsideInt.openHom_hom {X : TopCat} {V U : TopologicalSpace.Opens ↑X} (h : V ≤ U) : (openHom h).hom = CategoryTheory.sheafifyMap (Opens.grothendieckTopology ↑X) (Presheaf.zeroOutsideOpenHom h)

instance TopCat.Sheaf.zeroOutsideInt.instMonoAddCommGrpCatOpenHom {X : TopCat} {V U : TopologicalSpace.Opens ↑X} (h : V ≤ U) : CategoryTheory.Mono (openHom h)

@[reducible, inline]

noncomputable abbrev TopCat.Sheaf.zeroOutsideInt.sHomVal {X : TopCat} {U : TopologicalSpace.Opens ↑X} {F : Presheaf AddCommGrpCat X} (hF : F.IsSheaf) (s : ↑(F.obj (Opposite.op U))) : (zeroOutsideInt U).obj ⟶ F

Presheaf morphism out of zeroOutsideInt U induced by a section of a sheaf over U.

Equations

• TopCat.Sheaf.zeroOutsideInt.sHomVal hF s = CategoryTheory.sheafifyLift (Opens.grothendieckTopology ↑X) (TopCat.Presheaf.zeroOutside.sHom s) hF

noncomputable def TopCat.Sheaf.zeroOutsideInt.sHom {X : TopCat} {U : TopologicalSpace.Opens ↑X} {F : Sheaf AddCommGrpCat X} (s : ↑(F.presheaf.obj (Opposite.op U))) : zeroOutsideInt U ⟶ F

Sheaf morphism out of zeroOutsideInt U induced by a section of F over U.

Equations

• TopCat.Sheaf.zeroOutsideInt.sHom s = { hom := TopCat.Sheaf.zeroOutsideInt.sHomVal ⋯ s }

theorem TopCat.Sheaf.zeroOutsideInt.sHomVal_app_generator {X : TopCat} {U : TopologicalSpace.Opens ↑X} {F : Presheaf AddCommGrpCat X} (hF : F.IsSheaf) (s : ↑(F.obj (Opposite.op U))) : (CategoryTheory.ConcreteCategory.hom ((sHomVal hF s).app (Opposite.op U))) (generator U) = s

theorem TopCat.Sheaf.zeroOutsideInt.sHom_app_generator {X : TopCat} {U : TopologicalSpace.Opens ↑X} {F : Sheaf AddCommGrpCat X} (s : ↑(F.presheaf.obj (Opposite.op U))) : (CategoryTheory.ConcreteCategory.hom ((sHom s).hom.app (Opposite.op U))) (generator U) = s

theorem TopCat.Sheaf.zeroOutsideInt.openHom_val_app_generator {X : TopCat} {V U : TopologicalSpace.Opens ↑X} (h : V ≤ U) : (CategoryTheory.ConcreteCategory.hom ((openHom h).hom.app (Opposite.op V))) (generator V) = (CategoryTheory.ConcreteCategory.hom ((zeroOutsideInt U).obj.map (CategoryTheory.homOfLE h).op)) (generator U)

theorem stalk_zeroOutsideInt_zero_outside {X : TopCat} (V : TopologicalSpace.Opens ↑X) (x : ↑X) (hx : x ∉ V) (a : ↑((TopCat.Presheaf.stalkFunctor AddCommGrpCat x).obj (TopCat.Sheaf.zeroOutsideInt V).obj)) : a = 0

Stalks of zeroOutsideInt V vanish outside V.

theorem isZero_zeroOutsideInt_bot (X : TopCat) : CategoryTheory.Limits.IsZero (TopCat.Sheaf.zeroOutsideInt ⊥)

zeroOutsideInt ⊥ is the zero sheaf (all stalks vanish).

theorem stalk_zeroOutsideInt_eq_zsmul_generator {X : TopCat} (V : TopologicalSpace.Opens ↑X) (x : ↑X) (hx : x ∈ V) (a : ↑((TopCat.Presheaf.stalkFunctor AddCommGrpCat x).obj (TopCat.Sheaf.zeroOutsideInt V).obj)) : ∃ (n : ℤ), a = n • (CategoryTheory.ConcreteCategory.hom ((TopCat.Sheaf.zeroOutsideInt V).presheaf.germ V x hx)) (TopCat.Sheaf.zeroOutsideInt.generator V)

At a point inside the support open, every stalk element of zeroOutsideInt V is an integer multiple of the germ of the distinguished generator over V.

theorem zsmul_generator_injective {X : TopCat} (V : TopologicalSpace.Opens ↑X) (x : ↑X) (hx : x ∈ V) : Function.Injective fun (n : ℤ) => n • (CategoryTheory.ConcreteCategory.hom ((TopCat.Sheaf.zeroOutsideInt V).presheaf.germ V x hx)) (TopCat.Sheaf.zeroOutsideInt.generator V)

The map n ↦ n • gen from ℤ into stalk(zeroOutsideInt V, x) is injective for x ∈ V.