Coherence of symmetric powers under pullback

The canonical symmetric-power comparison f^* (Symⁿ M) ⟶ Symⁿ (f^* M) respects the identity and composition isomorphisms of module pullback. These equations concern the actual mate of the pushforward comparison, not a separately chosen isomorphism, and require no quasicoherence or finiteness hypotheses.

The pushforward equations are checked on sheafified sectionwise symmetric tensors; the pullback equations then follow from Mathlib's conjugacy of the canonical pullback and pushforward comparisons by CategoryTheory.Adjunction.app_comp_map_hom_app_of_mateEquiv and CategoryTheory.Adjunction.app_comp_map_inv_app_of_mateEquiv, exactly as for exterior powers in TauCeti.AlgebraicGeometry.Modules.ExteriorPower.Pullback.Coherence.

Main results

• TauCeti.AlgebraicGeometry.pushforwardSymmetricPowerComparison_id and TauCeti.AlgebraicGeometry.pushforwardSymmetricPowerComparison_comp: the corresponding equations for the comparison Symⁿ (f_* M) ⟶ f_* (Symⁿ M) of pushforward;
• TauCeti.AlgebraicGeometry.pullbackSymmetricPowerComparison_id: along 𝟙 X the comparison is induced by Scheme.Modules.pullbackId;
• TauCeti.AlgebraicGeometry.pullbackSymmetricPowerComparison_comp: along f ≫ g the comparison is the composite of the comparisons along g and f, through Scheme.Modules.pullbackComp.

References

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

theorem TauCeti.AlgebraicGeometry.pushforwardSymmetricPowerComparison_id {X : AlgebraicGeometry.Scheme} (n : ℕ) (M : X.Modules) : CategoryTheory.CategoryStruct.comp ((SheafOfModules.pushforwardSymmetricPowerComparison (AlgebraicGeometry.Scheme.Hom.toRingCatSheafHom (CategoryTheory.CategoryStruct.id X)) n).app M) ((AlgebraicGeometry.Scheme.Modules.pushforwardId X).hom.app ((SheafOfModules.symmetricPower X.sheaf n).obj M)) = (SheafOfModules.symmetricPower X.sheaf n).map ((AlgebraicGeometry.Scheme.Modules.pushforwardId X).hom.app M)

The symmetric-power comparison for identity pushforward agrees with the canonical identification of identity pushforward.

theorem TauCeti.AlgebraicGeometry.pushforwardSymmetricPowerComparison_id_assoc {X : AlgebraicGeometry.Scheme} (n : ℕ) (M : X.Modules) {Z : SheafOfModules (SheafOfModules.ringCatSheaf X.sheaf)} (h : (CategoryTheory.Functor.id X.Modules).obj ((SheafOfModules.symmetricPower X.sheaf n).obj M) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp ((SheafOfModules.pushforwardSymmetricPowerComparison (AlgebraicGeometry.Scheme.Hom.toRingCatSheafHom (CategoryTheory.CategoryStruct.id X)) n).app M) ((AlgebraicGeometry.Scheme.Modules.pushforwardId X).hom.app ((SheafOfModules.symmetricPower X.sheaf n).obj M))) h = CategoryTheory.CategoryStruct.comp ((SheafOfModules.symmetricPower X.sheaf n).map ((AlgebraicGeometry.Scheme.Modules.pushforwardId X).hom.app M)) h

The symmetric-power comparison for identity pushforward agrees with the canonical identification of identity pushforward.

theorem TauCeti.AlgebraicGeometry.pushforwardSymmetricPowerComparison_comp {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) (n : ℕ) (M : X.Modules) : CategoryTheory.CategoryStruct.comp ((SheafOfModules.pushforwardSymmetricPowerComparison (AlgebraicGeometry.Scheme.Hom.toRingCatSheafHom g) n).app ((AlgebraicGeometry.Scheme.Modules.pushforward f).obj M)) (CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.Scheme.Modules.pushforward g).map ((SheafOfModules.pushforwardSymmetricPowerComparison (AlgebraicGeometry.Scheme.Hom.toRingCatSheafHom f) n).app M)) ((AlgebraicGeometry.Scheme.Modules.pushforwardComp f g).hom.app ((SheafOfModules.symmetricPower X.sheaf n).obj M))) = CategoryTheory.CategoryStruct.comp ((SheafOfModules.symmetricPower Z.sheaf n).map ((AlgebraicGeometry.Scheme.Modules.pushforwardComp f g).hom.app M)) ((SheafOfModules.pushforwardSymmetricPowerComparison (AlgebraicGeometry.Scheme.Hom.toRingCatSheafHom (CategoryTheory.CategoryStruct.comp f g)) n).app M)

The symmetric-power comparison for composite pushforward is the composite of the two successive comparisons, through the canonical pushforward composition isomorphism.

