The arrow ideal of a path algebra, and its radical

The path algebra of a quiver is filtered by path length: pathSpan k Q n is the k-span of the paths of length at least n. Concatenation adds lengths, so the filtration is multiplicative, pathSpan k Q m * pathSpan k Q n ⊆ pathSpan k Q (m + n), and its first step is a two-sided ideal, the arrow ideal arrowIdeal k Q: the elements with no trivial path in their support, that is, those whose coordinates on the trivial paths all vanish. It is the ideal generated by the arrows, and its powers are the steps of the filtration: pathSpan k Q n is (arrowIdeal k Q) ^ n.

For a finite acyclic quiver the filtration dies: every path has length strictly less than the number of vertices, so pathSpan k Q (Nat.card Q) = ⊥ and every element of the arrow ideal is nilpotent, hence in the Jacobson radical over any commutative coefficient ring. The opposite inclusion holds for every finite quiver when the coefficient ring has zero Jacobson radical: the trivial-coefficient homomorphism, followed by evaluation at a vertex, sends radical elements into the scalar radical, so their trivial coordinates vanish. Thus for a finite acyclic quiver over such a ring, including a field, the radical is exactly the arrow ideal (TauCeti.jacobson_pathAlgebra_eq_arrowIdeal). Acyclicity is needed for the equality: the one-loop quiver has kQ ≅ k[X] (TauCeti.PathAlgebra.oneLoopAlgEquiv), which over a field has zero radical while its arrow ideal (X) is nonzero.

Main definitions

• TauCeti.pathSpan k Q n: the k-span of the paths of length at least n.
• TauCeti.arrowIdeal k Q: the arrow ideal, the ideal of elements supported on the paths of positive length, with TauCeti.arrowIdeal.instIsTwoSided recording that it is two-sided.

Main results

• TauCeti.mul_mem_pathSpan: the length filtration is multiplicative, and TauCeti.ofPath_mem_pathSpan_iff: a basis path lies in a step exactly when it is long enough.
• TauCeti.restrictScalars_arrowIdeal_pow: the steps of the length filtration are the powers of the arrow ideal, TauCeti.mem_arrowIdeal_pow in terms of membership, and TauCeti.ofPath_mem_arrowIdeal_pow_iff on a basis path.
• TauCeti.mem_arrowIdeal_iff_repr_nil: an element lies in the arrow ideal exactly when all its coordinates on the trivial paths vanish, TauCeti.mem_arrowIdeal_iff in terms of the lengths of the paths in its support, and TauCeti.ofPath_mem_arrowIdeal_iff on a basis path.
• TauCeti.arrowIdeal_eq_span_arrows: the arrow ideal is the ideal generated by the arrows.
• TauCeti.pathSpan_eq_bot_of_isAcyclic: for a finite acyclic quiver the filtration reaches ⊥ at the number of vertices, and TauCeti.isNilpotent_of_mem_arrowIdeal: every element of the arrow ideal is then nilpotent.
• TauCeti.jacobson_pathAlgebra_le_arrowIdeal: over a commutative ring with zero Jacobson radical, the radical of the path algebra of any finite quiver is contained in the arrow ideal.
• TauCeti.jacobson_pathAlgebra_eq_arrowIdeal: the Jacobson radical of the path algebra of a finite acyclic quiver over a commutative ring with zero radical is the arrow ideal.

Implementation notes

pathSpan is a k-submodule rather than an ideal, the multiplicativity statement being about the k-span in any case. Every step could be packaged as a two-sided ideal: the m = 0 and the n = 0 cases of multiplicativity, pathSpan k Q 0 being everything, close pathSpan k Q n under multiplication by the path algebra on either side. Only the first step is packaged separately here, as arrowIdeal k Q, that being the step the radical theorem is about; the higher steps are its powers, TauCeti.restrictScalars_arrowIdeal_pow identifying pathSpan k Q n with (arrowIdeal k Q) ^ n as a k-submodule, which is the form the radical powers rad ^ n and the admissible ideals rad ^ N ⊆ I ⊆ rad ^ 2 are stated against.

Membership is described by coordinates for the path basis and on a basis path, at both levels: TauCeti.mem_pathSpan_iff and TauCeti.mem_arrowIdeal_iff say that every path carrying a nonzero coordinate is long enough, which is how nilpotence of the arrow ideal is proved, while TauCeti.ofPath_mem_pathSpan_iff and TauCeti.ofPath_mem_arrowIdeal_iff recognize a basis path, which is how the ideal is recognized in practice. At the level of the arrow ideal the length condition collapses to the vanishing of the named coordinates on the trivial paths, which is TauCeti.mem_arrowIdeal_iff_repr_nil. The bridge from the arrow ideal to the pathSpan it is implemented by is private: these characterizations, together with TauCeti.restrictScalars_arrowIdeal_pow and TauCeti.arrowIdeal_eq_span_arrows, are what consumers need.

