Pullback and restriction of modules on schemes

Mathlib packages pullback of modules along scheme morphisms as a pseudofunctor (AlgebraicGeometry.Scheme.Modules.pseudofunctor), whose coherence conditions are equations of natural transformations. This file records them on components, in the forms used to compare iterated pullbacks of a single module, and shows that pullback preserves the structure sheaf 𝒪 compatibly with identities and composition.

For a scheme morphism f : X ⟶ Y and an open V ⊆ Y, restricting the pullback f^* M to f⁻¹ V agrees with pulling back the restriction M|_V along f ∣_ V. This compatibility lets local properties of modules, expressed on open covers, be transported along scheme morphisms. Being an isomorphism is such a local property: a morphism of modules is an isomorphism exactly when its pullbacks to the members of an open cover are.

Identifying modules on the slice site at an open U with modules on the open subscheme U, and pulling back along an isomorphism of schemes, preserve free modules, so trivializations of a module by free modules can be moved between slices, open subschemes and open immersions.

Pushforward of modules along a scheme morphism is lax symmetric monoidal, so pullback, its left adjoint, is oplax monoidal, with unit map the identification f^* 𝒪_Y ≅ 𝒪_X and tensor comparison compatible with symmetry (pullback_map_braiding_hom_comp_δ). These structures are compatible with composition: the composition isomorphism of pullbacks carries the comparison maps of (f ≫ g)^* to the composites of those of g^* and f^*.

Pullback along any scheme morphism preserves quasi-coherence, finite type, finite presentation and local freeness of modules. Local generators and presentations on an open cover pull back to local data on the preimage cover.

Main declarations

• AlgebraicGeometry.Scheme.Modules.pseudofunctor_associativity_app, AlgebraicGeometry.Scheme.Modules.pseudofunctor_left_unitality_app and AlgebraicGeometry.Scheme.Modules.pseudofunctor_right_unitality_app: the coherence conditions of the pullback pseudofunctor, on components;
• AlgebraicGeometry.Scheme.Modules.pullbackObjUnitIso: the isomorphism f^* 𝒪_Y ≅ 𝒪_X, with pullbackObjUnitIso_id, pullbackObjUnitIso_comp, and pullbackObjUnitIso_congr comparing it with identity, composition, and equality of scheme morphisms;
• AlgebraicGeometry.Scheme.Modules.pushforwardLaxMonoidal and AlgebraicGeometry.Scheme.Modules.pullbackOplaxMonoidal: the lax monoidal structure of pushforward and the oplax monoidal structure of pullback, with unit maps computed by AlgebraicGeometry.Scheme.Modules.pushforward_ε and AlgebraicGeometry.Scheme.Modules.pullback_η, and the tensor map of pullback by AlgebraicGeometry.Scheme.Modules.pullback_δ;
• AlgebraicGeometry.Scheme.Modules.isMonoidal_pushforwardComp_hom and AlgebraicGeometry.Scheme.Modules.pullback_comp_δ: the composition isomorphisms of pushforward and pullback respect the lax and oplax monoidal structures;
• AlgebraicGeometry.Scheme.Modules.restrictPullbackObjIso identifies these two restricted pullbacks;
• AlgebraicGeometry.Scheme.Modules.isIso_iff_of_isOpenCover: a morphism of modules is an isomorphism exactly when its pullbacks to the members of an open cover are;
• AlgebraicGeometry.Scheme.Modules.pullbackOver: pullback read on the slice sites over V and f⁻¹ V, with pullbackOverUnitIso and pullbackOverObjIso comparing it with the structure sheaves and with the pullback of 𝒪_Y-modules;
• AlgebraicGeometry.Scheme.Modules.overEquivFunctorObjFreeIso: the identification of modules on the slice at an open U with modules on the open subscheme U preserves free modules, so trivializations of a module pass between the slice and the open subscheme (AlgebraicGeometry.Scheme.Modules.restrictIsoFreeOfOverIsoFree, AlgebraicGeometry.Scheme.Modules.overIsoFreeOfRestrictIsoFree), and a trivialization of the pullback along an open immersion f is one of the restriction to f.opensRange (AlgebraicGeometry.Scheme.Modules.restrictOpensRangeIsoFree);
• SheafOfModules.LocalGeneratorsData.pullback and SheafOfModules.QuasicoherentData.pullback: local generators and quasi-coherent data carried along f;
• AlgebraicGeometry.Scheme.Modules.isQuasicoherent_pullback, AlgebraicGeometry.Scheme.Modules.isFiniteType_pullback, AlgebraicGeometry.Scheme.Modules.isFinitePresentation_pullback and AlgebraicGeometry.Scheme.Modules.isLocallyFree_pullback: pullback preserves quasi-coherent, finite type, finitely presented and locally free modules.

References

• The Stacks Project, Sheaves of Modules, sections Quasi-coherent modules, Modules of finite type, Modules of finite presentation and Locally free sheaves.

