The graded bimodule action on homotopy categories

For graded algebras A and B, the balanced tensor product M ⊗_B N of a graded (A, B)-bimodule M and a graded left B-module N (TauCeti.GradedModuleCat.bimoduleModuleTensor) totalizes to cochain complexes and descends to a bifunctor

K(grBimod (A, B)) ⥤ K(grMod B) ⥤ K(grMod A)

on homotopy categories of unbounded cochain complexes (CategoryTheory.Functor.map₂HomotopyCategory). The required total complexes exist because graded modules have all coproducts, and the action preserves coproducts in each variable, which supplies the hypotheses of Mathlib's associator for totalized bifunctors.

This file records the two structure isomorphisms of this action on homotopy categories:

• the regular graded bimodule A, placed in cohomological degree zero, acts as the identity functor of K(grMod A);
• acting by the total tensor product K₁ ⊗_B K₂ of two complexes of graded bimodules is isomorphic to acting by K₂ and then by K₁.

Together with the invariance of the action under homotopy equivalences of complexes of bimodules, these isomorphisms let a complex of bimodules with a two-sided tensor inverse up to homotopy act by an equivalence between homotopy categories of graded modules (TauCeti.GradedModuleCat.bimoduleModuleTensorHomotopyEquivalence); for instance, the braid complexes of a zigzag algebra act by autoequivalences.

Main definitions

• TauCeti.GradedModuleCat.bimoduleModuleTensorHomotopy: the action bifunctor on homotopy categories.
• TauCeti.GradedModuleCat.bimoduleModuleTensorHomotopyLeftUnitor: the regular bimodule in degree zero acts as the identity.
• TauCeti.GradedModuleCat.bimoduleModuleTensorHomotopyAssociator: acting by a total tensor product of complexes of bimodules is acting by its two factors in turn.
• TauCeti.GradedModuleCat.bimoduleModuleTensorHomotopyEquivalence: a complex of bimodules with a two-sided tensor inverse up to homotopy acts by an equivalence.

References

• M. Khovanov and P. Seidel, Quivers, Floer cohomology, and braid group actions, J. Amer. Math. Soc. 15 (2002), Section 2, for the action of complexes of bimodules on homotopy categories of modules by tensor product.

@[reducible, inline]

noncomputable abbrev TauCeti.GradedModuleCat.bimoduleModuleTensorHomotopy {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] {B : Type uB} [Ring B] [Algebra k B] (Γ : InternalGrading k A ℤ) (Δ : InternalGrading k B ℤ) [GradedAlgebra (Γ.piece ℤ)] [GradedAlgebra (Δ.piece ℤ)] : CategoryTheory.Functor (HomotopyCategory (GradedModuleCat ((Γ.tensorProduct Δ.opposite).piece ℤ)) (ComplexShape.up ℤ)) (CategoryTheory.Functor (HomotopyCategory (GradedModuleCat (Δ.piece ℤ)) (ComplexShape.up ℤ)) (HomotopyCategory (GradedModuleCat (Γ.piece ℤ)) (ComplexShape.up ℤ)))

The action of complexes of graded (A, B)-bimodules on the homotopy category of cochain complexes of graded B-modules: the totalized balanced tensor product K ⊗_B L, which only depends on K and L up to homotopy.

@[reducible, inline]

noncomputable abbrev TauCeti.GradedModuleCat.bimoduleModuleTensorHomotopyLeftUnitor {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] (Γ : InternalGrading k A ℤ) [GradedAlgebra (Γ.piece ℤ)] : (bimoduleModuleTensorHomotopy Γ Γ).obj ((HomotopyCategory.quotient (GradedModuleCat ((Γ.tensorProduct Γ.opposite).piece ℤ)) (ComplexShape.up ℤ)).obj ((HomologicalComplex.single (GradedModuleCat ((Γ.tensorProduct Γ.opposite).piece ℤ)) (ComplexShape.up ℤ) 0).obj (bimoduleUnit Γ))) ≅ CategoryTheory.Functor.id (HomotopyCategory (GradedModuleCat (Γ.piece ℤ)) (ComplexShape.up ℤ))

