Bounded-above flat complexes are K-flat for scheme-module tensor #
The increasing lower stupid-truncation tower of a strictly bounded-above complex has finite term support at every stage. When all terms of the input are flat over the identity, the finite K-flat theorem applies stagewise. Sequential colimits then recover the original complex and preserve K-flatness.
Main definitions #
This module introduces no new definitions. It uses the existing
CategoryTheory.CochainComplex.IsKFlat predicate and literal
AlgebraicGeometry.Scheme.Modules.totalTensor.
Main results #
AlgebraicGeometry.Scheme.Modules.isKFlat_totalTensor_of_boundedAbove_flatTermsproves two-slot K-flatness for a strictly bounded-above complex whose every term is flat over the identity.
Implementation notes #
Each lower stupid tail is supported in a finite interval. Flatness transfers across its component isomorphism to the input; the finite-support theorem proves K-flatness of that stage. The generic K-flat colimit theorem applies using sequential-colimit preservation of total tensor in both slots and the AB5 property of scheme-module sheaves. An isomorphism from the input to the tower's colimit transports the two localization clauses back to the input. This theorem does not assert an arbitrary unbounded flat-term complex is K-flat.
References #
The ingredients are the lower stupid-tower colimit theorem in
HomologicalComplex.isColimitStupidTruncGETowerCocone,
AlgebraicGeometry.Scheme.Modules.isKFlat_totalTensor_of_finiteFlatTerms,
CategoryTheory.CochainComplex.IsKFlat.colimit, and the sequential
total-tensor colimit results in Modules/Tensor/ComplexColimits.lean.
Tags #
scheme-module sheaf, flatness, bounded-above complex, K-flat complex, colimit
A strictly bounded-above complex with every term flat over the identity is K-flat for the literal scheme-module total tensor. The upper bound concerns terms, not merely cohomology; no claim about arbitrary unbounded complexes is made.