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 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.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

This is the vertex-projective part of Layer 3 of TauCetiRoadmap/ZigzagPreprojective/README.md. 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) [Field k] {V : Type u} (G : SimpleGraph V) [Finite V] (i : V) : nonisolatedZigzagQuotient k G

The vertex idempotent of the zigzag relation quotient.

Equations

• TauCeti.zigzagVertexIdempotent k G i = (TauCeti.zigzagMk k G) (TauCeti.PathAlgebra.vertexIdempotent k (TauCeti.DoubledQuiver.vertex G i))

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

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

Equations

• TauCeti.zigzagProjective k G i = Ideal.span {TauCeti.zigzagVertexIdempotent k G i}

@[simp]

theorem TauCeti.mem_zigzagProjective_iff (k : Type w) [Field k] {V : Type u} (G : SimpleGraph V) [Finite V] {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) [Field k] {V : Type u} (G : SimpleGraph V) [Finite V] (i : V) : ↥(zigzagProjective k G i)

The distinguished generator e_i of the vertex projective.

Equations

• TauCeti.zigzagProjectiveGenerator k G i = TauCeti.spanSingletonGenerator (TauCeti.zigzagVertexIdempotent k G i)

@[simp]

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

The vertex-projective grading

noncomputable def TauCeti.zigzagProjectiveGrade (k : Type w) [Field k] {V : Type u} (G : SimpleGraph V) [Finite V] (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.

Equations

• TauCeti.zigzagProjectiveGrade k G i d = Submodule.comap (Submodule.restrictScalars k (TauCeti.zigzagProjective k G i)).subtype (TauCeti.zigzagIntegerGrade k G d)

@[simp]

theorem TauCeti.mem_zigzagProjectiveGrade_iff (k : Type w) [Field k] {V : Type u} (G : SimpleGraph V) [Finite V] {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) [Field k] {V : Type u} (G : SimpleGraph V) [Finite V] (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].

Equations

• TauCeti.zigzagProjectiveShiftGrade k G i d = TauCeti.Graded.shift (TauCeti.zigzagProjectiveGrade k G i) (-d)

@[simp]

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

Projectivity

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

Right multiplication by e_i, corestricted to Z e_i.

Equations

• TauCeti.zigzagProjectiveProjection k G i = { toFun := fun (x : TauCeti.nonisolatedZigzagQuotient k G) => ⟨x * TauCeti.zigzagVertexIdempotent k G i, ⋯⟩, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem TauCeti.coe_zigzagProjectiveProjection (k : Type w) [Field k] {V : Type u} (G : SimpleGraph V) [Finite V] (i : V) (x : nonisolatedZigzagQuotient k G) : ↑((zigzagProjectiveProjection k G i) x) = x * zigzagVertexIdempotent k G i

@[simp]

theorem TauCeti.zigzagProjectiveProjection_coe (k : Type w) [Field k] {V : Type u} (G : SimpleGraph V) [Finite V] (i : V) (x : ↥(zigzagProjective k G i)) : (zigzagProjectiveProjection k G i) ↑x = x

Projecting an element of Z e_i back onto Z e_i fixes it.

theorem TauCeti.zigzagProjectiveProjection_comp_subtype (k : Type w) [Field k] {V : Type u} (G : SimpleGraph V) [Finite V] (i : V) : zigzagProjectiveProjection k G i ∘ₗ Submodule.subtype (zigzagProjective k G i) = LinearMap.id

The projection onto Z e_i splits its inclusion into the regular module.

theorem TauCeti.zigzagProjective_projective (k : Type w) [Field k] {V : Type u} (G : SimpleGraph V) [Finite V] (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) [Field k] {V : Type u} (G : SimpleGraph V) [Finite V] (i : V) : zigzagVertexIdempotent k G i ≠ 0

A vertex idempotent is nonzero in the zigzag relation quotient.

theorem TauCeti.isPrimitiveIdempotent_zigzagVertexIdempotent (k : Type w) [Field k] {V : Type u} (G : SimpleGraph V) [Finite V] (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) [Field k] {V : Type u} (G : SimpleGraph V) [Finite V] (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.

Equations

• TauCeti.ZigzagProjectiveBasisIndex G i = (Unit ⊕ { d : G.Dart // d.toProd.1 = i } ⊕ Unit)

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

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

Equations

• TauCeti.zigzagProjectiveBasisFun k G i (Sum.inl val) = TauCeti.zigzagProjectiveGenerator k G i
• TauCeti.zigzagProjectiveBasisFun k G i (Sum.inr (Sum.inl d)) = ⟨(TauCeti.zigzagMk k G) (TauCeti.PathAlgebra.ofArrow (TauCeti.DoubledQuiver.arrow G ⋯)), ⋯⟩
• TauCeti.zigzagProjectiveBasisFun k G i (Sum.inr (Sum.inr val)) = ⟨TauCeti.zigzagVolume k G i, ⋯⟩

@[simp]

theorem TauCeti.coe_zigzagProjectiveBasisFun_inl (k : Type w) [Field k] {V : Type u} (G : SimpleGraph V) [Finite V] (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) [Field k] {V : Type u} (G : SimpleGraph V) [Finite V] (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) [Field k] {V : Type u} (G : SimpleGraph V) [Finite V] (i : V) (a : Unit) : ↑(zigzagProjectiveBasisFun k G i (Sum.inr (Sum.inr a))) = zigzagVolume k G i

theorem TauCeti.linearIndependent_zigzagProjectiveBasisFun (k : Type w) [Field k] {V : Type u} (G : SimpleGraph V) [Finite V] (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) [Field k] {V : Type u} (G : SimpleGraph V) [Finite V] (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) [Field k] {V : Type u} (G : SimpleGraph V) [Finite V] (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.

Equations

• TauCeti.zigzagProjectiveBasis k G hns i = Module.Basis.mk ⋯ ⋯

@[simp]

theorem TauCeti.zigzagProjectiveBasis_apply (k : Type w) [Field k] {V : Type u} (G : SimpleGraph V) [Finite V] (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.finrank_zigzagProjective (k : Type w) [Field k] {V : Type u} (G : SimpleGraph V) [Finite V] [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.