The regular graded bimodule, placed in cohomological degree zero, acts as the identity functor on the homotopy category of cochain complexes of graded modules.

@[reducible, inline]

noncomputable abbrev TauCeti.GradedModuleCat.bimoduleModuleTensorHomotopyAssociator {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] {B : Type uB} {C : Type uC} [Ring B] [Ring C] [Algebra k B] [Algebra k C] (Γ : InternalGrading k A ℤ) (Δ : InternalGrading k B ℤ) (Θ : InternalGrading k C ℤ) [GradedAlgebra (Γ.piece ℤ)] [GradedAlgebra (Δ.piece ℤ)] [GradedAlgebra (Θ.piece ℤ)] (K₁ : CochainComplex (GradedModuleCat ((Γ.tensorProduct Δ.opposite).piece ℤ)) ℤ) (K₂ : CochainComplex (GradedModuleCat ((Δ.tensorProduct Θ.opposite).piece ℤ)) ℤ) : (bimoduleModuleTensorHomotopy Γ Θ).obj ((HomotopyCategory.quotient (GradedModuleCat ((Γ.tensorProduct Θ.opposite).piece ℤ)) (ComplexShape.up ℤ)).obj (HomologicalComplex.mapBifunctor K₁ K₂ (bimoduleTensor Γ Δ Θ) (ComplexShape.up ℤ))) ≅ ((bimoduleModuleTensorHomotopy Δ Θ).obj ((HomotopyCategory.quotient (GradedModuleCat ((Δ.tensorProduct Θ.opposite).piece ℤ)) (ComplexShape.up ℤ)).obj K₂)).comp ((bimoduleModuleTensorHomotopy Γ Δ).obj ((HomotopyCategory.quotient (GradedModuleCat ((Γ.tensorProduct Δ.opposite).piece ℤ)) (ComplexShape.up ℤ)).obj K₁))

Acting by the total tensor product of two complexes of graded bimodules is isomorphic, on the homotopy category of graded modules, to acting by the second complex and then by the first.

noncomputable def TauCeti.GradedModuleCat.bimoduleModuleTensorHomotopyEquivalence {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] {B : Type uA} [Ring B] [Algebra k B] (Γ : InternalGrading k A ℤ) (Δ : InternalGrading k B ℤ) [GradedAlgebra (Γ.piece ℤ)] [GradedAlgebra (Δ.piece ℤ)] (K : CochainComplex (GradedModuleCat ((Γ.tensorProduct Δ.opposite).piece ℤ)) ℤ) (K' : CochainComplex (GradedModuleCat ((Δ.tensorProduct Γ.opposite).piece ℤ)) ℤ) (e : HomotopyEquiv (HomologicalComplex.mapBifunctor K K' (bimoduleTensor Γ Δ Γ) (ComplexShape.up ℤ)) ((HomologicalComplex.single (GradedModuleCat ((Γ.tensorProduct Γ.opposite).piece ℤ)) (ComplexShape.up ℤ) 0).obj (bimoduleUnit Γ))) (e' : HomotopyEquiv (HomologicalComplex.mapBifunctor K' K (bimoduleTensor Δ Γ Δ) (ComplexShape.up ℤ)) ((HomologicalComplex.single (GradedModuleCat ((Δ.tensorProduct Δ.opposite).piece ℤ)) (ComplexShape.up ℤ) 0).obj (bimoduleUnit Δ))) : HomotopyCategory (GradedModuleCat (Δ.piece ℤ)) (ComplexShape.up ℤ) ≌ HomotopyCategory (GradedModuleCat (Γ.piece ℤ)) (ComplexShape.up ℤ)