theorem AlgebraicGeometry.Scheme.Modules.pseudofunctor_associativity_app {X Y Z W : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) (h : Z ⟶ W) (M : W.Modules) : CategoryTheory.CategoryStruct.comp ((pullbackComp f (CategoryTheory.CategoryStruct.comp g h)).inv.app M) (CategoryTheory.CategoryStruct.comp ((pullback f).map ((pullbackComp g h).inv.app M)) (CategoryTheory.CategoryStruct.comp ((pullbackComp f g).hom.app ((pullback h).obj M)) ((pullbackComp (CategoryTheory.CategoryStruct.comp f g) h).hom.app M))) = CategoryTheory.eqToHom ⋯

The associativity condition of the pullback pseudofunctor, on the component at a module.

theorem AlgebraicGeometry.Scheme.Modules.pseudofunctor_associativity_app_assoc {X Y Z W : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) (h : Z ⟶ W) (M : W.Modules) {Z✝ : X.Modules} (h✝ : (pullback (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g) h)).obj M ⟶ Z✝) : CategoryTheory.CategoryStruct.comp ((pullbackComp f (CategoryTheory.CategoryStruct.comp g h)).inv.app M) (CategoryTheory.CategoryStruct.comp ((pullback f).map ((pullbackComp g h).inv.app M)) (CategoryTheory.CategoryStruct.comp ((pullbackComp f g).hom.app ((pullback h).obj M)) (CategoryTheory.CategoryStruct.comp ((pullbackComp (CategoryTheory.CategoryStruct.comp f g) h).hom.app M) h✝))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) h✝

The associativity condition of the pullback pseudofunctor, on the component at a module.

theorem AlgebraicGeometry.Scheme.Modules.pseudofunctor_left_unitality_app {X Y : Scheme} (f : X ⟶ Y) (M : Y.Modules) : CategoryTheory.CategoryStruct.comp ((pullbackComp f (CategoryTheory.CategoryStruct.id Y)).inv.app M) ((pullback f).map ((pullbackId Y).hom.app M)) = CategoryTheory.eqToHom ⋯

The left unitality condition of the pullback pseudofunctor, on the component at a module.

theorem AlgebraicGeometry.Scheme.Modules.pseudofunctor_left_unitality_app_assoc {X Y : Scheme} (f : X ⟶ Y) (M : Y.Modules) {Z : X.Modules} (h : (pullback f).obj M ⟶ Z) : CategoryTheory.CategoryStruct.comp ((pullbackComp f (CategoryTheory.CategoryStruct.id Y)).inv.app M) (CategoryTheory.CategoryStruct.comp ((pullback f).map ((pullbackId Y).hom.app M)) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) h

The left unitality condition of the pullback pseudofunctor, on the component at a module.

theorem AlgebraicGeometry.Scheme.Modules.pseudofunctor_right_unitality_app {X Y : Scheme} (f : X ⟶ Y) (M : Y.Modules) : CategoryTheory.CategoryStruct.comp ((pullbackComp (CategoryTheory.CategoryStruct.id X) f).inv.app M) ((pullbackId X).hom.app ((pullback f).obj M)) = CategoryTheory.eqToHom ⋯

The right unitality condition of the pullback pseudofunctor, on the component at a module.

theorem AlgebraicGeometry.Scheme.Modules.pseudofunctor_right_unitality_app_assoc {X Y : Scheme} (f : X ⟶ Y) (M : Y.Modules) {Z : X.Modules} (h : (pullback f).obj M ⟶ Z) : CategoryTheory.CategoryStruct.comp ((pullbackComp (CategoryTheory.CategoryStruct.id X) f).inv.app M) (CategoryTheory.CategoryStruct.comp ((pullbackId X).hom.app ((pullback f).obj M)) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) h

The right unitality condition of the pullback pseudofunctor, on the component at a module.

theorem AlgebraicGeometry.Scheme.Modules.pullback_map_pullbackComp_hom_app_comp_pullbackComp_hom_app {X Y Z W : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) (h : Z ⟶ W) (M : W.Modules) : CategoryTheory.CategoryStruct.comp ((pullback f).map ((pullbackComp g h).hom.app M)) ((pullbackComp f (CategoryTheory.CategoryStruct.comp g h)).hom.app M) = CategoryTheory.CategoryStruct.comp ((pullbackComp f g).hom.app ((pullback h).obj M)) (CategoryTheory.CategoryStruct.comp ((pullbackComp (CategoryTheory.CategoryStruct.comp f g) h).hom.app M) (CategoryTheory.eqToHom ⋯))

The two ways of identifying f^* g^* h^* M with (f ≫ g ≫ h)^* M agree.

theorem AlgebraicGeometry.Scheme.Modules.pullback_map_pullbackComp_hom_app_comp_pullbackComp_hom_app_assoc {X Y Z W : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) (h : Z ⟶ W) (M : W.Modules) {Z✝ : X.Modules} (h✝ : (pullback (CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g h))).obj M ⟶ Z✝) : CategoryTheory.CategoryStruct.comp ((pullback f).map ((pullbackComp g h).hom.app M)) (CategoryTheory.CategoryStruct.comp ((pullbackComp f (CategoryTheory.CategoryStruct.comp g h)).hom.app M) h✝) = CategoryTheory.CategoryStruct.comp ((pullbackComp f g).hom.app ((pullback h).obj M)) (CategoryTheory.CategoryStruct.comp ((pullbackComp (CategoryTheory.CategoryStruct.comp f g) h).hom.app M) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) h✝))

