The quiver of irreducible morphisms of a finite-dimensional algebra

Let A be a finite-dimensional algebra over a field k. This file specializes TauCeti.IrreducibleMorphismQuiver to the finitely generated A-modules, IrreducibleMorphismQuiver k fun M : ModuleCat A ↦ Module.Finite A M. Its vertices are the isomorphism classes of finitely generated indecomposable A-modules, and its arrows index a k-basis of rad / rad² between representatives. For A = kQ/I over an algebraically closed field this is the underlying quiver of the Auslander–Reiten quiver of A; over other fields the arrows count dimensions over k, not the valuations over the residue division rings.

The instances here make the general API apply without further hypotheses:

• the morphism spaces between representatives are finite-dimensional (ModuleCat.finite_hom_of_finite), so every arrow set is finite;
• representatives have local endomorphism rings (TauCeti.isLocalRing_end_of_indecomposable, Fitting's lemma for the finite-dimensional endomorphism algebra), so TauCeti.IrreducibleMorphismQuiver.nonempty_arrows_of_iff and TauCeti.exists_isIrreducibleMorphism_irreducibleMorphismMk_eq apply to them.

The Auslander–Reiten translate ModuleCat.arTranslate is an Auslander–Reiten translation in the sense of TauCeti.ARTranslation (ModuleCat.arTranslation). Its partial translation on this quiver is undefined exactly at the projective vertices and is a bijection from the non-projective vertices onto the non-injective ones (TauCeti.ARTranslation.existsUnique_translate_eq_some_iff).

No algebraic closedness is assumed.

References

• I. Assem, D. Simson, A. Skowroński, Elements of the Representation Theory of Associative Algebras, Vol. I (2006), IV.4.
• M. Auslander, I. Reiten, S. O. Smalø, Representation Theory of Artin Algebras, Cambridge University Press (1995), VII.1.

theorem TauCeti.IrreducibleMorphismQuiver.finite_iff_isRepresentationFinite (k : Type u) (A : Type v) [Ring A] : Finite (IrreducibleMorphismQuiver k fun (M : ModuleCat A) => Module.Finite A ↑M) ↔ IsRepresentationFinite A

The quiver of irreducible morphisms of finitely generated modules has finitely many vertices exactly when the ring is representation-finite.

instance TauCeti.IrreducibleMorphismQuiver.instFiniteCarrierRepresentativeModuleCat {k : Type u} {A : Type v} [Ring A] (a : IrreducibleMorphismQuiver k fun (M : ModuleCat A) => Module.Finite A ↑M) : Module.Finite A ↑a.representative

instance TauCeti.IrreducibleMorphismQuiver.instIsLocalRingEndModuleCatRepresentativeFiniteCarrier {k : Type u} {A : Type v} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] (a : IrreducibleMorphismQuiver k fun (M : ModuleCat A) => Module.Finite A ↑M) : IsLocalRing (CategoryTheory.End a.representative)

theorem TauCeti.IsRepresentationFinite.finite_irreducibleMorphismQuiver_arrows {k : Type u} {A : Type v} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] (h : IsRepresentationFinite A) : Finite ((a : IrreducibleMorphismQuiver k fun (M : ModuleCat A) => Module.Finite A ↑M) × (b : IrreducibleMorphismQuiver k fun (M : ModuleCat A) => Module.Finite A ↑M) × (a ⟶ b))

For a representation-finite algebra, the quiver of irreducible morphisms of finitely generated modules has finitely many arrows in total.

noncomputable def ModuleCat.arTranslation (k : Type u) (A : Type v) [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] : TauCeti.ARTranslation fun (M : ModuleCat A) => Module.Finite A ↑M

The Auslander–Reiten translate of finitely generated modules over a finite-dimensional algebra, as a translation on their isomorphism classes.

@[simp]

theorem ModuleCat.arTranslation_obj (k : Type u) (A : Type v) [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] (M : ModuleCat A) (hM : Module.Finite A ↑M) : (arTranslation k A).obj M hM = arTranslate k M