The two support sequences of the zigzag braid tensor action

The highest nonzero term of a two-term bimodule complex is a subcomplex, and its lowest term is the quotient. Totalized tensoring with a module complex gives a short exact sequence, split in every cochain degree. The two supported rows are identified by the canonical two-summand totalization isomorphism.

For the positive braid complex the outer complexes are the regular tensor action and the vertex tensor action shifted cohomologically by one. For the inverse complex they are the internally shifted vertex action shifted cohomologically by minus one, and the regular action. The internal shift by minus two and these cohomological shifts are separate. The sequences are objects of a functor category, so their chain maps are natural in the module complex. No boundedness or flatness assumption on that complex is needed for these degreewise split sequences.

noncomputable def TauCeti.zigzagBraidTensorSupportSequence (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (i : V) : CategoryTheory.ShortComplex (CategoryTheory.Functor (CochainComplex (GradedModuleCat ((zigzagAlgebraInternalGrading k G).piece ℤ)) ℤ) (CochainComplex (GradedModuleCat ((zigzagAlgebraInternalGrading k G).piece ℤ)) ℤ))

The natural two-support sequence of the positive braid tensor action has outer functors T_Z and T_U[1]. The maps are chain maps, natural in every module complex.

noncomputable def TauCeti.zigzagBraidInverseTensorSupportSequence (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (i : V) : CategoryTheory.ShortComplex (CategoryTheory.Functor (CochainComplex (GradedModuleCat ((zigzagAlgebraInternalGrading k G).piece ℤ)) ℤ) (CochainComplex (GradedModuleCat ((zigzagAlgebraInternalGrading k G).piece ℤ)) ℤ))

The natural two-support sequence of the inverse braid tensor action has outer functors T_(U{-2})[-1] and T_Z, with distinct internal and cohomological shifts.

@[simp]

theorem TauCeti.zigzagBraidTensorSupportSequence_X₁ (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (i : V) : (zigzagBraidTensorSupportSequence k G i).X₁ = ((GradedModuleCat.bimoduleModuleTensor (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G)).obj (zigzagGradedBimodule k G)).mapHomologicalComplex (ComplexShape.up ℤ)

@[simp]

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

@[simp]

theorem TauCeti.zigzagBraidTensorSupportSequence_X₃ (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (i : V) : (zigzagBraidTensorSupportSequence k G i).X₃ = (((GradedModuleCat.bimoduleModuleTensor (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G)).obj (zigzagGradedBraidBimodule k G i)).mapHomologicalComplex (ComplexShape.up ℤ)).comp (CategoryTheory.shiftFunctor (CochainComplex (GradedModuleCat ((zigzagAlgebraInternalGrading k G).piece ℤ)) ℤ) 1)

@[simp]

theorem TauCeti.zigzagBraidInverseTensorSupportSequence_X₁ (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (i : V) : (zigzagBraidInverseTensorSupportSequence k G i).X₁ = (((GradedModuleCat.bimoduleModuleTensor (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G)).obj ((GradedModuleCat.shiftFunctor (-2)).obj (zigzagGradedBraidBimodule k G i))).mapHomologicalComplex (ComplexShape.up ℤ)).comp (CategoryTheory.shiftFunctor (CochainComplex (GradedModuleCat ((zigzagAlgebraInternalGrading k G).piece ℤ)) ℤ) (-1))

@[simp]

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

@[simp]

theorem TauCeti.zigzagBraidInverseTensorSupportSequence_X₃ (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (i : V) : (zigzagBraidInverseTensorSupportSequence k G i).X₃ = ((GradedModuleCat.bimoduleModuleTensor (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G)).obj (zigzagGradedBimodule k G)).mapHomologicalComplex (ComplexShape.up ℤ)

theorem TauCeti.zigzagBraidTensorSupportSequence_shortExact (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (i : V) : (zigzagBraidTensorSupportSequence k G i).ShortExact

The positive support sequence is short exact in the functor category.

theorem TauCeti.zigzagBraidInverseTensorSupportSequence_shortExact (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (i : V) : (zigzagBraidInverseTensorSupportSequence k G i).ShortExact

The inverse support sequence is short exact in the functor category.

noncomputable def TauCeti.zigzagBraidTensorSupportSequenceDegreewiseSplitting (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (i : V) (N : CochainComplex (GradedModuleCat ((zigzagAlgebraInternalGrading k G).piece ℤ)) ℤ) (j : ℤ) : (((zigzagBraidTensorSupportSequence k G i).map ((CategoryTheory.evaluation (CochainComplex (GradedModuleCat ((zigzagAlgebraInternalGrading k G).piece ℤ)) ℤ) (CochainComplex (GradedModuleCat ((zigzagAlgebraInternalGrading k G).piece ℤ)) ℤ)).obj N)).map (HomologicalComplex.eval (GradedModuleCat ((zigzagAlgebraInternalGrading k G).piece ℤ)) (ComplexShape.up ℤ) j)).Splitting

The positive support sequence has its canonical splitting after evaluating at a module complex and a cochain degree.

noncomputable def TauCeti.zigzagBraidTensorSupportSequenceDegreewiseIso (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (i : V) (N : CochainComplex (GradedModuleCat ((zigzagAlgebraInternalGrading k G).piece ℤ)) ℤ) (j : ℤ) : ((zigzagBraidTensorSupportSequence k G i).X₂.obj N).X j ≅ ((zigzagBraidTensorSupportSequence k G i).X₁.obj N).X j ⊞ ((zigzagBraidTensorSupportSequence k G i).X₃.obj N).X j

The actual positive totalization degree is the biproduct of its two public endpoints.

@[simp]

theorem TauCeti.zigzagBraidTensorSupportSequence_f_degreewiseIso_hom (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (i : V) (N : CochainComplex (GradedModuleCat ((zigzagAlgebraInternalGrading k G).piece ℤ)) ℤ) (j : ℤ) : CategoryTheory.CategoryStruct.comp (((zigzagBraidTensorSupportSequence k G i).f.app N).f j) (zigzagBraidTensorSupportSequenceDegreewiseIso k G i N j).hom = CategoryTheory.Limits.biprod.inl

The positive support inclusion is the first biproduct inclusion in each degree.

@[simp]

theorem TauCeti.zigzagBraidTensorSupportSequence_f_degreewiseIso_hom_assoc (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (i : V) (N : CochainComplex (GradedModuleCat ((zigzagAlgebraInternalGrading k G).piece ℤ)) ℤ) (j : ℤ) {Z : GradedModuleCat (zigzagAlgebraIntegerGrade k G)} (h : ((zigzagBraidTensorSupportSequence k G i).X₁.obj N).X j ⊞ ((zigzagBraidTensorSupportSequence k G i).X₃.obj N).X j ⟶ Z) : CategoryTheory.CategoryStruct.comp (((zigzagBraidTensorSupportSequence k G i).f.app N).f j) (CategoryTheory.CategoryStruct.comp (zigzagBraidTensorSupportSequenceDegreewiseIso k G i N j).hom h) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl h

The positive support inclusion is the first biproduct inclusion in each degree.

@[simp]

theorem TauCeti.zigzagBraidTensorSupportSequence_degreewiseIso_hom_snd (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (i : V) (N : CochainComplex (GradedModuleCat ((zigzagAlgebraInternalGrading k G).piece ℤ)) ℤ) (j : ℤ) : CategoryTheory.CategoryStruct.comp (zigzagBraidTensorSupportSequenceDegreewiseIso k G i N j).hom CategoryTheory.Limits.biprod.snd = ((zigzagBraidTensorSupportSequence k G i).g.app N).f j

The positive support projection is the second biproduct projection in each degree.

@[simp]

theorem TauCeti.zigzagBraidTensorSupportSequence_degreewiseIso_hom_snd_assoc (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (i : V) (N : CochainComplex (GradedModuleCat ((zigzagAlgebraInternalGrading k G).piece ℤ)) ℤ) (j : ℤ) {Z : GradedModuleCat (zigzagAlgebraIntegerGrade k G)} (h : ((zigzagBraidTensorSupportSequence k G i).X₃.obj N).X j ⟶ Z) : CategoryTheory.CategoryStruct.comp (zigzagBraidTensorSupportSequenceDegreewiseIso k G i N j).hom (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.snd h) = CategoryTheory.CategoryStruct.comp (((zigzagBraidTensorSupportSequence k G i).g.app N).f j) h

The positive support projection is the second biproduct projection in each degree.

noncomputable def TauCeti.zigzagBraidInverseTensorSupportSequenceDegreewiseSplitting (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (i : V) (N : CochainComplex (GradedModuleCat ((zigzagAlgebraInternalGrading k G).piece ℤ)) ℤ) (j : ℤ) : (((zigzagBraidInverseTensorSupportSequence k G i).map ((CategoryTheory.evaluation (CochainComplex (GradedModuleCat ((zigzagAlgebraInternalGrading k G).piece ℤ)) ℤ) (CochainComplex (GradedModuleCat ((zigzagAlgebraInternalGrading k G).piece ℤ)) ℤ)).obj N)).map (HomologicalComplex.eval (GradedModuleCat ((zigzagAlgebraInternalGrading k G).piece ℤ)) (ComplexShape.up ℤ) j)).Splitting

The inverse support sequence has its canonical splitting after evaluating at a module complex and a cochain degree.

noncomputable def TauCeti.zigzagBraidInverseTensorSupportSequenceDegreewiseIso (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (i : V) (N : CochainComplex (GradedModuleCat ((zigzagAlgebraInternalGrading k G).piece ℤ)) ℤ) (j : ℤ) : ((zigzagBraidInverseTensorSupportSequence k G i).X₂.obj N).X j ≅ ((zigzagBraidInverseTensorSupportSequence k G i).X₁.obj N).X j ⊞ ((zigzagBraidInverseTensorSupportSequence k G i).X₃.obj N).X j

The actual inverse totalization degree is the biproduct of its two public endpoints.

@[simp]

theorem TauCeti.zigzagBraidInverseTensorSupportSequence_f_degreewiseIso_hom (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (i : V) (N : CochainComplex (GradedModuleCat ((zigzagAlgebraInternalGrading k G).piece ℤ)) ℤ) (j : ℤ) : CategoryTheory.CategoryStruct.comp (((zigzagBraidInverseTensorSupportSequence k G i).f.app N).f j) (zigzagBraidInverseTensorSupportSequenceDegreewiseIso k G i N j).hom = CategoryTheory.Limits.biprod.inl

The inverse support inclusion is the first biproduct inclusion in each degree.

@[simp]

theorem TauCeti.zigzagBraidInverseTensorSupportSequence_f_degreewiseIso_hom_assoc (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (i : V) (N : CochainComplex (GradedModuleCat ((zigzagAlgebraInternalGrading k G).piece ℤ)) ℤ) (j : ℤ) {Z : GradedModuleCat (zigzagAlgebraIntegerGrade k G)} (h : ((zigzagBraidInverseTensorSupportSequence k G i).X₁.obj N).X j ⊞ ((zigzagBraidInverseTensorSupportSequence k G i).X₃.obj N).X j ⟶ Z) : CategoryTheory.CategoryStruct.comp (((zigzagBraidInverseTensorSupportSequence k G i).f.app N).f j) (CategoryTheory.CategoryStruct.comp (zigzagBraidInverseTensorSupportSequenceDegreewiseIso k G i N j).hom h) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl h

The inverse support inclusion is the first biproduct inclusion in each degree.

@[simp]

theorem TauCeti.zigzagBraidInverseTensorSupportSequence_degreewiseIso_hom_snd (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (i : V) (N : CochainComplex (GradedModuleCat ((zigzagAlgebraInternalGrading k G).piece ℤ)) ℤ) (j : ℤ) : CategoryTheory.CategoryStruct.comp (zigzagBraidInverseTensorSupportSequenceDegreewiseIso k G i N j).hom CategoryTheory.Limits.biprod.snd = ((zigzagBraidInverseTensorSupportSequence k G i).g.app N).f j

The inverse support projection is the second biproduct projection in each degree.

@[simp]

theorem TauCeti.zigzagBraidInverseTensorSupportSequence_degreewiseIso_hom_snd_assoc (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (i : V) (N : CochainComplex (GradedModuleCat ((zigzagAlgebraInternalGrading k G).piece ℤ)) ℤ) (j : ℤ) {Z : GradedModuleCat (zigzagAlgebraIntegerGrade k G)} (h : ((zigzagBraidInverseTensorSupportSequence k G i).X₃.obj N).X j ⟶ Z) : CategoryTheory.CategoryStruct.comp (zigzagBraidInverseTensorSupportSequenceDegreewiseIso k G i N j).hom (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.snd h) = CategoryTheory.CategoryStruct.comp (((zigzagBraidInverseTensorSupportSequence k G i).g.app N).f j) h

The inverse support projection is the second biproduct projection in each degree.