Matrix representations of signless preprojective algebras

Let G be a finite simple graph and m a finite type. Put a copy of kᵐ at every vertex and choose, for every pair of adjacent vertices i ∼ j, a matrix β i j for the arrow i → j of the doubled quiver. The backtrack v → w → v then acts at v by β w v * β v w, so the family is a representation of the signless preprojective algebra Π⁺(G) exactly when the signless matrix relations

∑_{w ∼ v} β w v * β v w = 0

hold at every vertex v. The representation is an algebra homomorphism Π⁺(G) → Matrix (V × m) (V × m) k sending the vertex idempotent at v to the block projection E_vv ⊗ 1 and the arrow i → j to the block E_ji ⊗ β i j.

Through such a representation, the matrix trace is a linear functional on Π⁺(G) which vanishes on commutators. An element whose image has nonzero trace therefore has nonzero class in the cyclic quotient Π⁺(G) / [Π⁺(G), Π⁺(G)], the zeroth Hochschild homology of Π⁺(G).

A representation of a subgraph extends by zero along a copy, by SimpleGraph.Copy.sum_extendByZero_mul_extendByZero.

Main definitions

• TauCeti.signlessMatrixRepresentation: the representation of Π⁺(G) determined by a family of matrices satisfying the signless relations.

Main results

• TauCeti.signlessMatrixRepresentation_vertexIdempotent, TauCeti.signlessMatrixRepresentation_ofPath_toPath and TauCeti.signlessMatrixRepresentation_ofArrow: the values on vertex idempotents and arrows.
• TauCeti.signlessMatrixRepresentation_backtrackElem: a backtrack v → w → v acts by the block E_vv ⊗ (β w v * β v w).
• TauCeti.signlessMatrixRepresentation_list_prod_backtrackElem: a nonempty product of backtracks at a common vertex v acts by the block E_vv ⊗ ∏ (β w v * β v w).
• TauCeti.trace_signlessMatrixRepresentation_list_prod_backtrackElem: the trace of a nonempty product of backtracks at a common vertex.
• TauCeti.exists_mem_signlessPreprojectiveGrade_notMem_commutatorSubmodule_of_trace_ne_zero: a product of backtracks of a subgraph acting with nonzero trace gives a nonzero class in the cyclic quotient of Π⁺(G).
• TauCeti.exists_mem_signlessPreprojectiveGrade_notMem_commutatorSubmodule_of_trace_eq_one: the same for an integer matrix family, whose product of backtracks has trace one, over every nontrivial commutative ring.

References

• S. Huerfano and M. Khovanov, A category for the adjoint representation, Section 3, for the signless relation.
• J.-L. Loday, Cyclic Homology, Section 1.1, for the cyclic quotient as zeroth Hochschild homology.

The representation

noncomputable def TauCeti.signlessMatrixRepresentation (k : Type w) [CommRing k] {V : Type u} {G : SimpleGraph V} {m : Type u_1} [Fintype V] [DecidableEq V] [Fintype m] [DecidableEq m] [DecidableRel G.Adj] (β : V → V → Matrix m m k) (hβ : ∀ (v : V), ∑ w ∈ G.neighborFinset v, β w v * β v w = 0) : signlessPreprojectiveAlgebra k (DoubledQuiver G) →ₐ[k] Matrix (V × m) (V × m) k

The matrix representation of a signless preprojective algebra: a family β of matrices, β i j for the arrow i → j of the doubled quiver, satisfying the signless relations ∑_{w ∼ v} β w v * β v w = 0 defines an algebra homomorphism from Π⁺(G) to block matrices. The vertex idempotent at v goes to the block projection E_vv ⊗ 1, and the arrow i → j to the block E_ji ⊗ β i j. The values of β at non-adjacent vertices are not used.

@[simp]

theorem TauCeti.signlessMatrixRepresentation_vertexIdempotent {k : Type w} [CommRing k] {V : Type u} {G : SimpleGraph V} {m : Type u_1} [Fintype V] [DecidableEq V] [Fintype m] [DecidableEq m] [DecidableRel G.Adj] (β : V → V → Matrix m m k) (hβ : ∀ (v : V), ∑ w ∈ G.neighborFinset v, β w v * β v w = 0) (v : V) : (signlessMatrixRepresentation k β hβ) ((signlessPreprojectiveMk k (DoubledQuiver G)) (PathAlgebra.vertexIdempotent k (DoubledQuiver.vertex G v))) = Matrix.kroneckerMap (fun (x1 x2 : k) => x1 * x2) (Matrix.single v v 1) 1

