Documentation

TauCeti.AlgebraicGeometry.Modules.Pullback.Quasicoherent

Pullback of tensor products with a quasicoherent factor #

For a morphism of schemes f : X ⟶ Y, the canonical comparison f^*(M ⊗ N) ⟶ f^*M ⊗ f^*N, the tensor map of the oplax monoidal pullback, is an isomorphism whenever either factor is quasicoherent (Scheme.Modules.isIso_pullback_δ_of_isQuasicoherent and Scheme.Modules.isIso_pullback_δ_of_isQuasicoherent_right). The target Y is arbitrary and the other factor is an arbitrary sheaf of modules; no flatness or finiteness is assumed.

Pullback along an open immersion j : U ⟶ Y is strong monoidal for all sheaves of modules (Scheme.Modules.isIso_pullback_δ_of_isOpenImmersion), and restriction along j is lax monoidal with invertible tensor map (Scheme.Modules.restrictFunctorLaxMonoidal, Scheme.Modules.isIso_restrictFunctor_μ).

These isomorphisms say that pulling back along f turns tensor products into tensor products as long as one factor is quasicoherent; in particular they apply to line bundles. This is what makes pullback of line-bundle classes multiplicative (LineBundleClass.pullback_mul), so that every morphism of schemes induces a homomorphism of Picard groups Pic(Y) →* Pic(X) (LineBundleClass.pullbackHom), as the Picard functor T ↦ Pic(X_T) requires.

References #

source
noncomputable def AlgebraicGeometry.Scheme.Modules.restrictRingCatSheafHom {U Y : Scheme} (j : U ⟶ Y) [IsOpenImmersion j] :
U.ringCatSheaf ⟶ ((Hom.opensFunctor j).sheafPushforwardContinuous RingCat (Opens.grothendieckTopology ↥U) (Opens.grothendieckTopology ↥Y)).obj Y.ringCatSheaf

The morphism of sheaves of rings along j.opensFunctor, given on sections by the inverses of the isomorphisms Scheme.Hom.appIso, along which Scheme.Modules.restrictFunctor j is the pushforward of sheaves of modules.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[instance_reducible]
    noncomputable instance AlgebraicGeometry.Scheme.Modules.restrictFunctorLaxMonoidal {U Y : Scheme} (j : U ⟶ Y) [IsOpenImmersion j] :
    (restrictFunctor j).LaxMonoidal

    Restriction of modules along an open immersion j is lax monoidal, as the pushforward of sheaves of modules along the functor of opens j.opensFunctor (TauCeti.SheafOfModules.pushforwardLaxMonoidal).

    Equations
    source
    theorem AlgebraicGeometry.Scheme.Modules.restrictAdjunction_unit_app_tensor {U Y : Scheme} (j : U ⟶ Y) [IsOpenImmersion j] (M N : Y.Modules) :
    (restrictAdjunction j).unit.app (CategoryTheory.MonoidalCategoryStruct.tensorObj M N) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom ((restrictAdjunction j).unit.app M) ((restrictAdjunction j).unit.app N)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ (pushforward j) ((restrictFunctor j).obj M) ((restrictFunctor j).obj N)) ((pushforward j).map (CategoryTheory.Functor.LaxMonoidal.μ (restrictFunctor j) M N)))

    The unit M ⟶ j_* (M|_U) of the restriction--pushforward adjunction along an open immersion is compatible with the tensor maps of restriction and pushforward.

    source
    theorem AlgebraicGeometry.Scheme.Modules.restrictAdjunction_counit_app_tensor {U Y : Scheme} (j : U ⟶ Y) [IsOpenImmersion j] (A B : U.Modules) :
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ (restrictFunctor j) ((pushforward j).obj A) ((pushforward j).obj B)) (CategoryTheory.CategoryStruct.comp ((restrictFunctor j).map (CategoryTheory.Functor.LaxMonoidal.μ (pushforward j) A B)) ((restrictAdjunction j).counit.app (CategoryTheory.MonoidalCategoryStruct.tensorObj A B))) = CategoryTheory.MonoidalCategoryStruct.tensorHom ((restrictAdjunction j).counit.app A) ((restrictAdjunction j).counit.app B)

    The counit (j_* A)|_U ⟶ A of the restriction--pushforward adjunction along an open immersion is compatible with the tensor maps of restriction and pushforward.

    source
    instance AlgebraicGeometry.Scheme.Modules.isIso_restrictFunctor_μ {U Y : Scheme} (j : U ⟶ Y) [IsOpenImmersion j] (M N : Y.Modules) :
    CategoryTheory.IsIso (CategoryTheory.Functor.LaxMonoidal.μ (restrictFunctor j) M N)

    Restriction of modules along an open immersion commutes with tensor products: its tensor map M|_U ⊗ N|_U ⟶ (M ⊗ N)|_U is an isomorphism.

    source
    instance AlgebraicGeometry.Scheme.Modules.isIso_pullback_δ_of_isOpenImmersion {U Y : Scheme} (j : U ⟶ Y) [IsOpenImmersion j] (M N : Y.Modules) :
    CategoryTheory.IsIso (CategoryTheory.Functor.OplaxMonoidal.δ (pullback j) M N)

    Pullback along an open immersion is strong monoidal: the tensor comparison j^*(M ⊗ N) ⟶ j^*M ⊗ j^*N is an isomorphism for all sheaves of modules M and N.

    source
    instance AlgebraicGeometry.Scheme.Modules.isIso_pullback_δ_of_isQuasicoherent {X Y : Scheme} (f : X ⟶ Y) (M N : Y.Modules) [SheafOfModules.IsQuasicoherent M] :
    CategoryTheory.IsIso (CategoryTheory.Functor.OplaxMonoidal.δ (pullback f) M N)

    Pullback preserves tensor products with a quasicoherent left factor: for every morphism of schemes f : X ⟶ Y, the tensor comparison f^*(M ⊗ N) ⟶ f^*M ⊗ f^*N is an isomorphism when M is quasicoherent. The right factor need not be quasicoherent.

    source
    instance AlgebraicGeometry.Scheme.Modules.isIso_pullback_δ_of_isQuasicoherent_right {X Y : Scheme} (f : X ⟶ Y) (M N : Y.Modules) [SheafOfModules.IsQuasicoherent N] :
    CategoryTheory.IsIso (CategoryTheory.Functor.OplaxMonoidal.δ (pullback f) M N)

    Pullback preserves tensor products with a quasicoherent right factor: for every morphism of schemes f : X ⟶ Y, the tensor comparison f^*(M ⊗ N) ⟶ f^*M ⊗ f^*N is an isomorphism when N is quasicoherent. The left factor need not be quasicoherent.