Of these, the basis-path ones are simp: their right-hand sides are smaller than their left. The membership iffs whose left-hand side is the bare f ∈ arrowIdeal k Q are not, because tagging one of them would rewrite the left-hand side of TauCeti.ofPath_mem_arrowIdeal_iff away, which the simpNF linter rejects.

The arrow ideal is built over a commutative base semiring: the multiplicativity of the filtration, which is what makes it an ideal, needs [CommSemiring k] (see the Multiplicative section), and being an Ideal needs the unit of the path algebra, hence [Finite Q]. The arrow ideal of a finite acyclic quiver lies in the radical over any commutative ring. No vertex idempotent lies in the radical over any nontrivial ring. The reverse radical inclusion and the equality require only that the commutative coefficient ring have zero Jacobson radical; no acyclicity is needed for the reverse inclusion.

References

Assem--Simson--Skowroński, Elements of the Representation Theory of Associative Algebras I, Ch. II and III.

noncomputable def TauCeti.pathSpan (k : Type w) (Q : Type u) [Semiring k] [Quiver Q] (n : ℕ) : Submodule k (pathAlgebra k Q)

The k-span of the paths of length at least n: the n-th step of the length filtration of the path algebra.

Equations

• TauCeti.pathSpan k Q n = Submodule.span k (⇑(TauCeti.pathAlgebraBasis k Q) '' {x : TauCeti.Quiver.TotalPath Q | n ≤ x.snd.snd.length})

theorem TauCeti.pathSpan_eq_span_image_basis (k : Type w) (Q : Type u) [Semiring k] [Quiver Q] (n : ℕ) : pathSpan k Q n = Submodule.span k (⇑(pathAlgebraBasis k Q) '' {x : Quiver.TotalPath Q | n ≤ x.snd.snd.length})

The length filtration is the span of the corresponding path-basis vectors.

theorem TauCeti.mem_pathSpan_iff {k : Type w} {Q : Type u} [Semiring k] [Quiver Q] {n : ℕ} {f : pathAlgebra k Q} : f ∈ pathSpan k Q n ↔ ∀ (x : Quiver.TotalPath Q), ((pathAlgebraBasis k Q).repr f) x ≠ 0 → n ≤ x.snd.snd.length

An element lies in the n-th step of the length filtration exactly when every path carrying a nonzero coordinate has length at least n.

theorem TauCeti.ofPath_mem_pathSpan {k : Type w} {Q : Type u} [Semiring k] [Quiver Q] {n : ℕ} {x : Quiver.TotalPath Q} (hx : n ≤ x.snd.snd.length) : PathAlgebra.ofPath x ∈ pathSpan k Q n

A path of length at least n lies in the n-th step of the length filtration.

@[simp]

theorem TauCeti.ofPath_mem_pathSpan_iff {k : Type w} {Q : Type u} [Semiring k] [Quiver Q] [Nontrivial k] {n : ℕ} {x : Quiver.TotalPath Q} : PathAlgebra.ofPath x ∈ pathSpan k Q n ↔ n ≤ x.snd.snd.length

A basis path lies in the n-th step of the length filtration exactly when it has length at least n: the filtration meets the path basis in the long enough paths.

@[simp]

theorem TauCeti.pathSpan_zero (k : Type w) (Q : Type u) [Semiring k] [Quiver Q] : pathSpan k Q 0 = ⊤

The length filtration starts at the whole path algebra.

theorem TauCeti.mem_pathSpan_zero {k : Type w} {Q : Type u} [Semiring k] [Quiver Q] (f : pathAlgebra k Q) : f ∈ pathSpan k Q 0

Everything lies in the zeroth step of the length filtration.

theorem TauCeti.pathSpan_le_pathSpan {k : Type w} {Q : Type u} [Semiring k] [Quiver Q] {m n : ℕ} (h : m ≤ n) : pathSpan k Q n ≤ pathSpan k Q m

The length filtration is decreasing.

theorem TauCeti.pathSpan_eq_bot_of_isAcyclic (k : Type w) (Q : Type u) [Semiring k] [Quiver Q] [Finite Q] (h : Quiver.IsAcyclic Q) : pathSpan k Q (Nat.card Q) = ⊥

The length filtration of a finite acyclic quiver dies at the number of vertices: every path of a finite acyclic quiver has length strictly less than the number of vertices.

