Exactness of flat pullback

Pullback along a flat morphism of schemes preserves monomorphisms and kernels between quasicoherent module sheaves. Together with right exactness of pullback, this transports exact complexes with quasicoherent second and third terms, and short exact sequences whose first two terms are quasicoherent, under flat base change.

The affine calculation uses tildeFunctorCompPullbackIso and Mathlib's finite-limit preservation theorem for flat extension of scalars. No finiteness or Noetherian hypothesis is needed.

References

• The Stacks Project, Tag 0250, exactness of flat pullback on quasicoherent modules.

theorem AlgebraicGeometry.Scheme.Hom.mono_pullback_map_of_flat {X Y : Scheme} (f : X ⟶ Y) [Flat f] {M N : Y.Modules} (g : M ⟶ N) [SheafOfModules.IsQuasicoherent M] [SheafOfModules.IsQuasicoherent N] [CategoryTheory.Mono g] : CategoryTheory.Mono ((Modules.pullback f).map g)

Pullback along a flat morphism preserves monomorphisms between quasicoherent sheaves. Neither scheme needs to be affine or Noetherian.

theorem AlgebraicGeometry.Scheme.Hom.shortExact_map_pullback_of_flat {X Y : Scheme} (f : X ⟶ Y) [Flat f] (S : CategoryTheory.ShortComplex Y.Modules) (hS : S.ShortExact) [SheafOfModules.IsQuasicoherent S.X₁] [SheafOfModules.IsQuasicoherent S.X₂] : (S.map (Modules.pullback f)).ShortExact

Flat pullback carries a short exact sequence to a short exact sequence when its first two terms are quasicoherent. No quasicoherence hypothesis on the third term is needed.

theorem AlgebraicGeometry.Scheme.Hom.exact_map_pullback_of_flat {X Y : Scheme} (f : X ⟶ Y) [Flat f] (S : CategoryTheory.ShortComplex Y.Modules) (hS : S.Exact) [SheafOfModules.IsQuasicoherent S.X₂] [SheafOfModules.IsQuasicoherent S.X₃] : (S.map (Modules.pullback f)).Exact

Flat pullback preserves an exact complex when its second and third terms are quasicoherent. No condition on the first term, finiteness, or Noetherian hypothesis is required.

theorem AlgebraicGeometry.Scheme.Hom.preservesKernel_pullback_of_flat {X Y : Scheme} (f : X ⟶ Y) [Flat f] {M N : Y.Modules} (g : M ⟶ N) [SheafOfModules.IsQuasicoherent M] [SheafOfModules.IsQuasicoherent N] : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair g 0) (Modules.pullback f)

Pullback along a flat morphism preserves the ambient kernel of a morphism between quasicoherent module sheaves.