The path algebra of the one-loop quiver

This file identifies the path algebra of the quiver TauCeti.Quiver.OneLoop with one vertex and one loop with the additive monoid algebra on ℕ, equivalently the polynomial algebra in one variable. It also shows that this path algebra is not a finite module over any nontrivial semiring; over a division ring, it is infinite-dimensional.

Main declarations

• TauCeti.PathAlgebra.oneLoopRingEquiv: over any semiring, its path algebra is AddMonoidAlgebra k ℕ.
• TauCeti.PathAlgebra.oneLoopAlgEquiv: over a commutative semiring, this is an algebra equivalence sending a path to the monomial of degree its length (TauCeti.PathAlgebra.oneLoopAlgEquiv_single).
• TauCeti.not_module_finite_pathAlgebra_oneLoop: the one-loop path algebra is not a finite module.

noncomputable def TauCeti.PathAlgebra.oneLoopRingEquiv (k : Type w) [Semiring k] : pathAlgebra k Quiver.OneLoop ≃+* AddMonoidAlgebra k ℕ

Over any semiring, the one-loop path algebra is the additive monoid algebra on ℕ.

Equations

• TauCeti.PathAlgebra.oneLoopRingEquiv k = { toEquiv := (TauCeti.PathAlgebra.oneLoopLinearEquiv✝ k).toAddEquiv.toEquiv, map_mul' := ⋯, map_add' := ⋯ }

@[simp]

theorem TauCeti.PathAlgebra.oneLoopRingEquiv_single (k : Type w) [Semiring k] (x : Quiver.TotalPath Quiver.OneLoop) (c : k) : (oneLoopRingEquiv k) (single x c) = AddMonoidAlgebra.single x.snd.snd.length c

The ring equivalence sends a path to the monomial of degree its length.

@[simp]

theorem TauCeti.PathAlgebra.oneLoopRingEquiv_symm_single (k : Type w) [Semiring k] (n : ℕ) (c : k) : (oneLoopRingEquiv k).symm (AddMonoidAlgebra.single n c) = single (Quiver.OneLoop.totalPathEquivNat.symm n) c

The inverse ring equivalence sends a monomial to the canonical path of its degree.

noncomputable def TauCeti.PathAlgebra.oneLoopAlgEquiv (k : Type w) [CommSemiring k] : pathAlgebra k Quiver.OneLoop ≃ₐ[k] AddMonoidAlgebra k ℕ

The path algebra of the quiver with one vertex and one loop is the additive monoid algebra on ℕ (equivalently, the polynomial algebra in one variable).

Equations

• TauCeti.PathAlgebra.oneLoopAlgEquiv k = { toEquiv := (TauCeti.PathAlgebra.oneLoopRingEquiv k).toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }

@[simp]

theorem TauCeti.PathAlgebra.oneLoopAlgEquiv_toRingEquiv (k : Type w) [CommSemiring k] : (oneLoopAlgEquiv k).toRingEquiv = oneLoopRingEquiv k

The underlying ring equivalence of oneLoopAlgEquiv is oneLoopRingEquiv.

@[simp]

theorem TauCeti.PathAlgebra.oneLoopAlgEquiv_single (k : Type w) [CommSemiring k] (x : Quiver.TotalPath Quiver.OneLoop) (c : k) : (oneLoopAlgEquiv k) (single x c) = AddMonoidAlgebra.single x.snd.snd.length c

The isomorphism oneLoopAlgEquiv sends a path with coefficient c to the monomial of degree its length with coefficient c.

@[simp]

theorem TauCeti.PathAlgebra.oneLoopAlgEquiv_symm_single (k : Type w) [CommSemiring k] (n : ℕ) (c : k) : (oneLoopAlgEquiv k).symm (AddMonoidAlgebra.single n c) = single (Quiver.OneLoop.totalPathEquivNat.symm n) c

The inverse algebra equivalence sends a monomial to the canonical path of its degree.

theorem TauCeti.not_module_finite_pathAlgebra_oneLoop (k : Type w) [Semiring k] [Nontrivial k] : ¬Module.Finite k (pathAlgebra k Quiver.OneLoop)

Over a nontrivial semiring, the path algebra of the one-loop quiver is not a finite module; over a division ring this says it is infinite-dimensional.