theorem TauCeti.mul_mem_pathSpan {k : Type w} {Q : Type u} [CommSemiring k] [Quiver Q] {m n : ℕ} {f g : pathAlgebra k Q} (hf : f ∈ pathSpan k Q m) (hg : g ∈ pathSpan k Q n) : f * g ∈ pathSpan k Q (m + n)

The length filtration is multiplicative: concatenating a path of length at least m with one of length at least n gives a path of length at least m + n.

theorem TauCeti.pow_mem_pathSpan {k : Type w} {Q : Type u} [CommSemiring k] [Quiver Q] [Finite Q] {f : pathAlgebra k Q} (hf : f ∈ pathSpan k Q 1) (n : ℕ) : f ^ n ∈ pathSpan k Q n

Powers of an element of the first step of the length filtration climb the filtration.

noncomputable def TauCeti.arrowIdeal (k : Type w) (Q : Type u) [CommSemiring k] [Quiver Q] [Finite Q] : Ideal (pathAlgebra k Q)

The arrow ideal of a path algebra: the elements whose coordinates on the trivial paths all vanish, equivalently the k-span of the paths of positive length. It is the ideal generated by the arrows of the quiver.

Equations

• TauCeti.arrowIdeal k Q = { carrier := ↑(TauCeti.pathSpan k Q 1), add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }

theorem TauCeti.mem_arrowIdeal_iff {k : Type w} {Q : Type u} [CommSemiring k] [Quiver Q] [Finite Q] {f : pathAlgebra k Q} : f ∈ arrowIdeal k Q ↔ ∀ (x : Quiver.TotalPath Q), ((pathAlgebraBasis k Q).repr f) x ≠ 0 → 0 < x.snd.snd.length

Membership in the arrow ideal, read off the path basis: an element lies in the arrow ideal exactly when every path carrying a nonzero coordinate has positive length.

theorem TauCeti.mem_arrowIdeal_iff_repr_nil {k : Type w} {Q : Type u} [CommSemiring k] [Quiver Q] [Finite Q] {f : pathAlgebra k Q} : f ∈ arrowIdeal k Q ↔ ∀ (v : Q), ((pathAlgebraBasis k Q).repr f) ⟨v, ⟨v, Quiver.Path.nil⟩⟩ = 0

Membership in the arrow ideal, as the vanishing of the trivial coordinates: an element lies in the arrow ideal exactly when its coordinate on the trivial path at each vertex vanishes. This is the form to check membership against, the trivial paths being the only ones of length zero.

instance TauCeti.arrowIdeal.instIsTwoSided {k : Type w} {Q : Type u} [CommSemiring k] [Quiver Q] [Finite Q] : (arrowIdeal k Q).IsTwoSided

The arrow ideal is two-sided: appending a path to a path of positive length leaves its length positive.

theorem TauCeti.ofPath_mem_arrowIdeal {k : Type w} {Q : Type u} [CommSemiring k] [Quiver Q] [Finite Q] {x : Quiver.TotalPath Q} (hx : 0 < x.snd.snd.length) : PathAlgebra.ofPath x ∈ arrowIdeal k Q

A path of positive length lies in the arrow ideal.

@[simp]

theorem TauCeti.ofPath_mem_arrowIdeal_iff {k : Type w} {Q : Type u} [CommSemiring k] [Quiver Q] [Finite Q] [Nontrivial k] {x : Quiver.TotalPath Q} : PathAlgebra.ofPath x ∈ arrowIdeal k Q ↔ 0 < x.snd.snd.length

A basis path lies in the arrow ideal exactly when it has positive length: the arrow ideal meets the path basis in the nontrivial paths.

theorem TauCeti.vertexIdempotent_notMem_arrowIdeal {k : Type w} {Q : Type u} [CommSemiring k] [Quiver Q] [Finite Q] [Nontrivial k] (v : Q) : PathAlgebra.vertexIdempotent k v ∉ arrowIdeal k Q

No vertex idempotent lies in the arrow ideal: a trivial path has length zero.

theorem TauCeti.ofArrow_mem_arrowIdeal {k : Type w} {Q : Type u} [CommSemiring k] [Quiver Q] [Finite Q] {a b : Q} (e : a ⟶ b) : PathAlgebra.ofArrow e ∈ arrowIdeal k Q

An arrow lies in the arrow ideal.

theorem TauCeti.ofPath_mem_arrowIdeal_pow {k : Type w} {Q : Type u} [CommSemiring k] [Quiver Q] [Finite Q] (x : Quiver.TotalPath Q) : PathAlgebra.ofPath x ∈ arrowIdeal k Q ^ x.snd.snd.length

