Documentation

TauCeti.RepresentationTheory.Quiver.AdmissibleIdeal.Presentation

Bound-quiver presentations of basic algebras #

Let A be an algebra with a nilpotent two-sided ideal J, a complete family of orthogonal idempotents e : Q → A, and for each arrow a : i ⟶ j of a quiver on Q an element f a of the corner e j * A * e i. These data define an algebra map kQ → A from the path algebra (TauCeti.PathAlgebra.liftAlgHomOfArrows). This file gives the two criteria that make it a bound-quiver presentation, a surjection with admissible kernel, so that A ≃ kQ ⧸ I with I admissible:

Both conditions hold when J is the Jacobson radical of a finite-dimensional basic algebra over an algebraically closed field: the Wedderburn blocks of A ⧸ J are copies of the field, their units lift to orthogonal idempotents of A, and the arrows are chosen as lifts of a basis of each corner of J ⧸ J ^ 2. This is Gabriel's theorem that such an algebra is a bound quiver algebra.

Main results #

Implementation notes #

The quiver built in the proof has the Wedderburn blocks of A ⧸ J as vertices, and as arrows i ⟶ j the indices of a basis of the (j, i)-corner of J ⧸ J ^ 2; this is how the ordinary quiver of A is defined. The theorem asserts only the existence of some finite quiver: neither that identification nor the description of the arrow counts by Ext¹ between simple modules is stated here.

References #

theorem TauCeti.PathAlgebra.liftAlgHomOfArrows_surjective {Q : Type u} [Quiver Q] [Fintype Q] {A : Type u_1} [Ring A] (e : Q → A) (he : CompleteOrthogonalIdempotents e) (f : {i j : Q} → (i ⟶ j) → A) (hl : ∀ {i j : Q} (a : i ⟶ j), e j * f a = f a) (hr : ∀ {i j : Q} (a : i ⟶ j), f a * e i = f a) (J : Ideal A) [J.IsTwoSided] {k : Type w} [CommSemiring k] [Algebra k A] (hJ : IsNilpotent J) (hquot : Submodule.span k (Set.range fun (i : Q) => (Ideal.Quotient.mk J) (e i)) = ⊤) (hlayer : ∀ (i j : Q), ∀ x ∈ J, (Ideal.Quotient.mk (J ^ 2)) (e j * x * e i) ∈ Submodule.span k (Set.range fun (a : i ⟶ j) => (Ideal.Quotient.mk (J ^ 2)) (f a))) :
Function.Surjective ⇑(liftAlgHomOfArrows k e he (fun {i j : Q} => f) ⋯ ⋯)

Generation criterion for a bound-quiver presentation. Let J be a nilpotent two-sided ideal. If the vertex idempotents span A ⧸ J, and for all vertices i and j the arrows i ⟶ j span the (j, i)-corner of the first layer J ⧸ J ^ 2, then the algebra map from the path algebra is surjective.

theorem TauCeti.PathAlgebra.isAdmissibleIdeal_ker_liftAlgHomOfArrows {Q : Type u} [Quiver Q] [Fintype Q] {A : Type u_1} [Ring A] (e : Q → A) (he : CompleteOrthogonalIdempotents e) (f : {i j : Q} → (i ⟶ j) → A) (hl : ∀ {i j : Q} (a : i ⟶ j), e j * f a = f a) (hr : ∀ {i j : Q} (a : i ⟶ j), f a * e i = f a) (J : Ideal A) [J.IsTwoSided] {k : Type w} [Field k] [Algebra k A] (hJ : IsNilpotent J) (hne : ∀ (i : Q), e i ≠ 0) (harrows : ∀ {i j : Q} (a : i ⟶ j), f a ∈ J) (hind : ∀ (i j : Q), LinearIndependent k fun (a : i ⟶ j) => (Ideal.Quotient.mk (J ^ 2)) (f a)) :
IsAdmissibleIdeal (RingHom.ker (liftAlgHomOfArrows k e he (fun {i j : Q} => f) ⋯ ⋯).toRingHom)

Admissibility criterion for a bound-quiver presentation. Let J be a nilpotent two-sided ideal containing the arrow values, and let the vertex idempotents be nonzero. If for all vertices i and j the classes of the arrows i ⟶ j in A ⧸ J ^ 2 are linearly independent, then the kernel of the algebra map from the path algebra is admissible.

theorem TauCeti.IsBasic.exists_surjective_pathAlgebra_isAdmissibleIdeal_ker {k : Type w} {A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] (hA : IsBasic A) :
∃ (Q : Type) (x : Quiver Q) (x_1 : Finite Q) (_ : ∀ (i j : Q), Finite (i ⟶ j)) (F : pathAlgebra k Q →ₐ[k] A), Function.Surjective ⇑F ∧ IsAdmissibleIdeal (RingHom.ker F.toRingHom)

Gabriel's presentation theorem for basic algebras. A finite-dimensional basic algebra over an algebraically closed field is a quotient of the path algebra of a finite quiver by an admissible ideal: there is a surjective algebra map kQ → A whose kernel is admissible.

theorem TauCeti.exists_quiver_admissibleIdeal_morita (k : Type w) (A : Type u) [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] :
∃ (Q : Type) (x : Quiver Q) (x_1 : Finite Q) (_ : ∀ (i j : Q), Finite (i ⟶ j)) (I : Ideal (pathAlgebra k Q)) (x_3 : I.IsTwoSided), IsAdmissibleIdeal I ∧ IsMoritaEquivalent k A (pathAlgebra k Q ⧸ I)

Gabriel's presentation theorem. Every finite-dimensional algebra A over an algebraically closed field k is Morita equivalent to a bound quiver algebra: there are a finite quiver Q and an admissible ideal I of the path algebra kQ such that A is Morita equivalent to kQ ⧸ I. The algebra kQ ⧸ I is isomorphic to the basic corner eAe of A (TauCeti.IsSemiperfectRing.exists_isIdempotentElem_full_isBasic_corner), presented by TauCeti.IsBasic.exists_surjective_pathAlgebra_isAdmissibleIdeal_ker.