A complex K of graded (A, B)-bimodules and a complex K' of graded (B, A)-bimodules whose tensor products K ⊗_B K' and K' ⊗_A K are homotopy equivalent to the regular bimodules A and B in degree zero give an equivalence between the homotopy categories of graded B-modules and of graded A-modules, acting by K, with inverse the action of K'.

@[simp]

theorem TauCeti.GradedModuleCat.bimoduleModuleTensorHomotopyEquivalence_functor {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] {B : Type uA} [Ring B] [Algebra k B] (Γ : InternalGrading k A ℤ) (Δ : InternalGrading k B ℤ) [GradedAlgebra (Γ.piece ℤ)] [GradedAlgebra (Δ.piece ℤ)] (K : CochainComplex (GradedModuleCat ((Γ.tensorProduct Δ.opposite).piece ℤ)) ℤ) (K' : CochainComplex (GradedModuleCat ((Δ.tensorProduct Γ.opposite).piece ℤ)) ℤ) (e : HomotopyEquiv (HomologicalComplex.mapBifunctor K K' (bimoduleTensor Γ Δ Γ) (ComplexShape.up ℤ)) ((HomologicalComplex.single (GradedModuleCat ((Γ.tensorProduct Γ.opposite).piece ℤ)) (ComplexShape.up ℤ) 0).obj (bimoduleUnit Γ))) (e' : HomotopyEquiv (HomologicalComplex.mapBifunctor K' K (bimoduleTensor Δ Γ Δ) (ComplexShape.up ℤ)) ((HomologicalComplex.single (GradedModuleCat ((Δ.tensorProduct Δ.opposite).piece ℤ)) (ComplexShape.up ℤ) 0).obj (bimoduleUnit Δ))) : (bimoduleModuleTensorHomotopyEquivalence Γ Δ K K' e e').functor = (bimoduleModuleTensorHomotopy Γ Δ).obj ((HomotopyCategory.quotient (GradedModuleCat ((Γ.tensorProduct Δ.opposite).piece ℤ)) (ComplexShape.up ℤ)).obj K)

The equivalence attached to K is the action of K.

@[simp]

theorem TauCeti.GradedModuleCat.bimoduleModuleTensorHomotopyEquivalence_inverse {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] {B : Type uA} [Ring B] [Algebra k B] (Γ : InternalGrading k A ℤ) (Δ : InternalGrading k B ℤ) [GradedAlgebra (Γ.piece ℤ)] [GradedAlgebra (Δ.piece ℤ)] (K : CochainComplex (GradedModuleCat ((Γ.tensorProduct Δ.opposite).piece ℤ)) ℤ) (K' : CochainComplex (GradedModuleCat ((Δ.tensorProduct Γ.opposite).piece ℤ)) ℤ) (e : HomotopyEquiv (HomologicalComplex.mapBifunctor K K' (bimoduleTensor Γ Δ Γ) (ComplexShape.up ℤ)) ((HomologicalComplex.single (GradedModuleCat ((Γ.tensorProduct Γ.opposite).piece ℤ)) (ComplexShape.up ℤ) 0).obj (bimoduleUnit Γ))) (e' : HomotopyEquiv (HomologicalComplex.mapBifunctor K' K (bimoduleTensor Δ Γ Δ) (ComplexShape.up ℤ)) ((HomologicalComplex.single (GradedModuleCat ((Δ.tensorProduct Δ.opposite).piece ℤ)) (ComplexShape.up ℤ) 0).obj (bimoduleUnit Δ))) : (bimoduleModuleTensorHomotopyEquivalence Γ Δ K K' e e').inverse = (bimoduleModuleTensorHomotopy Δ Γ).obj ((HomotopyCategory.quotient (GradedModuleCat ((Δ.tensorProduct Γ.opposite).piece ℤ)) (ComplexShape.up ℤ)).obj K')

The inverse of the equivalence attached to K is the action of K'.