Documentation

TauCeti.RepresentationTheory.Quiver.PathAlgebra.RelationIdeal

Ideals generated by one corner relator per vertex #

Let R be a quiver with finitely many vertices and arrows, k a commutative ring, and let every vertex v carry a relator r_v lying in the left corner e_v kR, so that e_v r_v = r_v. This file describes the two-sided ideal I the relators generate, and the relations among the arrows into a fixed vertex in the quotient A = kR / I.

Since kR is generated by its vertex idempotents and arrows,

I = ∑_v r_v kR + ∑_b b I,

and cutting this down to the corner of j keeps only the relator at j and the arrows into j (TauCeti.PathAlgebra.exists_eq_sum_ofArrow_mul_of_mem_span_of_vertexIdempotent_mul).

Write r_j = ∑_{b : i ⟶ j} b c_b, decomposing the relator along its last arrow. If y_b are elements with ∑_b b y_b ∈ I, then there is a single Y with e_i y_b ≡ e_i c_b Y modulo I for every arrow b : i ⟶ j (TauCeti.PathAlgebra.exists_sub_mul_mem_span_of_sum_ofArrow_mul_mem_span). In the language of right A-modules, the kernel of

⨁_{b : i ⟶ j} e_i A ⟶ e_j A,    (z_b) ↦ ∑_b b z_b

is the image of A ⟶ ⨁_b e_i A, y ↦ (e_i c_b y)_b; when moreover c_b e_j = c_b for every b, as for the preprojective relators, y may be replaced by e_j y, so the image is already that of e_j A. The uniqueness of the last-arrow decomposition in kR (TauCeti.PathAlgebra.sum_ofArrow_mul_eq_zero_iff) is what lifts a relation among the b z_b in A to the relator.

Main results #

References #

theorem TauCeti.PathAlgebra.vertexIdempotent_mul_eq_ite {k : Type w} {R : Type u} [Quiver R] [Semiring k] [DecidableEq R] {r : R → pathAlgebra k R} (hl : ∀ (v : R), vertexIdempotent k v * r v = r v) (u v : R) :
vertexIdempotent k u * r v = if u = v then r v else 0

Left multiplication by a vertex idempotent keeps a corner relator at that vertex and kills the relators at the other vertices.

theorem TauCeti.PathAlgebra.exists_eq_sum_mul_add_sum_ofArrow_mul_of_mem_span {k : Type w} {R : Type u} [Quiver R] [CommRing k] [Fintype R] [(a b : R) → Fintype (a ⟶ b)] {r : R → pathAlgebra k R} (hl : ∀ (v : R), vertexIdempotent k v * r v = r v) {F : pathAlgebra k R} (hF : F ∈ TwoSidedIdeal.span (Set.range r)) :
∃ (Y : R → pathAlgebra k R) (Z : (i : R) × (j : R) × (i ⟶ j) → pathAlgebra k R), (∀ (a : (i : R) × (j : R) × (i ⟶ j)), Z a ∈ TwoSidedIdeal.span (Set.range r)) ∧ F = ∑ v : R, r v * Y v + ∑ a : (i : R) × (j : R) × (i ⟶ j), ofArrow a.snd.snd * Z a

Every element of the relation ideal is a combination of relators and of arrows times elements of the ideal. This is the identity I = ∑ᵥ r_v · kR + ∑_b b · I, valid because the path algebra is generated by the vertex idempotents and the arrows.

theorem TauCeti.PathAlgebra.exists_eq_sum_ofArrow_mul_of_mem_span_of_vertexIdempotent_mul {k : Type w} {R : Type u} [Quiver R] [CommRing k] [Fintype R] [(a b : R) → Fintype (a ⟶ b)] {r : R → pathAlgebra k R} (hl : ∀ (v : R), vertexIdempotent k v * r v = r v) {j : R} {F : pathAlgebra k R} (hF : F ∈ TwoSidedIdeal.span (Set.range r)) (hjF : vertexIdempotent k j * F = F) :
∃ (Y : pathAlgebra k R) (Z : (i : R) → (i ⟶ j) → pathAlgebra k R), (∀ (i : R) (b : i ⟶ j), Z i b ∈ TwoSidedIdeal.span (Set.range r)) ∧ F = r j * Y + ∑ i : R, ∑ b : i ⟶ j, ofArrow b * Z i b

The corner form of the relation ideal. An element F of the relation ideal in the corner e_j kR is r_j Y + ∑_{b : i ⟶ j} b Z_b with every Z_b in the ideal: the relators at the other vertices and the arrows into the other vertices are killed by e_j.

theorem TauCeti.PathAlgebra.exists_sub_mul_mem_span_of_sum_ofArrow_mul_mem_span {k : Type w} {R : Type u} [Quiver R] [CommRing k] [Fintype R] [(a b : R) → Fintype (a ⟶ b)] {r : R → pathAlgebra k R} (hl : ∀ (v : R), vertexIdempotent k v * r v = r v) {j : R} {c : (i : R) → (i ⟶ j) → pathAlgebra k R} (hrj : r j = ∑ i : R, ∑ b : i ⟶ j, ofArrow b * c i b) {y : (i : R) → (i ⟶ j) → pathAlgebra k R} (hy : ∑ i : R, ∑ b : i ⟶ j, ofArrow b * y i b ∈ TwoSidedIdeal.span (Set.range r)) :
∃ (Y : pathAlgebra k R), ∀ (i : R) (b : i ⟶ j), vertexIdempotent k i * y i b - vertexIdempotent k i * c i b * Y ∈ TwoSidedIdeal.span (Set.range r)

The relations among the arrows into a vertex are generated by its relator. Let r_j = ∑_{b : i ⟶ j} b c_b. If ∑_b b y_b lies in the relation ideal I, then one element Y gives e_i y_b ≡ e_i c_b Y modulo I for every arrow b : i ⟶ j.

Read in A = kR / I, this is exactness of A ⟶ ⨁_b e_i A ⟶ e_j A, y ↦ (e_i c_b y)_b and (z_b) ↦ ∑_b b z_b, at its middle term. The element Y is arbitrary in kR; it may be taken in e_j kR only when c_b e_j = c_b for every b.