The two ways of identifying f^* g^* h^* M with (f ≫ g ≫ h)^* M agree.

theorem AlgebraicGeometry.Scheme.Modules.pullbackComp_inv_app_comp_pullback_map_pullbackComp_hom_app {X Y Z W : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) (h : Z ⟶ W) (M : W.Modules) : CategoryTheory.CategoryStruct.comp ((pullbackComp f g).inv.app ((pullback h).obj M)) ((pullback f).map ((pullbackComp g h).hom.app M)) = CategoryTheory.CategoryStruct.comp ((pullbackComp (CategoryTheory.CategoryStruct.comp f g) h).hom.app M) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) ((pullbackComp f (CategoryTheory.CategoryStruct.comp g h)).inv.app M))

Associativity of pullback, rearranged to pass from (f ≫ g)^* h^* M to f^* (g ≫ h)^* M.

theorem AlgebraicGeometry.Scheme.Modules.pullbackComp_inv_app_comp_pullback_map_pullbackComp_hom_app_assoc {X Y Z W : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) (h : Z ⟶ W) (M : W.Modules) {Z✝ : X.Modules} (h✝ : (pullback f).obj ((pullback (CategoryTheory.CategoryStruct.comp g h)).obj M) ⟶ Z✝) : CategoryTheory.CategoryStruct.comp ((pullbackComp f g).inv.app ((pullback h).obj M)) (CategoryTheory.CategoryStruct.comp ((pullback f).map ((pullbackComp g h).hom.app M)) h✝) = CategoryTheory.CategoryStruct.comp ((pullbackComp (CategoryTheory.CategoryStruct.comp f g) h).hom.app M) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp ((pullbackComp f (CategoryTheory.CategoryStruct.comp g h)).inv.app M) h✝))

Associativity of pullback, rearranged to pass from (f ≫ g)^* h^* M to f^* (g ≫ h)^* M.

theorem AlgebraicGeometry.Scheme.Modules.pullbackComp_inv_app_comp_pullback_map_pullbackComp_inv_app {X Y Z W : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) (h : Z ⟶ W) (M : W.Modules) : CategoryTheory.CategoryStruct.comp ((pullbackComp f (CategoryTheory.CategoryStruct.comp g h)).inv.app M) ((pullback f).map ((pullbackComp g h).inv.app M)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp ((pullbackComp (CategoryTheory.CategoryStruct.comp f g) h).inv.app M) ((pullbackComp f g).inv.app ((pullback h).obj M)))

Associativity of pullback, rearranged to pass from (f ≫ g ≫ h)^* M to f^* g^* h^* M through (f ≫ g)^* h^* M.

theorem AlgebraicGeometry.Scheme.Modules.pullbackComp_inv_app_comp_pullback_map_pullbackComp_inv_app_assoc {X Y Z W : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) (h : Z ⟶ W) (M : W.Modules) {Z✝ : X.Modules} (h✝ : (pullback f).obj ((pullback g).obj ((pullback h).obj M)) ⟶ Z✝) : CategoryTheory.CategoryStruct.comp ((pullbackComp f (CategoryTheory.CategoryStruct.comp g h)).inv.app M) (CategoryTheory.CategoryStruct.comp ((pullback f).map ((pullbackComp g h).inv.app M)) h✝) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp ((pullbackComp (CategoryTheory.CategoryStruct.comp f g) h).inv.app M) (CategoryTheory.CategoryStruct.comp ((pullbackComp f g).inv.app ((pullback h).obj M)) h✝))

Associativity of pullback, rearranged to pass from (f ≫ g ≫ h)^* M to f^* g^* h^* M through (f ≫ g)^* h^* M.

theorem AlgebraicGeometry.Scheme.Modules.pullbackCongr_hom_app_comp_pullbackComp_hom_app {X Y Z : Scheme} {a b : X ⟶ Y} (p : a = b) (f : Y ⟶ Z) (M : Z.Modules) : CategoryTheory.CategoryStruct.comp ((pullbackCongr p).hom.app ((pullback f).obj M)) ((pullbackComp b f).hom.app M) = CategoryTheory.CategoryStruct.comp ((pullbackComp a f).hom.app M) (CategoryTheory.eqToHom ⋯)

The composition isomorphism of pullback is compatible with replacing the first morphism by an equal one.

theorem AlgebraicGeometry.Scheme.Modules.pullbackCongr_hom_app_comp_pullbackComp_hom_app_assoc {X Y Z : Scheme} {a b : X ⟶ Y} (p : a = b) (f : Y ⟶ Z) (M : Z.Modules) {Z✝ : X.Modules} (h : (pullback (CategoryTheory.CategoryStruct.comp b f)).obj M ⟶ Z✝) : CategoryTheory.CategoryStruct.comp ((pullbackCongr p).hom.app ((pullback f).obj M)) (CategoryTheory.CategoryStruct.comp ((pullbackComp b f).hom.app M) h) = CategoryTheory.CategoryStruct.comp ((pullbackComp a f).hom.app M) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) h)

The composition isomorphism of pullback is compatible with replacing the first morphism by an equal one.