The matrix representation sends the vertex idempotent at v to the block projection.

@[simp]

theorem TauCeti.signlessMatrixRepresentation_ofPath_toPath {k : Type w} [CommRing k] {V : Type u} {G : SimpleGraph V} {m : Type u_1} [Fintype V] [DecidableEq V] [Fintype m] [DecidableEq m] [DecidableRel G.Adj] (β : V → V → Matrix m m k) (hβ : ∀ (v : V), ∑ w ∈ G.neighborFinset v, β w v * β v w = 0) {i j : V} (h : G.Adj i j) : (signlessMatrixRepresentation k β hβ) ((signlessPreprojectiveMk k (DoubledQuiver G)) (PathAlgebra.ofPath ⟨DoubledQuiver.vertex G i, ⟨DoubledQuiver.vertex G j, (DoubledQuiver.arrow G h).toPath⟩⟩)) = Matrix.kroneckerMap (fun (x1 x2 : k) => x1 * x2) (Matrix.single j i 1) (β i j)

The matrix representation sends the length-one path of the arrow i → j to the block E_ji ⊗ β i j. This is the simp-normal form of signlessMatrixRepresentation_ofArrow.

theorem TauCeti.signlessMatrixRepresentation_ofArrow {k : Type w} [CommRing k] {V : Type u} {G : SimpleGraph V} {m : Type u_1} [Fintype V] [DecidableEq V] [Fintype m] [DecidableEq m] [DecidableRel G.Adj] (β : V → V → Matrix m m k) (hβ : ∀ (v : V), ∑ w ∈ G.neighborFinset v, β w v * β v w = 0) {i j : V} (h : G.Adj i j) : (signlessMatrixRepresentation k β hβ) ((signlessPreprojectiveMk k (DoubledQuiver G)) (PathAlgebra.ofArrow (DoubledQuiver.arrow G h))) = Matrix.kroneckerMap (fun (x1 x2 : k) => x1 * x2) (Matrix.single j i 1) (β i j)

The matrix representation sends the arrow i → j to the block E_ji ⊗ β i j. This is not a simp lemma: ofArrow is not in simp-normal form, and signlessMatrixRepresentation_ofPath_toPath covers its normal form.

@[simp]

theorem TauCeti.signlessMatrixRepresentation_backtrackElem {k : Type w} [CommRing k] {V : Type u} {G : SimpleGraph V} {m : Type u_1} [Fintype V] [DecidableEq V] [Fintype m] [DecidableEq m] [DecidableRel G.Adj] (β : V → V → Matrix m m k) (hβ : ∀ (v : V), ∑ w ∈ G.neighborFinset v, β w v * β v w = 0) {v w : V} (h : G.Adj v w) : (signlessMatrixRepresentation k β hβ) ((signlessPreprojectiveMk k (DoubledQuiver G)) (DoubledQuiver.backtrackElem G k h)) = Matrix.kroneckerMap (fun (x1 x2 : k) => x1 * x2) (Matrix.single v v 1) (β w v * β v w)

The matrix representation sends the backtrack v → w → v to the block E_vv ⊗ (β w v * β v w).

