Quasi-isomorphisms under the two zigzag braid tensor actions

Tensoring with either the positive or inverse braid complex preserves quasi-isomorphisms between arbitrary unbounded cochain complexes of graded zigzag modules. Each tensor functor defines a morphism of the quasi-isomorphism localizer, hence induces a functor between any supplied localizations, including chosen derived categories.

theorem TauCeti.quasiIso_zigzagBraidTensor_map (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (i : V) {K L : CochainComplex (GradedModuleCat ((zigzagAlgebraInternalGrading k G).piece ℤ)) ℤ} (f : K ⟶ L) [QuasiIso f] : QuasiIso (((GradedModuleCat.bimoduleModuleTensor (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G)).map₂CochainComplex.obj (zigzagBraidComplex k G i)).map f)

The totalized positive braid tensor action preserves quasi-isomorphisms.

theorem TauCeti.quasiIso_zigzagBraidInverseTensor_map (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (i : V) {K L : CochainComplex (GradedModuleCat ((zigzagAlgebraInternalGrading k G).piece ℤ)) ℤ} (f : K ⟶ L) [QuasiIso f] : QuasiIso (((GradedModuleCat.bimoduleModuleTensor (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G)).map₂CochainComplex.obj (zigzagBraidInverseComplex k G i)).map f)

The totalized inverse braid tensor action preserves quasi-isomorphisms.

noncomputable def TauCeti.zigzagBraidTensorLocalizerMorphism (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (i : V) : CategoryTheory.LocalizerMorphism (HomologicalComplex.quasiIso (GradedModuleCat ((zigzagAlgebraInternalGrading k G).piece ℤ)) (ComplexShape.up ℤ)) (HomologicalComplex.quasiIso (GradedModuleCat ((zigzagAlgebraInternalGrading k G).piece ℤ)) (ComplexShape.up ℤ))

The positive braid tensor functor defines a morphism of the quasi-isomorphism localizer.

noncomputable def TauCeti.zigzagBraidInverseTensorLocalizerMorphism (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (i : V) : CategoryTheory.LocalizerMorphism (HomologicalComplex.quasiIso (GradedModuleCat ((zigzagAlgebraInternalGrading k G).piece ℤ)) (ComplexShape.up ℤ)) (HomologicalComplex.quasiIso (GradedModuleCat ((zigzagAlgebraInternalGrading k G).piece ℤ)) (ComplexShape.up ℤ))

The inverse braid tensor functor defines a morphism of the quasi-isomorphism localizer.

@[simp]

theorem TauCeti.zigzagBraidTensorLocalizerMorphism_functor (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (i : V) : (zigzagBraidTensorLocalizerMorphism k G i).functor = (GradedModuleCat.bimoduleModuleTensor (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G)).map₂CochainComplex.obj (zigzagBraidComplex k G i)

@[simp]

theorem TauCeti.zigzagBraidInverseTensorLocalizerMorphism_functor (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (i : V) : (zigzagBraidInverseTensorLocalizerMorphism k G i).functor = (GradedModuleCat.bimoduleModuleTensor (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G)).map₂CochainComplex.obj (zigzagBraidInverseComplex k G i)