Documentation

TauCeti.RepresentationTheory.Quiver.PathAlgebra.BacktrackRelator

Arrows acting injectively modulo weighted backtrack relators #

Let R be a finite quiver with an involutive reversal of arrows, such as the doubled quiver of a quiver or of a simple graph, and let ε be a labelling of its arrows by scalars in a commutative ring k. At every vertex u consider the weighted backtrack relator

r_u = ∑_{b : i ⟶ u} ε_b b b*,

written in Tau Ceti's later-factor-first convention, so that b b* traverses the reverse b* and then b. The preprojective relator (ε_b = ±1 according to whether b is an arrow of the original quiver or the reverse of one) and the signless relator (ε_b = 1) are of this form. Let A be the quotient of the path algebra kR by the two-sided ideal generated by the r_u, presented by a surjective algebra map π : kR → A with kernel that ideal.

For a vertex v the Koszul complex of the vertex module at v is

0 ⟶ e_v A ⟶ ⨁_{b : i ⟶ v} e_i A ⟶ e_v A,    y ↦ (ε_b b* y)_b,   (z_b) ↦ ∑_b b z_b.

Its two maps compose to left multiplication by r_v, hence to zero, and it is exact at its middle term for every labelling ε: the relations among the arrows into v are generated by r_v.

Exactness at the left end needs more. Choose an arrow α_u : u ⟶ t(u) at every vertex. If the choice is non-backtracking, meaning that the arrow chosen at t(u) is never the reverse of α_u, and the coefficient of the reverse β_u = α_u* is a unit for every u, then left multiplication by α_v is injective on e_v A, for every vertex v. Consequently the only y ∈ e_v A killed by the reverse b* of every arrow b into v is 0, so the left-hand map of the Koszul complex is injective.

Main results #

Implementation notes #

The local relation at u solves for one backtrack, β_u α_u = -ε_{β_u}⁻¹ ∑_{b ≠ β_u} ε_b b b*, the sum over the other arrows b into u. The non-backtracking condition says exactly that no α is a β, so the leading words β_u α_u of these rewriting rules never overlap, and as in Bergman's diamond lemma the rules define a left module directly. Its underlying k-module is free on the paths of R, and an arrow c acts on a path p by appending c, except that β_u acts on a path ending in α_u by the right-hand side of the rule, computed recursively on the shorter path. This action respects the relators, so A acts. The class map from paths to A is A-linear and recovers y from the action of y on the trivial paths, so the action is faithful. Since α_v acts on the paths ending at v by appending α_v, it acts injectively there, and so does α_v on e_v A.

The module is assembled by TauCeti.PathAlgebra.liftAlgHom on the product of the vertex components, so the argument works over every commutative ring.

References #

Linear combinations of paths #

The Koszul complex #

theorem TauCeti.PathAlgebra.sum_map_ofArrow_mul_smul_map_ofArrow_reverse_mul_eq_zero (k : Type w) {R : Type u} [CommRing k] [Quiver R] [Quiver.HasReverse R] [Fintype R] [(i j : R) → Fintype (i ⟶ j)] {ε : ⦃i j : R⦄ → (i ⟶ j) → k} {A : Type u_1} [Ring A] [Algebra k A] {r : R → pathAlgebra k R} (hr : ∀ (u : R), r u = ∑ i : R, ∑ b : i ⟶ u, ofArrow b * ε b • ofArrow (Quiver.reverse b)) {π : pathAlgebra k R →ₐ[k] A} (hrπ : ∀ (u : R), π (r u) = 0) (v : R) (y : A) :
∑ i : R, ∑ b : i ⟶ v, π (ofArrow b) * ε b • (π (ofArrow (Quiver.reverse b)) * y) = 0

The Koszul complex is a complex: the composite y ↦ ∑_b b (ε_b b* y) of its two maps at v is left multiplication by the relator r_v, which vanishes in A. This needs only that π kills every relator, not that its kernel is the ideal they generate.

