The space of irreducible morphisms of a linear category

Between two objects X and Y of a k-linear category with binary biproducts and local endomorphism rings, the morphisms lying in the radical but not in its square are exactly the irreducible ones (TauCeti.isIrreducibleMorphism_iff_mem_jacobsonRadical_and_notMem_jacobsonRadicalSq). Under those hypotheses the quotient rad(X, Y) / rad²(X, Y) is therefore the k-module whose nonzero classes are the irreducible morphisms X ⟶ Y, and it is the space the arrows X → Y of the Auslander-Reiten quiver are read off from. This file builds that quotient, TauCeti.irreducibleMorphismSpace k X Y, on top of the two submodules supplied by TauCeti.CategoryTheory.Preadditive.Radical.Basic.

The three things the Auslander-Reiten quiver needs of it are here. First, the detection statement: a class is nonzero exactly when the morphism representing it is irreducible, so the space is nontrivial exactly when an irreducible morphism X ⟶ Y exists — that is what makes "there is an arrow X → Y" mean "there is an irreducible morphism X ⟶ Y". Second, isomorphism invariance: conjugating by isomorphisms X ≅ X' and Y ≅ Y' induces a k-linear equivalence Irr(X, Y) ≃ₗ[k] Irr(X', Y'), functorially, which is what lets the arrows be indexed by isomorphism classes of indecomposables. Third, finite-dimensionality over a division ring whenever the ambient morphism space is finite-dimensional, which is what makes the quiver locally finite.

The detection statement is the only one that constrains the objects: it needs the two endomorphism rings to be local (the indecomposables of a Krull-Schmidt category) and the category to have binary biproducts, exactly as its input in Radical.Basic does. The construction of the quotient and its linear structure need none of that, so they are stated for an arbitrary k-linear category over a ring k.

What is not built here is the bimodule structure of Irr(X, Y) over the residue division rings End X / rad(End X) and End Y / rad(End Y). It is the dimensions over those rings, not the k-dimension computed below, that count the arrows X → Y of the Auslander-Reiten quiver; the two counts do agree whenever both residue division rings are k itself, as happens for instance over an algebraically closed k when the two endomorphism algebras are finite-dimensional over it, but that is only a sufficient condition — they also agree, vacuously, whenever Irr(X, Y) vanishes. So no statement below claims to compute an arrow multiplicity: what is proved is the k-dimension, its bound by finrank k (X ⟶ Y), and its positivity exactly when an irreducible morphism exists.

Main definitions

• TauCeti.irreducibleMorphismSpace k X Y: the space rad(X, Y) / rad²(X, Y) of irreducible morphisms, a k-module.
• TauCeti.irreducibleMorphismMk: the class of a radical morphism, as a k-linear map.
• TauCeti.irreducibleMorphismLift: the universal property, a k-linear map out of the space from one on radical morphisms that kills the square of the radical, unique with its values by TauCeti.irreducibleMorphismSpace_linearMap_ext.
• TauCeti.irreducibleMorphismSpaceCongr: the k-linear equivalence induced by a pair of isomorphisms of the source and the target.

Main results

• TauCeti.irreducibleMorphismMk_eq_zero_iff: a class vanishes exactly when its representative lies in the square of the radical, and TauCeti.irreducibleMorphismMk_eq_iff the corresponding criterion for two classes to agree.
• TauCeti.irreducibleMorphismSpace_linearMap_ext: the uniqueness half of the universal property — a k-linear map out of the space is determined by its values on classes of radical morphisms.
• TauCeti.irreducibleMorphismMk_ne_zero_iff: the detection statement — between objects with local endomorphism rings a class is nonzero exactly when its representative is an irreducible morphism.
• TauCeti.nontrivial_irreducibleMorphismSpace_iff and TauCeti.subsingleton_irreducibleMorphismSpace_iff: the space is nontrivial exactly when an irreducible morphism exists, and vanishes exactly when none does.
• TauCeti.irreducibleMorphismSpaceCongr_refl, TauCeti.irreducibleMorphismSpaceCongr_trans and TauCeti.irreducibleMorphismSpaceCongr_symm: the invariance is functorial in the two isomorphisms.
• TauCeti.exists_isIrreducibleMorphism_irreducibleMorphismMk_eq: every nonzero class is represented by an irreducible morphism.
• TauCeti.finrank_irreducibleMorphismSpace_le: over a division ring the space is no larger than the morphism space it is carved out of, and TauCeti.finrank_irreducibleMorphismSpace_pos_iff that its dimension is positive exactly when an irreducible morphism X ⟶ Y exists.

