A left-derived tensor interface on scheme-module complexes

Main definitions

• TensorAcyclicResolution packages a functorial tensor-acyclic replacement and the one-sided comparison data needed for both fixed-argument universal properties.
• LeftDerivedTensor is the actual bifunctor on the localized derived category, with a counit and Mathlib's Functor.IsLeftDerivedFunctor field in each variable.
• singleComplex and singleLeftTensorIso identify tensoring against a degree-zero left factor with the induced complex functor.

Main results

TensorAcyclicResolution.toLeftDerivedTensor proves both universal properties from the resolution data. exactLeftFunctor and fixedLeftComparison expose the exact invertible-left-factor case, while ofTensorInverts remains the separate genuinely two-variable identity-resolution construction.

Implementation notes

Mathlib's derived-functor API is single-variable only. The bifunctor interface therefore states the universal property once for each fixed complex. The exact fixed-left comparison is proved through the existing exact functor on module sheaves and the single-complex tensor comparison; it does not assert that arbitrary tensor factors preserve quasi-isomorphisms.

This module owns the localization-facing interface for the unbounded tensor product. It does not assert a monoidal structure on either complexes or the derived category.

There are two tempting routes which are deliberately recorded here as dead ends. First, MorphismProperty.IsMonoidal W (see Mathlib/CategoryTheory/Localization/Monoidal/Basic.lean:44) requires whiskering every W-morphism on the left by every object. For quasi-isomorphisms this is false: tensoring the quasi-isomorphism [𝒪 →ˢ 𝒪] → 𝒪/s with 𝒪/s produces homology in two degrees. Thus IsMonoidal quasiIso is neither proved nor carried as a field here; K-flat replacement exists precisely because this naive localization-descent route is unavailable. In particular, the dependent functorMonoidalOfComp route (Localization/Monoidal/Functor.lean:134) is unavailable too, since it requires a monoidal localized functor.

Second, HomologicalComplex.monoidalCategory (Mathlib/Algebra/Homology/Monoidal.lean:274-281) requires [∀ (X₁ X₂ : GradedObject I C), GradedObject.HasTensor X₁ X₂]. For I = ℤ this asks for coproducts over countably infinite anti-diagonals, whereas Coh X has only finite biproducts. Mathlib's worked example in that file is ChainComplex D ℕ, whose anti-diagonals are finite; there is no ℤ-indexed instance at this pin. Accordingly no declaration below asserts either of those dead routes.

TensorAcyclicResolution is a tensor-specific interface around the already-existing generic K-flat localization construction. Its two resolved-comparison fields are intentional: a generic two-sided K-flat replacement proves the localized bifunctor, but does not by itself make the comparison for an arbitrary fixed, non-K-flat factor invertible after resolving only the other factor. The missing comparison is therefore a hypothesis, not a marker or an axiom.

References

• Mathlib/CategoryTheory/Functor/Derived/LeftDerived.lean
• Mathlib/CategoryTheory/Localization/Bifunctor.lean
• DerivedAlgGeo/AlgebraicGeometry/DerivedCategory/Families/PullbackAcyclicResolution.lean
• DerivedAlgGeo/AlgebraicGeometry/Modules/Tensor/Invertible.lean

Tags

localization, left-derived-functor, tensor, K-flat, quasi-isomorphism

@[reducible, inline]

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

The complexes used by the unbounded scheme tensor interface.

Equations

• AlgebraicGeometry.DerivedCategory.SchemeTensorComplex X = CochainComplex X.Modules ℤ

@[reducible, inline]

abbrev AlgebraicGeometry.DerivedCategory.SchemeTensorQuasiIso (X : Scheme) : CategoryTheory.MorphismProperty (SchemeTensorComplex X)

The quasi-isomorphisms used by the unbounded scheme tensor interface.

Equations

• AlgebraicGeometry.DerivedCategory.SchemeTensorQuasiIso X = HomologicalComplex.quasiIso X.Modules (ComplexShape.up ℤ)

