The unbounded derived tensor product on schemes

This file specializes the generic K-flat localization construction to the total tensor product of unbounded complexes of 𝒪_X-modules. A SchemeKFlatResolution X is therefore concrete data for the actual sheafified tensor bifunctor, rather than an arbitrary derived-category operation.

AlgebraicGeometry.DerivedCategory.freeYonedaSchemeKFlatResolution now gives a canonical functorial resolution for every scheme. Proving that derived tensor preserves quasicoherent cohomology and then restricting it to Dqc X remain geometric steps.

Main definitions

• AlgebraicGeometry.DerivedCategory.SchemeKFlatResolution specializes the generic resolution interface to the literal scheme-module total tensor.
• AlgebraicGeometry.DerivedCategory.SchemeKFlatResolution.derivedTensor supplies the unbounded bifunctor from a resolution.

Main results

• AlgebraicGeometry.DerivedCategory.SchemeKFlatResolution.derivedTensorFactors identifies the localized bifunctor with the resolved total tensor.

Implementation notes

The canonical free-Yoneda inhabitant is defined downstream, so this generic scheme specialization does not import its construction.

References

The underlying localization construction is CategoryTheory.KFlatResolution.derivedTensor.

Tags

scheme, derived tensor, K-flat resolution, localization

Which tensor product this is

This is the unbounded tier of the Tensor/ owner, and it is the only tier that constructs anything: the bifunctor here is built from a supplied K-flat resolution on complexes of module sheaves. The other two tiers are contracts rather than constructions.

• Tensor/BoundedCoherent.lean supplies a derived tensor on the bounded coherent derived category as a named capability. It is not obtained from this file by restriction, and must not be read as one: the bounded coherent derived category of a singular scheme is not closed under arbitrary derived tensor, so no such restriction map exists in that generality.
• Tensor/Coherent.lean adds monoidal coherence to that capability, and Tensor/Relative.lean carries the relative tier -- compatibility of a coherent tensor with derived pullback along a morphism of scheme base changes.

MO1.10 (#1321) moved this file from DerivedCategory/KFlatTensor.lean so that the three tiers sit under one owner; the declaration names are unchanged. The Dqc-level K-flat tensor stays with its own owner at DerivedCategory/Dqc/KFlatTensor.lean.

@[reducible, inline]

abbrev AlgebraicGeometry.DerivedCategory.SchemeKFlatResolution (X : Scheme) : Type (u + 1)

A functorial K-flat resolution for the total tensor product of complexes of 𝒪_X-modules.

Equations

• AlgebraicGeometry.DerivedCategory.SchemeKFlatResolution X = CategoryTheory.KFlatResolution X.Modules (AlgebraicGeometry.Scheme.Modules.totalTensor X)

noncomputable def AlgebraicGeometry.DerivedCategory.SchemeKFlatResolution.derivedTensor {X : Scheme} (R : SchemeKFlatResolution X) : CategoryTheory.Functor (SchemeDerivedCategory X) (CategoryTheory.Functor (SchemeDerivedCategory X) (SchemeDerivedCategory X))

The honest unbounded derived tensor bifunctor supplied by a K-flat resolution.

Equations

• R.derivedTensor = CategoryTheory.KFlatResolution.derivedTensor R

noncomputable def AlgebraicGeometry.DerivedCategory.SchemeKFlatResolution.derivedTensorFactors {X : Scheme} (R : SchemeKFlatResolution X) : (((CategoryTheory.Functor.whiskeringLeft₂ (SchemeDerivedCategory X)).obj (SchemeDerivedCategory.Q X)).obj (SchemeDerivedCategory.Q X)).obj R.derivedTensor ≅ CategoryTheory.KFlatResolution.resolvedTensor R

On localized complexes, the scheme derived tensor is represented by total tensor after K-flat replacement in both variables.

Equations

• R.derivedTensorFactors = CategoryTheory.KFlatResolution.derivedTensorFactors R