Affine localization and K-flat pullback comparison

For a flat affine map, the supplied K-flat derived pullback agrees with exact pullback of all module sheaves, and hence with derived extension of scalars after affine sheafification. The localization specialization compares this with the affine localization functor. These ambient derived-category comparisons assert neither bounded-coherent descent nor arrow extension in a chosen t-heart.

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.specMapToBase_flat_of_ringFlat {R A : CommRingCat} (f : R ⟶ A) (hf : (CommRingCat.Hom.hom f).Flat) : Flat (CategoryTheory.Over.Hom.left (toIdentityBaseChange (CategoryTheory.Over.mk (Spec.map f))))

Flatness of the ring map gives flatness of its spectrum base change.

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.specMapPullback_preservesFiniteLimits_of_flat {R A : CommRingCat} (f : R ⟶ A) (hf : (CommRingCat.Hom.hom f).Flat) : CategoryTheory.Limits.PreservesFiniteLimits (Scheme.Modules.pullback (Spec.map f))

Flat affine pullback of all module sheaves preserves finite limits.

noncomputable def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.kFlatAffineExactSchemeModuleComparison {R A : CommRingCat} (f : R ⟶ A) [Flat (CategoryTheory.Over.Hom.left (toIdentityBaseChange (CategoryTheory.Over.mk (Spec.map f))))] [CategoryTheory.Limits.PreservesFiniteLimits (ModuleCat.extendScalars (CommRingCat.Hom.hom f))] [CategoryTheory.Limits.PreservesFiniteLimits (Scheme.Modules.pullback (Spec.map f))] (K : SchemeKFlatResolution (Spec R)) : (tilde.functor R).mapDerivedCategory.comp (kFlatLeftDerivedPullback K (toIdentityBaseChange (CategoryTheory.Over.mk (Spec.map f))) ⋯).functor ≅ (ModuleCat.extendScalars (CommRingCat.Hom.hom f)).mapDerivedCategory.comp (tilde.functor A).mapDerivedCategory

A supplied K-flat resolution computes the exact pullback along a flat affine map, compatibly with extension of scalars and affine sheafification. This is an ambient all-module-sheaf statement.

Equations

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

noncomputable def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.kFlatAffineLocalizationComparison {R A : Type u} [CommRing R] [CommRing A] (M : Submonoid R) [Algebra R A] [IsLocalization M A] (K : SchemeKFlatResolution (Spec (CommRingCat.of R))) : (tilde.functor (CommRingCat.of R)).mapDerivedCategory.comp (kFlatLeftDerivedPullback K (toIdentityBaseChange (CategoryTheory.Over.mk (Spec.map (CommRingCat.ofHom (algebraMap R A))))) ⋯).functor ≅ (Dqc.affineLocalizationDerivedPullback M).comp (tilde.functor (CommRingCat.of A)).mapDerivedCategory

For a localization, the K-flat affine pullback and derived localization agree after affine sheafification, given an explicitly supplied K-flat resolution. Flatness and finite-limit preservation are supplied internally from IsLocalization M A; no bounded-coherent or heart comparison is inferred.

Equations

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