The Krull-Schmidt theorem for quiver representations

A pointwise finite-dimensional representation of a finite quiver is a finite biproduct of indecomposable representations, and the summands of two such decompositions are matched by a bijection of their index sets under which corresponding summands are isomorphic. This is what makes "the indecomposable summands of a representation, with multiplicity" an invariant of the representation, and hence what makes "the indecomposable representations" of a quiver a well-defined family to count.

The theorem is not proved again here. It is the Krull-Schmidt theorem for modules over the path algebra, TauCeti.exists_indecomposable_iso_biproduct and TauCeti.exists_equiv_iso_of_iso_biproduct, read through the dictionary TauCeti.quiverRepEquivalence : QuiverRep k Q ≌ ModuleCat (pathAlgebra k Q). Three properties of that dictionary carry it across: both of its directions are right adjoints, hence additive by CategoryTheory.Functor.additive_of_isRightAdjoint, so they carry finite biproducts to finite biproducts; both are fully faithful, so they carry indecomposable objects to indecomposable objects (CategoryTheory.Functor.indecomposable_obj_of_map_bijective); and a pointwise finite-dimensional representation of a finite quiver goes to a module that is finite-dimensional over the base field (TauCeti.module_finite_quiverRepEquivalenceFunctorObj_of_isFinDim), hence Artinian and Noetherian over the path algebra, which is the finiteness hypothesis the module-level theorem asks for. The path algebra itself need not be finite-dimensional: over the quiver with one vertex and one loop it is k[X], and a representation of that quiver is a finite-dimensional vector space with an endomorphism, whose indecomposable summands are the cyclic modules k[X] / (p ^ e) with p irreducible, the Jordan blocks of the endomorphism when k is algebraically closed. That decomposition refines the primary decomposition of the module, whose p-primary component is the sum of all the summands for that p.

Main results

• TauCeti.QuiverRep.exists_indecomposable_iso_biproduct: existence, a pointwise finite-dimensional representation of a finite quiver is isomorphic to a finite biproduct of indecomposable representations, themselves pointwise finite-dimensional.
• TauCeti.QuiverRep.exists_equiv_iso_of_iso_biproduct: the Krull-Schmidt theorem, two decompositions of a pointwise finite-dimensional representation into indecomposable summands are matched by a bijection of the index sets under which corresponding summands are isomorphic, with TauCeti.QuiverRep.exists_equiv_iso_of_biproduct_iso the form with no ambient representation.
• TauCeti.QuiverRep.card_eq_card_of_iso_biproduct and TauCeti.QuiverRep.eq_of_iso_biproduct_fin: in particular the two decompositions have the same number of summands.
• TauCeti.QuiverRep.card_iso_eq_card_iso_of_iso_biproduct: the number of summands isomorphic to a fixed representation is the same in any two such decompositions, so the multiplicity of an indecomposable summand is an invariant.
• TauCeti.QuiverRep.isKrullSchmidt_isFinDim: the pointwise finite-dimensional representations form a Krull-Schmidt category.

References

See I. Assem, D. Simson, A. Skowroński, Elements of the Representation Theory of Associative Algebras, Vol. 1, Section I.4.

theorem TauCeti.QuiverRep.exists_indecomposable_iso_biproduct {k : Type u} {Q : Type v} [Field k] [Quiver Q] [Finite Q] (M : QuiverRep k Q) (hM : IsFinDim k Q M) : ∃ (n : ℕ) (P : Fin n → QuiverRep k Q), (∀ (i : Fin n), CategoryTheory.Indecomposable (P i)) ∧ (∀ (i : Fin n), IsFinDim k Q (P i)) ∧ Nonempty (M ≅ ⨁ P)

Existence of an indecomposable decomposition of a quiver representation. A pointwise finite-dimensional representation of a finite quiver is a finite biproduct of indecomposable representations, each of them again pointwise finite-dimensional.

The index type is Fin n, the shape TauCeti.exists_indecomposable_iso_biproduct produces the decomposition of the corresponding path-algebra module in.

theorem TauCeti.QuiverRep.exists_equiv_iso_of_iso_biproduct {k : Type u} {Q : Type v} [Field k] [Quiver Q] [Finite Q] {ι κ : Type} [Finite ι] [Finite κ] {P : ι → QuiverRep k Q} {R : κ → QuiverRep k Q} {M : QuiverRep k Q} (hM : IsFinDim k Q M) (eP : M ≅ ⨁ P) (eR : M ≅ ⨁ R) (hP : ∀ (i : ι), CategoryTheory.Indecomposable (P i)) (hR : ∀ (j : κ), CategoryTheory.Indecomposable (R j)) : ∃ (e : ι ≃ κ), ∀ (i : ι), Nonempty (P i ≅ R (e i))

