K-flat derived tensor on Dqc

A scheme K-flat resolution already constructs an honest derived tensor on the ambient derived category of all module sheaves. This file isolates the remaining geometric preservation statement and, from that evidence, restricts the bifunctor to the full subcategory with quasicoherent cohomology.

No unrelated tensor operation can inhabit this interface: the restricted bifunctor is built by ObjectProperty.lift₂ from SchemeKFlatResolution.derivedTensor, and forgetting the property witnesses recovers that ambient bifunctor definitionally.

def AlgebraicGeometry.DerivedCategory.SchemeKFlatResolution.PreservesQuasicoherentCohomology {X : Scheme} (R : SchemeKFlatResolution X) : Prop

The geometric condition needed for a K-flat derived tensor to restrict to Dqc(X).

Equations

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

def AlgebraicGeometry.DerivedCategory.SchemeKFlatResolution.ResolvedTensorPreservesQuasicoherentCohomology {X : Scheme} (R : SchemeKFlatResolution X) : Prop

A representative-level criterion for quasicoherence preservation. It asks only about the actual total tensor of the functorial K-flat replacements of two complexes.

Equations

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

theorem AlgebraicGeometry.DerivedCategory.SchemeKFlatResolution.preservesQuasicoherentCohomology_of_resolvedTensor {X : Scheme} (R : SchemeKFlatResolution X) (hR : R.ResolvedTensorPreservesQuasicoherentCohomology) : R.PreservesQuasicoherentCohomology

Quasicoherence preservation for the derived tensor follows from the corresponding claim on resolved complex representatives. Essential surjectivity of derived localization supplies the representatives, and derivedTensorFactors identifies their derived tensor with resolved total tensor.

noncomputable def AlgebraicGeometry.DerivedCategory.SchemeKFlatResolution.derivedTensorToDqc {X : Scheme} (R : SchemeKFlatResolution X) (hR : R.PreservesQuasicoherentCohomology) : CategoryTheory.Functor (Dqc.SchemeQuasicoherentDerivedCategory X) (CategoryTheory.Functor (Dqc.SchemeQuasicoherentDerivedCategory X) (Dqc.SchemeQuasicoherentDerivedCategory X))

Restrict the K-flat derived tensor to the honest quasicoherent-cohomology locus.

Equations

• R.derivedTensorToDqc hR = (AlgebraicGeometry.DerivedCategory.Dqc.schemeQuasicoherentCohomology X).lift₂ R.derivedTensor hR

@[simp]

theorem AlgebraicGeometry.DerivedCategory.SchemeKFlatResolution.derivedTensorToDqc_obj_obj_obj {X : Scheme} (R : SchemeKFlatResolution X) (hR : R.PreservesQuasicoherentCohomology) (E F : Dqc.SchemeQuasicoherentDerivedCategory X) : (((R.derivedTensorToDqc hR).obj E).obj F).obj = (R.derivedTensor.obj E.obj).obj F.obj

def AlgebraicGeometry.DerivedCategory.SchemeKFlatResolution.PreservesCompactObjects {X : Scheme} (R : SchemeKFlatResolution X) (hR : R.PreservesQuasicoherentCohomology) : Prop

The compactness condition needed in base-change constructions: the restricted K-flat tensor of two compact Dqc(X) objects is compact.

Equations

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

def AlgebraicGeometry.DerivedCategory.SchemeKFlatResolution.ResolvedTensorPreservesCompactObjects {X : Scheme} (R : SchemeKFlatResolution X) (hR : R.ResolvedTensorPreservesQuasicoherentCohomology) : Prop

A representative-level compactness criterion. The quasicoherence hypothesis gives the resolved total tensor an object of Dqc(X); compactness then only has to be checked on such objects coming directly from complexes.

Equations

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

theorem AlgebraicGeometry.DerivedCategory.SchemeKFlatResolution.preservesCompactObjects_of_resolvedTensor {X : Scheme} (R : SchemeKFlatResolution X) (hqc : R.ResolvedTensorPreservesQuasicoherentCohomology) (hcompact : R.ResolvedTensorPreservesCompactObjects hqc) : R.PreservesCompactObjects ⋯

Compactness preservation for the restricted derived tensor follows from the corresponding claim on resolved complex representatives.

noncomputable def AlgebraicGeometry.DerivedCategory.SchemeKFlatResolution.derivedTensorToDqcCompInclusion {X : Scheme} (R : SchemeKFlatResolution X) (hR : R.PreservesQuasicoherentCohomology) : (R.derivedTensorToDqc hR).comp ((CategoryTheory.Functor.whiskeringRight (Dqc.SchemeQuasicoherentDerivedCategory X) (Dqc.SchemeQuasicoherentDerivedCategory X) (SchemeDerivedCategory X)).obj (Dqc.SchemeQuasicoherentDerivedCategory.ι X)) ≅ (Dqc.SchemeQuasicoherentDerivedCategory.ι X).comp (R.derivedTensor.comp ((CategoryTheory.Functor.whiskeringLeft (Dqc.SchemeQuasicoherentDerivedCategory X) (SchemeDerivedCategory X) (SchemeDerivedCategory X)).obj (Dqc.SchemeQuasicoherentDerivedCategory.ι X)))

Forgetting the Dqc witnesses recovers the ambient K-flat derived tensor restricted along the two inclusions.

Equations

• R.derivedTensorToDqcCompInclusion hR = (AlgebraicGeometry.DerivedCategory.Dqc.schemeQuasicoherentCohomology X).lift₂CompιIso R.derivedTensor hR