The terms of a zigzag braid complex applied to a vertex projective

Let Z be the zigzag algebra of a finite simple graph and P_j = Z e_j its graded vertex projective. The braid complex B_i = [U_i ⟶ Z] has the vertex bimodule U_i = Z e_i ⊗_k e_i Z in cohomological degree -1 and the regular bimodule in degree 0. Tensoring over Z with P_j extracts the corner e_i Z e_j from the middle:

U_i ⊗_Z P_j ≅ Z e_i ⊗_k e_i Z e_j.

The corner is spanned by e_i and the volume x_i, of internal degrees 0 and 2, when j = i; by the arrow from j to i, of internal degree 1, when j is adjacent to i; and it vanishes otherwise. Hence, with M{d}_p = M_{p-d},

U_i ⊗_Z P_i ≅ P_i ⊞ P_i{2},    U_i ⊗_Z P_j ≅ P_i{1} (j adjacent to i),
U_i ⊗_Z P_j = 0 (j ≠ i not adjacent to i),    Z ⊗_Z P_j ≅ P_j,

as graded left Z-modules. These are the terms of the image of B_i under - ⊗_Z P_j. The calculation covers isolated vertices of the public componentwise algebra.

Main definitions

• TauCeti.zigzagBraidProjectiveTensorCornerEquiv: the carrier identification U_i ⊗_Z P_j ≃ e_i Z e_j ⊗_k Z e_i.
• TauCeti.zigzagBraidProjectiveTensorSelfIso: U_i ⊗_Z P_i ≅ P_i ⊞ P_i{2}.
• TauCeti.zigzagBraidProjectiveTensorAdjIso: U_i ⊗_Z P_j ≅ P_i{1} for j adjacent to i.
• TauCeti.zigzagBraidProjectiveUnitTensorIso: Z ⊗_Z P_j ≅ P_j.

Main results

• TauCeti.isZero_zigzagBraidProjectiveTensor: U_i ⊗_Z P_j vanishes when j ≠ i is not adjacent to i.

References

• R. S. Huerfano and M. Khovanov, A category for the adjoint representation, Section 4.6.
• M. Khovanov and P. Seidel, Quivers, Floer cohomology, and braid group actions, Section 2e.

The carrier identification

