The affine pullback unit as localization

For a multiplicative set in a commutative ring, the actual top sections of the pullback of a tilde module to the localized affine spectrum are naturally the localization of its top sections. The comparison carries the localization generator to the actual scheme-module pullback unit.

noncomputable def AlgebraicGeometry.Scheme.Modules.affineLocalizationTopNatIso {R : CommRingCat} (S : Submonoid ↑R) : let A := CommRingCat.of (Localization S); have f := CommRingCat.ofHom (algebraMap (↑R) (Localization S)); ((tilde.functor R).comp (fixedBaseSectionsFunctor (Spec R) (ΓSpecIso R).inv ⊤)).comp (ModuleCat.localizedModuleFunctor S) ≅ ((tilde.functor R).comp (pullback (Spec.map f))).comp (fixedBaseSectionsFunctor (Spec A) (ΓSpecIso A).inv ⊤)

The localization of fixed-base top sections of a tilde module is naturally the actual top sections of its scheme-module pullback to the localized spectrum.

Equations

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

theorem AlgebraicGeometry.Scheme.Modules.affineLocalizationTopNatIso_hom_localizedMk {R : CommRingCat} (S : Submonoid ↑R) (M : ModuleCat ↑R) (m : ↑M) : let A := CommRingCat.of (Localization S); let f := CommRingCat.ofHom (algebraMap (↑R) (Localization S)); (ModuleCat.Hom.hom ((affineLocalizationTopNatIso S).hom.app M)) ((((fixedBaseSectionsFunctor (Spec R) (ΓSpecIso R).inv ⊤).obj (tilde M)).localizedModuleMkLinearMap S) ((CategoryTheory.ConcreteCategory.hom (tilde.isoTop M).hom) m)) = (ModuleCat.Hom.hom (fixedBasePullbackTop (ΓSpecIso R).inv (Spec.map f) (tilde M))) ((CategoryTheory.ConcreteCategory.hom (tilde.isoTop M).hom) m)

The natural isomorphism sends the localization generator of a tilde section to that section's image under the actual pullback adjunction unit.

theorem AlgebraicGeometry.Scheme.Modules.affineLocalizationTopNatIso_hom_localizedMk_section {R : CommRingCat} (S : Submonoid ↑R) (M : ModuleCat ↑R) (x : ↑((fixedBaseSectionsFunctor (Spec R) (ΓSpecIso R).inv ⊤).obj (tilde M))) : let A := CommRingCat.of (Localization S); let f := CommRingCat.ofHom (algebraMap (↑R) (Localization S)); (ModuleCat.Hom.hom ((affineLocalizationTopNatIso S).hom.app M)) ((((fixedBaseSectionsFunctor (Spec R) (ΓSpecIso R).inv ⊤).obj (tilde M)).localizedModuleMkLinearMap S) x) = (ModuleCat.Hom.hom (fixedBasePullbackTop (ΓSpecIso R).inv (Spec.map f) (tilde M))) x

The compatibility holds for every top section, since tilde.isoTop is an isomorphism. Thus the actual pullback unit is the localization generator under the natural isomorphism, rather than only on a chosen presentation of sections.