The extended Dynkin quiver D~ₙ has infinite representation type

The quiver TauCeti.Quiver.AffineD m, whose underlying graph is the extended Dynkin diagram D~ₘ₊₄, has infinitely many finite-dimensional indecomposable representations over every field (TauCeti.not_isFiniteRepType_affineD).

The proof reduces to the four subspace quiver, the case m = 0, which is already known to have infinite representation type (TauCeti.not_isFiniteRepType_subspace_fin_four). A representation M of the four subspace quiver is stretched along the spine (TauCeti.affineDStretchRep): its centre space is placed at every spine vertex, with the identity on every spine arrow, and its four outer spaces at the four leaves, each leaf arrow acting as the corresponding arrow of M.

Stretching is fully faithful (TauCeti.fullyFaithfulAffineDStretchFunctor). A morphism between stretched representations commutes with the identity maps along the spine, so its components at all the spine vertices agree; that common component, together with the components at the leaves, is a morphism of the original representations. Stretching therefore preserves indecomposability and reflects isomorphism, and it preserves finite-dimensionality, so it embeds the finite-dimensional indecomposables of the four subspace quiver, up to isomorphism, in those of TauCeti.Quiver.AffineD m.

Main definitions

• TauCeti.affineDCollapseFunctor: the functor collapsing the spine to the four subspace centre.
• TauCeti.affineDStretchRep: a representation of the four subspace quiver, stretched along the spine of TauCeti.Quiver.AffineD m.
• TauCeti.affineDStretchFunctor: stretching, as a functor.

Main results

• TauCeti.fullyFaithfulAffineDStretchFunctor: stretching is fully faithful.
• TauCeti.IsFiniteRepType.subspace_fin_four_of_affineD: finite representation type of TauCeti.Quiver.AffineD m would force it on the four subspace quiver.
• TauCeti.not_isFiniteRepType_affineD: TauCeti.Quiver.AffineD m has infinite representation type over every field.

Implementation notes

TauCeti.affineDCollapseFunctor and TauCeti.affineDStretchRep carry @[expose] for the reason recorded on TauCeti.subspaceJordanRep: the vertex spaces are needed definitionally to state the homogeneous arrow equations. Stretching is precomposition with the functor collapsing the spine to the centre of the four subspace quiver, using CategoryTheory.Functor.whiskeringLeft.

References

• I. Assem, D. Simson, A. Skowroński, Elements of the Representation Theory of Associative Algebras, Volume I, Chapter VII.
• H. Derksen, J. Weyman, An Introduction to Quiver Representations, Chapter 4.

def TauCeti.affineDCollapseFunctor (m : ℕ) : CategoryTheory.Functor (CategoryTheory.Paths (Quiver.AffineD m)) (CategoryTheory.Paths (Quiver.Subspace (Fin 4)))

Collapse the spine to the centre of the four subspace quiver, sending spine arrows to identity paths and leaf arrows to the corresponding outer-to-centre paths.

@[simp]

theorem TauCeti.affineDCollapseFunctor_obj_leaf {m : ℕ} (i : Fin 4) : (affineDCollapseFunctor m).obj (Quiver.AffineD.leaf i) = Quiver.Subspace.outer i

The collapse sends each leaf to the corresponding outer vertex.

@[simp]

theorem TauCeti.affineDCollapseFunctor_obj_spine {m : ℕ} (j : Fin (m + 1)) : (affineDCollapseFunctor m).obj (Quiver.AffineD.spine j) = Quiver.Subspace.center

The collapse sends every spine vertex to the centre.

@[simp]

theorem TauCeti.affineDCollapseFunctor_map_leafArrow {m : ℕ} (i : Fin 4) : (affineDCollapseFunctor m).map (Quiver.AffineD.leafArrow m i).toPath = (Quiver.Subspace.arrow i).toPath

The collapse sends each leaf arrow to its corresponding outer-to-centre path.

@[simp]

theorem TauCeti.affineDCollapseFunctor_map_spineArrow {m : ℕ} (j : Fin m) : (affineDCollapseFunctor m).map (Quiver.AffineD.spineArrow j).toPath = CategoryTheory.CategoryStruct.id Quiver.Subspace.center

The collapse sends every spine arrow to the identity path at the centre.

noncomputable def TauCeti.affineDStretchRep {k : Type u} [Field k] (m : ℕ) (M : QuiverRep k (Quiver.Subspace (Fin 4))) : QuiverRep k (Quiver.AffineD m)

A representation of the four subspace quiver, stretched along the spine of TauCeti.Quiver.AffineD m: the centre space of M sits at every spine vertex, with the identity on every spine arrow, and the outer space indexed by i at the leaf indexed by i, whose arrow acts as the arrow of M from that outer vertex.

@[simp]

theorem TauCeti.affineDStretchRep_obj_leaf {k : Type u} [Field k] {m : ℕ} {M : QuiverRep k (Quiver.Subspace (Fin 4))} (i : Fin 4) : (affineDStretchRep m M).obj (Quiver.AffineD.leaf i) = M.obj (Quiver.Subspace.outer i)

The leaf indexed by i of a stretched representation carries the outer space of M indexed by i.

@[simp]

theorem TauCeti.affineDStretchRep_obj_spine {k : Type u} [Field k] {m : ℕ} {M : QuiverRep k (Quiver.Subspace (Fin 4))} (j : Fin (m + 1)) : (affineDStretchRep m M).obj (Quiver.AffineD.spine j) = M.obj Quiver.Subspace.center

