Homomorphisms from a path algebra prescribed on arrows

A complete family of orthogonal idempotents e : Q → A, together with an element f a in the corner e j A e i for each arrow a : i ⟶ j, determines a unique algebra homomorphism from the path algebra to A. No acyclicity or finiteness of the arrow types is needed.

liftAlgHomOfArrows constructs this homomorphism. Its vertex and arrow evaluation lemmas, and its recursion on paths, describe it without unfolding the construction. Its range is exactly the subalgebra generated by the assigned idempotents and arrows. In particular, choosing lifts of radical-layer generators in a finite-dimensional algebra gives the map used in a bound-quiver presentation.

The construction uses PathAlgebra.liftAlgHom, extending an assignment on all paths. The empty path must evaluate to its vertex idempotent, rather than to the unit of A.

References

• Assem--Simson--Skowroński, Elements of the Representation Theory of Associative Algebras I, Chapter II, Sections 1 and 3.

theorem TauCeti.PathAlgebra.algHom_ext_vertexIdempotent_ofArrow (k : Type w) {Q : Type u} [CommSemiring k] [Quiver Q] [Finite Q] {A : Type u_1} [Semiring A] [Algebra k A] {φ ψ : pathAlgebra k Q →ₐ[k] A} (hv : ∀ (i : Q), φ (vertexIdempotent k i) = ψ (vertexIdempotent k i)) (ha : ∀ {i j : Q} (a : i ⟶ j), φ (ofArrow a) = ψ (ofArrow a)) : φ = ψ

Algebra homomorphisms from a path algebra agree if they agree on vertices and arrows.

noncomputable def TauCeti.PathAlgebra.liftAlgHomOfArrows (k : Type w) {Q : Type u} [CommSemiring k] [Quiver Q] [Fintype Q] {A : Type u_1} [Semiring A] [Algebra k 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) : pathAlgebra k Q →ₐ[k] A

Extend a complete orthogonal family of vertex idempotents and corner-valued arrows to an algebra homomorphism. An arrow i ⟶ j is assigned an element fixed by e j on the left and by e i on the right, matching the later-factor-first path multiplication.

@[simp]

theorem TauCeti.PathAlgebra.liftAlgHomOfArrows_vertexIdempotent (k : Type w) {Q : Type u} [CommSemiring k] [Quiver Q] [Fintype Q] {A : Type u_1} [Semiring A] [Algebra k 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) (i : Q) : (liftAlgHomOfArrows k e he (fun {i j : Q} => f) ⋯ ⋯) (vertexIdempotent k i) = e i

The homomorphism sends a vertex idempotent to the prescribed idempotent.

@[simp]

theorem TauCeti.PathAlgebra.liftAlgHomOfArrows_ofPath_nil (k : Type w) {Q : Type u} [CommSemiring k] [Quiver Q] [Fintype Q] {A : Type u_1} [Semiring A] [Algebra k 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) (i : Q) : (liftAlgHomOfArrows k e he (fun {i j : Q} => f) ⋯ ⋯) (ofPath ⟨i, ⟨i, Quiver.Path.nil⟩⟩) = e i

The homomorphism sends a trivial path to its prescribed vertex idempotent.

@[simp]

theorem TauCeti.PathAlgebra.liftAlgHomOfArrows_ofPath_toPath (k : Type w) {Q : Type u} [CommSemiring k] [Quiver Q] [Fintype Q] {A : Type u_1} [Semiring A] [Algebra k 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) {i j : Q} (a : i ⟶ j) : (liftAlgHomOfArrows k e he (fun {i j : Q} => f) ⋯ ⋯) (ofPath ⟨i, ⟨j, a.toPath⟩⟩) = f a

The homomorphism sends the length-one path of an arrow to its prescribed value. This is also the simp-normal form of evaluation on ofArrow.

@[simp]

theorem TauCeti.PathAlgebra.liftAlgHomOfArrows_ofPath_cons (k : Type w) {Q : Type u} [CommSemiring k] [Quiver Q] [Fintype Q] {A : Type u_1} [Semiring A] [Algebra k 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) {i j l : Q} (p : Quiver.Path i j) (a : j ⟶ l) : (liftAlgHomOfArrows k e he (fun {i j : Q} => f) ⋯ ⋯) (ofPath ⟨i, ⟨l, p.cons a⟩⟩) = f a * (liftAlgHomOfArrows k e he (fun {i j : Q} => f) ⋯ ⋯) (ofPath ⟨i, ⟨j, p⟩⟩)

Evaluation of a path appended by an arrow multiplies the assigned arrow on the left.

theorem TauCeti.PathAlgebra.liftAlgHomOfArrows_unique (k : Type w) {Q : Type u} [CommSemiring k] [Quiver Q] [Fintype Q] {A : Type u_1} [Semiring A] [Algebra k 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) (φ : pathAlgebra k Q →ₐ[k] A) (hv : ∀ (i : Q), φ (vertexIdempotent k i) = e i) (ha : ∀ {i j : Q} (a : i ⟶ j), φ (ofArrow a) = f a) : φ = liftAlgHomOfArrows k e he (fun {i j : Q} => f) ⋯ ⋯

The constructed homomorphism is the only one with the prescribed vertex and arrow values.

theorem TauCeti.PathAlgebra.range_liftAlgHomOfArrows (k : Type w) {Q : Type u} [CommSemiring k] [Quiver Q] [Fintype Q] {A : Type u_1} [Semiring A] [Algebra k 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) : (liftAlgHomOfArrows k e he (fun {i j : Q} => f) ⋯ ⋯).range = Algebra.adjoin k (Set.range e ∪ Set.range fun (a : (i : Q) × (j : Q) × (i ⟶ j)) => f a.snd.snd)

The range is exactly the subalgebra generated by the assigned vertices and arrows.