The loop quiver has infinite representation type

A representation of the quiver •↺ with one vertex and one loop is a vector space together with an endomorphism of it. Two families of them are built here. The one-dimensional ones are the scalars: for c in the base field, TauCeti.oneLoopRep k c is the line k with the loop acting by multiplication by c; each is indecomposable, being a line, and two of them are isomorphic only when the scalars agree, an isomorphism intertwining the two multiplications on a vector where it does not vanish. The nilpotent Jordan blocks TauCeti.oneLoopNilpotentRep k n are the truncated polynomial algebras k[X]/(Xⁿ⁺¹) with the loop acting by multiplication by X; they have dimension n + 1, so they are pairwise non-isomorphic, and each is indecomposable because its endomorphisms are the multiplications by its own elements and k[X]/(Xⁿ⁺¹) has no idempotent but 0 and 1. They exist over every field, so the loop quiver has infinite representation type over every field; the scalar family would only settle the case of an infinite base field.

This is the boundary case that delimits where the theory of quiver representations needs acyclicity: •↺ is the smallest non-acyclic quiver, its path algebra is the infinite-dimensional k[X] (TauCeti.PathAlgebra.oneLoopAlgEquiv), and its finite-dimensional indecomposables are the cyclic torsion k[X]-modules k[X]/(pⁿ) for p irreducible -- the Jordan blocks when k is algebraically closed -- rather than anything finite.

Main declarations

• TauCeti.oneLoopRep: the line on which the loop of •↺ acts by a given scalar.
• TauCeti.oneLoopRepScalar: the scalar by which a morphism between two of them acts.
• TauCeti.oneLoopRepHom: conversely, the morphism attached to an intertwining scalar.
• TauCeti.oneLoopNilpotentRep: the nilpotent Jordan block k[X]/(Xⁿ⁺¹).

Main results

• TauCeti.indecomposable_oneLoopRep: the scalar representations are indecomposable.
• TauCeti.nonempty_oneLoopRep_iso_iff: two of them are isomorphic exactly when the scalars agree.
• TauCeti.indecomposable_oneLoopNilpotentRep: the nilpotent Jordan blocks are indecomposable.
• TauCeti.nonempty_oneLoopNilpotentRep_iso_iff: two of them are isomorphic exactly when their sizes agree.
• TauCeti.not_isFiniteRepType_oneLoop: over any field the loop quiver has infinite representation type.

Implementation notes

The scalar family runs through TauCeti.oneLoopRepScalar, the value at 1 of the single component of a morphism: •↺ has one vertex, so a natural transformation is one linear map, and that linear map is an endomorphism of the line k, hence multiplication by a scalar. Composition multiplies these scalars (in the opposite order), so the morphisms between scalar representations are exactly the scalars s with s * c = d * s: TauCeti.oneLoopRepHom builds the morphism from such a scalar, TauCeti.oneLoopRepScalar_oneLoopRepHom and TauCeti.oneLoopRep_hom_ext make the two constructions inverse to each other.

Indecomposability is proved throughout from TauCeti.indecomposable_of_injective_of_isLocalRing rather than from the brick criterion: for the Jordan blocks the endomorphism algebra is k[X]/(Xⁿ⁺¹), which is not a field, so the brick criterion does not apply, and an endomorphism is pinned down instead by its value at 1 (AdjoinRoot.eq_mulRight_of_root_mul, from TauCeti.RingTheory.AdjoinRoot.Basic). That value records the endomorphism faithfully in the truncated polynomial algebra, sending 0 to 0, the identity to 1 and squares to squares, and that algebra is local by TauCeti.isLocalRing_adjoinRoot_X_pow from TauCeti.RingTheory.Polynomial.Truncated; a scalar representation is the same criterion read in the base field.

The quiver •↺ itself -- TauCeti.Quiver.OneLoop, with its Quiver instance and its loop TauCeti.Quiver.OneLoop.loop -- is defined in TauCeti.RepresentationTheory.Quiver.OneLoop.Basic, which carries the vertex and arrow data alone; the path-algebra results cited under "References" are not imported here.

