Derived bifunctors from K-flat resolutions

This file isolates the categorical core of the unbounded derived tensor product.

Main definitions

Given a tensor bifunctor on cochain complexes, a KFlatResolution C tensor is a functorial quasi-isomorphic replacement by objects for which tensoring in either variable sends quasi-isomorphisms to isomorphisms after derived localization.

Main results

CategoryTheory.CochainComplex.isIso_Q_map_tensorRight_of_pointwiseReplacement transports inversion across one pointwise replacement. The resolution specializes this result in both slots.

Implementation notes

Resolving both inputs makes the complex-level tensor bifunctor invert quasi-isomorphisms in both variables. CategoryTheory.Localization.lift₂ therefore constructs an honest bifunctor on the unbounded derived category, together with its comparison to the underived bifunctor.

Only a bifunctor is required here, rather than a monoidal structure on complexes: associativity, unit, and symmetry play no role in localization. Existence of K-flat resolutions is deliberately separate. Scheme-module sheaves will supply the complex tensor and its resolutions through total tensor, K-flat replacement, and descent.

References

This construction uses Mathlib's derived localization and bifunctor localization.

Tags

derived tensor, K-flat resolution, localization

def CategoryTheory.CochainComplex.IsKFlat {C : Type u} [Category.{v, u} C] [Abelian C] (tensor : Functor (CochainComplex C ℤ) (Functor (CochainComplex C ℤ) (CochainComplex C ℤ))) (K : CochainComplex C ℤ) : Prop

A cochain complex is K-flat for tensor when tensoring with it in either variable sends quasi-isomorphisms to isomorphisms after derived localization.

The two clauses are kept explicit because the supplied bifunctor need not carry a braiding. For the total tensor of complexes of modules they agree by symmetry.

Equations

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

theorem CategoryTheory.CochainComplex.IsKFlat.tensorLeft_inverts {C : Type u} [Category.{v, u} C] [Abelian C] {tensor : Functor (CochainComplex C ℤ) (Functor (CochainComplex C ℤ) (CochainComplex C ℤ))} {K : CochainComplex C ℤ} (hK : IsKFlat tensor K) : CategoryTheory.CochainComplex.W✝.IsInvertedBy ((tensor.obj K).comp DerivedCategory.Q)

Left tensoring with a K-flat complex inverts quasi-isomorphisms.

theorem CategoryTheory.CochainComplex.IsKFlat.tensorRight_inverts {C : Type u} [Category.{v, u} C] [Abelian C] {tensor : Functor (CochainComplex C ℤ) (Functor (CochainComplex C ℤ) (CochainComplex C ℤ))} {K : CochainComplex C ℤ} (hK : IsKFlat tensor K) : CategoryTheory.CochainComplex.W✝.IsInvertedBy ((tensor.flip.obj K).comp DerivedCategory.Q)

Right tensoring with a K-flat complex inverts quasi-isomorphisms.

theorem CategoryTheory.CochainComplex.IsKFlat.colimit_of_preservesHomology {J : Type w₁} [Category.{w₂, w₁} J] {C : Type u} [Category.{v, u} C] [Abelian C] [Limits.HasColimitsOfShape J C] {tensor : Functor (CochainComplex C ℤ) (Functor (CochainComplex C ℤ) (CochainComplex C ℤ))} (F : Functor J (CochainComplex C ℤ)) [∀ (i : ℤ), Limits.PreservesColimitsOfShape J (HomologicalComplex.homologyFunctor C (ComplexShape.up ℤ) i)] [∀ (L : CochainComplex C ℤ), Limits.PreservesColimit F (tensor.obj L)] [∀ (L : CochainComplex C ℤ), Limits.PreservesColimit F (tensor.flip.obj L)] (hF : ∀ (j : J), IsKFlat tensor (F.obj j)) : IsKFlat tensor (Limits.colimit F)

Homology-preserving colimits retain K-flatness when tensoring either slot preserves this diagram's colimit. The tensor maps of a quasi-isomorphism are pointwise quasi-isomorphisms, then remain so at the colimit.

