Admissible ideals and bound quiver algebras

A two-sided ideal I of a path algebra kQ is admissible when it is squeezed between a power of the arrow ideal R and its square, R ^ N ≤ I ≤ R ^ 2. The two bounds say complementary things about the relations I imposes. The upper bound I ≤ R ^ 2 says that every relation is a combination of paths of length at least two: a relation involving a vertex idempotent or a single arrow would change the quiver data itself — identifying or collapsing vertices or arrows — rather than impose a relation on the paths of Q. The lower bound R ^ N ≤ I says that all long enough paths are killed, which is what cuts the quotient down to finite dimension.

The quotient kQ ⧸ I by an admissible ideal is a bound quiver algebra, and the two main results here are its two basic properties: it is finite-dimensional whenever the quiver has finitely many vertices and arrows, even when kQ itself is not, and every element of the arrow ideal becomes nilpotent in it.

Main definitions

• TauCeti.IsAdmissibleIdeal: the predicate R ^ N ≤ I ≤ R ^ 2 on a two-sided ideal of a path algebra, for the arrow ideal R = TauCeti.arrowIdeal k Q and some N.

Main results

• TauCeti.IsAdmissibleIdeal.finiteDimensional_quotient: a bound quiver algebra is finite-dimensional, over a quiver with finitely many vertices and finitely many arrows. No acyclicity is needed, and the one-loop quiver shows that this is a genuine gain: its path algebra k[X] is infinite-dimensional (TauCeti.not_module_finite_pathAlgebra_oneLoop) while the quotients k[X] ⧸ (Xⁿ) by the admissible ideals of TauCeti.isAdmissibleIdeal_arrowIdeal_pow are not.
• TauCeti.IsAdmissibleIdeal.isNilpotent_mk_of_mem_arrowIdeal: the image of an element of the arrow ideal in a bound quiver algebra is nilpotent.
• TauCeti.IsAdmissibleIdeal.ofPath_notMem_of_length_lt_two, together with TauCeti.IsAdmissibleIdeal.vertexIdempotent_notMem and TauCeti.IsAdmissibleIdeal.ofArrow_notMem: an admissible ideal contains no vertex idempotent and no arrow, so the quiver survives the passage to the quotient. In particular the quotient is nonzero, TauCeti.IsAdmissibleIdeal.nontrivial_quotient. More is true and is TauCeti.IsAdmissibleIdeal.linearIndependent_mk_ofPath_of_length_lt_two: the vertices and the arrows stay linearly independent in the quotient, so the quotient map is injective on their span.
• TauCeti.isAdmissibleIdeal_iff: admissibility checked entirely on the path basis.
• TauCeti.isAdmissibleIdeal_arrowIdeal_pow: the powers R ^ n with 2 ≤ n are admissible, and TauCeti.isAdmissibleIdeal_bot_of_isAcyclic: over a finite acyclic quiver the zero ideal is admissible, so kQ is itself a bound quiver algebra, with no relations.

Implementation notes

The exponent N of the lower bound is existentially quantified in the definition rather than carried as data: no result below depends on a particular choice, and quantifying it makes TauCeti.isAdmissibleIdeal_arrowIdeal_pow and TauCeti.isAdmissibleIdeal_bot_of_isAcyclic the statements they should be. The usual textbook phrasing adds 2 ≤ N, which is redundant: R ^ N decreases in N, so R ^ N ≤ I for some N gives it for every larger one.

Ideal R means left ideal in Mathlib, two-sidedness being the separate typeclass Ideal.IsTwoSided — which TauCeti.arrowIdeal carries. Admissibility is a notion about two-sided ideals: it is the quotient algebra kQ ⧸ I that it exists to describe, and the two inclusions R ^ N ≤ I ≤ R ^ 2 alone do not force I to be two-sided. TauCeti.IsAdmissibleIdeal therefore takes [I.IsTwoSided] as an argument of the predicate itself, so that the ideals it speaks of are exactly the admissible ones, and every consequence — in particular those about the quotient, where Ideal.Quotient asks for the same instance — is available from the predicate alone. For the ideals of TauCeti.isAdmissibleIdeal_arrowIdeal_pow and TauCeti.isAdmissibleIdeal_bot_of_isAcyclic the instance is found by synthesis.

Finite dimensionality is proved by spanning: the images of the paths of length less than N span the quotient, because every longer path already lies in I, and there are finitely many of them (TauCeti.Quiver.finite_setOf_length_lt). This is where the finiteness of the arrow types enters — the rest of the file needs only finitely many vertices, that being what makes kQ unital.

