The extended Dynkin quiver E₈~ has infinite representation type

A vector space V with an endomorphism f gives three flags in V⁶. The long arm is the standard full flag, the medium arm is the flag on the last two and last four coordinates, and the short arm is the image of (x,y,z) ↦ (x, x+z, y, x+f(y), z, y+z).

Preserving the first two flags forces a morphism to act by three upper triangular two-by-two blocks. Preserving the short subspace kills the off-diagonal entries, equates the diagonal maps and forces the common map to intertwine the endomorphisms. Thus the construction is fully faithful, preserves finite-dimensionality and indecomposability, and reflects isomorphisms. The loop quiver's nilpotent Jordan blocks give infinite representation type over every field, including finite fields and fields of characteristic two.

The construction and API follow the analogous E₆~ construction in TauCeti.RepresentationTheory.Quiver.AffineE6.FiniteRepType. The coordinate calculation uses no division.

References

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

def TauCeti.Quiver.AffineE8.arrowMap {k : Type u} [Semiring k] {V : Type t} [AddCommMonoid V] [Module k V] {a b : AffineE8} (e : a ⟶ b) (f : V →ₗ[k] V) : (Fin a.coordinateCount → V) →ₗ[k] Fin b.coordinateCount → V

The maps of the three standard flags associated to an endomorphism: prefix inclusions on the long arm, suffix inclusions on the medium arm, and the map involving f on the short arm.

@[simp]

theorem TauCeti.Quiver.AffineE8.arrowMap_apply {k : Type u} [Semiring k] {V : Type t} [AddCommMonoid V] [Module k V] {a b : AffineE8} (e : a ⟶ b) (f : V →ₗ[k] V) (x : Fin a.coordinateCount → V) : (arrowMap e f) x = match (motive := (b a : AffineE8) → (a ⟶ b) → (Fin a.coordinateCount → V) → Fin b.coordinateCount → V) b, a, e, x with | .(center), .(short), Arrow.short, x => ![x 0, x 0 + x 2, x 1, x 0 + f (x 1), x 2, x 1 + x 2] | .(medium4), .(medium2), Arrow.medium2, x => ![0, 0, x 0, x 1] | .(center), .(medium4), Arrow.medium4, x => ![0, 0, x 0, x 1, x 2, x 3] | .(long2), .(long1), Arrow.long1, x => ![x 0, 0] | .(long3), .(long2), Arrow.long2, x => ![x 0, x 1, 0] | .(long4), .(long3), Arrow.long3, x => ![x 0, x 1, x 2, 0] | .(long5), .(long4), Arrow.long4, x => ![x 0, x 1, x 2, x 3, 0] | .(center), .(long5), Arrow.long5, x => ![x 0, x 1, x 2, x 3, x 4, 0]

The flag arrow maps, in coordinates.

noncomputable def TauCeti.affineE8LoopRep {k : Type u} [Field k] (M : QuiverRep k Quiver.OneLoop) : QuiverRep k Quiver.AffineE8

A loop representation as three flags in the sixth power of its vertex space. The long arm is the standard full flag, the medium arm the last-two/last-four flag, and the short arm is (x,y,z) ↦ (x,x+z,y,x+f(y),z,y+z). The body is exposed so that the vertex-space types can be used in the coordinate API.

@[simp]

theorem TauCeti.affineE8LoopRep_obj {k : Type u} [Field k] {M : QuiverRep k Quiver.OneLoop} (v : Quiver.AffineE8) : (affineE8LoopRep M).obj v = ↧(Fin v.coordinateCount → ↑(M.obj Quiver.OneLoop.vertex))

The vertex spaces are powers of the loop vertex space, with the imaginary-root multiplicities.

@[simp]

theorem TauCeti.affineE8LoopRep_map_arrow {k : Type u} [Field k] {M : QuiverRep k Quiver.OneLoop} {a b : Quiver.AffineE8} (e : a ⟶ b) : (affineE8LoopRep M).map e.toPath = ModuleCat.ofHom (Quiver.AffineE8.arrowMap e (ModuleCat.Hom.hom (M.map Quiver.OneLoop.loop.toPath)))

The representation uses the standard flag map on each arrow.

theorem TauCeti.isFinDim_affineE8LoopRep {k : Type u} [Field k] {M : QuiverRep k Quiver.OneLoop} (hM : IsFinDim k Quiver.OneLoop M) : IsFinDim k Quiver.AffineE8 (affineE8LoopRep M)

A finite-dimensional loop representation gives finite-dimensional flag spaces.

noncomputable def TauCeti.affineE8LoopFunctor (k : Type u) [Field k] : CategoryTheory.Functor (QuiverRep k Quiver.OneLoop) (QuiverRep k Quiver.AffineE8)

A morphism of loop representations acts coordinatewise on every flag space.

@[simp]

theorem TauCeti.affineE8LoopFunctor_obj {k : Type u} [Field k] {M : QuiverRep k Quiver.OneLoop} : (affineE8LoopFunctor k).obj M = affineE8LoopRep M

The functor's object construction is the flag representation.

@[simp]

theorem TauCeti.affineE8LoopFunctor_map_app {k : Type u} [Field k] {M N : QuiverRep k Quiver.OneLoop} (φ : M ⟶ N) (v : Quiver.AffineE8) : ((affineE8LoopFunctor k).map φ).app v = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (ModuleCat.ofHom ((ModuleCat.Hom.hom (φ.app Quiver.OneLoop.vertex)).compLeft (Fin v.coordinateCount))) (CategoryTheory.eqToHom ⋯))

The functor acts coordinatewise on morphisms, transported to its vertex spaces.

noncomputable def TauCeti.fullyFaithfulAffineE8LoopFunctor {k : Type u} [Field k] : (affineE8LoopFunctor k).FullyFaithful

The loop-to-flag functor is fully faithful: every morphism is coordinatewise application of one linear map intertwining the loop actions.

@[simp]

theorem TauCeti.nonempty_affineE8LoopRep_iso_iff {k : Type u} [Field k] {M N : QuiverRep k Quiver.OneLoop} : Nonempty (affineE8LoopRep M ≅ affineE8LoopRep N) ↔ Nonempty (M ≅ N)

The flag construction reflects and preserves isomorphisms.

theorem TauCeti.indecomposable_affineE8LoopRep {k : Type u} [Field k] {M : QuiverRep k Quiver.OneLoop} (hM : CategoryTheory.Indecomposable M) : CategoryTheory.Indecomposable (affineE8LoopRep M)

A loop indecomposable gives an indecomposable configuration of three flags.

theorem TauCeti.IsFiniteRepType.oneLoop_of_affineE8 {k : Type u} [Field k] (h : IsFiniteRepType k Quiver.AffineE8) : IsFiniteRepType k Quiver.OneLoop

Finite representation type for the extended E₈ quiver would imply it for the loop quiver.

theorem TauCeti.not_isFiniteRepType_affineE8 (k : Type u) [Field k] : ¬IsFiniteRepType k Quiver.AffineE8

The extended Dynkin quiver E₈~ has infinite representation type over every field.