Symmetric powers and pushforward along a left adjoint of sites

Let F : C ⥤ D be left adjoint to G : D ⥤ C, both continuous, and let φ and ψ be compatible morphisms of sheaves of rings along F and G. Mathlib's SheafOfModules.pushforwardPushforwardAdj makes the pushforward along φ left adjoint to the pushforward along ψ. For the inclusion of an open subset U of a topological space, the pushforward along φ is restriction to U.

This file shows that the unit M ⟶ ψ_* φ_* M of this adjunction is compatible with the canonical symmetric-power comparisons Symⁿ (φ_* M) ⟶ φ_* (Symⁿ M) and Symⁿ (ψ_* N) ⟶ ψ_* (Symⁿ N) of the two pushforwards: on sections both sides restrict symmetric tensors along the counit of F ⊣ G. This is the symmetric-power analogue of TauCeti.SheafOfModules.pushforwardPushforwardAdj_unit_app_tensor, and it is what identifies the canonical symmetric-power comparison of a pullback along an open immersion with the inverse of the restriction isomorphism.

Main declaration

• TauCeti.SheafOfModules.pushforwardPushforwardAdj_unit_app_symmetricPower: the unit of the adjunction between pushforwards, evaluated on Symⁿ M, factors through the two symmetric-power comparisons.

References

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

theorem TauCeti.SheafOfModules.pushforwardPushforwardAdj_unit_app_symmetricPower {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} [J.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)] [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {K : CategoryTheory.GrothendieckTopology D} [K.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)] [CategoryTheory.HasWeakSheafify K AddCommGrpCat] [K.WEqualsLocallyBijective AddCommGrpCat] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} [F.IsContinuous J K] [G.IsContinuous K J] (adj : F ⊣ G) {S : CategoryTheory.Sheaf J CommRingCat} {R : CategoryTheory.Sheaf K CommRingCat} (φ : ringCatSheaf S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj (ringCatSheaf R)) (ψ : ringCatSheaf R ⟶ (G.sheafPushforwardContinuous RingCat K J).obj (ringCatSheaf S)) (H₁ : CategoryTheory.Functor.whiskerRight (CategoryTheory.NatTrans.op adj.counit) (ringCatSheaf R).obj = CategoryTheory.CategoryStruct.comp ψ.hom (G.op.whiskerLeft φ.hom)) (H₂ : CategoryTheory.CategoryStruct.comp φ.hom (CategoryTheory.CategoryStruct.comp (F.op.whiskerLeft ψ.hom) (CategoryTheory.Functor.whiskerRight (CategoryTheory.NatTrans.op adj.unit) (ringCatSheaf S).obj)) = CategoryTheory.CategoryStruct.id (ringCatSheaf S).obj) (n : ℕ) (M : SheafOfModules (ringCatSheaf R)) : (SheafOfModules.pushforwardPushforwardAdj adj φ ψ H₁ H₂).unit.app ((SheafOfModules.symmetricPower R n).obj M) = CategoryTheory.CategoryStruct.comp ((SheafOfModules.symmetricPower R n).map ((SheafOfModules.pushforwardPushforwardAdj adj φ ψ H₁ H₂).unit.app M)) (CategoryTheory.CategoryStruct.comp ((pushforwardSymmetricPowerComparison ψ n).app ((SheafOfModules.pushforward φ).obj M)) ((SheafOfModules.pushforward ψ).map ((pushforwardSymmetricPowerComparison φ n).app M)))

The unit Symⁿ M ⟶ ψ_* φ_* (Symⁿ M) of the adjunction between pushforwards is the symmetric power of the unit of M, followed by the symmetric-power comparisons of ψ_* and of φ_*. On sections over V both sides restrict a symmetric tensor along the counit F (G V) ⟶ V.