theorem TauCeti.AlgebraicGeometry.pushforwardSymmetricPowerComparison_comp_assoc {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) (n : ℕ) (M : X.Modules) {Z✝ : SheafOfModules (SheafOfModules.ringCatSheaf Z.sheaf)} (h : (AlgebraicGeometry.Scheme.Modules.pushforward (CategoryTheory.CategoryStruct.comp f g)).obj ((SheafOfModules.symmetricPower X.sheaf n).obj M) ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp ((SheafOfModules.pushforwardSymmetricPowerComparison (AlgebraicGeometry.Scheme.Hom.toRingCatSheafHom g) n).app ((AlgebraicGeometry.Scheme.Modules.pushforward f).obj M)) (CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.Scheme.Modules.pushforward g).map ((SheafOfModules.pushforwardSymmetricPowerComparison (AlgebraicGeometry.Scheme.Hom.toRingCatSheafHom f) n).app M)) ((AlgebraicGeometry.Scheme.Modules.pushforwardComp f g).hom.app ((SheafOfModules.symmetricPower X.sheaf n).obj M)))) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp ((SheafOfModules.symmetricPower Z.sheaf n).map ((AlgebraicGeometry.Scheme.Modules.pushforwardComp f g).hom.app M)) ((SheafOfModules.pushforwardSymmetricPowerComparison (AlgebraicGeometry.Scheme.Hom.toRingCatSheafHom (CategoryTheory.CategoryStruct.comp f g)) n).app M)) h

The symmetric-power comparison for composite pushforward is the composite of the two successive comparisons, through the canonical pushforward composition isomorphism.

@[simp]

theorem TauCeti.AlgebraicGeometry.pullbackSymmetricPowerComparison_id {X : AlgebraicGeometry.Scheme} (n : ℕ) (M : X.Modules) : CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.Scheme.Modules.pullbackSymmetricPowerComparison (CategoryTheory.CategoryStruct.id X) n).app M) ((SheafOfModules.symmetricPower X.sheaf n).map ((AlgebraicGeometry.Scheme.Modules.pullbackId X).hom.app M)) = (AlgebraicGeometry.Scheme.Modules.pullbackId X).hom.app ((SheafOfModules.symmetricPower X.sheaf n).obj M)

The symmetric-power comparison along the identity is induced by the canonical identity isomorphism of module pullback.

theorem TauCeti.AlgebraicGeometry.pullbackSymmetricPowerComparison_id_assoc {X : AlgebraicGeometry.Scheme} (n : ℕ) (M : X.Modules) {Z : X.Modules} (h : (SheafOfModules.symmetricPower X.sheaf n).obj M ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.Scheme.Modules.pullbackSymmetricPowerComparison (CategoryTheory.CategoryStruct.id X) n).app M) ((SheafOfModules.symmetricPower X.sheaf n).map ((AlgebraicGeometry.Scheme.Modules.pullbackId X).hom.app M))) h = CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.Scheme.Modules.pullbackId X).hom.app ((SheafOfModules.symmetricPower X.sheaf n).obj M)) h

The symmetric-power comparison along the identity is induced by the canonical identity isomorphism of module pullback.

theorem TauCeti.AlgebraicGeometry.pullbackSymmetricPowerComparison_comp {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) (n : ℕ) (M : Z.Modules) : CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.Scheme.Modules.pullbackSymmetricPowerComparison (CategoryTheory.CategoryStruct.comp f g) n).app M) ((SheafOfModules.symmetricPower X.sheaf n).map ((AlgebraicGeometry.Scheme.Modules.pullbackComp f g).inv.app M)) = CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.Scheme.Modules.pullbackComp f g).inv.app ((SheafOfModules.symmetricPower Z.sheaf n).obj M)) (CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.Scheme.Modules.pullback f).map ((AlgebraicGeometry.Scheme.Modules.pullbackSymmetricPowerComparison g n).app M)) ((AlgebraicGeometry.Scheme.Modules.pullbackSymmetricPowerComparison f n).app ((AlgebraicGeometry.Scheme.Modules.pullback g).obj M)))

The symmetric-power comparison for a composite agrees with the two successive comparisons, using the canonical composition isomorphism of module pullback.

theorem TauCeti.AlgebraicGeometry.pullbackSymmetricPowerComparison_comp_assoc {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) (n : ℕ) (M : Z.Modules) {Z✝ : X.Modules} (h : (SheafOfModules.symmetricPower X.sheaf n).obj ((AlgebraicGeometry.Scheme.Modules.pullback f).obj ((AlgebraicGeometry.Scheme.Modules.pullback g).obj M)) ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.Scheme.Modules.pullbackSymmetricPowerComparison (CategoryTheory.CategoryStruct.comp f g) n).app M) ((SheafOfModules.symmetricPower X.sheaf n).map ((AlgebraicGeometry.Scheme.Modules.pullbackComp f g).inv.app M))) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.Scheme.Modules.pullbackComp f g).inv.app ((SheafOfModules.symmetricPower Z.sheaf n).obj M)) (CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.Scheme.Modules.pullback f).map ((AlgebraicGeometry.Scheme.Modules.pullbackSymmetricPowerComparison g n).app M)) ((AlgebraicGeometry.Scheme.Modules.pullbackSymmetricPowerComparison f n).app ((AlgebraicGeometry.Scheme.Modules.pullback g).obj M)))) h

The symmetric-power comparison for a composite agrees with the two successive comparisons, using the canonical composition isomorphism of module pullback.