Finite flat complexes are K-flat for scheme-module tensor

A complex of scheme-module sheaves with finite term support is K-flat for the literal total tensor when every term in its support interval is flat over the identity. The fixed complex may have zero terms outside the interval; no flatness evidence is needed there.

Main definitions

This module introduces no new definitions. It specializes the existing CategoryTheory.CochainComplex.IsKFlat predicate to AlgebraicGeometry.Scheme.Modules.totalTensor.

Main results

• AlgebraicGeometry.Scheme.Modules.quasiIso_totalTensor_map_left_of_finiteFlatTerms sends a quasi-isomorphism through the second slot of total tensor.
• AlgebraicGeometry.Scheme.Modules.quasiIso_totalTensor_map_right_of_finiteFlatTerms sends a quasi-isomorphism through the first slot.
• AlgebraicGeometry.Scheme.Modules.isKFlat_totalTensor_of_finiteFlatTerms packages both directions into the generic K-flat predicate.

Implementation notes

The generic finite-strip theorem for bifunctor totals reduces both maps to columnwise quasi-isomorphisms. Flatness of each supported sheaf supplies those columnwise results through homology preservation of ordinary tensor. The right-slot proof uses the generic signed-flip comparison; no global braiding instance on complexes is required. This does not prove K-flatness of an unbounded complex of flat terms.

References

The finite-strip criterion is HomologicalComplex.quasiIso_mapBifunctorMap_id_left_of_finite_support_of_column_quasiIso and its right-slot counterpart. The flat-sheaf inputs are AlgebraicGeometry.Scheme.Modules.quasiIso_map_tensorLeftFunctor_of_isFlatOverId and AlgebraicGeometry.Scheme.Modules.quasiIso_map_tensorRight_of_isFlatOverId.

Tags

scheme-module sheaf, flatness, total tensor, K-flat complex, quasi-isomorphism

theorem AlgebraicGeometry.Scheme.Modules.quasiIso_totalTensor_map_left_of_finiteFlatTerms (X : Scheme) (K : CochainComplex X.Modules ℤ) (a b : ℤ) (hLower : ∀ p < a, CategoryTheory.Limits.IsZero (K.X p)) (hUpper : ∀ (p : ℤ), b < p → CategoryTheory.Limits.IsZero (K.X p)) (hFlat : ∀ (p : ℤ), a ≤ p → p ≤ b → IsFlatOver (CategoryTheory.CategoryStruct.id X) (K.X p)) {L M : CochainComplex X.Modules ℤ} (f : L ⟶ M) [QuasiIso f] : QuasiIso (((totalTensor X).obj K).map f)

Flatness gives quasi-isomorphisms columnwise, and finite support lets the finite-strip criterion pass them to the total. No flatness witness is needed outside the support interval.

theorem AlgebraicGeometry.Scheme.Modules.quasiIso_totalTensor_map_right_of_finiteFlatTerms (X : Scheme) (K : CochainComplex X.Modules ℤ) (a b : ℤ) (hLower : ∀ p < a, CategoryTheory.Limits.IsZero (K.X p)) (hUpper : ∀ (p : ℤ), b < p → CategoryTheory.Limits.IsZero (K.X p)) (hFlat : ∀ (p : ℤ), a ≤ p → p ≤ b → IsFlatOver (CategoryTheory.CategoryStruct.id X) (K.X p)) {L M : CochainComplex X.Modules ℤ} (f : L ⟶ M) [QuasiIso f] : QuasiIso (((totalTensor X).flip.obj K).map f)

The generic signed-flip comparison applies the finite-strip criterion with the supported complex fixed on the right, without a braiding instance on complexes.

theorem AlgebraicGeometry.Scheme.Modules.isKFlat_totalTensor_of_finiteFlatTerms (X : Scheme) (K : CochainComplex X.Modules ℤ) (a b : ℤ) (hLower : ∀ p < a, CategoryTheory.Limits.IsZero (K.X p)) (hUpper : ∀ (p : ℤ), b < p → CategoryTheory.Limits.IsZero (K.X p)) (hFlat : ∀ (p : ℤ), a ≤ p → p ≤ b → IsFlatOver (CategoryTheory.CategoryStruct.id X) (K.X p)) : CategoryTheory.CochainComplex.IsKFlat (totalTensor X) K

The two total-map results supply the localization clauses of the generic K-flat predicate. This proves K-flatness of the supplied complex without constructing a resolution.