Every spine vertex of a stretched representation carries the centre space of M.

@[simp]

theorem TauCeti.affineDStretchRep_map_leafArrow {k : Type u} [Field k] {m : ℕ} {M : QuiverRep k (Quiver.Subspace (Fin 4))} (i : Fin 4) : (affineDStretchRep m M).map (Quiver.AffineD.leafArrow m i).toPath = M.map (Quiver.Subspace.arrow i).toPath

The leaf arrow indexed by i acts on a stretched representation as the arrow of M from the outer vertex indexed by i.

@[simp]

theorem TauCeti.affineDStretchRep_map_spineArrow {k : Type u} [Field k] {m : ℕ} {M : QuiverRep k (Quiver.Subspace (Fin 4))} (j : Fin m) : (affineDStretchRep m M).map (Quiver.AffineD.spineArrow j).toPath = CategoryTheory.CategoryStruct.id (M.obj Quiver.Subspace.center)

Every spine arrow acts on a stretched representation as the identity.

theorem TauCeti.isFinDim_affineDStretchRep {k : Type u} [Field k] {m : ℕ} {M : QuiverRep k (Quiver.Subspace (Fin 4))} (hM : IsFinDim k (Quiver.Subspace (Fin 4)) M) : IsFinDim k (Quiver.AffineD m) (affineDStretchRep m M)

A stretched representation of a finite-dimensional representation is finite-dimensional: its vertex spaces are vertex spaces of M.

noncomputable def TauCeti.affineDStretchFunctor (k : Type u) [Field k] (m : ℕ) : CategoryTheory.Functor (QuiverRep k (Quiver.Subspace (Fin 4))) (QuiverRep k (Quiver.AffineD m))

Stretching along the spine of TauCeti.Quiver.AffineD m, as a functor: on a morphism it acts by its centre component at every spine vertex and by its outer components at the leaves.

@[simp]

theorem TauCeti.affineDStretchFunctor_obj {k : Type u} [Field k] {m : ℕ} {M : QuiverRep k (Quiver.Subspace (Fin 4))} : (affineDStretchFunctor k m).obj M = affineDStretchRep m M

The stretching functor sends a representation to its stretch.

@[simp]

theorem TauCeti.affineDStretchFunctor_map_app_leaf {k : Type u} [Field k] {m : ℕ} {M N : QuiverRep k (Quiver.Subspace (Fin 4))} (f : M ⟶ N) (i : Fin 4) : ((affineDStretchFunctor k m).map f).app (Quiver.AffineD.leaf i) ≍ f.app (Quiver.Subspace.outer i)

Stretching a morphism uses its outer component at each leaf.

@[simp]

theorem TauCeti.affineDStretchFunctor_map_app_spine {k : Type u} [Field k] {m : ℕ} {M N : QuiverRep k (Quiver.Subspace (Fin 4))} (f : M ⟶ N) (j : Fin (m + 1)) : ((affineDStretchFunctor k m).map f).app (Quiver.AffineD.spine j) ≍ f.app Quiver.Subspace.center

Stretching a morphism uses its centre component at every spine vertex.

Full faithfulness

noncomputable def TauCeti.fullyFaithfulAffineDStretchFunctor (k : Type u) [Field k] (m : ℕ) : (affineDStretchFunctor k m).FullyFaithful

Stretching along the spine of TauCeti.Quiver.AffineD m is fully faithful. A morphism of stretched representations has equal components at all the spine vertices, and that common component together with the leaf components is a morphism of the original representations.

@[simp]

theorem TauCeti.nonempty_affineDStretchRep_iso_iff {k : Type u} [Field k] {m : ℕ} {M N : QuiverRep k (Quiver.Subspace (Fin 4))} : Nonempty (affineDStretchRep m M ≅ affineDStretchRep m N) ↔ Nonempty (M ≅ N)

Stretching reflects and preserves isomorphism: two representations of the four subspace quiver are isomorphic exactly when their stretches along the spine of TauCeti.Quiver.AffineD m are.

theorem TauCeti.indecomposable_affineDStretchRep {k : Type u} [Field k] {m : ℕ} {M : QuiverRep k (Quiver.Subspace (Fin 4))} (hM : CategoryTheory.Indecomposable M) : CategoryTheory.Indecomposable (affineDStretchRep m M)

The stretch of an indecomposable representation is indecomposable: stretching is fully faithful, so it matches the idempotent endomorphisms of M with those of its stretch.

Infinite representation type

theorem TauCeti.IsFiniteRepType.subspace_fin_four_of_affineD {k : Type u} [Field k] {m : ℕ} (h : IsFiniteRepType k (Quiver.AffineD m)) : IsFiniteRepType k (Quiver.Subspace (Fin 4))

Finite representation type of TauCeti.Quiver.AffineD m would force it on the four subspace quiver: stretching carries the finite-dimensional indecomposables of the four subspace quiver to finite-dimensional indecomposables of TauCeti.Quiver.AffineD m and reflects isomorphism among them.

theorem TauCeti.not_isFiniteRepType_affineD (k : Type u) [Field k] (m : ℕ) : ¬IsFiniteRepType k (Quiver.AffineD m)

The extended Dynkin quiver D~ₘ₊₄ has infinite representation type over every field. The stretches along its spine of the Jordan block configurations of four subspaces (TauCeti.subspaceJordanRep) are infinitely many pairwise non-isomorphic finite-dimensional indecomposables.