Vertex projectives of a zigzag algebra

For a finite simple graph without isolated vertices, this file constructs the left projective module at a vertex i as the principal left ideal Z e_i in the zigzag relation quotient. Right multiplication by e_i is a projection from the regular module onto this ideal, so the module is projective. Its idempotent is primitive, so the module is also indecomposable.

The principal-ideal construction, grading, and projectivity work over any commutative ring. Indecomposability and the basis and dimension results below use a field.

The vertex projective has an explicit basis: the idempotent e_i, the arrows whose tail is i, and the volume class x_i. Thus its dimension is 2 + deg(i). The choice of arrows with tail i, rather than head i, is forced by Tau Ceti's later-factor-first convention: Z e_i consists of paths which begin at i.

Main definitions

• TauCeti.zigzagProjective: the left ideal Z e_i.
• TauCeti.zigzagProjectiveGrade: the signed path-length grading restricted to Z e_i.
• TauCeti.zigzagProjectiveShiftGrade: the grading of the shifted projective P_i{d}.
• TauCeti.ZigzagProjectiveBasisIndex: one vertex generator, the darts leaving i, and one volume generator.
• TauCeti.zigzagProjectiveBasis: the corresponding basis of Z e_i.

Main results

• TauCeti.completeOrthogonalIdempotents_zigzagVertexIdempotent: the vertex idempotents are a complete family of orthogonal idempotents.
• TauCeti.zigzagProjective_projective: Z e_i is projective as a left Z-module.
• TauCeti.isIndecomposableModule_zigzagProjective: Z e_i is indecomposable.
• TauCeti.finrank_zigzagProjective: dim_k Z e_i = 2 + deg(i).

References

See Huerfano--Khovanov, A category for the adjoint representation, Section 3, and Ehrig--Tubbenhauer, Algebraic properties of zigzag algebras, Section 2.

@[reducible, inline]

noncomputable abbrev TauCeti.zigzagVertexIdempotent (k : Type w) {V : Type u} (G : SimpleGraph V) [Finite V] [CommRing k] (i : V) : nonisolatedZigzagQuotient k G

The vertex idempotent of the zigzag relation quotient.

theorem TauCeti.isIdempotentElem_zigzagVertexIdempotent (k : Type w) {V : Type u} (G : SimpleGraph V) [Finite V] [CommRing k] (i : V) : IsIdempotentElem (zigzagVertexIdempotent k G i)

The vertex idempotent of the zigzag relation quotient is idempotent.

noncomputable def TauCeti.zigzagProjective (k : Type w) {V : Type u} (G : SimpleGraph V) [Finite V] [CommRing k] (i : V) : Ideal (nonisolatedZigzagQuotient k G)

The left projective of the zigzag relation quotient at i, namely the principal left ideal Z e_i.

theorem TauCeti.zigzagProjective_def (k : Type w) {V : Type u} (G : SimpleGraph V) [Finite V] [CommRing k] (i : V) : zigzagProjective k G i = Ideal.span {zigzagVertexIdempotent k G i}

The vertex projective is the principal left ideal generated by its vertex idempotent.

@[simp]

theorem TauCeti.mem_zigzagProjective_iff (k : Type w) {V : Type u} (G : SimpleGraph V) [Finite V] [CommRing k] {i : V} {x : nonisolatedZigzagQuotient k G} : x ∈ zigzagProjective k G i ↔ x * zigzagVertexIdempotent k G i = x

Membership in Z e_i: an element belongs to the vertex projective exactly when right multiplication by e_i fixes it.

noncomputable def TauCeti.zigzagProjectiveGenerator (k : Type w) {V : Type u} (G : SimpleGraph V) [Finite V] [CommRing k] (i : V) : ↥(zigzagProjective k G i)

The distinguished generator e_i of the vertex projective.

@[simp]

