The quiver of irreducible morphisms of a linear category

Let C be a k-linear category over a division ring k, and let P be a property of objects of C, such as finite generation or pointwise finite dimensionality. The vertices of TauCeti.IrreducibleMorphismQuiver k P are the isomorphism classes of indecomposable objects satisfying P. For each pair of vertices, choose representatives and a k-basis of their space rad / rad² of irreducible morphisms, TauCeti.irreducibleMorphismSpace; the arrows index that basis.

The number of arrows is independent of the representatives (card_arrows_of). Between objects with local endomorphism rings, in a category with binary biproducts, every basis vector is represented by an irreducible morphism (exists_isIrreducibleMorphism_irreducibleMorphismMk_eq_arrowBasis), and an arrow exists exactly when an irreducible morphism exists (nonempty_arrows_of_iff). No finiteness of the morphism spaces is needed for these statements; it is needed only for finiteness of the arrow sets.

When every indecomposable has endomorphism ring with residue division ring k, as over an algebraically closed field for finite-dimensional objects, this is the underlying quiver of the Auslander–Reiten quiver. Over other fields the arrows index a basis over the ground field, not over the residue division rings, so the valuations of the Auslander–Reiten quiver are not recorded.

The vertex type is a structure wrapping Mathlib's CategoryTheory.Skeleton of the full subcategory, identified with it by IrreducibleMorphismQuiver.equivSkeleton, so that the ground ring k determining the arrows is part of the type. The choices of representatives and bases are noncomputable.

References

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

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

The isomorphism classes of indecomposable objects satisfying P. Its quiver structure, over a division ring k acting linearly on C, has as arrows a chosen k-basis of rad / rad² between representatives.

• isoClass : CategoryTheory.Skeleton (CategoryTheory.ObjectProperty.FullSubcategory fun (X : C) => P X ∧ CategoryTheory.Indecomposable X)

  The isomorphism class, as an element of Mathlib's skeleton of the full subcategory.

theorem TauCeti.IrreducibleMorphismQuiver.ext_iff {C : Type u} {inst✝ : CategoryTheory.Category.{v, u} C} {inst✝¹ : CategoryTheory.Preadditive C} {inst✝² : CategoryTheory.Limits.HasBinaryBiproducts C} {k : Type w} {P : CategoryTheory.ObjectProperty C} {x y : IrreducibleMorphismQuiver k P} : x = y ↔ x.isoClass = y.isoClass

theorem TauCeti.IrreducibleMorphismQuiver.ext {C : Type u} {inst✝ : CategoryTheory.Category.{v, u} C} {inst✝¹ : CategoryTheory.Preadditive C} {inst✝² : CategoryTheory.Limits.HasBinaryBiproducts C} {k : Type w} {P : CategoryTheory.ObjectProperty C} {x y : IrreducibleMorphismQuiver k P} (isoClass : x.isoClass = y.isoClass) : x = y