References

This implements the "admissible ideal" part of Layer 3A of TauCetiRoadmap/RepresentationTheory/QuiverRepresentations/README.md, the finite-dimensional algebra infrastructure that its kQ/I presentation theorem rests on. See Assem--Simson-- Skowroński, Elements of the Representation Theory of Associative Algebras I, Ch. II.2.

structure TauCeti.IsAdmissibleIdeal {k : Type w} {Q : Type u} [CommSemiring k] [Quiver Q] [Finite Q] (I : Ideal (pathAlgebra k Q)) [I.IsTwoSided] : Prop

A two-sided ideal of a path algebra is admissible when some power of the arrow ideal is contained in it and it is contained in the square of the arrow ideal. The quotient of the path algebra by an admissible ideal is a bound quiver algebra.

• exists_arrowIdeal_pow_le : ∃ (N : ℕ), arrowIdeal k Q ^ N ≤ I

  Some power of the arrow ideal is contained in I: all long enough paths are killed.

• le_arrowIdeal_sq : I ≤ arrowIdeal k Q ^ 2

  I is contained in the square of the arrow ideal: every relation is supported on the paths of length at least two.

theorem TauCeti.IsAdmissibleIdeal.le_arrowIdeal {k : Type w} {Q : Type u} [CommSemiring k] [Quiver Q] [Finite Q] {I : Ideal (pathAlgebra k Q)} [I.IsTwoSided] (h : IsAdmissibleIdeal I) : I ≤ arrowIdeal k Q

An admissible ideal is contained in the arrow ideal.

theorem TauCeti.IsAdmissibleIdeal.exists_ofPath_mem {k : Type w} {Q : Type u} [CommSemiring k] [Quiver Q] [Finite Q] {I : Ideal (pathAlgebra k Q)} [I.IsTwoSided] (h : IsAdmissibleIdeal I) : ∃ (N : ℕ), ∀ (x : Quiver.TotalPath Q), N ≤ x.snd.snd.length → PathAlgebra.ofPath x ∈ I

An admissible ideal contains every long enough path: this is the lower bound, read on the path basis.

theorem TauCeti.IsAdmissibleIdeal.ofPath_notMem_of_length_lt_two {k : Type w} {Q : Type u} [CommSemiring k] [Quiver Q] [Finite Q] {I : Ideal (pathAlgebra k Q)} [I.IsTwoSided] [Nontrivial k] (h : IsAdmissibleIdeal I) {x : Quiver.TotalPath Q} (hx : x.snd.snd.length < 2) : PathAlgebra.ofPath x ∉ I

An admissible ideal contains no short path: this is the upper bound, read on the path basis. It excludes one at a time the basis paths of length less than two, the vertex idempotents and the arrows; that no nonzero combination of them is erased either is TauCeti.IsAdmissibleIdeal.linearIndependent_mk_ofPath_of_length_lt_two.

theorem TauCeti.IsAdmissibleIdeal.vertexIdempotent_notMem {k : Type w} {Q : Type u} [CommSemiring k] [Quiver Q] [Finite Q] {I : Ideal (pathAlgebra k Q)} [I.IsTwoSided] [Nontrivial k] (h : IsAdmissibleIdeal I) (a : Q) : PathAlgebra.vertexIdempotent k a ∉ I

No vertex idempotent lies in an admissible ideal: the vertices survive in the quotient.

theorem TauCeti.IsAdmissibleIdeal.ofArrow_notMem {k : Type w} {Q : Type u} [CommSemiring k] [Quiver Q] [Finite Q] {I : Ideal (pathAlgebra k Q)} [I.IsTwoSided] [Nontrivial k] (h : IsAdmissibleIdeal I) {a b : Q} (e : a ⟶ b) : PathAlgebra.ofArrow e ∉ I

No arrow lies in an admissible ideal: the arrows survive in the quotient.

theorem TauCeti.IsAdmissibleIdeal.ne_top {k : Type w} {Q : Type u} [CommSemiring k] [Quiver Q] [Finite Q] {I : Ideal (pathAlgebra k Q)} [I.IsTwoSided] [Nontrivial k] [Nonempty Q] (h : IsAdmissibleIdeal I) : I ≠ ⊤

An admissible ideal of the path algebra of a nonempty quiver is proper.

theorem TauCeti.isAdmissibleIdeal_iff {k : Type w} {Q : Type u} [CommSemiring k] [Quiver Q] [Finite Q] {I : Ideal (pathAlgebra k Q)} [I.IsTwoSided] : IsAdmissibleIdeal I ↔ (∃ (N : ℕ), ∀ (x : Quiver.TotalPath Q), N ≤ x.snd.snd.length → PathAlgebra.ofPath x ∈ I) ∧ I ≤ arrowIdeal k Q ^ 2