theorem AlgebraicGeometry.Scheme.Modules.pullbackComp_inv_app_comp_pullback_map_pullbackCongr_hom_app {X Y Z : Scheme} (f : X ⟶ Y) {a b : Y ⟶ Z} (p : a = b) (M : Z.Modules) : CategoryTheory.CategoryStruct.comp ((pullbackComp f a).inv.app M) ((pullback f).map ((pullbackCongr p).hom.app M)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) ((pullbackComp f b).inv.app M)

The composition isomorphism of pullback is compatible with replacing the second morphism by an equal one.

theorem AlgebraicGeometry.Scheme.Modules.pullbackComp_inv_app_comp_pullback_map_pullbackCongr_hom_app_assoc {X Y Z : Scheme} (f : X ⟶ Y) {a b : Y ⟶ Z} (p : a = b) (M : Z.Modules) {Z✝ : X.Modules} (h : (pullback f).obj ((pullback b).obj M) ⟶ Z✝) : CategoryTheory.CategoryStruct.comp ((pullbackComp f a).inv.app M) (CategoryTheory.CategoryStruct.comp ((pullback f).map ((pullbackCongr p).hom.app M)) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp ((pullbackComp f b).inv.app M) h)

The composition isomorphism of pullback is compatible with replacing the second morphism by an equal one.

noncomputable def AlgebraicGeometry.Scheme.Modules.pullbackObjUnitIso {X Y : Scheme} (f : X ⟶ Y) : (pullback f).obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit Y.Modules) ≅ CategoryTheory.MonoidalCategoryStruct.tensorUnit X.Modules

Pullback along a morphism of schemes preserves the structure sheaf: f^* 𝒪_Y ≅ 𝒪_X, the isomorphism being Mathlib's comparison SheafOfModules.pullbackObjUnitToUnit.

Equations

• AlgebraicGeometry.Scheme.Modules.pullbackObjUnitIso f = CategoryTheory.asIso (SheafOfModules.pullbackObjUnitToUnit (AlgebraicGeometry.Scheme.Hom.toRingCatSheafHom f))

@[simp]

theorem AlgebraicGeometry.Scheme.Modules.pullbackObjUnitIso_hom {X Y : Scheme} (f : X ⟶ Y) : (pullbackObjUnitIso f).hom = SheafOfModules.pullbackObjUnitToUnit (Hom.toRingCatSheafHom f)

The hom of pullbackObjUnitIso is Mathlib's structure sheaf comparison map.

theorem AlgebraicGeometry.Scheme.Modules.pullbackPushforwardAdjunction_homEquiv_pullbackObjUnitIso_hom {X Y : Scheme} (f : X ⟶ Y) : ((pullbackPushforwardAdjunction f).homEquiv (CategoryTheory.MonoidalCategoryStruct.tensorUnit Y.Modules) (CategoryTheory.MonoidalCategoryStruct.tensorUnit X.Modules)) (pullbackObjUnitIso f).hom = SheafOfModules.unitToPushforwardObjUnit (Hom.toRingCatSheafHom f)

The transpose of f^* 𝒪_Y ≅ 𝒪_X is the map 𝒪_Y ⟶ f_* 𝒪_X given by f on sections.

