The partial translation on the quiver of irreducible morphisms

An Auslander–Reiten translate on a class P of objects of a category is recorded by TauCeti.ARTranslation P: an operation τ on the objects satisfying P that preserves P and isomorphism, is indecomposable on an indecomposable object exactly when that object is not projective, is injective exactly on projectives, reflects isomorphism on non-projective indecomposables, and reaches every non-injective indecomposable. These are the properties of D Tr on finitely generated modules over a finite-dimensional algebra (ModuleCat.arTranslate) and on finite-dimensional quiver representations (TauCeti.arTranslate).

Such a translate descends to a partial map ARTranslation.translate on the vertices of TauCeti.IrreducibleMorphismQuiver k P, undefined exactly at the projective vertices. Its values are non-injective vertices, it is injective where defined, and every non-injective vertex is a value (ARTranslation.existsUnique_translate_eq_some_iff). So it is a bijection from the non-projective vertices onto the non-injective ones, the partial translation of the Auslander–Reiten quiver.

References

• M. Auslander, I. Reiten, S. O. Smalø, Representation Theory of Artin Algebras, Cambridge University Press (1995), Sections IV.1 and VII.1.

structure TauCeti.ARTranslation {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] (P : CategoryTheory.ObjectProperty C) : Type u

An Auslander–Reiten translate on the objects satisfying P: an operation preserving P and isomorphism, indecomposable exactly away from projectives, injective exactly on projectives, reflecting isomorphism on non-projective indecomposables, and reaching every non-injective indecomposable.

• obj (M : C) (hM : P M) : C

  The translate of an object satisfying P.

• prop_obj (M : C) (hM : P M) : P (self.obj M hM)

  The translate satisfies P.

• nonempty_iso_obj_of_iso {M N : C} (hM : P M) (hN : P N) (e : M ≅ N) : Nonempty (self.obj M hM ≅ self.obj N hN)

  Isomorphic objects have isomorphic translates.

• indecomposable_obj_iff (M : C) (hM : P M) (hI : CategoryTheory.Indecomposable M) : CategoryTheory.Indecomposable (self.obj M hM) ↔ ¬CategoryTheory.Projective M

  The translate of an indecomposable is indecomposable exactly when it is not projective.

• injective_obj_iff (M : C) (hM : P M) : CategoryTheory.Injective (self.obj M hM) ↔ CategoryTheory.Projective M

  The translate is injective exactly when the object is projective.

• nonempty_iso_of_nonempty_iso_obj {M N : C} (hM : P M) (hN : P N) (hiM : CategoryTheory.Indecomposable M) (hiN : CategoryTheory.Indecomposable N) (hpM : ¬CategoryTheory.Projective M) : Nonempty (self.obj M hM ≅ self.obj N hN) → Nonempty (M ≅ N)

  On non-projective indecomposables, isomorphic translates come from isomorphic objects.

• exists_nonempty_iso_obj (N : C) (hN : P N) (hiN : CategoryTheory.Indecomposable N) (hinj : ¬CategoryTheory.Injective N) : ∃ (M : C) (hM : P M), CategoryTheory.Indecomposable M ∧ ¬CategoryTheory.Projective M ∧ Nonempty (self.obj M hM ≅ N)

  Every non-injective indecomposable is a translate of a non-projective indecomposable.

noncomputable def TauCeti.ARTranslation.translate {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {k : Type w} {P : CategoryTheory.ObjectProperty C} (T : ARTranslation P) (a : IrreducibleMorphismQuiver k P) : Option (IrreducibleMorphismQuiver k P)

The partial translation on isomorphism classes: the translate away from projectives, and none on projectives.

@[simp]

theorem TauCeti.ARTranslation.translate_eq_none_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {k : Type w} {P : CategoryTheory.ObjectProperty C} (T : ARTranslation P) (a : IrreducibleMorphismQuiver k P) : T.translate a = none ↔ CategoryTheory.Projective a.representative

Translation is undefined exactly at projective classes.

@[simp]

theorem TauCeti.ARTranslation.translate_of_eq_none_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {k : Type w} {P : CategoryTheory.ObjectProperty C} (T : ARTranslation P) {M : C} (hM : P M) (hI : CategoryTheory.Indecomposable M) : T.translate (IrreducibleMorphismQuiver.of k hM hI) = none ↔ CategoryTheory.Projective M

The class of an object has undefined translation exactly when the object is projective.

theorem TauCeti.ARTranslation.translate_of {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {k : Type w} {P : CategoryTheory.ObjectProperty C} (T : ARTranslation P) {M : C} (hM : P M) (hI : CategoryTheory.Indecomposable M) (hp : ¬CategoryTheory.Projective M) : T.translate (IrreducibleMorphismQuiver.of k hM hI) = some (IrreducibleMorphismQuiver.of k ⋯ ⋯)

Any representative computes translation: the class of a non-projective object is sent to the class of its translate.

@[simp]

theorem TauCeti.ARTranslation.translate_of_eq_some_of_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {k : Type w} {P : CategoryTheory.ObjectProperty C} (T : ARTranslation P) {M N : C} (hM : P M) (hI : CategoryTheory.Indecomposable M) (hN : P N) (hJ : CategoryTheory.Indecomposable N) : T.translate (IrreducibleMorphismQuiver.of k hM hI) = some (IrreducibleMorphismQuiver.of k hN hJ) ↔ ¬CategoryTheory.Projective M ∧ Nonempty (T.obj M hM ≅ N)

Translation of one class is another class exactly when the first is non-projective and its translate is isomorphic to a representative of the second.

theorem TauCeti.ARTranslation.not_injective_of_translate_eq_some {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {k : Type w} {P : CategoryTheory.ObjectProperty C} (T : ARTranslation P) {a b : IrreducibleMorphismQuiver k P} (h : T.translate a = some b) : ¬CategoryTheory.Injective b.representative

Every defined translation lands at a non-injective class.

theorem TauCeti.ARTranslation.eq_of_translate_eq_some {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {k : Type w} {P : CategoryTheory.ObjectProperty C} (T : ARTranslation P) {a b c : IrreducibleMorphismQuiver k P} (ha : T.translate a = some c) (hb : T.translate b = some c) : a = b

Two classes with the same defined translation are equal.

theorem TauCeti.ARTranslation.translate_injective {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {k : Type w} {P : CategoryTheory.ObjectProperty C} (T : ARTranslation P) : Function.Injective fun (a : { a : IrreducibleMorphismQuiver k P // ¬CategoryTheory.Projective a.representative }) => T.translate ↑a

Translation is injective on the non-projective vertices.

@[simp]

theorem TauCeti.ARTranslation.existsUnique_translate_eq_some_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {k : Type w} {P : CategoryTheory.ObjectProperty C} (T : ARTranslation P) (b : IrreducibleMorphismQuiver k P) : (∃! a : IrreducibleMorphismQuiver k P, T.translate a = some b) ↔ ¬CategoryTheory.Injective b.representative

A vertex has a unique preimage under defined translation exactly when it is non-injective. Thus translation bijects the non-projective and the non-injective classes.