theorem TauCeti.PathAlgebra.sum_map_ofArrow_mul_eq_zero_iff (k : Type w) {R : Type u} [CommRing k] [Quiver R] [Quiver.HasReverse R] [Fintype R] [(i j : R) → Fintype (i ⟶ j)] {ε : ⦃i j : R⦄ → (i ⟶ j) → k} {A : Type u_1} [Ring A] [Algebra k A] {r : R → pathAlgebra k R} (hr : ∀ (u : R), r u = ∑ i : R, ∑ b : i ⟶ u, ofArrow b * ε b • ofArrow (Quiver.reverse b)) {π : pathAlgebra k R →ₐ[k] A} (hπ : ∀ (f : pathAlgebra k R), π f = 0 ↔ f ∈ TwoSidedIdeal.span (Set.range r)) (hπs : Function.Surjective ⇑π) (v : R) {z : (i : R) → (i ⟶ v) → A} (hz : ∀ (i : R) (b : i ⟶ v), π (vertexIdempotent k i) * z i b = z i b) :
∑ i : R, ∑ b : i ⟶ v, π (ofArrow b) * z i b = 0 ↔ ∃ (y : A), π (vertexIdempotent k v) * y = y ∧ ∀ (i : R) (b : i ⟶ v), z i b = ε b • (π (ofArrow (Quiver.reverse b)) * y)

Exactness of the Koszul complex at its middle term. Let z_b ∈ e_i A for the arrows b : i ⟶ v. Then ∑_b b z_b = 0 exactly when there is one y ∈ e_v A with z_b = ε_b b* y for every b.

The rewriting rules #

The action of the path algebra #

The relators act by zero #

Reading paths back in the quotient #

Injectivity #

theorem TauCeti.PathAlgebra.map_ofArrow_mul_eq_zero_iff_of_ne_reverse (k : Type w) {R : Type u} [CommRing k] [Quiver R] [Quiver.HasInvolutiveReverse R] {σ : (v : R) → Quiver.Star v} {ε : ⦃i j : R⦄ → (i ⟶ j) → k} [Fintype R] [(i j : R) → Fintype (i ⟶ j)] {A : Type u_1} [Ring A] [Algebra k A] (hσ : ∀ (v : R), σ (σ v).fst ≠ Quiver.Star.mk (Quiver.reverse (σ v).snd)) (hε : ∀ (v : R), IsUnit (ε (Quiver.reverse (σ v).snd))) {r : R → pathAlgebra k R} (hr : ∀ (u : R), r u = ∑ i : R, ∑ b : i ⟶ u, ofArrow b * ε b • ofArrow (Quiver.reverse b)) {π : pathAlgebra k R →ₐ[k] A} (hπ : ∀ (f : pathAlgebra k R), π f = 0 ↔ f ∈ TwoSidedIdeal.span (Set.range r)) (hπs : Function.Surjective ⇑π) (v : R) {y : A} (hy : π (vertexIdempotent k v) * y = y) :
π (ofArrow (σ v).snd) * y = 0 ↔ y = 0

An arrow of a non-backtracking choice acts injectively. Let A be the quotient of the path algebra kR by the weighted backtrack relators r_u = ∑_{b : i ⟶ u} ε_b b b*, presented by the surjective algebra map π with kernel the ideal they generate. Let α_u = σ u be a choice of an arrow out of every vertex such that the arrow chosen at the head of α_u is never the reverse of α_u, and such that ε_{α_u*} is a unit. Then for y ∈ e_v A, α_v y = 0 exactly when y = 0.

theorem TauCeti.PathAlgebra.forall_map_ofArrow_reverse_mul_eq_zero_iff_of_ne_reverse (k : Type w) {R : Type u} [CommRing k] [Quiver R] [Quiver.HasInvolutiveReverse R] {σ : (v : R) → Quiver.Star v} {ε : ⦃i j : R⦄ → (i ⟶ j) → k} [Fintype R] [(i j : R) → Fintype (i ⟶ j)] {A : Type u_1} [Ring A] [Algebra k A] (hσ : ∀ (v : R), σ (σ v).fst ≠ Quiver.Star.mk (Quiver.reverse (σ v).snd)) (hε : ∀ (v : R), IsUnit (ε (Quiver.reverse (σ v).snd))) {r : R → pathAlgebra k R} (hr : ∀ (u : R), r u = ∑ i : R, ∑ b : i ⟶ u, ofArrow b * ε b • ofArrow (Quiver.reverse b)) {π : pathAlgebra k R →ₐ[k] A} (hπ : ∀ (f : pathAlgebra k R), π f = 0 ↔ f ∈ TwoSidedIdeal.span (Set.range r)) (hπs : Function.Surjective ⇑π) (v : R) {y : A} (hy : π (vertexIdempotent k v) * y = y) :
(∀ (i : R) (b : i ⟶ v), π (ofArrow (Quiver.reverse b)) * y = 0) ↔ y = 0

Exactness of the Koszul complex at its left end, for a non-backtracking choice. Under the hypotheses of TauCeti.PathAlgebra.map_ofArrow_mul_eq_zero_iff_of_ne_reverse, for y ∈ e_v A, b* y = 0 for every arrow b into v exactly when y = 0.