theorem CategoryTheory.CochainComplex.IsKFlat.colimit {J : Type w₁} [Category.{w₂, w₁} J] {C : Type u} [Category.{v, u} C] [Abelian C] [Limits.HasColimitsOfShape J C] [HasExactColimitsOfShape J C] {tensor : Functor (CochainComplex C ℤ) (Functor (CochainComplex C ℤ) (CochainComplex C ℤ))} [∀ (L : CochainComplex C ℤ), Limits.PreservesColimitsOfShape J (tensor.obj L)] [∀ (L : CochainComplex C ℤ), Limits.PreservesColimitsOfShape J (tensor.flip.obj L)] (F : Functor J (CochainComplex C ℤ)) (hF : ∀ (j : J), IsKFlat tensor (F.obj j)) : IsKFlat tensor (Limits.colimit F)

Exact colimits commute with homology, so the homology-preserving K-flat closure applies. In an AB5 category this includes filtered diagrams once tensor preservation is supplied in both slots.

theorem CategoryTheory.CochainComplex.isIso_Q_map_tensorRight_of_pointwiseReplacement {C : Type u} [Category.{v, u} C] [Abelian C] {tensor : Functor (CochainComplex C ℤ) (Functor (CochainComplex C ℤ) (CochainComplex C ℤ))} {K L : CochainComplex C ℤ} (hK : CategoryTheory.CochainComplex.W✝.IsInvertedBy ((tensor.obj K).comp DerivedCategory.Q)) (hL : CategoryTheory.CochainComplex.W✝.IsInvertedBy ((tensor.obj L).comp DerivedCategory.Q)) (g : K ⟶ L) (hg : CategoryTheory.CochainComplex.W✝ g) (M P : CochainComplex C ℤ) (q : P ⟶ M) (hq : CategoryTheory.CochainComplex.W✝ q) (hP : CategoryTheory.CochainComplex.W✝.IsInvertedBy ((tensor.flip.obj P).comp DerivedCategory.Q)) : IsIso (DerivedCategory.Q.map ((tensor.map g).app M))

A pointwise replacement q : P ⟶ M transports right-slot tensor inversion from P to M when tensoring by either endpoint inverts q. No functorial resolution of arbitrary complexes is needed for this square.

theorem CategoryTheory.CochainComplex.quasiIso_map_of_comparison {C : Type u} [Category.{v, u} C] [Abelian C] {Res : Functor (CochainComplex C ℤ) (CochainComplex C ℤ)} (comparison : Res ⟶ Functor.id (CochainComplex C ℤ)) (hcomparison : ∀ (K : CochainComplex C ℤ), HomologicalComplex.quasiIso C (ComplexShape.up ℤ) (comparison.app K)) {K L : CochainComplex C ℤ} (f : K ⟶ L) (hf : HomologicalComplex.quasiIso C (ComplexShape.up ℤ) f) : HomologicalComplex.quasiIso C (ComplexShape.up ℤ) (Res.map f)

A functorial replacement of cochain complexes equipped with a componentwise quasi-isomorphic comparison to the identity functor preserves quasi-isomorphisms.

Only the comparison is used. No K-flatness, K-projectivity, or exactness hypothesis enters, so every functorial resolution interface in this library can reuse the statement rather than reproving it.

structure CategoryTheory.KFlatResolution (C : Type u) [Category.{v, u} C] [Abelian C] (tensor : Functor (CochainComplex C ℤ) (Functor (CochainComplex C ℤ) (CochainComplex C ℤ))) : Type (max u v)

A functorial two-sided K-flat replacement for a complex-level tensor bifunctor.

• resolution : Functor (CochainComplex C ℤ) (CochainComplex C ℤ)

  Functorial K-flat replacement.

• comparison : self.resolution ⟶ Functor.id (CochainComplex C ℤ)

  Comparison from the replacement to the original complex.

• comparison_quasiIso (K : CochainComplex C ℤ) : HomologicalComplex.quasiIso C (ComplexShape.up ℤ) (self.comparison.app K)

  Every comparison component is a quasi-isomorphism.

• isKFlat (K : CochainComplex C ℤ) : CochainComplex.IsKFlat tensor (self.resolution.obj K)

  Every replacement is K-flat for the supplied tensor bifunctor.