TauCeti.oneLoopRep and TauCeti.oneLoopNilpotentRep carry @[expose] because the vertex space of the representation has to reduce to k, resp. to k[X]/(Xⁿ⁺¹), for the statements below to elaborate at all: a functor built by CategoryTheory.Paths.lift reveals its value on objects only through its definition, and without it even TauCeti.oneLoopRep_map_loop_apply fails to typecheck.

References

This proves the ¬ IsFiniteRepType half of the loop-quiver worked example of TauCetiRoadmap/RepresentationTheory/QuiverRepresentations/README.md, whose other half -- that the path algebra is k[X] and is infinite-dimensional -- is TauCeti.PathAlgebra.oneLoopAlgEquiv together with TauCeti.not_finiteDimensional_pathAlgebra_oneLoop.

def TauCeti.oneLoopRep (k : Type u) [Field k] (c : k) : QuiverRep k Quiver.OneLoop

The line on which the loop acts by the scalar c: the one-dimensional representation of the quiver •↺ given by the base field at its only vertex, with the loop acting by multiplication by c.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.oneLoopRep_obj {k : Type u} [Field k] (c : k) (v : CategoryTheory.Paths Quiver.OneLoop) : (oneLoopRep k c).obj v = ModuleCat.of k k

The vertex space of TauCeti.oneLoopRep is the base field.

theorem TauCeti.dimVector_oneLoopRep {k : Type u} [Field k] (c : k) (v : Quiver.OneLoop) : dimVector (oneLoopRep k c) v = 1

TauCeti.oneLoopRep k c is a line: its dimension vector is 1.

theorem TauCeti.oneLoopRep_map_loop {k : Type u} [Field k] (c : k) : (oneLoopRep k c).map Quiver.OneLoop.loop.toPath = ModuleCat.ofHom (c • LinearMap.id)

The loop of •↺ acts on TauCeti.oneLoopRep k c by multiplication by c.

@[simp]

theorem TauCeti.oneLoopRep_map_loop_apply {k : Type u} [Field k] (c x : k) : (ModuleCat.Hom.hom ((oneLoopRep k c).map Quiver.OneLoop.loop.toPath)) x = c * x

The action of the loop, read on an element of the vertex space.

def TauCeti.oneLoopRepScalar {k : Type u} [Field k] {c d : k} (f : oneLoopRep k c ⟶ oneLoopRep k d) : k

The scalar of a morphism of scalar representations of •↺: its single component is an endomorphism of the line k, hence multiplication by this value at 1.

Equations

• TauCeti.oneLoopRepScalar f = (ModuleCat.Hom.hom (f.app TauCeti.Quiver.OneLoop.vertex)) 1

@[simp]

theorem TauCeti.oneLoopRepScalar_apply {k : Type u} [Field k] {c d : k} (f : oneLoopRep k c ⟶ oneLoopRep k d) (x : k) : (ModuleCat.Hom.hom (f.app Quiver.OneLoop.vertex)) x = oneLoopRepScalar f * x

A morphism of scalar representations acts by multiplication by its scalar.

@[simp]

theorem TauCeti.oneLoopRepScalar_comp {k : Type u} [Field k] {c d e : k} (f : oneLoopRep k c ⟶ oneLoopRep k d) (g : oneLoopRep k d ⟶ oneLoopRep k e) : oneLoopRepScalar (CategoryTheory.CategoryStruct.comp f g) = oneLoopRepScalar g * oneLoopRepScalar f

Composition multiplies the scalars, in the order opposite to composition.

@[simp]

theorem TauCeti.oneLoopRepScalar_id {k : Type u} [Field k] (c : k) : oneLoopRepScalar (CategoryTheory.CategoryStruct.id (oneLoopRep k c)) = 1

The identity has scalar 1.

@[simp]

theorem TauCeti.oneLoopRepScalar_zero {k : Type u} [Field k] (c d : k) : oneLoopRepScalar 0 = 0

The zero morphism has scalar 0.

def TauCeti.oneLoopRepHom {k : Type u} [Field k] {c d : k} (s : k) (hs : s * c = d * s) : oneLoopRep k c ⟶ oneLoopRep k d