theorem AlgebraicGeometry.Scheme.Modules.unitToPushforwardObjUnit_comp {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (SheafOfModules.unitToPushforwardObjUnit (Hom.toRingCatSheafHom g)) (CategoryTheory.CategoryStruct.comp ((pushforward g).map (SheafOfModules.unitToPushforwardObjUnit (Hom.toRingCatSheafHom f))) ((pushforwardComp f g).hom.app (SheafOfModules.unit X.ringCatSheaf))) = SheafOfModules.unitToPushforwardObjUnit (Hom.toRingCatSheafHom (CategoryTheory.CategoryStruct.comp f g))

The map 𝒪_Z ⟶ (f ≫ g)_* 𝒪_X given by f ≫ g on sections is the composite of the maps given by g and by f.

theorem AlgebraicGeometry.Scheme.Modules.pullbackObjUnitIso_id (X : Scheme) : (pullbackObjUnitIso (CategoryTheory.CategoryStruct.id X)).hom = (pullbackId X).hom.app (CategoryTheory.MonoidalCategoryStruct.tensorUnit X.Modules)

Along the identity, 𝟙^* 𝒪_X ≅ 𝒪_X is the identity isomorphism of pullback.

theorem AlgebraicGeometry.Scheme.Modules.pullbackObjUnitIso_comp {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp ((pullbackComp f g).inv.app (CategoryTheory.MonoidalCategoryStruct.tensorUnit Z.Modules)) (CategoryTheory.CategoryStruct.comp ((pullback f).map (pullbackObjUnitIso g).hom) (pullbackObjUnitIso f).hom) = (pullbackObjUnitIso (CategoryTheory.CategoryStruct.comp f g)).hom

The isomorphism (f ≫ g)^* 𝒪_Z ≅ 𝒪_X is the composite of f^* (g^* 𝒪_Z ≅ 𝒪_Y) and f^* 𝒪_Y ≅ 𝒪_X, through the composition isomorphism of pullback.

theorem AlgebraicGeometry.Scheme.Modules.pullbackObjUnitIso_comp_assoc {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) {Z✝ : X.Modules} (h : CategoryTheory.MonoidalCategoryStruct.tensorUnit X.Modules ⟶ Z✝) : CategoryTheory.CategoryStruct.comp ((pullbackComp f g).inv.app (CategoryTheory.MonoidalCategoryStruct.tensorUnit Z.Modules)) (CategoryTheory.CategoryStruct.comp ((pullback f).map (pullbackObjUnitIso g).hom) (CategoryTheory.CategoryStruct.comp (pullbackObjUnitIso f).hom h)) = CategoryTheory.CategoryStruct.comp (pullbackObjUnitIso (CategoryTheory.CategoryStruct.comp f g)).hom h

The isomorphism (f ≫ g)^* 𝒪_Z ≅ 𝒪_X is the composite of f^* (g^* 𝒪_Z ≅ 𝒪_Y) and f^* 𝒪_Y ≅ 𝒪_X, through the composition isomorphism of pullback.

theorem AlgebraicGeometry.Scheme.Modules.pullbackObjUnitIso_congr {X Y : Scheme} {f g : X ⟶ Y} (hf : f = g) : CategoryTheory.CategoryStruct.comp ((pullbackCongr hf).hom.app (CategoryTheory.MonoidalCategoryStruct.tensorUnit Y.Modules)) (pullbackObjUnitIso g).hom = (pullbackObjUnitIso f).hom

The canonical identification of a pulled-back structure sheaf is unchanged when the scheme morphism is replaced by an equal morphism.

@[instance_reducible]

noncomputable instance AlgebraicGeometry.Scheme.Modules.pushforwardLaxMonoidal {X Y : Scheme} (f : X ⟶ Y) : (pushforward f).LaxMonoidal

Pushforward of modules along a morphism of schemes is lax monoidal (TauCeti.SheafOfModules.pushforwardLaxMonoidal): its tensor map f_* M ⊗ f_* N ⟶ f_* (M ⊗ N) is induced by m ⊗ n ↦ m ⊗ n on sections, and its unit map 𝒪_Y ⟶ f_* 𝒪_X is given by f on sections (pushforward_ε).

Equations

• AlgebraicGeometry.Scheme.Modules.pushforwardLaxMonoidal f = TauCeti.SheafOfModules.pushforwardLaxMonoidal (AlgebraicGeometry.Scheme.Hom.toRingCatSheafHom f)

@[instance_reducible]

noncomputable instance AlgebraicGeometry.Scheme.Modules.pushforwardLaxBraided {X Y : Scheme} (f : X ⟶ Y) : (pushforward f).LaxBraided

Pushforward of modules along a scheme morphism respects the symmetry of tensor products.

Equations

• AlgebraicGeometry.Scheme.Modules.pushforwardLaxBraided f = TauCeti.SheafOfModules.pushforwardLaxBraided (AlgebraicGeometry.Scheme.Hom.toRingCatSheafHom f)

@[simp]

theorem AlgebraicGeometry.Scheme.Modules.pushforward_ε {X Y : Scheme} (f : X ⟶ Y) : CategoryTheory.Functor.LaxMonoidal.ε (pushforward f) = SheafOfModules.unitToPushforwardObjUnit (Hom.toRingCatSheafHom f)

The unit map 𝒪_Y ⟶ f_* 𝒪_X of the pushforward of modules is given by f on sections.

@[instance_reducible]

noncomputable instance AlgebraicGeometry.Scheme.Modules.pullbackOplaxMonoidal {X Y : Scheme} (f : X ⟶ Y) : (pullback f).OplaxMonoidal

Pullback of modules along a morphism of schemes is oplax monoidal, as the left adjoint of the lax monoidal pushforward: it carries comparison maps f^* (M ⊗ N) ⟶ f^* M ⊗ f^* N, and its unit map is pullbackObjUnitIso f (pullback_η). The comparison maps are the mates of the tensor map of pushforward (pullback_δ).

Equations

• AlgebraicGeometry.Scheme.Modules.pullbackOplaxMonoidal f = (AlgebraicGeometry.Scheme.Modules.pullbackPushforwardAdjunction f).leftAdjointOplaxMonoidal

instance AlgebraicGeometry.Scheme.Modules.isMonoidal_pullbackPushforwardAdjunction {X Y : Scheme} (f : X ⟶ Y) : (pullbackPushforwardAdjunction f).IsMonoidal

The pullback--pushforward adjunction of modules along a morphism of schemes is compatible with the oplax monoidal structure of pullback and the lax monoidal structure of pushforward.

@[simp]

theorem AlgebraicGeometry.Scheme.Modules.pullback_η {X Y : Scheme} (f : X ⟶ Y) : CategoryTheory.Functor.OplaxMonoidal.η (pullback f) = (pullbackObjUnitIso f).hom

The unit map f^* 𝒪_Y ⟶ 𝒪_X of the pullback of modules is the isomorphism pullbackObjUnitIso f.

theorem AlgebraicGeometry.Scheme.Modules.pullback_δ {X Y : Scheme} (f : X ⟶ Y) (M N : Y.Modules) : CategoryTheory.Functor.OplaxMonoidal.δ (pullback f) M N = ((pullbackPushforwardAdjunction f).homEquiv (CategoryTheory.MonoidalCategoryStruct.tensorObj ((CategoryTheory.Functor.id Y.Modules).obj M) ((CategoryTheory.Functor.id Y.Modules).obj N)) (CategoryTheory.MonoidalCategoryStruct.tensorObj ((pullback f).obj M) ((pullback f).obj N))).symm (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom ((pullbackPushforwardAdjunction f).unit.app M) ((pullbackPushforwardAdjunction f).unit.app N)) (CategoryTheory.Functor.LaxMonoidal.μ (pushforward f) ((pullback f).obj M) ((pullback f).obj N)))

The tensor map f^* (M ⊗ N) ⟶ f^* M ⊗ f^* N of the pullback of modules is the mate, under the pullback--pushforward adjunction, of the composite of the units M ⟶ f_* f^* M and N ⟶ f_* f^* N with the tensor map f_* f^* M ⊗ f_* f^* N ⟶ f_* (f^* M ⊗ f^* N) of pushforward.

theorem AlgebraicGeometry.Scheme.Modules.pullback_map_braiding_hom_comp_δ {X Y : Scheme} (f : X ⟶ Y) (M N : Y.Modules) : CategoryTheory.CategoryStruct.comp ((pullback f).map (β_ M N).hom) (CategoryTheory.Functor.OplaxMonoidal.δ (pullback f) N M) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OplaxMonoidal.δ (pullback f) M N) (β_ ((pullback f).obj M) ((pullback f).obj N)).hom

