Exact pullback along flat morphisms

The canonical module pullback-to-stalk comparison lives in AlgebraicGeometry.Modules.Pullback.Stalk. A flat scheme morphism has flat maps on local rings, so extension of scalars preserves finite limits at every stalk. Joint reflection by module stalks then proves that module-sheaf pullback preserves finite limits, and hence is exact.

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.flatStalkMap_preservesFiniteLimits {S : Scheme} {T U : SchemeBaseChange S} (f : T ⟶ U) [Flat (CategoryTheory.Over.Hom.left f)] (x : ↥(CategoryTheory.Over.left T)) : CategoryTheory.Limits.PreservesFiniteLimits (ModuleCat.extendScalars (CommRingCat.Hom.hom (Scheme.Hom.stalkMap (CategoryTheory.Over.Hom.left f) x)))

At every point of a flat scheme morphism, extension of scalars along the induced local-ring map preserves finite limits.

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.flatPullbackStalkModel_preservesFiniteLimits {S : Scheme} {T U : SchemeBaseChange S} (f : T ⟶ U) [Flat (CategoryTheory.Over.Hom.left f)] (x : ↥(CategoryTheory.Over.left T)) : CategoryTheory.Limits.PreservesFiniteLimits ((Scheme.Modules.moduleStalkFunctor (CategoryTheory.Over.left U) ((CategoryTheory.Over.Hom.left f) x)).comp (ModuleCat.extendScalars (CommRingCat.Hom.hom (Scheme.Hom.stalkMap (CategoryTheory.Over.Hom.left f) x))))

The stalkwise model for pullback along a flat scheme morphism preserves finite limits.

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.modulePullback_preservesFiniteLimits_of_flat {S : Scheme} {T U : SchemeBaseChange S} (f : T ⟶ U) [Flat (CategoryTheory.Over.Hom.left f)] : CategoryTheory.Limits.PreservesFiniteLimits (modulePullback f)

Module-sheaf pullback along a flat morphism preserves finite limits.

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.isExactPullback_of_flat {S : Scheme} {T U : SchemeBaseChange S} (f : T ⟶ U) [Flat (CategoryTheory.Over.Hom.left f)] : IsExactPullback f

Pullback along a flat morphism of scheme base changes is exact.

@[instance 800]

instance AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.isExactPullbackOfFlat {S : Scheme} {T U : SchemeBaseChange S} (f : T ⟶ U) [Flat (CategoryTheory.Over.Hom.left f)] : IsExactPullback f

Exact pullback along flat morphisms is available to the derived pullback API without a caller-supplied exactness instance.