Right-projective terms of the zigzag braid complexes

For a vertex i, the underlying right module of the vertex bimodule is e_i Z ⊗[k] Z e_i. The right ideal e_i Z is projective over Zᵐᵒᵖ, and Z e_i is a direct summand of the free k-module Z. Mathlib's projectivity of tensor products, transported through the existing factor identification, therefore makes the vertex bimodule projective as a right Z-module.

The regular bimodule is a free right module, and internal shifts preserve its carrier and scalar actions. The canonical term isomorphisms of the two braid complexes then give right projectivity in every cohomological degree, with the remaining terms zero. These statements hold over every commutative coefficient ring and include isolated vertices of the componentwise algebra.

Each assertion uses the canonical restricted action of Zᵐᵒᵖ, obtained from the second factor of the enveloping algebra. These are the module-theoretic inputs for studying the tensor action on acyclic complexes.

theorem TauCeti.projective_zigzagGradedBraidBimodule_right (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (i : V) : Module.Projective (↑(zigzagAlgebra k G))ᵐᵒᵖ (zigzagGradedBraidBimodule k G i).carrier

The vertex bimodule is projective for its restricted right action of the zigzag algebra.

theorem TauCeti.projective_zigzagBraidComplex_X_right (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (i : V) (n : ℤ) : Module.Projective (↑(zigzagAlgebra k G))ᵐᵒᵖ ((zigzagBraidComplex k G i).X n).carrier

Every term of the braid complex is projective for the restricted right action.

theorem TauCeti.projective_zigzagBraidInverseComplex_X_right (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (i : V) (n : ℤ) : Module.Projective (↑(zigzagAlgebra k G))ᵐᵒᵖ ((zigzagBraidInverseComplex k G i).X n).carrier

Every term of the inverse braid complex is projective for the restricted right action.