Documentation

TauCeti.AlgebraicGeometry.Modules.SymmetricPower.Pullback.Basic

Pullback comparison for symmetric powers of modules on schemes #

For a morphism of schemes f : X ⟶ Y, this file specializes the sheaf-theoretic comparison to the canonical natural map f^* (Symⁿ M) ⟶ Symⁿ (f^* M). Its transpose is characterized by the pullback--pushforward adjunction equation. In degree one the comparison is an isomorphism.

The comparison is the input for proving that symmetric powers commute with pullback on quasicoherent modules. That stronger invertibility statement in arbitrary degree requires the affine calculation and descent; it is proved in TauCeti.AlgebraicGeometry.Modules.SymmetricPower.Pullback.Quasicoherent.

Main declaration #

References #

source
noncomputable def AlgebraicGeometry.Scheme.Modules.pullbackSymmetricPowerComparison {X Y : Scheme} (f : X ⟶ Y) (n : ℕ) :
(SheafOfModules.symmetricPower Y.sheaf n).comp (pullback f) ⟶ (pullback f).comp (SheafOfModules.symmetricPower X.sheaf n)

The canonical comparison f^* (Symⁿ M) ⟶ Symⁿ (f^* M) for modules on schemes, obtained from the sheaf comparison along f.toRingCatSheafHom.

Instances For
    source
    theorem AlgebraicGeometry.Scheme.Modules.pullbackSymmetricPowerComparison_eq {X Y : Scheme} (f : X ⟶ Y) (n : ℕ) :
    pullbackSymmetricPowerComparison f n = TauCeti.SheafOfModules.pullbackSymmetricPowerComparison (pullbackPushforwardAdjunction f) n

    The scheme comparison is the sheaf comparison for the scheme pullback adjunction.

    source
    theorem AlgebraicGeometry.Scheme.Modules.mateEquiv_pullbackSymmetricPowerComparison {X Y : Scheme} (f : X ⟶ Y) (n : ℕ) :
    (CategoryTheory.mateEquiv (pullbackPushforwardAdjunction f) (pullbackPushforwardAdjunction f)) (pullbackSymmetricPowerComparison f n) = TauCeti.SheafOfModules.pushforwardSymmetricPowerComparison (Hom.toRingCatSheafHom f) n

    The mate of the scheme comparison under the pullback--pushforward adjunction is the pushforward comparison along f.toRingCatSheafHom.

    source
    theorem AlgebraicGeometry.Scheme.Modules.unit_comp_pushforward_map_pullbackSymmetricPowerComparison_app {X Y : Scheme} (f : X ⟶ Y) (n : ℕ) (M : Y.Modules) :
    CategoryTheory.CategoryStruct.comp ((pullbackPushforwardAdjunction f).unit.app ((SheafOfModules.symmetricPower Y.sheaf n).obj M)) ((pushforward f).map ((pullbackSymmetricPowerComparison f n).app M)) = CategoryTheory.CategoryStruct.comp ((SheafOfModules.symmetricPower Y.sheaf n).map ((pullbackPushforwardAdjunction f).unit.app M)) ((TauCeti.SheafOfModules.pushforwardSymmetricPowerComparison (Hom.toRingCatSheafHom f) n).app ((pullback f).obj M))

    The adjunction equation characterizing the pullback comparison for modules on schemes.

    source
    theorem AlgebraicGeometry.Scheme.Modules.pullbackSymmetricPowerComparison_app_comp_symmetricPowerOneIso {X Y : Scheme} (f : X ⟶ Y) (M : Y.Modules) :
    CategoryTheory.CategoryStruct.comp ((pullbackSymmetricPowerComparison f 1).app M) ((SheafOfModules.symmetricPowerOneIso X.sheaf).hom.app ((pullback f).obj M)) = (pullback f).map ((SheafOfModules.symmetricPowerOneIso Y.sheaf).hom.app M)

    In degree one, the pullback comparison is the identity of f^* M, read through the identifications Sym¹ M ≅ M.

    source
    instance AlgebraicGeometry.Scheme.Modules.isIso_pullbackSymmetricPowerComparison_one {X Y : Scheme} (f : X ⟶ Y) :
    CategoryTheory.IsIso (pullbackSymmetricPowerComparison f 1)

    The pullback comparison for modules on schemes is an isomorphism in degree one.