Pullback of constant sheaves

Let u : C ⥤ D be a continuous functor from a site (C, J) to a site (D, K), whose sheaf pushforward u_* : Sheaf K A ⥤ Sheaf J A has the left adjoint u^* = u.sheafPullback A J K. For every X : A there is a canonical comparison u^* (X_J) ⟶ X_K between the pullback of the constant sheaf on (C, J) and the constant sheaf on (D, K): it is adjoint to the map of presheaves X ⟶ (X_K)(u -) induced by sheafification.

When u is final, which holds for instance when u is representably flat (CategoryTheory.Functor.final_of_representablyFlat), so in particular for a morphism of sites, this comparison is an isomorphism: maps out of either side into a sheaf F on (D, K) are cones with apex X over F, restricted along u in the first case.

Main declarations

• CategoryTheory.Functor.sheafPullbackConstantSheafHom: the comparison u^* (X_J) ⟶ X_K.
• CategoryTheory.Functor.sheafPullbackConstantSheafHom_naturality: the comparison is natural in X.
• CategoryTheory.Functor.sheafPullbackConstantSheafIso: the comparison as an isomorphism, for u final.
• CategoryTheory.Functor.whiskerLeft_toSheafify_comp_sheafPullbackConstantSheafIso_inv: the inverse comparison X_K ⟶ u^* (X_J), read on sections over objects u(U), is the unit of the adjunction u^* ⊣ u_* on the constant section X ⟶ X_J(U).

noncomputable def CategoryTheory.Functor.sheafPullbackConstantSheafHom {C : Type u_1} [Category.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, u_2} D] (u : Functor C D) (A : Type u_3) [Category.{v_3, u_3} A] (J : GrothendieckTopology C) (K : GrothendieckTopology D) [u.IsContinuous J K] [(u.sheafPushforwardContinuous A J K).IsRightAdjoint] [HasWeakSheafify J A] [HasWeakSheafify K A] (X : A) : (u.sheafPullback A J K).obj ((presheafToSheaf J A).obj ((const Cᵒᵖ).obj X)) ⟶ (presheafToSheaf K A).obj ((const Dᵒᵖ).obj X)

The canonical comparison u^* (X_J) ⟶ X_K from the pullback of the constant sheaf with value X on (C, J) to the constant sheaf with value X on (D, K), both written as sheafifications of constant presheaves (Mathlib's constantSheaf is by definition this sheafification). It is adjoint, for the composite of sheafification and u^* ⊣ u_*, to the map of presheaves X ⟶ (X_K)(u -) given by the canonical map to the sheafification.

theorem CategoryTheory.Functor.homEquiv_sheafPullbackConstantSheafHom_comp {C : Type u_1} [Category.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, u_2} D] (u : Functor C D) (A : Type u_3) [Category.{v_3, u_3} A] (J : GrothendieckTopology C) (K : GrothendieckTopology D) [u.IsContinuous J K] [(u.sheafPushforwardContinuous A J K).IsRightAdjoint] [HasWeakSheafify J A] [HasWeakSheafify K A] (X : A) {F : Sheaf K A} (g : (presheafToSheaf K A).obj ((const Dᵒᵖ).obj X) ⟶ F) : (((sheafificationAdjunction J A).comp (u.sheafAdjunctionContinuous A J K)).homEquiv ((const Cᵒᵖ).obj X) F) (CategoryStruct.comp (u.sheafPullbackConstantSheafHom A J K X) g) = u.op.whiskerLeft (((sheafificationAdjunction K A).homEquiv ((const Dᵒᵖ).obj X) F) g)

Maps out of X_K and out of u^* (X_J) into a sheaf F on (D, K) correspond to cones with apex X over F and over F(u -) respectively; precomposition with sheafPullbackConstantSheafHom is restriction of cones along u.

@[simp]

theorem CategoryTheory.Functor.sheafPullbackConstantSheafHom_naturality {C : Type u_1} [Category.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, u_2} D] (u : Functor C D) (A : Type u_3) [Category.{v_3, u_3} A] (J : GrothendieckTopology C) (K : GrothendieckTopology D) [u.IsContinuous J K] [(u.sheafPushforwardContinuous A J K).IsRightAdjoint] [HasWeakSheafify J A] [HasWeakSheafify K A] {X Y : A} (f : X ⟶ Y) : CategoryStruct.comp ((u.sheafPullback A J K).map ((presheafToSheaf J A).map ((const Cᵒᵖ).map f))) (u.sheafPullbackConstantSheafHom A J K Y) = CategoryStruct.comp (u.sheafPullbackConstantSheafHom A J K X) ((presheafToSheaf K A).map ((const Dᵒᵖ).map f))

The comparison u^* (X_J) ⟶ X_K is natural in X.

@[simp]

theorem CategoryTheory.Functor.sheafPullbackConstantSheafHom_naturality_assoc {C : Type u_1} [Category.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, u_2} D] (u : Functor C D) (A : Type u_3) [Category.{v_3, u_3} A] (J : GrothendieckTopology C) (K : GrothendieckTopology D) [u.IsContinuous J K] [(u.sheafPushforwardContinuous A J K).IsRightAdjoint] [HasWeakSheafify J A] [HasWeakSheafify K A] {X Y : A} (f : X ⟶ Y) {Z : Sheaf K A} (h : (presheafToSheaf K A).obj ((const Dᵒᵖ).obj Y) ⟶ Z) : CategoryStruct.comp ((u.sheafPullback A J K).map ((presheafToSheaf J A).map ((const Cᵒᵖ).map f))) (CategoryStruct.comp (u.sheafPullbackConstantSheafHom A J K Y) h) = CategoryStruct.comp (u.sheafPullbackConstantSheafHom A J K X) (CategoryStruct.comp ((presheafToSheaf K A).map ((const Dᵒᵖ).map f)) h)