def CategoryTheory.KFlatResolution.comparisonApp {C : Type u} [Category.{v, u} C] [Abelian C] {tensor : Functor (CochainComplex C ℤ) (Functor (CochainComplex C ℤ) (CochainComplex C ℤ))} (R : KFlatResolution C tensor) (K : CochainComplex C ℤ) : R.resolution.obj K ⟶ K

The comparison component, with its identity-functor codomain normalized.

Equations

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

theorem CategoryTheory.KFlatResolution.comparisonApp_naturality {C : Type u} [Category.{v, u} C] [Abelian C] {tensor : Functor (CochainComplex C ℤ) (Functor (CochainComplex C ℤ) (CochainComplex C ℤ))} (R : KFlatResolution C tensor) {K L : CochainComplex C ℤ} (f : K ⟶ L) : CategoryStruct.comp (R.resolution.map f) (R.comparisonApp L) = CategoryStruct.comp (R.comparisonApp K) f

theorem CategoryTheory.KFlatResolution.comparisonApp_naturality_assoc {C : Type u} [Category.{v, u} C] [Abelian C] {tensor : Functor (CochainComplex C ℤ) (Functor (CochainComplex C ℤ) (CochainComplex C ℤ))} (R : KFlatResolution C tensor) {K L : CochainComplex C ℤ} (f : K ⟶ L) {Z : CochainComplex C ℤ} (h : L ⟶ Z) : CategoryStruct.comp (R.resolution.map f) (CategoryStruct.comp (R.comparisonApp L) h) = CategoryStruct.comp (R.comparisonApp K) (CategoryStruct.comp f h)

theorem CategoryTheory.KFlatResolution.map_quasiIso {C : Type u} [Category.{v, u} C] [Abelian C] {tensor : Functor (CochainComplex C ℤ) (Functor (CochainComplex C ℤ) (CochainComplex C ℤ))} (R : KFlatResolution C tensor) {K L : CochainComplex C ℤ} (f : K ⟶ L) (hf : CategoryTheory.KFlatResolution.W✝ f) : CategoryTheory.KFlatResolution.W✝ (R.resolution.map f)

A K-flat replacement functor preserves quasi-isomorphisms.

theorem CategoryTheory.KFlatResolution.isIso_Q_map_tensorRight_of_inverts {C : Type u} [Category.{v, u} C] [Abelian C] {tensor : Functor (CochainComplex C ℤ) (Functor (CochainComplex C ℤ) (CochainComplex C ℤ))} (R : KFlatResolution C tensor) {K L : CochainComplex C ℤ} (hK : CategoryTheory.KFlatResolution.W✝.IsInvertedBy ((tensor.obj K).comp DerivedCategory.Q)) (hL : CategoryTheory.KFlatResolution.W✝.IsInvertedBy ((tensor.obj L).comp DerivedCategory.Q)) (g : K ⟶ L) (hg : CategoryTheory.KFlatResolution.W✝ g) (M : CochainComplex C ℤ) : IsIso (DerivedCategory.Q.map ((tensor.map g).app M))

The K-flat resolution supplies a pointwise replacement for right-slot tensor transport; only the left-inversion clauses at the two endpoints are needed.

theorem CategoryTheory.KFlatResolution.isIso_Q_map_tensorLeft_of_inverts {C : Type u} [Category.{v, u} C] [Abelian C] {tensor : Functor (CochainComplex C ℤ) (Functor (CochainComplex C ℤ) (CochainComplex C ℤ))} (R : KFlatResolution C tensor) {K L : CochainComplex C ℤ} (hK : CategoryTheory.KFlatResolution.W✝.IsInvertedBy ((tensor.flip.obj K).comp DerivedCategory.Q)) (hL : CategoryTheory.KFlatResolution.W✝.IsInvertedBy ((tensor.flip.obj L).comp DerivedCategory.Q)) (g : K ⟶ L) (hg : CategoryTheory.KFlatResolution.W✝ g) (M : CochainComplex C ℤ) : IsIso (DerivedCategory.Q.map ((tensor.obj M).map g))

The flipped pointwise transport gives left-slot tensor inversion; only the right-inversion clauses at the two endpoints are needed.