theorem TauCeti.coe_zigzagProjectiveGenerator (k : Type w) {V : Type u} (G : SimpleGraph V) [Finite V] [CommRing k] (i : V) : ↑(zigzagProjectiveGenerator k G i) = zigzagVertexIdempotent k G i

The vertex-projective grading

noncomputable def TauCeti.zigzagProjectiveGrade (k : Type w) {V : Type u} (G : SimpleGraph V) [Finite V] [CommRing k] (i : V) (d : ℤ) : Submodule k ↥(zigzagProjective k G i)

The signed degree-d part of the vertex projective P_i, obtained by restricting the integer-indexed grading of the zigzag algebra.

@[simp]

theorem TauCeti.mem_zigzagProjectiveGrade_iff (k : Type w) {V : Type u} (G : SimpleGraph V) [Finite V] [CommRing k] {i : V} {d : ℤ} {x : ↥(zigzagProjective k G i)} : x ∈ zigzagProjectiveGrade k G i d ↔ ↑x ∈ zigzagIntegerGrade k G d

noncomputable def TauCeti.zigzagProjectiveShiftGrade (k : Type w) {V : Type u} (G : SimpleGraph V) [Finite V] [CommRing k] (i : V) (d : ℤ) : ℤ → Submodule k ↥(zigzagProjective k G i)

The grading of the internal shift P_i{d}, normalized by (P_i{d})_p = (P_i)_{p-d} and hence [P_i{1}] = q[P_i].

@[simp]

theorem TauCeti.zigzagProjectiveShiftGrade_apply (k : Type w) {V : Type u} (G : SimpleGraph V) [Finite V] [CommRing k] (i : V) (d p : ℤ) : zigzagProjectiveShiftGrade k G i d p = zigzagProjectiveGrade k G i (p - d)

theorem TauCeti.zigzagProjective_projective (k : Type w) {V : Type u} (G : SimpleGraph V) [Finite V] [CommRing k] (i : V) : Module.Projective (nonisolatedZigzagQuotient k G) ↥(zigzagProjective k G i)

The vertex ideal Z e_i is a projective left module over the zigzag relation quotient.

Indecomposability

theorem TauCeti.zigzagVertexIdempotent_ne_zero (k : Type w) {V : Type u} (G : SimpleGraph V) [Finite V] [Field k] (i : V) : zigzagVertexIdempotent k G i ≠ 0

A vertex idempotent is nonzero in the zigzag relation quotient.

theorem TauCeti.isPrimitiveIdempotent_zigzagVertexIdempotent (k : Type w) {V : Type u} (G : SimpleGraph V) [Finite V] [Field k] (hns : ∀ (i : V), ∃ (j : V), G.Adj i j) (i : V) : IsPrimitiveIdempotent (zigzagVertexIdempotent k G i)

The vertex idempotents of a zigzag relation quotient are primitive. Modulo the Jacobson radical they are the coordinate idempotents in the product V → k; an idempotent summand which vanishes there lies in the nilpotent radical and is therefore zero.

theorem TauCeti.isIndecomposableModule_zigzagProjective (k : Type w) {V : Type u} (G : SimpleGraph V) [Finite V] [Field k] (hns : ∀ (i : V), ∃ (j : V), G.Adj i j) (i : V) : IsIndecomposableModule (nonisolatedZigzagQuotient k G) ↥(zigzagProjective k G i)

The vertex projective Z e_i is indecomposable as a left module over the zigzag relation quotient.

The vertex-projective basis

@[reducible, inline]

abbrev TauCeti.ZigzagProjectiveBasisIndex {V : Type u} (G : SimpleGraph V) (i : V) : Type u

Basis indices for Z e_i: its vertex generator, the darts with tail i, and its volume generator.

noncomputable def TauCeti.zigzagProjectiveBasisFun (k : Type w) {V : Type u} (G : SimpleGraph V) [Finite V] [Field k] (i : V) : ZigzagProjectiveBasisIndex G i → ↥(zigzagProjective k G i)

The vertex, outgoing-arrow and volume family in Z e_i.