The morphism of scalar representations attached to an intertwining scalar: multiplication by s at the only vertex, which is natural along the loop exactly when s * c = d * s.

Equations

• TauCeti.oneLoopRepHom s hs = CategoryTheory.Paths.liftNatTrans (fun (x : TauCeti.Quiver.OneLoop) => ModuleCat.ofHom (s • LinearMap.id)) ⋯

@[simp]

theorem TauCeti.oneLoopRepScalar_oneLoopRepHom {k : Type u} [Field k] {c d : k} (s : k) (hs : s * c = d * s) : oneLoopRepScalar (oneLoopRepHom s hs) = s

The scalar of TauCeti.oneLoopRepHom s hs is s.

theorem TauCeti.oneLoopRep_hom_ext {k : Type u} [Field k] {c d : k} {f g : oneLoopRep k c ⟶ oneLoopRep k d} (h : oneLoopRepScalar f = oneLoopRepScalar g) : f = g

A morphism of scalar representations is determined by its scalar. The quiver has one vertex, so a natural transformation is its single component, and that component is multiplication by the scalar.

theorem TauCeti.oneLoopRepScalar_intertwine {k : Type u} [Field k] {c d : k} (f : oneLoopRep k c ⟶ oneLoopRep k d) : oneLoopRepScalar f * c = d * oneLoopRepScalar f

A morphism intertwines the two loop actions: naturality along the loop says that its scalar s satisfies s * c = d * s. Over a field this forces c = d as soon as s is nonzero.

@[simp]

theorem TauCeti.oneLoopRepHom_oneLoopRepScalar {k : Type u} [Field k] {c d : k} (f : oneLoopRep k c ⟶ oneLoopRep k d) : oneLoopRepHom (oneLoopRepScalar f) ⋯ = f

Every morphism of scalar representations is the one attached to its scalar, so TauCeti.oneLoopRepHom and TauCeti.oneLoopRepScalar identify the morphisms oneLoopRep k c ⟶ oneLoopRep k d with the scalars s satisfying s * c = d * s.

theorem TauCeti.isFinDim_oneLoopRep {k : Type u} [Field k] (c : k) : IsFinDim k Quiver.OneLoop (oneLoopRep k c)

TauCeti.oneLoopRep k c is finite-dimensional: it is a line.

theorem TauCeti.not_isZero_oneLoopRep {k : Type u} [Field k] (c : k) : ¬CategoryTheory.Limits.IsZero (oneLoopRep k c)

TauCeti.oneLoopRep k c is nonzero: the vector space at its vertex is the base field, which is not the zero module.

theorem TauCeti.indecomposable_oneLoopRep {k : Type u} [Field k] (c : k) : CategoryTheory.Indecomposable (oneLoopRep k c)

TauCeti.oneLoopRep k c is indecomposable. Its only vertex carries a line, so its scalar records an endomorphism faithfully in the field k, a local ring, sending 0 to 0, the identity to 1 and squares to squares.

theorem TauCeti.eq_of_nonempty_oneLoopRep_iso {k : Type u} [Field k] {c d : k} (h : Nonempty (oneLoopRep k c ≅ oneLoopRep k d)) : c = d

Two scalar representations of •↺ are isomorphic only if their scalars agree. The scalar of an isomorphism is invertible, because the scalars of the two composites multiply to 1, and intertwining then equates the two loop actions.

@[simp]

theorem TauCeti.nonempty_oneLoopRep_iso_iff {k : Type u} [Field k] {c d : k} : Nonempty (oneLoopRep k c ≅ oneLoopRep k d) ↔ c = d

Two scalar representations of •↺ are isomorphic exactly when their scalars agree.

noncomputable def TauCeti.oneLoopNilpotentRep (k : Type u) [Field k] (n : ℕ) : QuiverRep k Quiver.OneLoop

