Scalar extension of the actual pullback map on sections

The pullback adjunction unit is linear over the source base ring. If its target is also a module over a larger ring compatibly with the structural maps, the scalar-extension adjunction transposes the actual unit map to a map from extended global sections. This does not assert it is an isomorphism.

noncomputable def AlgebraicGeometry.Scheme.Modules.fixedBasePullbackTopAfterExtension {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 ψ) : (ModuleCat.extendScalars (CommRingCat.Hom.hom a)).obj ((fixedBaseSectionsFunctor Y φ ⊤).obj M) ⟶ (fixedBaseSectionsFunctor Z ψ ⊤).obj ((pullback f).obj M)

Extend scalars in the actual top-section pullback unit along a compatible base-ring map. The result is the unique A-linear map whose value on 1 ⊗ x is the ordinary pullback-unit section of x.

Equations

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

theorem AlgebraicGeometry.Scheme.Modules.fixedBasePullbackTopAfterExtension_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 ⊤)) (compat : CategoryTheory.CategoryStruct.comp φ (Hom.appTop f) = CategoryTheory.CategoryStruct.comp a ψ) (x : ↑(M.presheaf.obj (Opposite.op ⊤))) : (ModuleCat.Hom.hom (fixedBasePullbackTopAfterExtension φ f M a ψ compat)) (1 ⊗ₜ[↑R] x) = (CategoryTheory.ConcreteCategory.hom (Hom.app ((pullbackPushforwardAdjunction f).unit.app M) ⊤)) x

Scalar extension sends a pure generator to the actual top component of the pullback adjunction unit.