The canonical tensor comparison of module pullback respects symmetry, without any flatness, finiteness or quasi-coherence hypothesis.

theorem AlgebraicGeometry.Scheme.Modules.pullback_map_braiding_hom_comp_δ_assoc {X Y : Scheme} (f : X ⟶ Y) (M N : Y.Modules) {Z : X.Modules} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj ((pullback f).obj N) ((pullback f).obj M) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((pullback f).map (β_ M N).hom) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OplaxMonoidal.δ (pullback f) N M) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OplaxMonoidal.δ (pullback f) M N) (CategoryTheory.CategoryStruct.comp (β_ ((pullback f).obj M) ((pullback f).obj N)).hom h)

The canonical tensor comparison of module pullback respects symmetry, without any flatness, finiteness or quasi-coherence hypothesis.

instance AlgebraicGeometry.Scheme.Modules.instIsIsoηPullback_tauCeti {X Y : Scheme} (f : X ⟶ Y) : CategoryTheory.IsIso (CategoryTheory.Functor.OplaxMonoidal.η (pullback f))

instance AlgebraicGeometry.Scheme.Modules.isMonoidal_pushforwardComp_hom {X Y : Scheme} (f : X ⟶ Y) {Z : Scheme} (g : Y ⟶ Z) : CategoryTheory.NatTrans.IsMonoidal (pushforwardComp f g).hom

The identification pushforward f ⋙ pushforward g ≅ pushforward (f ≫ g) is an isomorphism of lax monoidal functors (TauCeti.SheafOfModules.isMonoidal_pushforwardComp_hom).

instance AlgebraicGeometry.Scheme.Modules.isMonoidal_pushforwardCongr_hom {X Y : Scheme} (f : X ⟶ Y) {f' : X ⟶ Y} (h : f = f') : CategoryTheory.NatTrans.IsMonoidal (pushforwardCongr h).hom

The identification pushforward f ≅ pushforward f' for equal morphisms f = f' is an isomorphism of lax monoidal functors.

theorem AlgebraicGeometry.Scheme.Modules.pullback_comp_δ {X Y : Scheme} (f : X ⟶ Y) {Z : Scheme} (g : Y ⟶ Z) (M N : Z.Modules) : CategoryTheory.Functor.OplaxMonoidal.δ (pullback (CategoryTheory.CategoryStruct.comp f g)) M N = CategoryTheory.CategoryStruct.comp ((pullbackComp f g).inv.app (CategoryTheory.MonoidalCategoryStruct.tensorObj M N)) (CategoryTheory.CategoryStruct.comp ((pullback f).map (CategoryTheory.Functor.OplaxMonoidal.δ (pullback g) M N)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OplaxMonoidal.δ (pullback f) ((pullback g).obj M) ((pullback g).obj N)) (CategoryTheory.MonoidalCategoryStruct.tensorHom ((pullbackComp f g).hom.app M) ((pullbackComp f g).hom.app N))))

The tensor map (f ≫ g)^* (M ⊗ N) ⟶ (f ≫ g)^* M ⊗ (f ≫ g)^* N of the pullback along a composite is, through the composition isomorphism pullbackComp f g, the composite f^* g^* (M ⊗ N) ⟶ f^* (g^* M ⊗ g^* N) ⟶ f^* g^* M ⊗ f^* g^* N of the tensor maps of the two pullbacks. With pullbackObjUnitIso_comp for the unit maps, this says that pullbackComp f g is an isomorphism of oplax monoidal functors.

noncomputable def AlgebraicGeometry.Scheme.Modules.restrictPullbackObjIso {X Y : Scheme} (f : X ⟶ Y) (V : Y.Opens) (M : Y.Modules) : ((pullback f).obj M).restrict ((TopologicalSpace.Opens.map f.base).obj V).ι ≅ (pullback (f ∣_ V)).obj (M.restrict V.ι)