noncomputable def CategoryTheory.KFlatResolution.resolvedTensor {C : Type u} [Category.{v, u} C] [Abelian C] {tensor : Functor (CochainComplex C ℤ) (Functor (CochainComplex C ℤ) (CochainComplex C ℤ))} (R : KFlatResolution C tensor) : Functor (CochainComplex C ℤ) (Functor (CochainComplex C ℤ) (DerivedCategory C))

Apply tensor after K-flat replacement in both inputs and then localize.

Equations

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

@[simp]

theorem CategoryTheory.KFlatResolution.resolvedTensor_obj_obj {C : Type u} [Category.{v, u} C] [Abelian C] {tensor : Functor (CochainComplex C ℤ) (Functor (CochainComplex C ℤ) (CochainComplex C ℤ))} (R : KFlatResolution C tensor) (K L : CochainComplex C ℤ) : (R.resolvedTensor.obj K).obj L = DerivedCategory.Q.obj ((tensor.obj (R.resolution.obj K)).obj (R.resolution.obj L))

theorem CategoryTheory.KFlatResolution.resolvedTensor_inverts {C : Type u} [Category.{v, u} C] [Abelian C] {tensor : Functor (CochainComplex C ℤ) (Functor (CochainComplex C ℤ) (CochainComplex C ℤ))} (R : KFlatResolution C tensor) : CategoryTheory.KFlatResolution.W✝.IsInvertedBy₂ CategoryTheory.KFlatResolution.W✝ R.resolvedTensor

Resolving both variables makes tensor invert quasi-isomorphisms in both variables.

noncomputable def CategoryTheory.KFlatResolution.derivedTensor {C : Type u} [Category.{v, u} C] [Abelian C] {tensor : Functor (CochainComplex C ℤ) (Functor (CochainComplex C ℤ) (CochainComplex C ℤ))} (R : KFlatResolution C tensor) : Functor (DerivedCategory C) (Functor (DerivedCategory C) (DerivedCategory C))

The unbounded derived bifunctor constructed by resolving both inputs and descending through quasi-isomorphism localization.

Equations

• R.derivedTensor = CategoryTheory.Localization.lift₂ R.resolvedTensor ⋯ DerivedCategory.Q DerivedCategory.Q

noncomputable def CategoryTheory.KFlatResolution.derivedTensorFactors {C : Type u} [Category.{v, u} C] [Abelian C] {tensor : Functor (CochainComplex C ℤ) (Functor (CochainComplex C ℤ) (CochainComplex C ℤ))} (R : KFlatResolution C tensor) : (((Functor.whiskeringLeft₂ (DerivedCategory C)).obj DerivedCategory.Q).obj DerivedCategory.Q).obj R.derivedTensor ≅ R.resolvedTensor

Pulling the derived bifunctor back to complexes recovers resolved tensor.

Equations

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

noncomputable def CategoryTheory.KFlatResolution.resolvedTensorComparison {C : Type u} [Category.{v, u} C] [Abelian C] {tensor : Functor (CochainComplex C ℤ) (Functor (CochainComplex C ℤ) (CochainComplex C ℤ))} (R : KFlatResolution C tensor) : R.resolvedTensor ⟶ tensor.comp ((Functor.whiskeringRight (CochainComplex C ℤ) (CochainComplex C ℤ) (DerivedCategory C)).obj DerivedCategory.Q)

The natural comparison from resolved tensor to the original bifunctor followed by derived localization.

Equations

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

noncomputable def CategoryTheory.KFlatResolution.derivedTensorCounit {C : Type u} [Category.{v, u} C] [Abelian C] {tensor : Functor (CochainComplex C ℤ) (Functor (CochainComplex C ℤ) (CochainComplex C ℤ))} (R : KFlatResolution C tensor) : (((Functor.whiskeringLeft₂ (DerivedCategory C)).obj DerivedCategory.Q).obj DerivedCategory.Q).obj R.derivedTensor ⟶ tensor.comp ((Functor.whiskeringRight (CochainComplex C ℤ) (CochainComplex C ℤ) (DerivedCategory C)).obj DerivedCategory.Q)

Comparison from the derived bifunctor evaluated on localized complexes to the original bifunctor followed by localization.

Equations

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