Extension by zero on a lower interval

For a preordered set P and U : P, a presheaf on Over U with values in a category with a zero object extends to P by assigning zero outside the lower interval of U. This extension preserves finite limits and colimits and is left adjoint to restriction. For the open subsets of a space, sheafifying this construction gives extension by zero along an open inclusion.

The sheaf exactness instance supports the comparison of cohomology on an open with cohomology of the restricted sheaf in TauCeti.CategoryTheory.Sites.SheafCohomology.Over.

Main declarations

• TauCeti.CategoryTheory.PresheafExtensionByZero.functor: extension by zero of presheaves.
• TauCeti.CategoryTheory.PresheafExtensionByZero.adjunction: its adjunction to restriction.
• TauCeti.CategoryTheory.SheafExtensionByZero.preservesFiniteLimits_sheafPullback: left exactness of Mathlib's canonical extension functor for abelian sheaves.

References

• R. Hartshorne, Algebraic Geometry, II, Exercise 1.19.

noncomputable def TauCeti.CategoryTheory.PresheafExtensionByZero.functor {P : Type u} [Preorder P] (U : P) {D : Type v} [CategoryTheory.Category.{w, v} D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasZeroMorphisms D] : CategoryTheory.Functor (CategoryTheory.Functor (CategoryTheory.Over U)ᵒᵖ D) (CategoryTheory.Functor Pᵒᵖ D)

Extension by zero as a functor between categories of presheaves.

Equations

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

noncomputable def TauCeti.CategoryTheory.PresheafExtensionByZero.evaluationIso {P : Type u} [Preorder P] (U : P) {D : Type v} [CategoryTheory.Category.{w, v} D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasZeroMorphisms D] {V : P} (h : V ≤ U) : (functor U).comp ((CategoryTheory.evaluation Pᵒᵖ D).obj (Opposite.op V)) ≅ (CategoryTheory.evaluation (CategoryTheory.Over U)ᵒᵖ D).obj (Opposite.op (CategoryTheory.Over.mk (CategoryTheory.homOfLE h)))

Evaluating the extension below U is naturally isomorphic to evaluating the original presheaf.

Equations

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

theorem TauCeti.CategoryTheory.PresheafExtensionByZero.map_comp_evaluationIso_hom_app {P : Type u} [Preorder P] (U : P) {D : Type v} [CategoryTheory.Category.{w, v} D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasZeroMorphisms D] (F : CategoryTheory.Functor (CategoryTheory.Over U)ᵒᵖ D) {V W : P} (hWV : W ≤ V) (hV : V ≤ U) : CategoryTheory.CategoryStruct.comp (((functor U).obj F).map (CategoryTheory.homOfLE hWV).op) ((evaluationIso U ⋯).hom.app F) = CategoryTheory.CategoryStruct.comp ((evaluationIso U hV).hom.app F) (F.map (CategoryTheory.Over.homMk (CategoryTheory.homOfLE hWV) ⋯).op)

The identification evaluationIso is compatible with restriction maps below U.

theorem TauCeti.CategoryTheory.PresheafExtensionByZero.map_comp_evaluationIso_hom_app_assoc {P : Type u} [Preorder P] (U : P) {D : Type v} [CategoryTheory.Category.{w, v} D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasZeroMorphisms D] (F : CategoryTheory.Functor (CategoryTheory.Over U)ᵒᵖ D) {V W : P} (hWV : W ≤ V) (hV : V ≤ U) {Z : D} (h : ((CategoryTheory.evaluation (CategoryTheory.Over U)ᵒᵖ D).obj (Opposite.op (CategoryTheory.Over.mk (CategoryTheory.homOfLE ⋯)))).obj F ⟶ Z) : CategoryTheory.CategoryStruct.comp (((functor U).obj F).map (CategoryTheory.homOfLE hWV).op) (CategoryTheory.CategoryStruct.comp ((evaluationIso U ⋯).hom.app F) h) = CategoryTheory.CategoryStruct.comp ((evaluationIso U hV).hom.app F) (CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.Over.homMk (CategoryTheory.homOfLE hWV) ⋯).op) h)

The identification evaluationIso is compatible with restriction maps below U.

theorem TauCeti.CategoryTheory.PresheafExtensionByZero.isZero_obj_of_not_le {P : Type u} [Preorder P] (U : P) {D : Type v} [CategoryTheory.Category.{w, v} D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasZeroMorphisms D] (F : CategoryTheory.Functor (CategoryTheory.Over U)ᵒᵖ D) {V : P} (h : ¬V ≤ U) : CategoryTheory.Limits.IsZero (((functor U).obj F).obj (Opposite.op V))

Extension by zero vanishes outside the lower interval.

instance TauCeti.CategoryTheory.PresheafExtensionByZero.instPreservesFiniteLimitsFunctorOppositeOverFunctorOfHasFiniteLimits {P : Type u} [Preorder P] (U : P) {D : Type v} [CategoryTheory.Category.{w, v} D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasZeroMorphisms D] [CategoryTheory.Limits.HasFiniteLimits D] : CategoryTheory.Limits.PreservesFiniteLimits (functor U)

Extension by zero preserves finite limits.

instance TauCeti.CategoryTheory.PresheafExtensionByZero.instPreservesFiniteColimitsFunctorOppositeOverFunctorOfHasFiniteColimits {P : Type u} [Preorder P] (U : P) {D : Type v} [CategoryTheory.Category.{w, v} D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasZeroMorphisms D] [CategoryTheory.Limits.HasFiniteColimits D] : CategoryTheory.Limits.PreservesFiniteColimits (functor U)

Extension by zero preserves finite colimits.

noncomputable def TauCeti.CategoryTheory.PresheafExtensionByZero.adjunction {P : Type u} [Preorder P] (U : P) {D : Type v} [CategoryTheory.Category.{w, v} D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasZeroMorphisms D] : functor U ⊣ (CategoryTheory.Functor.whiskeringLeft (CategoryTheory.Over U)ᵒᵖ Pᵒᵖ D).obj (CategoryTheory.Over.forget U).op

Extension by zero is left adjoint to restriction to the lower interval.

Equations

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

instance TauCeti.CategoryTheory.SheafExtensionByZero.preservesFiniteLimits_sheafPullback {P : Type u} [Preorder P] (U : P) (J : CategoryTheory.GrothendieckTopology P) [CategoryTheory.HasSheafify J AddCommGrpCat] : CategoryTheory.Limits.PreservesFiniteLimits ((CategoryTheory.Over.forget U).sheafPullback AddCommGrpCat (J.over U) J)

On a preorder site, the left adjoint to restriction to a lower interval is exact. In particular, this applies to extension by zero along an open inclusion.