Admissibility, read entirely on the path basis: the lower bound need only be checked on the basis paths, since a k-submodule containing every path of length at least N contains their whole span, which is R ^ N. This is how admissibility of a concretely given ideal of relations is verified.

theorem TauCeti.isAdmissibleIdeal_arrowIdeal_pow (k : Type w) (Q : Type u) [CommSemiring k] [Quiver Q] [Finite Q] {n : ℕ} (hn : 2 ≤ n) : IsAdmissibleIdeal (arrowIdeal k Q ^ n)

The powers of the arrow ideal from the second on are admissible. These are the monomial relations: R ^ n is the ideal spanned by the paths of length at least n.

theorem TauCeti.isAdmissibleIdeal_bot_of_isAcyclic (k : Type w) (Q : Type u) [CommSemiring k] [Quiver Q] [Finite Q] (h : Quiver.IsAcyclic Q) : IsAdmissibleIdeal ⊥

Over a finite acyclic quiver the zero ideal is admissible: the path algebra is itself a bound quiver algebra, with no relations. Acyclicity supplies the truncation by itself: every path is shorter than the number of vertices, so the arrow ideal is already nilpotent.

The bound quiver algebra

theorem TauCeti.IsAdmissibleIdeal.isNilpotent_mk_of_mem_arrowIdeal {k : Type w} {Q : Type u} [CommRing k] [Quiver Q] [Finite Q] {I : Ideal (pathAlgebra k Q)} [I.IsTwoSided] (h : IsAdmissibleIdeal I) {f : pathAlgebra k Q} (hf : f ∈ arrowIdeal k Q) : IsNilpotent ((Ideal.Quotient.mk I) f)

Every element of the arrow ideal is nilpotent in a bound quiver algebra: its N-th power is supported on the paths of length at least N, which the ideal has already killed. Over an acyclic quiver this holds already in kQ (TauCeti.isNilpotent_of_mem_arrowIdeal); admissibility is what replaces acyclicity in general.

theorem TauCeti.IsAdmissibleIdeal.linearIndependent_mk_ofPath_of_length_lt_two {k : Type w} {Q : Type u} [CommRing k] [Quiver Q] [Finite Q] {I : Ideal (pathAlgebra k Q)} [I.IsTwoSided] (h : IsAdmissibleIdeal I) : LinearIndependent k fun (x : { x : Quiver.TotalPath Q // x.snd.snd.length < 2 }) => (Ideal.Quotient.mk I) (PathAlgebra.ofPath ↑x)

The vertices and the arrows stay independent in a bound quiver algebra: the images of the paths of length less than two are linearly independent over k, so the quotient map is injective on their span. This is the upper bound I ≤ R ^ 2 read on the quotient, and it says more than the individual nonmemberships TauCeti.IsAdmissibleIdeal.vertexIdempotent_notMem and TauCeti.IsAdmissibleIdeal.ofArrow_notMem: distinct vertices stay distinct, distinct arrows stay distinct, and no nonzero combination of them is erased.

theorem TauCeti.IsAdmissibleIdeal.nontrivial_quotient {k : Type w} {Q : Type u} [CommRing k] [Quiver Q] [Finite Q] {I : Ideal (pathAlgebra k Q)} [I.IsTwoSided] [Nontrivial k] [Nonempty Q] (h : IsAdmissibleIdeal I) : Nontrivial (pathAlgebra k Q ⧸ I)

A bound quiver algebra over a nonempty quiver is nonzero: an admissible ideal is proper, the vertex idempotents escaping it.

theorem TauCeti.IsAdmissibleIdeal.finiteDimensional_quotient {k : Type w} {Q : Type u} [Field k] [Quiver Q] [Finite Q] [∀ (a b : Q), Finite (a ⟶ b)] {I : Ideal (pathAlgebra k Q)} [I.IsTwoSided] (h : IsAdmissibleIdeal I) : FiniteDimensional k (pathAlgebra k Q ⧸ I)

A bound quiver algebra is finite-dimensional. The images of the paths of length less than N span it, because a longer path already lies in the ideal, and a quiver with finitely many vertices and finitely many arrows has only finitely many paths of bounded length. The path algebra itself need not be finite-dimensional: that needs finitely many paths of every length, hence acyclicity, whereas the bound R ^ N ≤ I supplies the missing truncation.