The nilpotent Jordan block of size n + 1: the truncated polynomial algebra k[X]/(Xⁿ⁺¹) at the only vertex of •↺, with the loop acting by multiplication by X.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.oneLoopNilpotentRep_obj {k : Type u} [Field k] (n : ℕ) (v : CategoryTheory.Paths Quiver.OneLoop) : (oneLoopNilpotentRep k n).obj v = ModuleCat.of k (AdjoinRoot (Polynomial.X ^ (n + 1)))

The vertex space of TauCeti.oneLoopNilpotentRep is k[X]/(Xⁿ⁺¹).

theorem TauCeti.oneLoopNilpotentRep_map_loop {k : Type u} [Field k] (n : ℕ) : (oneLoopNilpotentRep k n).map Quiver.OneLoop.loop.toPath = ModuleCat.ofHom (LinearMap.mulLeft k (AdjoinRoot.root (Polynomial.X ^ (n + 1))))

The loop of •↺ acts on TauCeti.oneLoopNilpotentRep k n by multiplication by the root.

@[simp]

theorem TauCeti.oneLoopNilpotentRep_map_loop_apply {k : Type u} [Field k] (n : ℕ) (x : AdjoinRoot (Polynomial.X ^ (n + 1))) : (ModuleCat.Hom.hom ((oneLoopNilpotentRep k n).map Quiver.OneLoop.loop.toPath)) x = AdjoinRoot.root (Polynomial.X ^ (n + 1)) * x

The action of the loop, read on an element of the vertex space.

theorem TauCeti.isFinDim_oneLoopNilpotentRep {k : Type u} [Field k] (n : ℕ) : IsFinDim k Quiver.OneLoop (oneLoopNilpotentRep k n)

TauCeti.oneLoopNilpotentRep k n is finite-dimensional: its vertex space is k[X]/(Xⁿ⁺¹).

theorem TauCeti.dimVector_oneLoopNilpotentRep {k : Type u} [Field k] (n : ℕ) (v : Quiver.OneLoop) : dimVector (oneLoopNilpotentRep k n) v = n + 1

The dimension vector of TauCeti.oneLoopNilpotentRep k n is n + 1.

theorem TauCeti.not_isZero_oneLoopNilpotentRep {k : Type u} [Field k] (n : ℕ) : ¬CategoryTheory.Limits.IsZero (oneLoopNilpotentRep k n)

TauCeti.oneLoopNilpotentRep k n is nonzero: its vertex space is the nontrivial ring k[X]/(Xⁿ⁺¹).

theorem TauCeti.indecomposable_oneLoopNilpotentRep {k : Type u} [Field k] (n : ℕ) : CategoryTheory.Indecomposable (oneLoopNilpotentRep k n)

TauCeti.oneLoopNilpotentRep k n is indecomposable. An endomorphism commutes with multiplication by the root, hence is multiplication by its value at 1 (TauCeti.AdjoinRoot.eq_mulRight_of_root_mul), so that value records it faithfully in k[X]/(Xⁿ⁺¹), a local ring (TauCeti.isLocalRing_adjoinRoot_X_pow), sending 0 to 0, the identity to 1 and squares to squares.

theorem TauCeti.eq_of_nonempty_oneLoopNilpotentRep_iso {k : Type u} [Field k] {m n : ℕ} (h : Nonempty (oneLoopNilpotentRep k m ≅ oneLoopNilpotentRep k n)) : m = n

Nilpotent Jordan blocks of different sizes are non-isomorphic: their dimension vectors differ.

@[simp]

theorem TauCeti.nonempty_oneLoopNilpotentRep_iso_iff {k : Type u} [Field k] {m n : ℕ} : Nonempty (oneLoopNilpotentRep k m ≅ oneLoopNilpotentRep k n) ↔ m = n

Two nilpotent Jordan blocks are isomorphic exactly when their sizes agree.

theorem TauCeti.not_isFiniteRepType_oneLoop (k : Type u) [Field k] : ¬IsFiniteRepType k Quiver.OneLoop

The loop quiver has infinite representation type over every field. The nilpotent Jordan blocks TauCeti.oneLoopNilpotentRep k n are finite-dimensional, indecomposable, and pairwise non-isomorphic, so ℕ indexes an infinite family of them.