Pullback commutes with restriction to opens: for an open V ⊆ Y, the restriction of f^* M to the preimage f⁻¹ V is the pullback of M|_V along f ∣_ V : f⁻¹ V ⟶ V.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def AlgebraicGeometry.Scheme.Modules.pullbackOver {X Y : Scheme} (f : X ⟶ Y) (V : Y.Opens) : CategoryTheory.Functor (SheafOfModules (CategoryTheory.Sheaf.over Y.ringCatSheaf V)) (SheafOfModules (CategoryTheory.Sheaf.over X.ringCatSheaf ((TopologicalSpace.Opens.map f.base).obj V)))

Pullback along f read on slice sites: sheaves of modules over the slice of Y at an open V are identified with 𝒪_V-modules, pulled back along f ∣_ V : f⁻¹ V ⟶ V, and read as sheaves of modules over the slice of X at f⁻¹ V.

Equations

• One or more equations did not get rendered due to their size.

instance AlgebraicGeometry.Scheme.Modules.instIsLeftAdjointSheafOfModulesOverOpensCarrierCarrierCommRingCatOverRingCatRingCatSheafObjOpensMapBasePullbackOver {X Y : Scheme} (f : X ⟶ Y) (V : Y.Opens) : (pullbackOver f V).IsLeftAdjoint

noncomputable def AlgebraicGeometry.Scheme.Modules.pullbackOverUnitIso {X Y : Scheme} (f : X ⟶ Y) (V : Y.Opens) : SheafOfModules.unit (CategoryTheory.Sheaf.over X.ringCatSheaf ((TopologicalSpace.Opens.map f.base).obj V)) ≅ (pullbackOver f V).obj (SheafOfModules.unit (CategoryTheory.Sheaf.over Y.ringCatSheaf V))

Pullback read on slice sites preserves the structure sheaf.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def AlgebraicGeometry.Scheme.Modules.pullbackOverObjIso {X Y : Scheme} (f : X ⟶ Y) (V : Y.Opens) (M : Y.Modules) : (pullbackOver f V).obj (SheafOfModules.over M V) ≅ SheafOfModules.over ((pullback f).obj M) ((TopologicalSpace.Opens.map f.base).obj V)

Pullback read on slice sites computes the restriction of the pullback: it sends M.over V to (f^* M).over (f⁻¹ V).

Equations

• One or more equations did not get rendered due to their size.

theorem AlgebraicGeometry.Scheme.Modules.isIso_iff_of_isOpenCover {X : Scheme} {ι : Type u_1} {U : ι → X.Opens} (hU : TopologicalSpace.IsOpenCover U) {A B : X.Modules} (φ : A ⟶ B) : CategoryTheory.IsIso φ ↔ ∀ (i : ι), CategoryTheory.IsIso ((pullback (U i).ι).map φ)

A morphism of modules is an isomorphism exactly when its pullbacks to the members of an open cover are isomorphisms.

noncomputable def AlgebraicGeometry.Scheme.Modules.overEquivFunctorObjFreeIso {X : Scheme} (U : X.Opens) (I : Type u) : (overEquiv U).functor.obj (SheafOfModules.free I) ≅ SheafOfModules.free I

The identification of modules on the slice site over an open U with modules on the open subscheme U preserves free modules.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def AlgebraicGeometry.Scheme.Modules.restrictIsoFreeOfOverIsoFree {X : Scheme} (M : X.Modules) (U : X.Opens) {I : Type u} (e : SheafOfModules.over M U ≅ SheafOfModules.free I) : M.restrict U.ι ≅ SheafOfModules.free I

A trivialization of M on the slice site over an open U gives a trivialization of the restriction of M to the open subscheme U.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def AlgebraicGeometry.Scheme.Modules.overIsoFreeOfRestrictIsoFree {X : Scheme} (M : X.Modules) (U : X.Opens) {I : Type u} (e : M.restrict U.ι ≅ SheafOfModules.free I) : SheafOfModules.over M U ≅ SheafOfModules.free I

A trivialization of the restriction of M to the open subscheme U gives a trivialization of M on the slice site over U.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def AlgebraicGeometry.Scheme.Modules.restrictOpensRangeIsoFree {X Y : Scheme} (M : Y.Modules) (f : X ⟶ Y) [IsOpenImmersion f] {I : Type u} (e : (pullback f).obj M ≅ SheafOfModules.free I) : M.restrict (Hom.opensRange f).ι ≅ SheafOfModules.free I

A trivialization of the pullback of M along an open immersion f gives a trivialization of the restriction of M to the open image of f.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def SheafOfModules.LocalGeneratorsData.pullback {X Y : AlgebraicGeometry.Scheme} {M : Y.Modules} (q : LocalGeneratorsData M) (f : X ⟶ Y) : LocalGeneratorsData ((AlgebraicGeometry.Scheme.Modules.pullback f).obj M)

Local generators of an 𝒪_Y-module M on a cover V i of Y, carried along f to local generators of f^* M on the cover f⁻¹ (V i) of X.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem SheafOfModules.LocalGeneratorsData.pullback_I {X Y : AlgebraicGeometry.Scheme} {M : Y.Modules} (q : LocalGeneratorsData M) (f : X ⟶ Y) : (q.pullback f).I = q.I

@[simp]