@[reducible, inline]

noncomputable abbrev AlgebraicGeometry.DerivedCategory.singleComplex (X : Scheme) (L : X.Modules) : SchemeTensorComplex X

The degree-zero complex used to expose an exact fixed left tensor factor.

Equations

• AlgebraicGeometry.DerivedCategory.singleComplex X L = (HomologicalComplex.single X.Modules (ComplexShape.up ℤ) 0).obj L

noncomputable def AlgebraicGeometry.DerivedCategory.singleLeftTensorIso (X : Scheme) (L : X.Modules) : (Scheme.Modules.totalTensor X).obj (singleComplex X L) ≅ L.tensorLeftFunctor.mapHomologicalComplex (ComplexShape.up ℤ)

The comparison between tensoring by a degree-zero complex and the corresponding fixed-left functor on complexes. The component proof uses the actual total-complex coproduct and is natural in the remaining complex argument. It holds for every module sheaf L, since tensoring by L is additive; it does not assume that arbitrary tensor factors preserve quasi-isomorphisms.

Equations

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

noncomputable def AlgebraicGeometry.DerivedCategory.exactLeftFunctor (X : Scheme) (L : X.Modules) [(have this := L; this).IsInvertible] : CategoryTheory.Functor (SchemeDerivedCategory X) (SchemeDerivedCategory X)

The derived functor induced by tensoring on the left with an invertible module sheaf.

Equations

• AlgebraicGeometry.DerivedCategory.exactLeftFunctor X L = L.tensorLeftFunctor.mapDerivedCategory

noncomputable def AlgebraicGeometry.DerivedCategory.exactLeftCounit (X : Scheme) (L : X.Modules) [(have this := L; this).IsInvertible] : (SchemeDerivedCategory.Q X).comp (exactLeftFunctor X L) ⟶ ((Scheme.Modules.totalTensor X).obj (singleComplex X L)).comp (SchemeDerivedCategory.Q X)

The counit comparing the exact fixed-left derived functor with total tensor on a degree-zero left factor.

Equations

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

instance AlgebraicGeometry.DerivedCategory.exactLeftCounit_isIso (X : Scheme) (L : X.Modules) [(have this := L; this).IsInvertible] : CategoryTheory.IsIso (exactLeftCounit X L)

theorem AlgebraicGeometry.DerivedCategory.exactLeftIsLeftDerived (X : Scheme) (L : X.Modules) [(have this := L; this).IsInvertible] : (exactLeftFunctor X L).IsLeftDerivedFunctor (exactLeftCounit X L) (SchemeTensorQuasiIso X)

The exact fixed-left adapter is a left-derived functor for the total tensor restricted to a degree-zero invertible left factor.

structure AlgebraicGeometry.DerivedCategory.TensorAcyclicResolution (X : Scheme) : Type (u + 1)

A tensor-acyclic replacement of complexes of 𝒪_X-modules.

The first four fields are the functorial replacement, its quasi-isomorphic comparison, and the two-sided localization-inversion datum needed by Localization.lift₂. The last two fields are the one-sided acyclicity needed for the two fixed-argument left-derived universal properties. They are stronger than the generic KFlatResolution fields in exactly the place where a fixed arbitrary tensor factor need not preserve quasi-isomorphisms.

• resolution : CategoryTheory.Functor (SchemeTensorComplex X) (SchemeTensorComplex X)

  Functorial replacement of complexes.

• comparison : self.resolution ⟶ CategoryTheory.Functor.id (SchemeTensorComplex X)

  Comparison from the replacement to the original complex.

• comparison_quasiIso (K : SchemeTensorComplex X) : SchemeTensorQuasiIso X (self.comparison.app K)

  Every comparison component is a quasi-isomorphism.