A basis path lies in the power of the arrow ideal named by its length: a path is the product of its arrows, one factor for each.

theorem TauCeti.mem_arrowIdeal_pow {k : Type w} {Q : Type u} [CommSemiring k] [Quiver Q] [Finite Q] {n : ℕ} {f : pathAlgebra k Q} : f ∈ arrowIdeal k Q ^ n ↔ f ∈ pathSpan k Q n

The powers of the arrow ideal are the steps of the length filtration, in terms of membership: a product of n elements of the arrow ideal is supported on the paths of length at least n, and conversely such a path is a product of n arrows and a shorter path.

@[simp]

theorem TauCeti.ofPath_mem_arrowIdeal_pow_iff {k : Type w} {Q : Type u} [CommSemiring k] [Quiver Q] [Finite Q] [Nontrivial k] {n : ℕ} {x : Quiver.TotalPath Q} : PathAlgebra.ofPath x ∈ arrowIdeal k Q ^ n ↔ n ≤ x.snd.snd.length

A basis path lies in the n-th power of the arrow ideal exactly when it has length at least n: the powers of the arrow ideal meet the path basis in the long enough paths.

theorem TauCeti.arrowIdeal_eq_span_arrows (k : Type w) (Q : Type u) [CommSemiring k] [Quiver Q] [Finite Q] : arrowIdeal k Q = Ideal.span (Set.range fun (e : (a : Q) × (b : Q) × (a ⟶ b)) => PathAlgebra.ofArrow e.snd.snd)

The arrow ideal is the ideal generated by the arrows, which is what its name says. Every path of positive length factors as a shorter path times its first arrow — the path algebra writes the later factor first — so it is a left multiple of an arrow.

theorem TauCeti.restrictScalars_arrowIdeal_pow (k : Type w) (Q : Type u) [CommSemiring k] [Quiver Q] [Finite Q] (n : ℕ) : Submodule.restrictScalars k (arrowIdeal k Q ^ n) = pathSpan k Q n

The length filtration is the filtration by the powers of the arrow ideal: the n-th step pathSpan k Q n is the k-submodule underlying (arrowIdeal k Q) ^ n. This is what makes every step an ideal, and the form the radical powers are measured against.

theorem TauCeti.isNilpotent_of_mem_arrowIdeal {k : Type w} {Q : Type u} [CommSemiring k] [Quiver Q] [Finite Q] (h : Quiver.IsAcyclic Q) {f : pathAlgebra k Q} (hf : f ∈ arrowIdeal k Q) : IsNilpotent f

Every element of the arrow ideal of a finite acyclic quiver is nilpotent: its Nat.card Q-th power lies in a step of the length filtration that has already died.

theorem TauCeti.arrowIdeal_le_jacobson {k : Type w} {Q : Type u} [Quiver Q] [Finite Q] [CommRing k] (h : Quiver.IsAcyclic Q) : arrowIdeal k Q ≤ Ring.jacobson (pathAlgebra k Q)

The arrow ideal of a finite acyclic quiver over a commutative ring is contained in the Jacobson radical.

theorem TauCeti.vertexIdempotent_notMem_jacobson {k : Type w} {Q : Type u} [Quiver Q] [Finite Q] [Ring k] [Nontrivial k] (v : Q) : PathAlgebra.vertexIdempotent k v ∉ Ring.jacobson (pathAlgebra k Q)

No vertex idempotent lies in the Jacobson radical over a nontrivial ring of coefficients.

theorem TauCeti.jacobson_pathAlgebra_le_arrowIdeal (k : Type w) (Q : Type u) [CommRing k] [Quiver Q] [Finite Q] (hk : Ring.jacobson k = ⊥) : Ring.jacobson (pathAlgebra k Q) ≤ arrowIdeal k Q

The radical of the path algebra of any finite quiver over a commutative ring with zero Jacobson radical is contained in the arrow ideal. Evaluation of the trivial coefficients at each vertex is a surjection onto the coefficient ring, so it sends radical elements to zero.

theorem TauCeti.jacobson_pathAlgebra_eq_arrowIdeal (k : Type w) (Q : Type u) [CommRing k] [Quiver Q] [Finite Q] (hk : Ring.jacobson k = ⊥) (h : Quiver.IsAcyclic Q) : Ring.jacobson (pathAlgebra k Q) = arrowIdeal k Q

The Jacobson radical of the path algebra of a finite acyclic quiver is its arrow ideal.

The coefficient ring need only have zero Jacobson radical. The arrow ideal is nilpotent, hence inside the radical, and the trivial-coordinate maps give the opposite inclusion.