noncomputable def TauCeti.zigzagBraidProjectiveTensorCornerEquiv (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (i j : V) : ((fun (i j : V) => GradedModuleCat.bimoduleModuleTensorObj (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagGradedBraidBimodule k G i) (zigzagAlgebraGradedProjective k G j)) i j).carrier ≃ₗ[k] TensorProduct k ↥(cornerSubmodule k ((fun (i : V) => (zigzagAlgebraBasis k G) (Sum.inl i)) i) ((fun (i : V) => (zigzagAlgebraBasis k G) (Sum.inl i)) j)) ↥((fun (i : V) => Ideal.span {(fun (i : V) => (zigzagAlgebraBasis k G) (Sum.inl i)) i}) i)

Extract the corner e_i Z e_j from the tensor product of the vertex bimodule U_i with the vertex projective P_j, leaving the left ideal Z e_i as the other factor.

@[simp]

theorem TauCeti.zigzagBraidProjectiveTensorCornerEquiv_tmul (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (i j : V) (l : ↥((fun (i : V) => Ideal.span {(fun (i : V) => (zigzagAlgebraBasis k G) (Sum.inl i)) i}) i)) (r : ↥((fun (i : V) => Ideal.span {MulOpposite.op ((fun (i : V) => (zigzagAlgebraBasis k G) (Sum.inl i)) i)}) i)) (n : ↥((fun (i : V) => Ideal.span {(fun (i : V) => (zigzagAlgebraBasis k G) (Sum.inl i)) i}) j)) : (zigzagBraidProjectiveTensorCornerEquiv k G i j) (GradedModuleCat.bimoduleModuleTensorTmul (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagGradedBraidBimodule k G i) (zigzagAlgebraGradedProjective k G j) ((zigzagBraidBimoduleFactorsEquiv k G i).symm (l ⊗ₜ[k] r)) n) = (spanSingletonBalancedTensorProductEquivCorner k ⋯) (BalancedTensorProduct.tmul k (↑(zigzagAlgebra k G)) r n) ⊗ₜ[k] l

On pure tensors, corner extraction multiplies the right ideal factor of U_i into P_j.

@[simp]

theorem TauCeti.zigzagBraidProjectiveTensorCornerEquiv_symm_tmul (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (i j : V) (c : ↥(cornerSubmodule k ((fun (i : V) => (zigzagAlgebraBasis k G) (Sum.inl i)) i) ((fun (i : V) => (zigzagAlgebraBasis k G) (Sum.inl i)) j))) (l : ↥((fun (i : V) => Ideal.span {(fun (i : V) => (zigzagAlgebraBasis k G) (Sum.inl i)) i}) i)) : (zigzagBraidProjectiveTensorCornerEquiv k G i j).symm (c ⊗ₜ[k] l) = GradedModuleCat.bimoduleModuleTensorTmul (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagGradedBraidBimodule k G i) (zigzagAlgebraGradedProjective k G j) ((zigzagBraidBimoduleFactorsEquiv k G i).symm (l ⊗ₜ[k] spanSingletonGenerator (MulOpposite.op ((fun (i : V) => (zigzagAlgebraBasis k G) (Sum.inl i)) i)))) ⟨↑c, ⋯⟩

The inverse of corner extraction inserts the right generator e_i of the vertex bimodule and reads the corner element in P_j.

Inserting shifted vertex projectives

The diagonal corner

noncomputable def TauCeti.zigzagBraidProjectiveTensorSelfIso (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (i : V) : (fun (i j : V) => GradedModuleCat.bimoduleModuleTensorObj (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagGradedBraidBimodule k G i) (zigzagAlgebraGradedProjective k G j)) i i ≅ zigzagAlgebraGradedProjective k G i ⊞ (zigzagAlgebraGradedProjective k G i).shiftObj 2

U_i ⊗_Z P_i ≅ P_i ⊞ P_i{2}: the diagonal corner e_i Z e_i is spanned by the vertex idempotent, of internal degree 0, and the volume, of internal degree 2.

@[simp]

theorem TauCeti.zigzagBraidProjectiveTensorSelfIso_inv_inl (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (i : V) (z : ↥((fun (i : V) => Ideal.span {(fun (i : V) => (zigzagAlgebraBasis k G) (Sum.inl i)) i}) i)) : (zigzagBraidProjectiveTensorSelfIso k G i).inv.hom (CategoryTheory.Limits.biprod.inl.hom z) = (zigzagBraidProjectiveTensorCornerEquiv k G i i).symm ((zigzagAlgebraSelfCornerEquiv k G i).symm (1, 0) ⊗ₜ[k] z)

The summand P_i of U_i ⊗_Z P_i is inserted along the vertex idempotent of the diagonal corner.

@[simp]

theorem TauCeti.zigzagBraidProjectiveTensorSelfIso_inv_inr (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (i : V) (z : ↥((fun (i : V) => Ideal.span {(fun (i : V) => (zigzagAlgebraBasis k G) (Sum.inl i)) i}) i)) : (zigzagBraidProjectiveTensorSelfIso k G i).inv.hom (CategoryTheory.Limits.biprod.inr.hom z) = (zigzagBraidProjectiveTensorCornerEquiv k G i i).symm ((zigzagAlgebraSelfCornerEquiv k G i).symm (0, 1) ⊗ₜ[k] z)

The summand P_i{2} of U_i ⊗_Z P_i is inserted along the volume of the diagonal corner.

Adjacent corners

noncomputable def TauCeti.zigzagBraidProjectiveTensorAdjIso (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] {i j : V} (h : G.Adj j i) : (fun (i j : V) => GradedModuleCat.bimoduleModuleTensorObj (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagGradedBraidBimodule k G i) (zigzagAlgebraGradedProjective k G j)) i j ≅ (zigzagAlgebraGradedProjective k G i).shiftObj 1

U_i ⊗_Z P_j ≅ P_i{1} for j adjacent to i: the corner e_i Z e_j is spanned by the arrow from j to i, of internal degree 1.

@[simp]

theorem TauCeti.zigzagBraidProjectiveTensorAdjIso_inv_apply (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] {i j : V} (h : G.Adj j i) (z : ↥((fun (i : V) => Ideal.span {(fun (i : V) => (zigzagAlgebraBasis k G) (Sum.inl i)) i}) i)) : (zigzagBraidProjectiveTensorAdjIso k G h).inv.hom z = (zigzagBraidProjectiveTensorCornerEquiv k G i j).symm ((zigzagAlgebraAdjacentCornerEquiv k G h).symm 1 ⊗ₜ[k] z)

The inverse of the adjacent isomorphism inserts P_i{1} along the arrow from j to i.

Vanishing corners and the regular bimodule

theorem TauCeti.isZero_zigzagBraidProjectiveTensor (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] {i j : V} (hij : i ≠ j) (hadj : ¬G.Adj i j) : CategoryTheory.Limits.IsZero ((fun (i j : V) => GradedModuleCat.bimoduleModuleTensorObj (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagGradedBraidBimodule k G i) (zigzagAlgebraGradedProjective k G j)) i j)

U_i ⊗_Z P_j = 0 for j ≠ i not adjacent to i: the corner e_i Z e_j vanishes.

noncomputable def TauCeti.zigzagBraidProjectiveUnitTensorIso (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (j : V) : GradedModuleCat.bimoduleModuleTensorObj (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagGradedBimodule k G) (zigzagAlgebraGradedProjective k G j) ≅ zigzagAlgebraGradedProjective k G j

Z ⊗_Z P_j ≅ P_j: the regular bimodule acts as the identity on the vertex projective.

@[simp]

theorem TauCeti.zigzagBraidProjectiveUnitTensorIso_hom_tmul (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (j : V) (x : (zigzagGradedBimodule k G).carrier) (n : ↥((fun (i : V) => Ideal.span {(fun (i : V) => (zigzagAlgebraBasis k G) (Sum.inl i)) i}) j)) : (zigzagBraidProjectiveUnitTensorIso k G j).hom.hom (GradedModuleCat.bimoduleModuleTensorTmul (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagGradedBimodule k G) (zigzagAlgebraGradedProjective k G j) x n) = (Bimodule.of (AlgHom.id k ↑(zigzagAlgebra k G))).symm x • n

The identification Z ⊗_Z P_j ≅ P_j is the action of Z on P_j.