Module pullback on affine spectra

For a map of commutative rings, pulling back the tilde of a module along the induced map of affine schemes agrees with extension of scalars followed by tilde. The comparison is underived and is obtained from the two standard adjunctions and the affine global-sections comparison. Its mate equation below identifies the actual pullback unit on top sections with the tensor generator.

noncomputable def AlgebraicGeometry.Scheme.Modules.pullbackSpecMapTildeIso {R S : CommRingCat} (f : R ⟶ S) : (tilde.functor R).comp (pullback (Spec.map f)) ≅ (ModuleCat.extendScalars (CommRingCat.Hom.hom f)).comp (tilde.functor S)

On affine spectra, scheme-module pullback after tilde is extension of scalars followed by target tilde. This is an isomorphism of ordinary functors; it does not assert that either side computes a derived pullback.

Equations

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

theorem AlgebraicGeometry.Scheme.Modules.pullbackSpecMapTildeIso_unit {R S : CommRingCat} (f : R ⟶ S) (M : ModuleCat ↑R) : CategoryTheory.CategoryStruct.comp (tilde.isoTop M).hom (CategoryTheory.CategoryStruct.comp (moduleSpecΓFunctor.map ((pullbackPushforwardAdjunction (Spec.map f)).unit.app (tilde M))) (CategoryTheory.CategoryStruct.comp ((gammaPushforwardNatIso f).hom.app ((pullback (Spec.map f)).obj (tilde M))) ((ModuleCat.restrictScalars (CommRingCat.Hom.hom f)).map (moduleSpecΓFunctor.map ((pullbackSpecMapTildeIso f).hom.app M))))) = CategoryTheory.CategoryStruct.comp ((ModuleCat.extendRestrictScalarsAdj (CommRingCat.Hom.hom f)).unit.app M) ((ModuleCat.restrictScalars (CommRingCat.Hom.hom f)).map (tilde.adjunction.unit.app ((ModuleCat.extendScalars (CommRingCat.Hom.hom f)).obj M)))

The affine tilde/pullback comparison is the mate of the actual scheme-module pullback unit. After identifying the two global-sections functors, this equation says that applying pullbackSpecMapTildeIso to the section obtained from that unit agrees with the tensor extension unit followed by the target tilde/Γ unit. No localization or derived claim enters.

theorem AlgebraicGeometry.Scheme.Modules.pullbackSpecMapTildeIso_unit_apply {R S : CommRingCat} (f : R ⟶ S) (M : ModuleCat ↑R) (m : ↑M) : (ModuleCat.Hom.hom (CategoryTheory.CategoryStruct.comp (tilde.isoTop M).hom (CategoryTheory.CategoryStruct.comp (moduleSpecΓFunctor.map ((pullbackPushforwardAdjunction (Spec.map f)).unit.app (tilde M))) (CategoryTheory.CategoryStruct.comp ((gammaPushforwardNatIso f).hom.app ((pullback (Spec.map f)).obj (tilde M))) ((ModuleCat.restrictScalars (CommRingCat.Hom.hom f)).map (moduleSpecΓFunctor.map ((pullbackSpecMapTildeIso f).hom.app M))))))) m = (CategoryTheory.ConcreteCategory.hom (tilde.isoTop ((ModuleCat.extendScalars (CommRingCat.Hom.hom f)).obj M)).hom) (1 ⊗ₜ[↑R] m)

On a section m, the actual affine pullback unit becomes 1 ⊗ m under the tilde/Γ and affine pullback comparisons. The right-hand side is the canonical section of the tilde of the scalar-extended module, not a chosen non-natural Γ isomorphism.

noncomputable def AlgebraicGeometry.Scheme.Modules.pullbackSpecMapTildeMapHomologicalComplexIso {R S : CommRingCat} (f : R ⟶ S) : ((tilde.functor R).mapHomologicalComplex (ComplexShape.up ℤ)).comp ((pullback (Spec.map f)).mapHomologicalComplex (ComplexShape.up ℤ)) ≅ ((ModuleCat.extendScalars (CommRingCat.Hom.hom f)).mapHomologicalComplex (ComplexShape.up ℤ)).comp ((tilde.functor S).mapHomologicalComplex (ComplexShape.up ℤ))

The affine tilde/pullback comparison induces the corresponding isomorphism on cochain complexes.

Equations

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