• tensor_inverts : (SchemeTensorQuasiIso X).IsInvertedBy₂ (SchemeTensorQuasiIso X) (self.resolution.comp ((Scheme.Modules.totalTensor X).comp (((CategoryTheory.Functor.whiskeringLeft (SchemeTensorComplex X) (CochainComplex X.Modules ℤ) (CochainComplex X.Modules ℤ)).obj self.resolution).comp ((CategoryTheory.Functor.whiskeringRight (SchemeTensorComplex X) (CochainComplex X.Modules ℤ) (SchemeDerivedCategory X)).obj (SchemeDerivedCategory.Q X)))))

  Resolving both inputs makes total tensor invert quasi-isomorphisms after localization.

• left_resolved_comparison_isIso (K L : SchemeTensorComplex X) : CategoryTheory.IsIso ((SchemeDerivedCategory.Q X).map (CategoryTheory.CategoryStruct.comp (((Scheme.Modules.totalTensor X).map (self.comparison.app K)).app (self.resolution.obj (self.resolution.obj L))) (((Scheme.Modules.totalTensor X).obj K).map (self.comparison.app (self.resolution.obj L)))))

  The comparison is acyclic for a fixed first argument after resolving the second twice.

• right_resolved_comparison_isIso (K L : SchemeTensorComplex X) : CategoryTheory.IsIso ((SchemeDerivedCategory.Q X).map (CategoryTheory.CategoryStruct.comp (((Scheme.Modules.totalTensor X).map (self.comparison.app (self.resolution.obj K))).app (self.resolution.obj L)) (((Scheme.Modules.totalTensor X).obj (self.resolution.obj K)).map (self.comparison.app L))))

  The comparison is acyclic for a fixed second argument after resolving the first.

noncomputable def AlgebraicGeometry.DerivedCategory.TensorAcyclicResolution.resolvedTensor {X : Scheme} (R : TensorAcyclicResolution X) : CategoryTheory.Functor (SchemeTensorComplex X) (CategoryTheory.Functor (SchemeTensorComplex X) (SchemeDerivedCategory X))

The resolved tensor functor belonging to an acyclic resolution.

Equations

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

def AlgebraicGeometry.DerivedCategory.TensorAcyclicResolution.comparisonApp {X : Scheme} (R : TensorAcyclicResolution X) (K : SchemeTensorComplex X) : R.resolution.obj K ⟶ K

The comparison component with the identity functor normalized.

Equations

• R.comparisonApp K = R.comparison.app K

theorem AlgebraicGeometry.DerivedCategory.TensorAcyclicResolution.comparisonApp_naturality {X : Scheme} (R : TensorAcyclicResolution X) {K L : SchemeTensorComplex X} (f : K ⟶ L) : CategoryTheory.CategoryStruct.comp (R.resolution.map f) (R.comparisonApp L) = CategoryTheory.CategoryStruct.comp (R.comparisonApp K) f

Naturality of the normalized replacement-to-identity comparison, used below to move a map through the resolved tensor before applying the localization comparison.

theorem AlgebraicGeometry.DerivedCategory.TensorAcyclicResolution.comparisonApp_naturality_assoc {X : Scheme} (R : TensorAcyclicResolution X) {K L : SchemeTensorComplex X} (f : K ⟶ L) {Z : SchemeTensorComplex X} (h : L ⟶ Z) : CategoryTheory.CategoryStruct.comp (R.resolution.map f) (CategoryTheory.CategoryStruct.comp (R.comparisonApp L) h) = CategoryTheory.CategoryStruct.comp (R.comparisonApp K) (CategoryTheory.CategoryStruct.comp f h)

Naturality of the normalized replacement-to-identity comparison, used below to move a map through the resolved tensor before applying the localization comparison.

