The top tensor term of an adjacent braid product

The two middle corners of U_i ⊗[Z] U_j ⊗[Z] U_i are generated by opposite arrows when i and j are adjacent. Extracting these corners leaves the two outer factors of U_i. Each arrow has internal degree one, so the resulting vertex bimodule is shifted by two. This is the top term of the adjacent triple-product cancellation.

noncomputable def TauCeti.zigzagBraidAdjacentTripleUnderlyingEquiv (k : Type u_1) [CommRing k] {V : Type u_2} (G : SimpleGraph V) [Finite V] {i j : V} (h : G.Adj j i) : (GradedModuleCat.bimoduleTensorObj (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (GradedModuleCat.bimoduleTensorObj (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagGradedBraidBimodule k G i) (zigzagGradedBraidBimodule k G j)) (zigzagGradedBraidBimodule k G i)).carrier ≃ₗ[k] (zigzagGradedBraidBimodule k G i).carrier

The two adjacent middle-arrow coordinates identify the triple carrier with the vertex bimodule carrier. Its internal grading is accounted for by the degree-two insertion.

@[simp]

theorem TauCeti.zigzagBraidAdjacentTripleUnderlyingEquiv_tmul (k : Type u_1) [CommRing k] {V : Type u_2} (G : SimpleGraph V) [Finite V] {i j : V} (h : G.Adj j i) (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)) (l' : ↥((fun (i : V) => Ideal.span {(fun (i : V) => (zigzagAlgebraBasis k G) (Sum.inl i)) i}) j)) (r' : ↥((fun (i : V) => Ideal.span {MulOpposite.op ((fun (i : V) => (zigzagAlgebraBasis k G) (Sum.inl i)) i)}) j)) (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)) : (zigzagBraidAdjacentTripleUnderlyingEquiv k G h) (GradedModuleCat.bimoduleTensorTmul (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (GradedModuleCat.bimoduleTensorObj (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagGradedBraidBimodule k G i) (zigzagGradedBraidBimodule k G j)) (zigzagGradedBraidBimodule k G i) (GradedModuleCat.bimoduleTensorTmul (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagGradedBraidBimodule k G i) (zigzagGradedBraidBimodule k G j) ((zigzagBraidBimoduleFactorsEquiv k G i).symm (l ⊗ₜ[k] r)) ((zigzagBraidBimoduleFactorsEquiv k G j).symm (l' ⊗ₜ[k] r'))) ((zigzagBraidBimoduleFactorsEquiv k G i).symm (l'' ⊗ₜ[k] r''))) = (zigzagAdjacentBalancedTensorEquiv k G ⋯) (BalancedTensorProduct.tmul k (↑(zigzagAlgebra k G)) r' l'') • (zigzagAdjacentBalancedTensorEquiv k G h) (BalancedTensorProduct.tmul k (↑(zigzagAlgebra k G)) r l') • (zigzagBraidBimoduleFactorsEquiv k G i).symm (l ⊗ₜ[k] r'')

On pure vertex factors, the two middle arrow coordinates multiply the surviving outer factors. This formula concerns carriers; the two internal arrow degrees sum to two.

noncomputable def TauCeti.zigzagBraidAdjacentTripleInsert (k : Type u_1) [CommRing k] {V : Type u_2} (G : SimpleGraph V) [Finite V] {i j : V} (h : G.Adj j i) : (zigzagGradedBraidBimodule k G i).shiftObj 2 ⟶ GradedModuleCat.bimoduleTensorObj (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (GradedModuleCat.bimoduleTensorObj (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagGradedBraidBimodule k G i) (zigzagGradedBraidBimodule k G j)) (zigzagGradedBraidBimodule k G i)

Insert the two opposite middle arrows. The total internal degree is two, so the source is the vertex bimodule shifted by two and this morphism has degree zero.

noncomputable def TauCeti.zigzagBraidAdjacentTripleIso (k : Type u_1) [CommRing k] {V : Type u_2} (G : SimpleGraph V) [Finite V] {i j : V} (h : G.Adj j i) : GradedModuleCat.bimoduleTensorObj (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (GradedModuleCat.bimoduleTensorObj (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagGradedBraidBimodule k G i) (zigzagGradedBraidBimodule k G j)) (zigzagGradedBraidBimodule k G i) ≅ (zigzagGradedBraidBimodule k G i).shiftObj 2

At adjacent vertices, the top actual triple tensor is the vertex bimodule shifted by two.

@[simp]

theorem TauCeti.zigzagBraidAdjacentTripleIso_inv (k : Type u_1) [CommRing k] {V : Type u_2} (G : SimpleGraph V) [Finite V] {i j : V} (h : G.Adj j i) : (zigzagBraidAdjacentTripleIso k G h).inv = zigzagBraidAdjacentTripleInsert k G h

The inverse graded comparison is the insertion of the two opposite arrows.

@[simp]

theorem TauCeti.zigzagBraidAdjacentTripleInsert_hom_factors (k : Type u_1) [CommRing k] {V : Type u_2} (G : SimpleGraph V) [Finite V] {i j : V} (h : G.Adj j i) (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)) : (zigzagBraidAdjacentTripleInsert k G h).hom ((zigzagBraidBimoduleFactorsEquiv k G i).symm (l ⊗ₜ[k] r)) = GradedModuleCat.bimoduleTensorTmul (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (GradedModuleCat.bimoduleTensorObj (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagGradedBraidBimodule k G i) (zigzagGradedBraidBimodule k G j)) (zigzagGradedBraidBimodule k G i) (GradedModuleCat.bimoduleTensorTmul (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagGradedBraidBimodule k G i) (zigzagGradedBraidBimodule k G j) ((zigzagBraidBimoduleFactorsEquiv k G i).symm (l ⊗ₜ[k] spanSingletonGenerator (MulOpposite.op ((fun (i : V) => (zigzagAlgebraBasis k G) (Sum.inl i)) i)))) ((zigzagBraidBimoduleFactorsEquiv k G j).symm (((zigzagAlgebraBasis k G) (Sum.inr (Sum.inl { fst := j, snd := i, adj := h })) • spanSingletonGenerator ((fun (i : V) => (zigzagAlgebraBasis k G) (Sum.inl i)) j)) ⊗ₜ[k] spanSingletonGenerator (MulOpposite.op ((fun (i : V) => (zigzagAlgebraBasis k G) (Sum.inl i)) j))))) ((zigzagBraidBimoduleFactorsEquiv k G i).symm (((zigzagAlgebraBasis k G) (Sum.inr (Sum.inl { fst := i, snd := j, adj := ⋯ })) • spanSingletonGenerator ((fun (i : V) => (zigzagAlgebraBasis k G) (Sum.inl i)) i)) ⊗ₜ[k] r))

On outer ideal factors, the inverse graded comparison inserts the two middle arrows.

@[simp]

theorem TauCeti.zigzagBraidAdjacentTripleIso_hom_apply (k : Type u_1) [CommRing k] {V : Type u_2} (G : SimpleGraph V) [Finite V] {i j : V} (h : G.Adj j i) (t : (GradedModuleCat.bimoduleTensorObj (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (GradedModuleCat.bimoduleTensorObj (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagGradedBraidBimodule k G i) (zigzagGradedBraidBimodule k G j)) (zigzagGradedBraidBimodule k G i)).carrier) : (zigzagBraidAdjacentTripleIso k G h).hom.hom t = (zigzagBraidAdjacentTripleUnderlyingEquiv k G h) t

The forward graded comparison computes by the two middle-arrow coordinates.