def TauCeti.IrreducibleMorphismQuiver.equivSkeleton {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {k : Type w} {P : CategoryTheory.ObjectProperty C} : IrreducibleMorphismQuiver k P ≃ CategoryTheory.Skeleton (CategoryTheory.ObjectProperty.FullSubcategory fun (X : C) => P X ∧ CategoryTheory.Indecomposable X)

The vertices are the skeleton of the indecomposable objects satisfying P.

@[simp]

theorem TauCeti.IrreducibleMorphismQuiver.equivSkeleton_apply {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {k : Type w} {P : CategoryTheory.ObjectProperty C} (a : IrreducibleMorphismQuiver k P) : equivSkeleton a = a.isoClass

equivSkeleton reads off the skeleton class.

@[simp]

theorem TauCeti.IrreducibleMorphismQuiver.isoClass_equivSkeleton_symm {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {k : Type w} {P : CategoryTheory.ObjectProperty C} (a : CategoryTheory.Skeleton (CategoryTheory.ObjectProperty.FullSubcategory fun (X : C) => P X ∧ CategoryTheory.Indecomposable X)) : (equivSkeleton.symm a).isoClass = a

The inverse of equivSkeleton wraps a skeleton class.

def TauCeti.IrreducibleMorphismQuiver.of {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {P : CategoryTheory.ObjectProperty C} (k : Type w) {M : C} (hM : P M) (hI : CategoryTheory.Indecomposable M) : IrreducibleMorphismQuiver k P

The vertex represented by an indecomposable object satisfying P.

@[simp]

theorem TauCeti.IrreducibleMorphismQuiver.isoClass_of {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {k : Type w} {P : CategoryTheory.ObjectProperty C} {M : C} (hM : P M) (hI : CategoryTheory.Indecomposable M) : (of k hM hI).isoClass = CategoryTheory.toSkeleton { obj := M, property := ⋯ }

The vertex of an object corresponds to its skeleton class.

@[simp]

theorem TauCeti.IrreducibleMorphismQuiver.equivSkeleton_symm_toSkeleton {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {k : Type w} {P : CategoryTheory.ObjectProperty C} (M : CategoryTheory.ObjectProperty.FullSubcategory fun (X : C) => P X ∧ CategoryTheory.Indecomposable X) : equivSkeleton.symm (CategoryTheory.toSkeleton M) = of k ⋯ ⋯

A skeleton class becomes the vertex of the same object.

@[simp]

theorem TauCeti.IrreducibleMorphismQuiver.of_eq_of_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {k : Type w} {P : CategoryTheory.ObjectProperty C} {M N : C} (hM : P M) (hI : CategoryTheory.Indecomposable M) (hN : P N) (hJ : CategoryTheory.Indecomposable N) : of k hM hI = of k hN hJ ↔ Nonempty (M ≅ N)

Two objects determine the same vertex exactly when they are isomorphic.

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

A chosen object in the isomorphism class of a vertex.

theorem TauCeti.IrreducibleMorphismQuiver.representative_property {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {k : Type w} {P : CategoryTheory.ObjectProperty C} (a : IrreducibleMorphismQuiver k P) : P a.representative ∧ CategoryTheory.Indecomposable a.representative

A representative satisfies P and is indecomposable.

noncomputable def TauCeti.IrreducibleMorphismQuiver.representativeIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {P : CategoryTheory.ObjectProperty C} (k : Type w) {M : C} (hM : P M) (hI : CategoryTheory.Indecomposable M) : (of k hM hI).representative ≅ M

The chosen representative of an object's vertex is isomorphic to that object.

@[simp]

theorem TauCeti.IrreducibleMorphismQuiver.of_representative {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {k : Type w} {P : CategoryTheory.ObjectProperty C} (a : IrreducibleMorphismQuiver k P) : of k ⋯ ⋯ = a

Taking the class of a chosen representative recovers the vertex.

@[instance_reducible]

noncomputable instance TauCeti.IrreducibleMorphismQuiver.instQuiver {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {k : Type w} {P : CategoryTheory.ObjectProperty C} [DivisionRing k] [CategoryTheory.Linear k C] : Quiver (IrreducibleMorphismQuiver k P)

Arrows index a ground-ring basis of the irreducible morphism space between representatives.

noncomputable def TauCeti.IrreducibleMorphismQuiver.arrowBasis {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {k : Type w} {P : CategoryTheory.ObjectProperty C} [DivisionRing k] [CategoryTheory.Linear k C] (a b : IrreducibleMorphismQuiver k P) : Module.Basis (a ⟶ b) k (irreducibleMorphismSpace k a.representative b.representative)

The basis of rad / rad² indexed by the arrows of the quiver.

instance TauCeti.IrreducibleMorphismQuiver.instFiniteHomOfFiniteDimensionalIrreducibleMorphismSpaceRepresentative {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {k : Type w} {P : CategoryTheory.ObjectProperty C} [DivisionRing k] [CategoryTheory.Linear k C] (a b : IrreducibleMorphismQuiver k P) [FiniteDimensional k (irreducibleMorphismSpace k a.representative b.representative)] : Finite (a ⟶ b)

theorem TauCeti.IrreducibleMorphismQuiver.card_arrows {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {k : Type w} {P : CategoryTheory.ObjectProperty C} [DivisionRing k] [CategoryTheory.Linear k C] (a b : IrreducibleMorphismQuiver k P) : Nat.card (a ⟶ b) = Module.finrank k (irreducibleMorphismSpace k a.representative b.representative)

The arrow count is the dimension of the irreducible morphism space. Both sides are 0 when that space is infinite-dimensional.

theorem TauCeti.IrreducibleMorphismQuiver.card_arrows_of {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {k : Type w} {P : CategoryTheory.ObjectProperty C} [DivisionRing k] [CategoryTheory.Linear k C] {M N : C} (hM : P M) (hI : CategoryTheory.Indecomposable M) (hN : P N) (hJ : CategoryTheory.Indecomposable N) : Nat.card (of k hM hI ⟶ of k hN hJ) = Module.finrank k (irreducibleMorphismSpace k M N)

The arrow count can be computed on any representatives of the two classes.

theorem TauCeti.IrreducibleMorphismQuiver.nonempty_arrows_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {k : Type w} {P : CategoryTheory.ObjectProperty C} [DivisionRing k] [CategoryTheory.Linear k C] (a b : IrreducibleMorphismQuiver k P) : Nonempty (a ⟶ b) ↔ Nontrivial (irreducibleMorphismSpace k a.representative b.representative)

There is an arrow between two vertices exactly when the irreducible morphism space between their representatives is nonzero.

theorem TauCeti.IrreducibleMorphismQuiver.exists_isIrreducibleMorphism_irreducibleMorphismMk_eq_arrowBasis {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {k : Type w} {P : CategoryTheory.ObjectProperty C} [DivisionRing k] [CategoryTheory.Linear k C] (a b : IrreducibleMorphismQuiver k P) [IsLocalRing (CategoryTheory.End a.representative)] [IsLocalRing (CategoryTheory.End b.representative)] (i : a ⟶ b) : ∃ (f : ↥(jacobsonRadicalSubmodule k a.representative b.representative)), IsIrreducibleMorphism ↑f ∧ (irreducibleMorphismMk k a.representative b.representative) f = (a.arrowBasis b) i

Every arrow's basis vector is represented by an irreducible morphism, when the two representatives have local endomorphism rings.

theorem TauCeti.IrreducibleMorphismQuiver.nonempty_arrows_of_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {k : Type w} {P : CategoryTheory.ObjectProperty C} [DivisionRing k] [CategoryTheory.Linear k C] {M N : C} (hM : P M) (hI : CategoryTheory.Indecomposable M) (hN : P N) (hJ : CategoryTheory.Indecomposable N) [IsLocalRing (CategoryTheory.End M)] [IsLocalRing (CategoryTheory.End N)] : Nonempty (of k hM hI ⟶ of k hN hJ) ↔ ∃ (f : M ⟶ N), IsIrreducibleMorphism f

Between objects with local endomorphism rings, there is an arrow between their classes exactly when they admit an irreducible morphism.