Exact tensoring by a flat scheme-module sheaf

A module sheaf flat over the identity makes ordinary tensoring exact in either slot. The results here show that each partial tensor functor preserves homology and its termwise action preserves quasi-isomorphisms of complexes of any shape. These results treat a flat sheaf fixed in degree zero; K-flatness of a complex of flat sheaves and arbitrary derived pullback remain separate.

Main definitions

This module introduces no new public definitions. Private stalk comparison and tensor-commutativity adapters support the results below, which extend existing partial tensor functors on scheme-module sheaves.

Main results

• AlgebraicGeometry.Scheme.Modules.tensorLeftFunctor_preservesHomology_of_isFlatOverId
• AlgebraicGeometry.Scheme.Modules.tensorRight_preservesHomology_of_isFlatOverId
• AlgebraicGeometry.Scheme.Modules.quasiIso_map_tensorLeftFunctor_of_isFlatOverId
• AlgebraicGeometry.Scheme.Modules.quasiIso_map_tensorRight_of_isFlatOverId

Implementation notes

PresheafOfModules.stalkTensorEquiv and PresheafOfModules.stalkMapAdd_whiskerLeft transfer Module.Flat.lTensor_preserves_injective_linearMap to sheaf stalks. Joint stalk reflection then gives mono preservation. Tensor colimits supply cokernels, so CategoryTheory.Functor.preservesHomology_of_preservesMonos_and_cokernels gives homology preservation. A private natural tensor-commutativity isomorphism handles the right slot. HomologicalComplex.quasiIso_map_of_preservesHomology gives the arbitrary-shape quasi-isomorphism corollaries.

References

• Mathlib/RingTheory/Flat/Basic.lean: flat-module tensor injectivity.
• Mathlib/CategoryTheory/Abelian/Exact.lean: homology preservation from monomorphisms and cokernels.
• Mathlib/Algebra/Homology/QuasiIso.lean: mapped quasi-isomorphisms under a homology-preserving functor.

Tags

flat module sheaf, tensor product, homology, quasi-isomorphism

theorem AlgebraicGeometry.Scheme.Modules.tensorLeftFunctor_preservesHomology_of_isFlatOverId (X : Scheme) (L : X.Modules) (hL : IsFlatOver (CategoryTheory.CategoryStruct.id X) L) : L.tensorLeftFunctor.PreservesHomology

Stalkwise flatness preserves injectivity through the tensor-stalk comparison. Joint stalk reflection gives mono preservation; tensor colimits supply cokernels.

theorem AlgebraicGeometry.Scheme.Modules.tensorRightFiniteColimits (X : Scheme) (L : X.Modules) : CategoryTheory.Limits.PreservesFiniteColimits (CategoryTheory.MonoidalCategory.tensorRight L)

theorem AlgebraicGeometry.Scheme.Modules.tensorRightAdditive (X : Scheme) (L : X.Modules) : (CategoryTheory.MonoidalCategory.tensorRight L).Additive

theorem AlgebraicGeometry.Scheme.Modules.tensorRight_preservesHomology_of_isFlatOverId (X : Scheme) (L : X.Modules) (hL : IsFlatOver (CategoryTheory.CategoryStruct.id X) L) : (CategoryTheory.MonoidalCategory.tensorRight L).PreservesHomology

Tensor symmetry transports the left-slot mono result to the right slot; colimit preservation supplies the cokernel condition.

theorem AlgebraicGeometry.Scheme.Modules.quasiIso_map_tensorLeftFunctor_of_isFlatOverId (X : Scheme) (L : X.Modules) (hL : IsFlatOver (CategoryTheory.CategoryStruct.id X) L) {ι : Type v} {c : ComplexShape ι} {K K' : HomologicalComplex X.Modules c} (f : K ⟶ K') [QuasiIso f] : QuasiIso ((L.tensorLeftFunctor.mapHomologicalComplex c).map f)

Homology preservation of left tensor gives the termwise complex result for any shape. The fixed flat sheaf is a degree-zero factor, not a K-flat complex.

theorem AlgebraicGeometry.Scheme.Modules.quasiIso_map_tensorRight_of_isFlatOverId (X : Scheme) (L : X.Modules) (hL : IsFlatOver (CategoryTheory.CategoryStruct.id X) L) {ι : Type v} {c : ComplexShape ι} {K K' : HomologicalComplex X.Modules c} (f : K ⟶ K') [QuasiIso f] : QuasiIso (((CategoryTheory.MonoidalCategory.tensorRight L).mapHomologicalComplex c).map f)

Tensor symmetry supplies the right-slot homology preservation used termwise on any complex shape, with the flat sheaf fixed as a degree-zero factor.