Implementation notes

The quotient is formed inside the submodule rad(X, Y), so its elements are classes of elements of the subtype ↥(jacobsonRadicalSubmodule k X Y); every statement below is therefore phrased with the underlying morphism (f : X ⟶ Y) of such an element, so that a caller never has to see the subtype's own submodule, which is private. The alternative, quotienting the whole morphism space by rad², is a different module — it has the non-radical morphisms in it as well — and is not what an arrow of the Auslander-Reiten quiver counts.

TauCeti.irreducibleMorphismSpace is a plain def rather than an abbreviation, with its additive and k-module structures transported by inferInstanceAs, so that the quotient is not unfolded by simp in goals that mention it. Its body is not exposed, and the submodule it divides by is private, so that no caller depends on the subtype-quotient representation: the API below stands in for Mathlib's quotient operations, with TauCeti.irreducibleMorphismMk for Submodule.Quotient.mk, TauCeti.irreducibleMorphismMk_surjective for quotient induction, TauCeti.irreducibleMorphismLift for Submodule.liftQ and TauCeti.irreducibleMorphismSpace_linearMap_ext for Submodule.linearMap_qext.

Conjugation by a pair of isomorphisms needs no quotient theory, so the equivalence of radicals it induces, TauCeti.jacobsonRadicalSubmoduleCongr, lives with the radical itself in TauCeti.CategoryTheory.Preadditive.Radical.Basic; the induced equivalence of quotients built here is Mathlib's Submodule.Quotient.equiv applied to it.

References

• M. Auslander, I. Reiten, S. Smalø, Representation Theory of Artin Algebras, CUP (1995), V.7 and VII.1, where rad / rad² is introduced as the space the arrows of the Auslander-Reiten quiver are counted by.
• I. Assem, D. Simson, A. Skowroński, Elements of the Representation Theory of Associative Algebras, Vol. 1, LMS Student Texts 65, CUP (2006), IV.1 and VII.1.

The quotient rad / rad²