noncomputable def AlgebraicGeometry.DerivedCategory.TensorAcyclicResolution.resolvedTensorComparison {X : Scheme} (R : TensorAcyclicResolution X) : R.resolvedTensor ⟶ (Scheme.Modules.totalTensor X).comp ((CategoryTheory.Functor.whiskeringRight (CochainComplex X.Modules ℤ) (CochainComplex X.Modules ℤ) (SchemeDerivedCategory X)).obj (SchemeDerivedCategory.Q X))

The comparison from resolved total tensor to ordinary total tensor followed by localization.

Equations

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

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

The bifunctor on the derived category obtained by resolving both variables.

Equations

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

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

Pulling the derived tensor back to complexes recovers the resolved tensor.

Equations

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

noncomputable def AlgebraicGeometry.DerivedCategory.TensorAcyclicResolution.counit {X : Scheme} (R : TensorAcyclicResolution X) : (((CategoryTheory.Functor.whiskeringLeft₂ (SchemeDerivedCategory X)).obj (SchemeDerivedCategory.Q X)).obj (SchemeDerivedCategory.Q X)).obj R.derivedTensor ⟶ (Scheme.Modules.totalTensor X).comp ((CategoryTheory.Functor.whiskeringRight (CochainComplex X.Modules ℤ) (CochainComplex X.Modules ℤ) (SchemeDerivedCategory X)).obj (SchemeDerivedCategory.Q X))

The counit from the localized derived tensor to degreewise total tensor.

Equations

• R.counit = CategoryTheory.CategoryStruct.comp R.derivedTensorFactors.hom R.resolvedTensorComparison

structure AlgebraicGeometry.DerivedCategory.LeftDerivedTensor (X : Scheme) : Type (u + 1)

A genuine bifunctorial left-derived tensor on the unbounded scheme-derived category.

The two universal-property fields are deliberately indexed by complexes representing the fixed argument. This makes the comparison against the actual degreewise tensor visible and prevents an unrelated bifunctor from satisfying the interface.

• functor : CategoryTheory.Functor (SchemeDerivedCategory X) (CategoryTheory.Functor (SchemeDerivedCategory X) (SchemeDerivedCategory X))

  The derived tensor bifunctor.

• counit : (((CategoryTheory.Functor.whiskeringLeft₂ (SchemeDerivedCategory X)).obj (SchemeDerivedCategory.Q X)).obj (SchemeDerivedCategory.Q X)).obj self.functor ⟶ (Scheme.Modules.totalTensor X).comp ((CategoryTheory.Functor.whiskeringRight (CochainComplex X.Modules ℤ) (CochainComplex X.Modules ℤ) (SchemeDerivedCategory X)).obj (SchemeDerivedCategory.Q X))

  Comparison from localization followed by the derived tensor to degreewise total tensor.

• isLeftDerived_left (K : SchemeTensorComplex X) : (self.functor.obj ((SchemeDerivedCategory.Q X).obj K)).IsLeftDerivedFunctor (self.counit.app K) (SchemeTensorQuasiIso X)

  The fixed-first-argument left-derived universal property.

• isLeftDerived_right (L : SchemeTensorComplex X) : (self.functor.flip.obj ((SchemeDerivedCategory.Q X).obj L)).IsLeftDerivedFunctor (CategoryTheory.NatTrans.flipApp self.counit L) (SchemeTensorQuasiIso X)

  The fixed-second-argument left-derived universal property.

noncomputable def AlgebraicGeometry.DerivedCategory.TensorAcyclicResolution.toLeftDerivedTensor {X : Scheme} (R : TensorAcyclicResolution X) : LeftDerivedTensor X

A tensor-acyclic resolution constructs the bifunctor and proves both fixed-argument universal properties.

Equations

• R.toLeftDerivedTensor = { functor := R.derivedTensor, counit := R.counit, isLeftDerived_left := ⋯, isLeftDerived_right := ⋯ }

noncomputable def AlgebraicGeometry.DerivedCategory.LeftDerivedTensor.leftDerivedUnique {X : Scheme} (P Q : LeftDerivedTensor X) (K : SchemeTensorComplex X) : P.functor.obj ((SchemeDerivedCategory.Q X).obj K) ≅ Q.functor.obj ((SchemeDerivedCategory.Q X).obj K)