The comparison u^* (X_J) ⟶ X_K is natural in X.

instance CategoryTheory.Functor.instIsIsoSheafSheafPullbackConstantSheafHomOfFinal {C : Type u_1} [Category.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, u_2} D] (u : Functor C D) (A : Type u_3) [Category.{v_3, u_3} A] (J : GrothendieckTopology C) (K : GrothendieckTopology D) [u.IsContinuous J K] [(u.sheafPushforwardContinuous A J K).IsRightAdjoint] [HasWeakSheafify J A] [HasWeakSheafify K A] [u.Final] (X : A) : IsIso (u.sheafPullbackConstantSheafHom A J K X)

noncomputable def CategoryTheory.Functor.sheafPullbackConstantSheafIso {C : Type u_1} [Category.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, u_2} D] (u : Functor C D) (A : Type u_3) [Category.{v_3, u_3} A] (J : GrothendieckTopology C) (K : GrothendieckTopology D) [u.IsContinuous J K] [(u.sheafPushforwardContinuous A J K).IsRightAdjoint] [HasWeakSheafify J A] [HasWeakSheafify K A] [u.Final] (X : A) : (u.sheafPullback A J K).obj ((constantSheaf J A).obj X) ≅ (constantSheaf K A).obj X

For u final, the pullback of the constant sheaf with value X on (C, J) is the constant sheaf with value X on (D, K), through sheafPullbackConstantSheafHom.

@[simp]

theorem CategoryTheory.Functor.sheafPullbackConstantSheafIso_hom {C : Type u_1} [Category.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, u_2} D] (u : Functor C D) (A : Type u_3) [Category.{v_3, u_3} A] (J : GrothendieckTopology C) (K : GrothendieckTopology D) [u.IsContinuous J K] [(u.sheafPushforwardContinuous A J K).IsRightAdjoint] [HasWeakSheafify J A] [HasWeakSheafify K A] [u.Final] (X : A) : (u.sheafPullbackConstantSheafIso A J K X).hom = u.sheafPullbackConstantSheafHom A J K X

@[simp]

theorem CategoryTheory.Functor.sheafPullbackConstantSheafIso_inv_naturality {C : Type u_1} [Category.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, u_2} D] (u : Functor C D) (A : Type u_3) [Category.{v_3, u_3} A] (J : GrothendieckTopology C) (K : GrothendieckTopology D) [u.IsContinuous J K] [(u.sheafPushforwardContinuous A J K).IsRightAdjoint] [HasWeakSheafify J A] [HasWeakSheafify K A] [u.Final] {X Y : A} (f : X ⟶ Y) : CategoryStruct.comp ((constantSheaf K A).map f) (u.sheafPullbackConstantSheafIso A J K Y).inv = CategoryStruct.comp (u.sheafPullbackConstantSheafIso A J K X).inv ((u.sheafPullback A J K).map ((constantSheaf J A).map f))

For u final, the inverse comparison X_K ⟶ u^* (X_J) is natural in X.

@[simp]

theorem CategoryTheory.Functor.sheafPullbackConstantSheafIso_inv_naturality_assoc {C : Type u_1} [Category.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, u_2} D] (u : Functor C D) (A : Type u_3) [Category.{v_3, u_3} A] (J : GrothendieckTopology C) (K : GrothendieckTopology D) [u.IsContinuous J K] [(u.sheafPushforwardContinuous A J K).IsRightAdjoint] [HasWeakSheafify J A] [HasWeakSheafify K A] [u.Final] {X Y : A} (f : X ⟶ Y) {Z : Sheaf K A} (h : (u.sheafPullback A J K).obj ((constantSheaf J A).obj Y) ⟶ Z) : CategoryStruct.comp ((constantSheaf K A).map f) (CategoryStruct.comp (u.sheafPullbackConstantSheafIso A J K Y).inv h) = CategoryStruct.comp (u.sheafPullbackConstantSheafIso A J K X).inv (CategoryStruct.comp ((u.sheafPullback A J K).map ((constantSheaf J A).map f)) h)

For u final, the inverse comparison X_K ⟶ u^* (X_J) is natural in X.

theorem CategoryTheory.Functor.whiskerLeft_toSheafify_comp_sheafPullbackConstantSheafIso_inv {C : Type u_1} [Category.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, u_2} D] (u : Functor C D) (A : Type u_3) [Category.{v_3, u_3} A] (J : GrothendieckTopology C) (K : GrothendieckTopology D) [u.IsContinuous J K] [(u.sheafPushforwardContinuous A J K).IsRightAdjoint] [HasWeakSheafify J A] [HasWeakSheafify K A] [u.Final] (X : A) : u.op.whiskerLeft (CategoryStruct.comp (toSheafify K ((const Dᵒᵖ).obj X)) (u.sheafPullbackConstantSheafIso A J K X).inv.hom) = CategoryStruct.comp (toSheafify J ((const Cᵒᵖ).obj X)) ((u.sheafAdjunctionContinuous A J K).unit.app ((constantSheaf J A).obj X)).hom

The inverse comparison X_K ⟶ u^* (X_J), restricted to the objects u(U), is the unit of the adjunction u^* ⊣ u_* on the constant sections: on sections over u(U) it sends the constant section to the image of the constant section of X_J over U.