Pullback of top sections over a fixed base ring

The actual scheme-module pullback adjunction unit induces a map on top sections. This file equips that map with its fixed-base-ring linearity for an arbitrary scheme morphism. It does not assert that the map is a localization, an isomorphism, or a derived global-sections comparison.

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

The actual pullback unit on top sections, as a map of R-modules.

Equations

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

@[simp]

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

On elements, the fixed-base linear map is exactly the top component of the ordinary pullback adjunction unit.

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

Naturality of the actual pullback-unit map on fixed-base top sections.

Equations

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