Localizing the two-open section pullback

Fixed-base sections of a module sheaf on a union are a pullback of the sections on its two opens. Canonical module localization is exact, so the localized cone is still a pullback. This is only a statement about localized sections of the source sheaf on these two opens and their union: identifying them with sections on a geometric base change requires separate affine-chart comparisons. No objectwise-localized sheaf is constructed here.

noncomputable def AlgebraicGeometry.localizedFixedBaseSectionsTwoOpenLimit {R : CommRingCat} (Y : Scheme) (φ : R ⟶ Y.presheaf.obj (Opposite.op ⊤)) (M : Y.Modules) (U V : Y.Opens) (S : Submonoid ↑R) : CategoryTheory.Limits.IsLimit ((ModuleCat.localizedModuleFunctor S).mapCone (((modulesToFixedBaseSheaf Y φ).obj M).interUnionPullbackCone U V))

The two-open pullback cone remains a limit after localizing its four section modules at S.

Equations

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