Functorial K-flat resolution from the free-Yoneda total

Resolving each good truncation of an arbitrary input produces a bounded-above complex with identity-flat terms. The bounded-above K-flat theorem applies to these resolved stages. Their free-Yoneda totals form a colimiting cocone over the free-Yoneda total of the original input, so exact sequential colimits and two-slot total-tensor colimit preservation pass K-flatness to every input.

Main definitions

• AlgebraicGeometry.DerivedCategory.freeYonedaSchemeKFlatResolution inhabits the existing AlgebraicGeometry.DerivedCategory.SchemeKFlatResolution interface with the canonical functorial free-Yoneda total and its already-proved quasi-isomorphic augmentation.

Main results

• AlgebraicGeometry.Scheme.Modules.isKFlat_freeYonedaSheafCoproductTotalComplexFunctor_obj proves K-flatness of the canonical free-Yoneda total for every input complex.

Implementation notes

The tower resolves K.truncLE n afresh at each stage. A good truncation of a flat-term complex need not itself have flat terms at its cutoff. The proof uses the existing mapped-tower colimit, not preservation of every filtered colimit by the free-Yoneda functor. It transports both slots of K-flatness through the canonical colimit isomorphism. This construction alone does not establish acyclicity under arbitrary nonflat scheme pullback.

References

The support bound comes from FlatResolutionTotalization.lean; the stagewise criterion is AlgebraicGeometry.Scheme.Modules.isKFlat_totalTensor_of_boundedAbove_flatTerms; colimit closure is CategoryTheory.CochainComplex.IsKFlat.colimit.

Tags

scheme-module sheaf, free-Yoneda resolution, K-flat complex, derived tensor

theorem AlgebraicGeometry.Scheme.Modules.isKFlat_freeYonedaSheafCoproductTotalComplexFunctor_obj (X : Scheme) (K : CochainComplex X.Modules ℤ) : CategoryTheory.CochainComplex.IsKFlat (totalTensor X) ((freeYonedaSheafCoproductTotalComplexFunctor X).obj K)

The canonical free-Yoneda total of every scheme-module complex is K-flat for the literal total tensor in both slots. No boundedness or flatness premise is imposed on the input.

noncomputable def AlgebraicGeometry.DerivedCategory.freeYonedaSchemeKFlatResolution (X : Scheme) : SchemeKFlatResolution X

The canonical free-Yoneda total and augmentation give a functorial K-flat resolution of every complex of scheme-module sheaves.

Equations

• One or more equations did not get rendered due to their size.