theorem SheafOfModules.LocalGeneratorsData.pullback_generators {X Y : AlgebraicGeometry.Scheme} {M : Y.Modules} (q : LocalGeneratorsData M) (f : X ⟶ Y) (i : q.I) : (q.pullback f).generators i = (q.generators i).mapIso (AlgebraicGeometry.Scheme.Modules.pullbackOver f (q.X i)) (AlgebraicGeometry.Scheme.Modules.pullbackOverUnitIso f (q.X i)) (AlgebraicGeometry.Scheme.Modules.pullbackOverObjIso f (q.X i) M)

@[simp]

theorem SheafOfModules.LocalGeneratorsData.pullback_X {X Y : AlgebraicGeometry.Scheme} {M : Y.Modules} (q : LocalGeneratorsData M) (f : X ⟶ Y) (i : q.I) : (q.pullback f).X i = (TopologicalSpace.Opens.map f.base).obj (q.X i)

instance AlgebraicGeometry.Scheme.Modules.instIsFiniteTypeOpensCarrierCarrierCommRingCatPullback {X Y : Scheme} {M : Y.Modules} (q : SheafOfModules.LocalGeneratorsData M) [q.IsFiniteType] (f : X ⟶ Y) : (q.pullback f).IsFiniteType

Carrying local generators along a morphism of schemes preserves finiteness.

instance AlgebraicGeometry.Scheme.Modules.instIsLocallyFreeDataOpensCarrierCarrierCommRingCatPullback {X Y : Scheme} {M : Y.Modules} (q : SheafOfModules.LocalGeneratorsData M) [q.IsLocallyFreeData] (f : X ⟶ Y) : (q.pullback f).IsLocallyFreeData

Carrying locally free data along a morphism of schemes gives locally free data.

noncomputable def SheafOfModules.QuasicoherentData.pullback {X Y : AlgebraicGeometry.Scheme} {M : Y.Modules} (q : QuasicoherentData M) (f : X ⟶ Y) : QuasicoherentData ((AlgebraicGeometry.Scheme.Modules.pullback f).obj M)

Quasi-coherent data of an 𝒪_Y-module M on a cover V i of Y, carried along f to quasi-coherent data of f^* M on the cover f⁻¹ (V i) of X.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem SheafOfModules.QuasicoherentData.pullback_X {X Y : AlgebraicGeometry.Scheme} {M : Y.Modules} (q : QuasicoherentData M) (f : X ⟶ Y) (i : q.I) : (q.pullback f).X i = (TopologicalSpace.Opens.map f.base).obj (q.X i)

@[simp]

theorem SheafOfModules.QuasicoherentData.pullback_I {X Y : AlgebraicGeometry.Scheme} {M : Y.Modules} (q : QuasicoherentData M) (f : X ⟶ Y) : (q.pullback f).I = q.I

@[simp]

theorem SheafOfModules.QuasicoherentData.pullback_presentation {X Y : AlgebraicGeometry.Scheme} {M : Y.Modules} (q : QuasicoherentData M) (f : X ⟶ Y) (i : q.I) : (q.pullback f).presentation i = Presentation.ofIsIso (AlgebraicGeometry.Scheme.Modules.pullbackOverObjIso f (q.X i) M).hom ((q.presentation i).map (AlgebraicGeometry.Scheme.Modules.pullbackOver f (q.X i)) (AlgebraicGeometry.Scheme.Modules.pullbackOverUnitIso f (q.X i)))

instance AlgebraicGeometry.Scheme.Modules.instIsFinitePresentationOpensCarrierCarrierCommRingCatPullback {X Y : Scheme} {M : Y.Modules} (q : SheafOfModules.QuasicoherentData M) [q.IsFinitePresentation] (f : X ⟶ Y) : (q.pullback f).IsFinitePresentation

Carrying finite quasi-coherent data along a morphism of schemes gives finite quasi-coherent data.

instance AlgebraicGeometry.Scheme.Modules.isQuasicoherent_pullback {X Y : Scheme} (f : X ⟶ Y) (M : Y.Modules) [SheafOfModules.IsQuasicoherent M] : SheafOfModules.IsQuasicoherent ((pullback f).obj M)

The pullback of a quasi-coherent module along a morphism of schemes is quasi-coherent.

instance AlgebraicGeometry.Scheme.Modules.isFiniteType_pullback {X Y : Scheme} (f : X ⟶ Y) (M : Y.Modules) [SheafOfModules.IsFiniteType M] : SheafOfModules.IsFiniteType ((pullback f).obj M)

The pullback of a module of finite type along a morphism of schemes is of finite type.

instance AlgebraicGeometry.Scheme.Modules.isFinitePresentation_pullback {X Y : Scheme} (f : X ⟶ Y) (M : Y.Modules) [SheafOfModules.IsFinitePresentation M] : SheafOfModules.IsFinitePresentation ((pullback f).obj M)

The pullback of a finitely presented module along a morphism of schemes is finitely presented.

instance AlgebraicGeometry.Scheme.Modules.isLocallyFree_pullback {X Y : Scheme} (f : X ⟶ Y) (M : Y.Modules) [SheafOfModules.IsLocallyFree M] : SheafOfModules.IsLocallyFree ((pullback f).obj M)

The pullback of a locally free module along a morphism of schemes is locally free.