The pullback unit on sections over an arbitrary open

For a scheme morphism f : Z ⟶ Y and a base-ring map φ : R ⟶ Γ(Y, ⊤), the actual pullback adjunction unit gives an R-linear map from sections of M on U to sections of f⁺ M on f ⁻¹ᵁ U. The map is natural in M and commutes with restriction of opens. No affine, quasi-coherent, localization, or derived hypothesis is used.

noncomputable def AlgebraicGeometry.Scheme.Modules.fixedBasePullbackOpen {R : CommRingCat} {Z Y : Scheme} (φ : R ⟶ Y.presheaf.obj (Opposite.op ⊤)) (f : Z ⟶ Y) (M : Y.Modules) (U : Y.Opens) : (fixedBaseSectionsFunctor Y φ U).obj M ⟶ (fixedBaseSectionsFunctor Z (CategoryTheory.CategoryStruct.comp φ (Hom.appTop f)) ((TopologicalSpace.Opens.map f.base).obj U)).obj ((pullback f).obj M)

The actual pullback adjunction unit on sections of U, linear over R.

Equations

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

@[simp]

theorem AlgebraicGeometry.Scheme.Modules.fixedBasePullbackOpen_apply {R : CommRingCat} {Z Y : Scheme} (φ : R ⟶ Y.presheaf.obj (Opposite.op ⊤)) (f : Z ⟶ Y) (M : Y.Modules) (U : Y.Opens) (x : ↑(M.presheaf.obj (Opposite.op U))) : (ModuleCat.Hom.hom (fixedBasePullbackOpen φ f M U)) x = (CategoryTheory.ConcreteCategory.hom (Hom.app ((pullbackPushforwardAdjunction f).unit.app M) U)) x

On elements the linear map is the component of the ordinary adjunction unit.

noncomputable def AlgebraicGeometry.Scheme.Modules.fixedBasePullbackOpenNat {R : CommRingCat} {Z Y : Scheme} (φ : R ⟶ Y.presheaf.obj (Opposite.op ⊤)) (f : Z ⟶ Y) (U : Y.Opens) : fixedBaseSectionsFunctor Y φ U ⟶ (pullback f).comp (fixedBaseSectionsFunctor Z (CategoryTheory.CategoryStruct.comp φ (Hom.appTop f)) ((TopologicalSpace.Opens.map f.base).obj U))

Naturality of the open-section pullback unit in the module sheaf.

Equations

• AlgebraicGeometry.Scheme.Modules.fixedBasePullbackOpenNat φ f U = { app := fun (M : Y.Modules) => AlgebraicGeometry.Scheme.Modules.fixedBasePullbackOpen φ f M U, naturality := ⋯ }

theorem AlgebraicGeometry.Scheme.Modules.fixedBasePullbackOpen_restrict {R : CommRingCat} {Z Y : Scheme} (φ : R ⟶ Y.presheaf.obj (Opposite.op ⊤)) (f : Z ⟶ Y) (M : Y.Modules) {U V : Y.Opens} (h : U ≤ V) : CategoryTheory.CategoryStruct.comp (fixedBasePullbackOpen φ f M V) (((modulesToFixedBaseSheaf Z (CategoryTheory.CategoryStruct.comp φ (Hom.appTop f))).obj ((pullback f).obj M)).presheaf.map ((TopologicalSpace.Opens.map f.base).map (CategoryTheory.homOfLE h)).op) = CategoryTheory.CategoryStruct.comp (((modulesToFixedBaseSheaf Y φ).obj M).presheaf.map (CategoryTheory.homOfLE h).op) (fixedBasePullbackOpen φ f M U)

The open-section pullback unit commutes with restriction from V to U.