The canonical comparison of two left-derived tensors, for a fixed complex representative.

It is the unique comparison induced by their common counit to Scheme.Modules.totalTensor X after applying Functor.leftDerivedUnique to the fixed-first argument functors.

Equations

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

noncomputable def AlgebraicGeometry.DerivedCategory.LeftDerivedTensor.fixedLeftComparison {X : Scheme} (P : LeftDerivedTensor X) (L : X.Modules) [(have this := L; this).IsInvertible] : P.functor.obj ((SchemeDerivedCategory.Q X).obj (singleComplex X L)) ≅ exactLeftFunctor X L

The fixed-left comparison with the exact functor induced by an invertible module sheaf.

Equations

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

noncomputable def AlgebraicGeometry.DerivedCategory.LeftDerivedTensor.leftDerivedUniqueFlip {X : Scheme} (P Q : LeftDerivedTensor X) (L : SchemeTensorComplex X) : P.functor.flip.obj ((SchemeDerivedCategory.Q X).obj L) ≅ Q.functor.flip.obj ((SchemeDerivedCategory.Q X).obj L)

The analogous comparison after fixing the second argument. It uses the common counit and Functor.leftDerivedUnique for the fixed-second-variable functors.

Equations

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

noncomputable def AlgebraicGeometry.DerivedCategory.TensorAcyclicResolution.ofTensorInverts (X : Scheme) (hTensor : (SchemeTensorQuasiIso X).IsInvertedBy₂ (SchemeTensorQuasiIso X) ((Scheme.Modules.totalTensor X).comp ((CategoryTheory.Functor.whiskeringRight (CochainComplex X.Modules ℤ) (CochainComplex X.Modules ℤ) (SchemeDerivedCategory X)).obj (SchemeDerivedCategory.Q X)))) : TensorAcyclicResolution X

The identity resolution is available only when the supplied tensor already inverts both variables' quasi-isomorphisms after localization.

Equations

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

@[reducible, inline]

noncomputable abbrev AlgebraicGeometry.DerivedCategory.TensorAcyclicResolution.identity (X : Scheme) (hTensor : (SchemeTensorQuasiIso X).IsInvertedBy₂ (SchemeTensorQuasiIso X) ((Scheme.Modules.totalTensor X).comp ((CategoryTheory.Functor.whiskeringRight (CochainComplex X.Modules ℤ) (CochainComplex X.Modules ℤ) (SchemeDerivedCategory X)).obj (SchemeDerivedCategory.Q X)))) : TensorAcyclicResolution X

Compatibility name for the exact identity resolution.

Equations

• AlgebraicGeometry.DerivedCategory.TensorAcyclicResolution.identity X hTensor = AlgebraicGeometry.DerivedCategory.TensorAcyclicResolution.ofTensorInverts X hTensor

def AlgebraicGeometry.DerivedCategory.TensorAcyclicResolution.ofKFlat {X : Scheme} (R : SchemeKFlatResolution X) (hleft : ∀ (K L : SchemeTensorComplex X), CategoryTheory.IsIso ((SchemeDerivedCategory.Q X).map (CategoryTheory.CategoryStruct.comp (((Scheme.Modules.totalTensor X).map (R.comparison.app K)).app (R.resolution.obj (R.resolution.obj L))) (((Scheme.Modules.totalTensor X).obj K).map (R.comparison.app (R.resolution.obj L)))))) : TensorAcyclicResolution X

Adapt the generic SchemeKFlatResolution. The explicit left acyclicity hypothesis is the additional comparison that generic K-flatness does not provide for an arbitrary fixed factor.

Equations

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