The Krull-Schmidt theorem for quiver representations. If a pointwise finite-dimensional representation of a finite quiver is isomorphic to a finite biproduct of indecomposable representations in two ways, the two families of summands are matched by a bijection of their index sets under which corresponding summands are isomorphic.

TauCeti.QuiverRep.exists_indecomposable_iso_biproduct supplies such an isomorphism.

theorem TauCeti.QuiverRep.exists_equiv_iso_of_biproduct_iso {k : Type u} {Q : Type v} [Field k] [Quiver Q] [Finite Q] {ι κ : Type} [Finite ι] [Finite κ] {P : ι → QuiverRep k Q} {R : κ → QuiverRep k Q} (h : IsFinDim k Q (⨁ P)) (e : ⨁ P ≅ ⨁ R) (hP : ∀ (i : ι), CategoryTheory.Indecomposable (P i)) (hR : ∀ (j : κ), CategoryTheory.Indecomposable (R j)) : ∃ (f : ι ≃ κ), ∀ (i : ι), Nonempty (P i ≅ R (f i))

The Krull-Schmidt theorem with no ambient representation: an isomorphism between two finite biproducts of indecomposable, pointwise finite-dimensional representations matches their summands by a bijection of the index sets.

theorem TauCeti.QuiverRep.card_eq_card_of_iso_biproduct {k : Type u} {Q : Type v} [Field k] [Quiver Q] [Finite Q] {ι κ : Type} [Finite ι] [Finite κ] {P : ι → QuiverRep k Q} {R : κ → QuiverRep k Q} {M : QuiverRep k Q} (hM : IsFinDim k Q M) (eP : M ≅ ⨁ P) (eR : M ≅ ⨁ R) (hP : ∀ (i : ι), CategoryTheory.Indecomposable (P i)) (hR : ∀ (j : κ), CategoryTheory.Indecomposable (R j)) : Nat.card ι = Nat.card κ

Two decompositions of a pointwise finite-dimensional representation as a biproduct of indecomposable representations have the same number of summands.

theorem TauCeti.QuiverRep.card_iso_eq_card_iso_of_iso_biproduct {k : Type u} {Q : Type v} [Field k] [Quiver Q] [Finite Q] {ι κ : Type} [Finite ι] [Finite κ] {P : ι → QuiverRep k Q} {R : κ → QuiverRep k Q} {M : QuiverRep k Q} (hM : IsFinDim k Q M) (eP : M ≅ ⨁ P) (eR : M ≅ ⨁ R) (hP : ∀ (i : ι), CategoryTheory.Indecomposable (P i)) (hR : ∀ (j : κ), CategoryTheory.Indecomposable (R j)) (N : QuiverRep k Q) : Nat.card { i : ι // Nonempty (P i ≅ N) } = Nat.card { j : κ // Nonempty (R j ≅ N) }

The multiplicity of an indecomposable summand of a quiver representation is well defined: the number of summands isomorphic to a fixed representation N is the same in any two indecomposable biproduct decompositions of a pointwise finite-dimensional representation.

theorem TauCeti.QuiverRep.eq_of_iso_biproduct_fin {k : Type u} {Q : Type v} [Field k] [Quiver Q] [Finite Q] {M : QuiverRep k Q} (hM : IsFinDim k Q M) {m n : ℕ} {P : Fin m → QuiverRep k Q} {R : Fin n → QuiverRep k Q} (eP : M ≅ ⨁ P) (eR : M ≅ ⨁ R) (hP : ∀ (i : Fin m), CategoryTheory.Indecomposable (P i)) (hR : ∀ (j : Fin n), CategoryTheory.Indecomposable (R j)) : m = n

The number of summands of an indecomposable biproduct decomposition of a pointwise finite-dimensional representation is well defined: two Fin-indexed decompositions have the same length. This is the form in which TauCeti.QuiverRep.exists_indecomposable_iso_biproduct produces its decompositions.

Pointwise finite-dimensional representations form a Krull-Schmidt category

instance TauCeti.QuiverRep.isKrullSchmidt_isFinDim {k : Type u} {Q : Type v} [Field k] [Quiver Q] [Finite Q] : IsKrullSchmidt (CategoryTheory.ObjectProperty.FullSubcategory (IsFinDim k Q))

Pointwise finite-dimensional representations of a finite quiver form a Krull-Schmidt category: every such representation is a finite biproduct of indecomposable ones (TauCeti.QuiverRep.exists_indecomposable_iso_biproduct), whose endomorphism rings are local by Fitting's lemma (TauCeti.isLocalRing_end_of_indecomposable), since their endomorphisms form a finite-dimensional space (TauCeti.QuiverRep.finiteDimensional_hom).