Scalar extension of the pullback unit on open sections

For compatible maps R ⟶ Γ(Y, ⊤) and A ⟶ Γ(Z, ⊤), the actual pullback adjunction unit on an arbitrary open U transposes to an A-linear map from extended sections of M on U to sections of f⁺ M on f ⁻¹ᵁ U. This is an underived map; no localization or isomorphism assertion is made.

noncomputable def AlgebraicGeometry.Scheme.Modules.fixedBasePullbackOpenAfterExtension {R A : CommRingCat} {Y Z : Scheme} (φ : R ⟶ Y.presheaf.obj (Opposite.op ⊤)) (f : Z ⟶ Y) (M : Y.Modules) (a : R ⟶ A) (ψ : A ⟶ Z.presheaf.obj (Opposite.op ⊤)) (U : Y.Opens) (compat : CategoryTheory.CategoryStruct.comp φ (Hom.appTop f) = CategoryTheory.CategoryStruct.comp a ψ) : (ModuleCat.extendScalars (CommRingCat.Hom.hom a)).obj ((fixedBaseSectionsFunctor Y φ U).obj M) ⟶ (fixedBaseSectionsFunctor Z ψ ((TopologicalSpace.Opens.map f.base).obj U)).obj ((pullback f).obj M)

The actual open-section pullback unit, transposed across extension of scalars.

Equations

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

theorem AlgebraicGeometry.Scheme.Modules.fixedBasePullbackOpenAfterExtension_one_tmul {R A : CommRingCat} {Y Z : Scheme} (φ : R ⟶ Y.presheaf.obj (Opposite.op ⊤)) (f : Z ⟶ Y) (M : Y.Modules) (a : R ⟶ A) (ψ : A ⟶ Z.presheaf.obj (Opposite.op ⊤)) (U : Y.Opens) (compat : CategoryTheory.CategoryStruct.comp φ (Hom.appTop f) = CategoryTheory.CategoryStruct.comp a ψ) (x : ↑(M.presheaf.obj (Opposite.op U))) : (ModuleCat.Hom.hom (fixedBasePullbackOpenAfterExtension φ f M a ψ U compat)) (1 ⊗ₜ[↑R] x) = (CategoryTheory.ConcreteCategory.hom (Hom.app ((pullbackPushforwardAdjunction f).unit.app M) U)) x

On 1 ⊗ x, the extended map is literally the ordinary pullback unit at U.

theorem AlgebraicGeometry.Scheme.Modules.fixedBasePullbackOpenAfterExtension_restrict {R A : CommRingCat} {Y Z : Scheme} (φ : R ⟶ Y.presheaf.obj (Opposite.op ⊤)) (f : Z ⟶ Y) (M : Y.Modules) (a : R ⟶ A) (ψ : A ⟶ Z.presheaf.obj (Opposite.op ⊤)) {U V : Y.Opens} (h : U ≤ V) (compat : CategoryTheory.CategoryStruct.comp φ (Hom.appTop f) = CategoryTheory.CategoryStruct.comp a ψ) : CategoryTheory.CategoryStruct.comp (fixedBasePullbackOpenAfterExtension φ f M a ψ V compat) (((modulesToFixedBaseSheaf Z ψ).obj ((pullback f).obj M)).presheaf.map ((TopologicalSpace.Opens.map f.base).map (CategoryTheory.homOfLE h)).op) = CategoryTheory.CategoryStruct.comp ((ModuleCat.extendScalars (CommRingCat.Hom.hom a)).map (((modulesToFixedBaseSheaf Y φ).obj M).presheaf.map (CategoryTheory.homOfLE h).op)) (fixedBasePullbackOpenAfterExtension φ f M a ψ U compat)

The scalar-extended actual pullback unit commutes with restriction of opens. The proof transposes the already proved R-linear restriction square through the extension/restriction-of-scalars adjunction.

theorem AlgebraicGeometry.Scheme.Modules.fixedBasePullbackOpenAfterExtension_top {R A : CommRingCat} {Y Z : Scheme} (φ : R ⟶ Y.presheaf.obj (Opposite.op ⊤)) (f : Z ⟶ Y) (M : Y.Modules) (a : R ⟶ A) (ψ : A ⟶ Z.presheaf.obj (Opposite.op ⊤)) (compat : CategoryTheory.CategoryStruct.comp φ (Hom.appTop f) = CategoryTheory.CategoryStruct.comp a ψ) : fixedBasePullbackOpenAfterExtension φ f M a ψ ⊤ compat = fixedBasePullbackTopAfterExtension φ f M a ψ compat

At the top open, the arbitrary-open scalar-extended unit is the previously defined scalar-extended global-section unit.