Pullback and restriction of scheme-module sheaves

For a scheme morphism f : X ⟶ Y and an open U ⊆ Y, restriction of f⁺ M to f⁻¹ U agrees with pullback of M|_U along the restricted morphism f|_U : X|_{f⁻¹ U} ⟶ Y|_U.

The statement is expressed in Mathlib's slice-site category, because this is the common root used by local generators, finite presentations, and intrinsic local freeness. The proof is assembled only from the scheme-module pullback pseudofunctor and the equivalence between slice-site modules and modules on an open subscheme.

The file also packages pullback on slices as one functor between slice-site module categories, pullbackOverFunctor, with its adjunction to pushforward on slices. The point is where the instances are stated: Presentation.map and the other slice-level transports ask for colimit preservation of a functor between SheafOfModules categories, and the pullback functor on X.Modules carries its instances at the Scheme.Modules wrapper's category instance, where that search does not find them (see Modules/Affine/Equivalence.lean). Composing with the two slice equivalences and taking the adjunction of the composite states colimit preservation in the form the transports meet.

Main definitions

• pullbackOverFunctor, pushforwardOverFunctor, pullbackOverAdjunction: pullback on slices, as a left adjoint between slice-site module categories.
• pullbackOverIso: the restriction square for pullback, on objects.
• pullbackRestrictUnitIso, pullbackOverUnitIso: pullback on slices fixes the structure sheaf, the identification Presentation.map consumes.
• Scheme.Hom.coversTop_preimage: the preimages of a cover cover.

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

Pullback along f, on the slice over U : Y.Opens, as a functor between slice-site module categories: transport to the open subscheme, pull back along f ∣_ U, transport back.

Equations

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

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

Pushforward along f, on the slice over U : Y.Opens, the right adjoint of pullbackOverFunctor.

Equations

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

noncomputable def AlgebraicGeometry.Scheme.Modules.pullbackOverAdjunction {X Y : Scheme} (f : X ⟶ Y) (U : Y.Opens) : pullbackOverFunctor f U ⊣ pushforwardOverFunctor f U

Pullback on slices is left adjoint to pushforward on slices: the composite of the two slice equivalences' adjunctions with pullbackPushforwardAdjunction.

Equations

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

instance AlgebraicGeometry.Scheme.Modules.pullbackOverFunctor_preservesColimits {X Y : Scheme} (f : X ⟶ Y) (U : Y.Opens) : CategoryTheory.Limits.PreservesColimitsOfSize.{u, u, u, u, u + 1, u + 1} (pullbackOverFunctor f U)

Pullback on slices preserves colimits. Not inherited from Scheme.Modules.pullback, whose left-adjoint instance is registered at the Scheme.Modules wrapper's category instance: stated on the composite through pullbackOverAdjunction, the instance lives at the slice-site category instances, which is where SheafOfModules.Presentation.map looks for it.

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

Restricting a pulled-back module to an inverse-image open agrees with pulling back the restriction along the restricted scheme morphism, that is, with pullbackOverFunctor.

Equations

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

noncomputable def AlgebraicGeometry.Scheme.Modules.pullbackRestrictUnitIso {X Y : Scheme} (f : X ⟶ Y) (U : Y.Opens) : SheafOfModules.unit (↑((TopologicalSpace.Opens.map f.base).obj U)).ringCatSheaf ≅ (pullback (f ∣_ U)).obj (SheafOfModules.unit (↑U).ringCatSheaf)

Pullback along f ∣_ U sends the structure sheaf to the structure sheaf; the inverse of Mathlib's pullbackObjUnitToUnit, an isomorphism because inverse image on opens is final (TopologicalSpace.Opens.map_final).

Equations

• AlgebraicGeometry.Scheme.Modules.pullbackRestrictUnitIso f U = (CategoryTheory.asIso (SheafOfModules.pullbackObjUnitToUnit (AlgebraicGeometry.Scheme.Hom.toRingCatSheafHom (f ∣_ U)))).symm

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

Pullback on slices sends the structure sheaf to the structure sheaf: the three factors' identifications composed, in the shape SheafOfModules.Presentation.map consumes for pullbackOverFunctor.

Equations

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

theorem AlgebraicGeometry.Scheme.Hom.coversTop_preimage {X Y : Scheme} (f : X ⟶ Y) {ι : Type u} {V : ι → Y.Opens} (hV : (Opens.grothendieckTopology ↥Y).CoversTop V) : (Opens.grothendieckTopology ↥X).CoversTop fun (i : ι) => (TopologicalSpace.Opens.map f.base).obj (V i)

The preimages under f of a family of opens covering Y cover X. This is the step every chart-by-chart transport along f ends with.