theorem TauCeti.zigzagProjectiveBasisFun_inl (k : Type w) {V : Type u} (G : SimpleGraph V) [Finite V] [Field k] (i : V) (a : Unit) : zigzagProjectiveBasisFun k G i (Sum.inl a) = zigzagProjectiveGenerator k G i

The degree-zero projective basis vector is its distinguished vertex generator.

@[simp]

theorem TauCeti.coe_zigzagProjectiveBasisFun_inl (k : Type w) {V : Type u} (G : SimpleGraph V) [Finite V] [Field k] (i : V) (a : Unit) : ↑(zigzagProjectiveBasisFun k G i (Sum.inl a)) = zigzagVertexIdempotent k G i

@[simp]

theorem TauCeti.coe_zigzagProjectiveBasisFun_inr_inl (k : Type w) {V : Type u} (G : SimpleGraph V) [Finite V] [Field k] (i : V) (d : { d : G.Dart // d.toProd.1 = i }) : ↑(zigzagProjectiveBasisFun k G i (Sum.inr (Sum.inl d))) = (zigzagMk k G) (PathAlgebra.ofArrow (DoubledQuiver.arrow G ⋯))

@[simp]

theorem TauCeti.coe_zigzagProjectiveBasisFun_inr_inr (k : Type w) {V : Type u} (G : SimpleGraph V) [Finite V] [Field k] (i : V) (a : Unit) : ↑(zigzagProjectiveBasisFun k G i (Sum.inr (Sum.inr a))) = zigzagVolume k G i

theorem TauCeti.linearIndependent_zigzagProjectiveBasisFun (k : Type w) {V : Type u} (G : SimpleGraph V) [Finite V] [Field k] (hns : ∀ (i : V), ∃ (j : V), G.Adj i j) (i : V) : LinearIndependent k (zigzagProjectiveBasisFun k G i)

The vertex, outgoing-arrow and volume family in Z e_i is linearly independent.

theorem TauCeti.span_range_zigzagProjectiveBasisFun_eq_top (k : Type w) {V : Type u} (G : SimpleGraph V) [Finite V] [Field k] (i : V) : Submodule.span k (Set.range (zigzagProjectiveBasisFun k G i)) = ⊤

The vertex, outgoing-arrow and volume family spans Z e_i.

noncomputable def TauCeti.zigzagProjectiveBasis (k : Type w) {V : Type u} (G : SimpleGraph V) [Finite V] [Field k] (hns : ∀ (i : V), ∃ (j : V), G.Adj i j) (i : V) : Module.Basis (ZigzagProjectiveBasisIndex G i) k ↥(zigzagProjective k G i)

The vertex, outgoing-arrow and volume basis of Z e_i.

@[simp]

theorem TauCeti.zigzagProjectiveBasis_apply (k : Type w) {V : Type u} (G : SimpleGraph V) [Finite V] [Field k] (hns : ∀ (i : V), ∃ (j : V), G.Adj i j) (i : V) (b : ZigzagProjectiveBasisIndex G i) : (zigzagProjectiveBasis k G hns i) b = zigzagProjectiveBasisFun k G i b

theorem TauCeti.completeOrthogonalIdempotents_zigzagVertexIdempotent (k : Type w) {V : Type u} (G : SimpleGraph V) [CommRing k] [Fintype V] : CompleteOrthogonalIdempotents (zigzagVertexIdempotent k G)

The vertex idempotents of the zigzag relation quotient are a complete orthogonal family of idempotents: they are idempotent, pairwise orthogonal, and sum to 1.

theorem TauCeti.finrank_zigzagProjective (k : Type w) {V : Type u} (G : SimpleGraph V) [Field k] [Fintype V] [DecidableRel G.Adj] (hns : ∀ (i : V), ∃ (j : V), G.Adj i j) (i : V) : Module.finrank k ↥(zigzagProjective k G i) = 2 + G.degree i

The dimension of the vertex projective is two plus the degree of its vertex.