The path algebra of a quiver as a retract of the doubled path algebra

The doubled quiver Quiver.Symmetrify Q contains Q through the prefunctor Quiver.Symmetrify.of, which is the identity on vertices, so TauCeti.PathAlgebra.mapAlgHom includes the path algebra kQ in the doubled path algebra kQ^sym (the path algebra of Quiver.Symmetrify Q). This file constructs an algebra homomorphism in the other direction,

kQ^sym → kQ,

which fixes the vertex idempotents and the arrows of Q and sends every formal reverse to zero: a path of the doubled quiver goes to itself when it uses only arrows of Q, and to zero as soon as it uses a formal reverse. It is a retraction of the inclusion, so kQ is a quotient algebra of kQ^sym.

Its use is that it kills every product in which a formal reverse occurs, such as the two backtracks a a* and a* a of an arrow; this is what lets it descend to quotients of kQ^sym by relations built from such products, notably the preprojective algebra.

Main definitions

• TauCeti.PathAlgebra.symmetrifyRetraction: the algebra homomorphism kQ^sym →ₐ[k] kQ killing the formal reverses.

Main results

• TauCeti.PathAlgebra.symmetrifyRetraction_vertexIdempotent, TauCeti.PathAlgebra.symmetrifyRetraction_ofArrow_of and TauCeti.PathAlgebra.symmetrifyRetraction_ofArrow_reverse_of: its values on the generators.
• TauCeti.PathAlgebra.symmetrifyRetraction_comp_mapAlgHom_of: it is a retraction of the inclusion kQ →ₐ[k] kQ^sym, which is therefore injective (TauCeti.PathAlgebra.mapAlgHom_of_injective), while the retraction is surjective (TauCeti.PathAlgebra.symmetrifyRetraction_surjective).

noncomputable def TauCeti.PathAlgebra.symmetrifyRetraction (k : Type w) {Q : Type u} [CommSemiring k] [Quiver Q] [Finite Q] : pathAlgebra k (Quiver.Symmetrify Q) →ₐ[k] pathAlgebra k Q

The algebra homomorphism kQ^sym →ₐ[k] kQ from the path algebra of the doubled quiver to the path algebra of Q which fixes the vertex idempotents and the arrows of Q and kills every formal reverse. A doubled path goes to itself when it uses only arrows of Q, and to zero otherwise.

Equations

• TauCeti.PathAlgebra.symmetrifyRetraction k = TauCeti.PathAlgebra.liftAlgHom k (fun (x : TauCeti.Quiver.TotalPath (Quiver.Symmetrify Q)) => TauCeti.PathAlgebra.retractPath✝ k x.snd.snd) ⋯ ⋯ ⋯

@[simp]

theorem TauCeti.PathAlgebra.symmetrifyRetraction_vertexIdempotent (k : Type w) {Q : Type u} [CommSemiring k] [Quiver Q] [Finite Q] (v : Q) : (symmetrifyRetraction k) (vertexIdempotent k v) = vertexIdempotent k v

The retraction fixes every vertex idempotent.

theorem TauCeti.PathAlgebra.symmetrifyRetraction_ofArrow_of (k : Type w) {Q : Type u} [CommSemiring k] [Quiver Q] [Finite Q] {a b : Q} (f : a ⟶ b) : (symmetrifyRetraction k) (ofArrow (Quiver.Symmetrify.of.map f)) = ofArrow f

The retraction fixes every arrow of Q.

theorem TauCeti.PathAlgebra.symmetrifyRetraction_ofArrow_reverse_of (k : Type w) {Q : Type u} [CommSemiring k] [Quiver Q] [Finite Q] {a b : Q} (f : a ⟶ b) : (symmetrifyRetraction k) (ofArrow (Quiver.reverse (Quiver.Symmetrify.of.map f))) = 0

The retraction kills every formal reverse.

@[simp]

theorem TauCeti.PathAlgebra.symmetrifyRetraction_ofPath_mapTotalPath_of (k : Type w) {Q : Type u} [CommSemiring k] [Quiver Q] [Finite Q] (x : Quiver.TotalPath Q) : (symmetrifyRetraction k) (ofPath (Quiver.Symmetrify.of.mapTotalPath x)) = ofPath x

The retraction sends a path of Q, viewed in the doubled quiver, back to itself.

@[simp]

theorem TauCeti.PathAlgebra.symmetrifyRetraction_comp_mapAlgHom_of (k : Type w) {Q : Type u} [CommSemiring k] [Quiver Q] [Finite Q] : (symmetrifyRetraction k).comp (mapAlgHom k Quiver.Symmetrify.of ⋯) = AlgHom.id k (pathAlgebra k Q)

The retraction is a left inverse of the inclusion kQ →ₐ[k] kQ^sym induced by Quiver.Symmetrify.of.

theorem TauCeti.PathAlgebra.mapAlgHom_of_injective (k : Type w) {Q : Type u} [CommSemiring k] [Quiver Q] [Finite Q] : Function.Injective ⇑(mapAlgHom k Quiver.Symmetrify.of ⋯)

The inclusion kQ →ₐ[k] kQ^sym induced by Quiver.Symmetrify.of is injective.

theorem TauCeti.PathAlgebra.symmetrifyRetraction_surjective (k : Type w) {Q : Type u} [CommSemiring k] [Quiver Q] [Finite Q] : Function.Surjective ⇑(symmetrifyRetraction k)

The retraction kQ^sym →ₐ[k] kQ is surjective.