theorem TauCeti.signlessMatrixRepresentation_list_prod_backtrackElem {k : Type w} [CommRing k] {V : Type u} {G : SimpleGraph V} {m : Type u_1} [Fintype V] [DecidableEq V] [Fintype m] [DecidableEq m] [DecidableRel G.Adj] (β : V → V → Matrix m m k) (hβ : ∀ (v : V), ∑ w ∈ G.neighborFinset v, β w v * β v w = 0) {v : V} (l : List { w : V // G.Adj v w }) (hl : l ≠ []) : (signlessMatrixRepresentation k β hβ) (List.map (fun (w : { w : V // G.Adj v w }) => (signlessPreprojectiveMk k (DoubledQuiver G)) (DoubledQuiver.backtrackElem G k ⋯)) l).prod = Matrix.kroneckerMap (fun (x1 x2 : k) => x1 * x2) (Matrix.single v v 1) (List.map (fun (w : { w : V // G.Adj v w }) => β (↑w) v * β v ↑w) l).prod

The matrix representation sends a nonempty product of backtracks v → w → v at a common vertex v to the block E_vv ⊗ ∏ (β w v * β v w), the blocks multiplied in the same order.

theorem TauCeti.trace_signlessMatrixRepresentation_list_prod_backtrackElem {k : Type w} [CommRing k] {V : Type u} {G : SimpleGraph V} {m : Type u_1} [Fintype V] [DecidableEq V] [Fintype m] [DecidableEq m] [DecidableRel G.Adj] (β : V → V → Matrix m m k) (hβ : ∀ (v : V), ∑ w ∈ G.neighborFinset v, β w v * β v w = 0) {v : V} (l : List { w : V // G.Adj v w }) (hl : l ≠ []) : ((signlessMatrixRepresentation k β hβ) (List.map (fun (w : { w : V // G.Adj v w }) => (signlessPreprojectiveMk k (DoubledQuiver G)) (DoubledQuiver.backtrackElem G k ⋯)) l).prod).trace = (List.map (fun (w : { w : V // G.Adj v w }) => β (↑w) v * β v ↑w) l).prod.trace

The trace of the image of a nonempty product of backtracks v → w → v at a common vertex v is the trace of the product of their blocks at v.

Nonzero cyclic classes

theorem TauCeti.exists_mem_signlessPreprojectiveGrade_notMem_commutatorSubmodule_of_trace_ne_zero {k : Type w} [CommRing k] {V : Type u} {G : SimpleGraph V} {m : Type u_1} [Fintype V] [DecidableRel G.Adj] [Fintype m] [DecidableEq m] {W : Type u_2} [Fintype W] {H : SimpleGraph W} [DecidableRel H.Adj] (f : H.Copy G) (β : W → W → Matrix m m k) (hβ : ∀ (x : W), ∑ y ∈ H.neighborFinset x, β y x * β x y = 0) {c : W} (l : List { a : W // H.Adj c a }) (htr : (List.map (fun (a : { a : W // H.Adj c a }) => β (↑a) c * β c ↑a) l).prod.trace ≠ 0) : ∃ x ∈ signlessPreprojectiveGrade k (DoubledQuiver G) (2 * l.length), x ∉ commutatorSubmodule k (signlessPreprojectiveAlgebra k (DoubledQuiver G))

Nonzero cyclic classes from a matrix representation of a subgraph. Let f be a copy of a graph H in G, not necessarily induced, and let β be a family of matrices on H satisfying the signless relations. If a product of backtracks c → a → c at a vertex c of H acts at c by a matrix of nonzero trace, then the corresponding product of backtracks of G at f c is an element of path degree 2 * l.length of Π⁺(G) which does not lie in the commutator submodule [Π⁺(G), Π⁺(G)]: its class in the cyclic quotient is nonzero.

theorem TauCeti.sum_mapMatrix_intCast_mul_mapMatrix_intCast (k : Type w) [CommRing k] {m : Type u_1} [Fintype m] [DecidableEq m] {W : Type u_2} [Fintype W] {H : SimpleGraph W} [DecidableRel H.Adj] (β : W → W → Matrix m m ℤ) (h₀ : ∀ (v w : W), ¬H.Adj v w → β v w = 0) (h : ∀ (v : W), ∑ w : W, β w v * β v w = 0) (v : W) : ∑ w ∈ H.neighborFinset v, (Int.castRingHom k).mapMatrix (β w v) * (Int.castRingHom k).mapMatrix (β v w) = 0

An integer matrix family which vanishes off the edges of H and satisfies the signless relations, as sums over all vertices, satisfies them over every commutative ring.

theorem TauCeti.exists_mem_signlessPreprojectiveGrade_notMem_commutatorSubmodule_of_trace_eq_one (k : Type w) [CommRing k] {V : Type u} {G : SimpleGraph V} {m : Type u_1} [Fintype V] [DecidableRel G.Adj] [Fintype m] [DecidableEq m] {W : Type u_2} [Fintype W] {H : SimpleGraph W} [Nontrivial k] (f : H.Copy G) (β : W → W → Matrix m m ℤ) (h₀ : ∀ (v w : W), ¬H.Adj v w → β v w = 0) (h : ∀ (v : W), ∑ w : W, β w v * β v w = 0) {c : W} (l : List { a : W // H.Adj c a }) (htr : (List.map (fun (a : { a : W // H.Adj c a }) => β (↑a) c * β c ↑a) l).prod.trace = 1) : ∃ x ∈ signlessPreprojectiveGrade k (DoubledQuiver G) (2 * l.length), x ∉ commutatorSubmodule k (signlessPreprojectiveAlgebra k (DoubledQuiver G))

Nonzero cyclic classes from an integer matrix representation of a subgraph. An integer matrix family on H which vanishes off the edges and satisfies the signless relations, together with a product of backtracks at a vertex c of H acting at c with trace one, gives an element of path degree 2 * l.length of Π⁺(G) outside [Π⁺(G), Π⁺(G)] along any copy of H in G, over every nontrivial commutative ring.