noncomputable def AlgebraicGeometry.DerivedCategory.TensorAcyclicResolution.exactComparison {X : Scheme} (R : TensorAcyclicResolution X) (hTensor : (SchemeTensorQuasiIso X).IsInvertedBy₂ (SchemeTensorQuasiIso X) ((Scheme.Modules.totalTensor X).comp ((CategoryTheory.Functor.whiskeringRight (CochainComplex X.Modules ℤ) (CochainComplex X.Modules ℤ) (SchemeDerivedCategory X)).obj (SchemeDerivedCategory.Q X)))) (K : SchemeTensorComplex X) : R.toLeftDerivedTensor.functor.obj ((SchemeDerivedCategory.Q X).obj K) ≅ (ofTensorInverts X hTensor).toLeftDerivedTensor.functor.obj ((SchemeDerivedCategory.Q X).obj K)

A general resolution and the exact identity construction agree by the fixed-argument Functor.leftDerivedUnique comparison.

Equations

• R.exactComparison hTensor K = R.toLeftDerivedTensor.leftDerivedUnique (AlgebraicGeometry.DerivedCategory.TensorAcyclicResolution.ofTensorInverts X hTensor).toLeftDerivedTensor K

theorem AlgebraicGeometry.DerivedCategory.TensorAcyclicResolution.exactComparison_hom_counit {X : Scheme} (R : TensorAcyclicResolution X) (hTensor : (SchemeTensorQuasiIso X).IsInvertedBy₂ (SchemeTensorQuasiIso X) ((Scheme.Modules.totalTensor X).comp ((CategoryTheory.Functor.whiskeringRight (CochainComplex X.Modules ℤ) (CochainComplex X.Modules ℤ) (SchemeDerivedCategory X)).obj (SchemeDerivedCategory.Q X)))) (K : SchemeTensorComplex X) : CategoryTheory.CategoryStruct.comp ((SchemeDerivedCategory.Q X).whiskerLeft (R.exactComparison hTensor K).hom) ((ofTensorInverts X hTensor).toLeftDerivedTensor.counit.app K) = R.toLeftDerivedTensor.counit.app K

The exact identity comparison intertwines the two constructions' common tensor counits. The proof is the Functor.leftDerivedNatTrans_fac equation for the universal-property comparison, specialized to the identity natural transformation of the ordinary tensor target.

theorem AlgebraicGeometry.DerivedCategory.TensorAcyclicResolution.exactComparison_hom_counit_assoc {X : Scheme} (R : TensorAcyclicResolution X) (hTensor : (SchemeTensorQuasiIso X).IsInvertedBy₂ (SchemeTensorQuasiIso X) ((Scheme.Modules.totalTensor X).comp ((CategoryTheory.Functor.whiskeringRight (CochainComplex X.Modules ℤ) (CochainComplex X.Modules ℤ) (SchemeDerivedCategory X)).obj (SchemeDerivedCategory.Q X)))) (K : SchemeTensorComplex X) {Z : CategoryTheory.Functor (CochainComplex X.Modules ℤ) (SchemeDerivedCategory X)} (h : ((Scheme.Modules.totalTensor X).comp ((CategoryTheory.Functor.whiskeringRight (CochainComplex X.Modules ℤ) (CochainComplex X.Modules ℤ) (SchemeDerivedCategory X)).obj (SchemeDerivedCategory.Q X))).obj K ⟶ Z) : CategoryTheory.CategoryStruct.comp ((SchemeDerivedCategory.Q X).whiskerLeft (R.exactComparison hTensor K).hom) (CategoryTheory.CategoryStruct.comp ((ofTensorInverts X hTensor).toLeftDerivedTensor.counit.app K) h) = CategoryTheory.CategoryStruct.comp (R.toLeftDerivedTensor.counit.app K) h

The exact identity comparison intertwines the two constructions' common tensor counits. The proof is the Functor.leftDerivedNatTrans_fac equation for the universal-property comparison, specialized to the identity natural transformation of the ordinary tensor target.