def TauCeti.irreducibleMorphismSpace {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (k : Type u_1) [Ring k] [CategoryTheory.Linear k C] (X Y : C) : Type v

The space of irreducible morphisms X ⟶ Y, the quotient rad(X, Y) / rad²(X, Y).

In a category with binary biproducts, between objects with local endomorphism rings, its nonzero classes are exactly the irreducible morphisms (TauCeti.irreducibleMorphismMk_ne_zero_iff); it is the space the arrows X → Y of the Auslander-Reiten quiver are read off from.

Equations

• TauCeti.irreducibleMorphismSpace k X Y = (↥(TauCeti.jacobsonRadicalSubmodule k X Y) ⧸ TauCeti.jacobsonRadicalSqSubmoduleIn✝ k X Y)

@[instance_reducible]

instance TauCeti.instAddCommGroupIrreducibleMorphismSpace {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (k : Type u_1) [Ring k] [CategoryTheory.Linear k C] (X Y : C) : AddCommGroup (irreducibleMorphismSpace k X Y)

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance TauCeti.instModuleIrreducibleMorphismSpace {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (k : Type u_1) [Ring k] [CategoryTheory.Linear k C] (X Y : C) : Module k (irreducibleMorphismSpace k X Y)

Equations

• One or more equations did not get rendered due to their size.

def TauCeti.irreducibleMorphismMk {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (k : Type u_1) [Ring k] [CategoryTheory.Linear k C] (X Y : C) : ↥(jacobsonRadicalSubmodule k X Y) →ₗ[k] irreducibleMorphismSpace k X Y

The class of a radical morphism in the space of irreducible morphisms, as a k-linear map.

Equations

• TauCeti.irreducibleMorphismMk k X Y = (TauCeti.jacobsonRadicalSqSubmoduleIn✝ k X Y).mkQ

theorem TauCeti.irreducibleMorphismMk_surjective {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {k : Type u_1} [Ring k] [CategoryTheory.Linear k C] {X Y : C} : Function.Surjective ⇑(irreducibleMorphismMk k X Y)

Every element of the space of irreducible morphisms is the class of a radical morphism. This is the induction principle for the space: obtain ⟨f, rfl⟩ := irreducibleMorphismMk_surjective x replaces an element by the class of a radical morphism.

@[simp]

theorem TauCeti.irreducibleMorphismMk_eq_zero_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {k : Type u_1} [Ring k] [CategoryTheory.Linear k C] {X Y : C} {f : ↥(jacobsonRadicalSubmodule k X Y)} : (irreducibleMorphismMk k X Y) f = 0 ↔ ↑f ∈ jacobsonRadicalSq X Y

A class vanishes exactly when its representative lies in the square of the radical.

@[simp]

theorem TauCeti.irreducibleMorphismMk_eq_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {k : Type u_1} [Ring k] [CategoryTheory.Linear k C] {X Y : C} {f g : ↥(jacobsonRadicalSubmodule k X Y)} : (irreducibleMorphismMk k X Y) f = (irreducibleMorphismMk k X Y) g ↔ ↑f - ↑g ∈ jacobsonRadicalSq X Y

Two radical morphisms have the same class exactly when they differ by an element of the square of the radical.

def TauCeti.irreducibleMorphismLift {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {k : Type u_1} [Ring k] [CategoryTheory.Linear k C] {X Y : C} {M : Type u_2} [AddCommGroup M] [Module k M] (g : ↥(jacobsonRadicalSubmodule k X Y) →ₗ[k] M) (hg : ∀ (f : ↥(jacobsonRadicalSubmodule k X Y)), ↑f ∈ jacobsonRadicalSq X Y → g f = 0) : irreducibleMorphismSpace k X Y →ₗ[k] M

The universal property of the space of irreducible morphisms: a k-linear map on radical morphisms that vanishes on the square of the radical descends to the quotient. Together with TauCeti.irreducibleMorphismLift_irreducibleMorphismMk and TauCeti.irreducibleMorphismMk_surjective this is how a map out of TauCeti.irreducibleMorphismSpace is built and computed with.

Equations

• TauCeti.irreducibleMorphismLift g hg = (TauCeti.jacobsonRadicalSqSubmoduleIn✝ k X Y).liftQ g ⋯

@[simp]

theorem TauCeti.irreducibleMorphismLift_irreducibleMorphismMk {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {k : Type u_1} [Ring k] [CategoryTheory.Linear k C] {X Y : C} {M : Type u_2} [AddCommGroup M] [Module k M] (g : ↥(jacobsonRadicalSubmodule k X Y) →ₗ[k] M) (hg : ∀ (f : ↥(jacobsonRadicalSubmodule k X Y)), ↑f ∈ jacobsonRadicalSq X Y → g f = 0) (f : ↥(jacobsonRadicalSubmodule k X Y)) : (irreducibleMorphismLift g hg) ((irreducibleMorphismMk k X Y) f) = g f

The map descending a k-linear map along TauCeti.irreducibleMorphismMk is the map itself.

theorem TauCeti.irreducibleMorphismSpace_linearMap_ext {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {k : Type u_1} [Ring k] [CategoryTheory.Linear k C] {X Y : C} {M : Type u_2} [AddCommGroup M] [Module k M] ⦃g₁ g₂ : irreducibleMorphismSpace k X Y →ₗ[k] M⦄ (h : ∀ (f : ↥(jacobsonRadicalSubmodule k X Y)), g₁ ((irreducibleMorphismMk k X Y) f) = g₂ ((irreducibleMorphismMk k X Y) f)) : g₁ = g₂

A k-linear map out of the space of irreducible morphisms is determined by its values on classes of radical morphisms. This is the uniqueness half of the universal property, so that TauCeti.irreducibleMorphismLift is the only map with the values TauCeti.irreducibleMorphismLift_irreducibleMorphismMk gives it.

theorem TauCeti.irreducibleMorphismSpace_linearMap_ext_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {k : Type u_1} [Ring k] [CategoryTheory.Linear k C] {X Y : C} {M : Type u_2} [AddCommGroup M] [Module k M] {g₁ g₂ : irreducibleMorphismSpace k X Y →ₗ[k] M} : g₁ = g₂ ↔ ∀ (f : ↥(jacobsonRadicalSubmodule k X Y)), g₁ ((irreducibleMorphismMk k X Y) f) = g₂ ((irreducibleMorphismMk k X Y) f)

Detection of irreducible morphisms

theorem TauCeti.irreducibleMorphismMk_ne_zero_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {k : Type u_1} [Ring k] [CategoryTheory.Linear k C] [CategoryTheory.Limits.HasBinaryBiproducts C] {X Y : C} [IsLocalRing (CategoryTheory.End X)] [IsLocalRing (CategoryTheory.End Y)] {f : ↥(jacobsonRadicalSubmodule k X Y)} : (irreducibleMorphismMk k X Y) f ≠ 0 ↔ IsIrreducibleMorphism ↑f

The nonzero classes are the irreducible morphisms. In a category with binary biproducts, between objects with local endomorphism rings, a radical morphism is irreducible exactly when it is not a composite of two radical morphisms (TauCeti.isIrreducibleMorphism_iff_mem_jacobsonRadical_and_notMem_jacobsonRadicalSq), which is exactly the nonvanishing of its class. This is the sense in which TauCeti.irreducibleMorphismSpace is the space of irreducible morphisms.

theorem TauCeti.nontrivial_irreducibleMorphismSpace_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {k : Type u_1} [Ring k] [CategoryTheory.Linear k C] [CategoryTheory.Limits.HasBinaryBiproducts C] {X Y : C} [IsLocalRing (CategoryTheory.End X)] [IsLocalRing (CategoryTheory.End Y)] : Nontrivial (irreducibleMorphismSpace k X Y) ↔ ∃ (f : X ⟶ Y), IsIrreducibleMorphism f

The space of irreducible morphisms is nontrivial exactly when an irreducible morphism exists, in a category with binary biproducts and between objects with local endomorphism rings. This is what makes "there is an arrow X → Y in the Auslander-Reiten quiver" and "there is an irreducible morphism X ⟶ Y" the same statement.

theorem TauCeti.exists_isIrreducibleMorphism_irreducibleMorphismMk_eq {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {k : Type u_1} [Ring k] [CategoryTheory.Linear k C] [CategoryTheory.Limits.HasBinaryBiproducts C] {X Y : C} [IsLocalRing (CategoryTheory.End X)] [IsLocalRing (CategoryTheory.End Y)] {x : irreducibleMorphismSpace k X Y} (hx : x ≠ 0) : ∃ (f : ↥(jacobsonRadicalSubmodule k X Y)), IsIrreducibleMorphism ↑f ∧ (irreducibleMorphismMk k X Y) f = x

Every nonzero class is represented by an irreducible morphism, in a category with binary biproducts and between objects with local endomorphism rings. Together with TauCeti.irreducibleMorphismMk_surjective this says that the irreducible morphisms X ⟶ Y exhaust the nonzero elements of TauCeti.irreducibleMorphismSpace k X Y.

theorem TauCeti.subsingleton_irreducibleMorphismSpace_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {k : Type u_1} [Ring k] [CategoryTheory.Linear k C] [CategoryTheory.Limits.HasBinaryBiproducts C] {X Y : C} [IsLocalRing (CategoryTheory.End X)] [IsLocalRing (CategoryTheory.End Y)] : Subsingleton (irreducibleMorphismSpace k X Y) ↔ ∀ (f : X ⟶ Y), ¬IsIrreducibleMorphism f

The space of irreducible morphisms vanishes exactly when there is no irreducible morphism, under the same hypotheses of binary biproducts and local endomorphism rings: the contrapositive form of TauCeti.nontrivial_irreducibleMorphismSpace_iff.

Invariance of the quotient under isomorphism

noncomputable def TauCeti.irreducibleMorphismSpaceCongr {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (k : Type u_1) [Ring k] [CategoryTheory.Linear k C] {X X' Y Y' : C} (e : X ≅ X') (e' : Y ≅ Y') : irreducibleMorphismSpace k X Y ≃ₗ[k] irreducibleMorphismSpace k X' Y'

The space of irreducible morphisms depends only on the isomorphism classes of its two objects: a pair of isomorphisms X ≅ X' and Y ≅ Y' induces a k-linear equivalence Irr(X, Y) ≃ₗ[k] Irr(X', Y'). This is what lets the arrows of the Auslander-Reiten quiver be indexed by isomorphism classes of indecomposables rather than by objects.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.irreducibleMorphismSpaceCongr_mk {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (k : Type u_1) [Ring k] [CategoryTheory.Linear k C] {X X' Y Y' : C} (e : X ≅ X') (e' : Y ≅ Y') (f : ↥(jacobsonRadicalSubmodule k X Y)) : (irreducibleMorphismSpaceCongr k e e') ((irreducibleMorphismMk k X Y) f) = (irreducibleMorphismMk k X' Y') ((jacobsonRadicalSubmoduleCongr k e e') f)

Conjugation of the quotient is computed on representatives: the image of the class of a radical morphism f is the class of its conjugate TauCeti.jacobsonRadicalSubmoduleCongr k e e' f.

@[simp]

theorem TauCeti.irreducibleMorphismSpaceCongr_refl {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (k : Type u_1) [Ring k] [CategoryTheory.Linear k C] (X Y : C) : irreducibleMorphismSpaceCongr k (CategoryTheory.Iso.refl X) (CategoryTheory.Iso.refl Y) = LinearEquiv.refl k (irreducibleMorphismSpace k X Y)

Conjugating by the identity isomorphisms does nothing.

@[simp]

theorem TauCeti.irreducibleMorphismSpaceCongr_trans {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (k : Type u_1) [Ring k] [CategoryTheory.Linear k C] {X X' Y Y' X'' Y'' : C} (e : X ≅ X') (e' : Y ≅ Y') (d : X' ≅ X'') (d' : Y' ≅ Y'') : irreducibleMorphismSpaceCongr k e e' ≪≫ₗ irreducibleMorphismSpaceCongr k d d' = irreducibleMorphismSpaceCongr k (e ≪≫ d) (e' ≪≫ d')

Conjugating by a composite of isomorphisms is conjugating twice.

@[simp]

theorem TauCeti.irreducibleMorphismSpaceCongr_symm {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (k : Type u_1) [Ring k] [CategoryTheory.Linear k C] {X X' Y Y' : C} (e : X ≅ X') (e' : Y ≅ Y') : (irreducibleMorphismSpaceCongr k e e').symm = irreducibleMorphismSpaceCongr k e.symm e'.symm

The inverse of conjugating by a pair of isomorphisms is conjugating by the inverse pair.

Finite-dimensionality

instance TauCeti.instFiniteDimensionalIrreducibleMorphismSpaceOfHom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (k : Type u_1) [DivisionRing k] [CategoryTheory.Linear k C] (X Y : C) [FiniteDimensional k (X ⟶ Y)] : FiniteDimensional k (irreducibleMorphismSpace k X Y)

theorem TauCeti.finrank_irreducibleMorphismSpace_le {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (k : Type u_1) [DivisionRing k] [CategoryTheory.Linear k C] (X Y : C) [FiniteDimensional k (X ⟶ Y)] : Module.finrank k (irreducibleMorphismSpace k X Y) ≤ Module.finrank k (X ⟶ Y)

The space of irreducible morphisms is no larger than the morphism space it is carved out of. This is the bound that makes the Auslander-Reiten quiver of a category with finite-dimensional morphism spaces locally finite. Finite-dimensionality of X ⟶ Y is a genuine hypothesis and not merely a convenience: without it the right-hand side is 0 by the convention for Module.finrank, while the quotient can perfectly well be finite-dimensional and nonzero.

theorem TauCeti.finrank_irreducibleMorphismSpace_pos_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (k : Type u_1) [DivisionRing k] [CategoryTheory.Linear k C] (X Y : C) [FiniteDimensional k (irreducibleMorphismSpace k X Y)] [CategoryTheory.Limits.HasBinaryBiproducts C] [IsLocalRing (CategoryTheory.End X)] [IsLocalRing (CategoryTheory.End Y)] : 0 < Module.finrank k (irreducibleMorphismSpace k X Y) ↔ ∃ (f : X ⟶ Y), IsIrreducibleMorphism f

The dimension of the space of irreducible morphisms is positive exactly when there is an irreducible morphism X ⟶ Y, in a category with binary biproducts and between objects with local endomorphism rings: the dimension count of TauCeti.nontrivial_irreducibleMorphismSpace_iff. Only the quotient itself has to be finite-dimensional here, which the instance above supplies whenever X ⟶ Y is.