Irreducible morphisms

A morphism f : X ⟶ Y is irreducible when it is neither a split monomorphism nor a split epimorphism, and every factorization f = g ≫ h has g a split mono or h a split epi. So f admits no "genuine" intermediate object: any object Z it factors through contains X as a retract, split off by the first factor g : X ⟶ Z, or contains Y as a retract, split off by the second factor h : Z ⟶ Y.

Irreducible morphisms are what the arrows of the Auslander-Reiten quiver of a finite-dimensional algebra record. An arrow there is not an individual irreducible morphism: what governs the arrows from indecomposable finite-dimensional modules [X] to [Y] is the space of irreducible morphisms X ⟶ Y, the quotient rad(X, Y) / rad²(X, Y). This is a bimodule over the division rings End(Y) / rad End(Y) and End(X) / rad End(X). Over an algebraically closed field those division rings are the field itself, and then the arrows represent a basis, so their number is the dimension of that space; over a general field the quiver is a valued one, carrying the two one-sided dimensions of the bimodule instead. The components of the maps in an almost-split sequence, after decomposing the middle term into indecomposable summands, are irreducible morphisms. Nothing in the definition is special to modules, so this file develops the notion for an arbitrary category and specializes only where the statement forces it.

Main results

• TauCeti.IsIrreducibleMorphism: the definition, with TauCeti.isIrreducibleMorphism_iff spelling out its three clauses as the introduction and elimination rule.
• TauCeti.IsIrreducibleMorphism.not_isIso: an irreducible morphism is not an isomorphism.
• TauCeti.IsIrreducibleMorphism.comp_iso and TauCeti.IsIrreducibleMorphism.iso_comp, with the iff forms TauCeti.isIrreducibleMorphism_comp_iso_iff and TauCeti.isIrreducibleMorphism_iso_comp_iff: irreducibility only depends on the morphism up to isomorphisms of its source and target, so it descends to the arrows of a skeleton.
• TauCeti.not_isIrreducibleMorphism_zero: a zero morphism is never irreducible, and its consequence TauCeti.IsIrreducibleMorphism.ne_zero.
• TauCeti.IsIrreducibleMorphism.mono_or_epi: an irreducible morphism with an image whose factor map is epi is a monomorphism or an epimorphism, and by TauCeti.IsIrreducibleMorphism.not_mono_and_epi never both in a balanced category, so there, as in an abelian category, TauCeti.IsIrreducibleMorphism.mono_iff_not_epi is a genuine dichotomy.

The split-morphism cancellation lemmas include TauCeti.isSplitMono_of_isSplitMono_comp and TauCeti.isSplitEpi_of_isSplitEpi_comp.

Implementation notes

The definition is a conjunction; the three components are available as TauCeti.IsIrreducibleMorphism.not_isSplitMono, TauCeti.IsIrreducibleMorphism.not_isSplitEpi and TauCeti.IsIrreducibleMorphism.factors, so that no proof has to project through And by hand. The body of the definition is not exposed outside this module, so ⟨_, _, _⟩ is not available to establish it downstream; TauCeti.isIrreducibleMorphism_iff is the introduction rule.

The factorization property quantifies over all objects of the ambient category. In applications to finite-dimensional representations, choose the category of finite-dimensional representations as the ambient category. Irreducibility is inherited by a full subcategory containing the source and target, but irreducibility in that subcategory need not imply irreducibility in the larger category.

The dichotomy mono_or_epi is proved by feeding the image factorization f = e ≫ i to the definition: when e is epi, as it is in a category with equalizers, if it splits it is an isomorphism and f is mono; i is mono, so if it splits it is an isomorphism and f is epi.

References

• M. Auslander, I. Reiten, S. Smalø, Representation Theory of Artin Algebras, CUP (1995), V.5.
• 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.

Cancelling a split morphism off a composite

theorem TauCeti.isSplitMono_of_isSplitMono_comp {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [CategoryTheory.IsSplitMono (CategoryTheory.CategoryStruct.comp f g)] : CategoryTheory.IsSplitMono f

The first factor of a split monomorphism is a split monomorphism.

theorem TauCeti.isSplitEpi_of_isSplitEpi_comp {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [CategoryTheory.IsSplitEpi (CategoryTheory.CategoryStruct.comp f g)] : CategoryTheory.IsSplitEpi g

The second factor of a split epimorphism is a split epimorphism.

theorem TauCeti.isSplitEpi_of_isSplitEpi_comp_iso {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Y' : C} (f : X ⟶ Y) (e : Y ≅ Y') [CategoryTheory.IsSplitEpi (CategoryTheory.CategoryStruct.comp f e.hom)] : CategoryTheory.IsSplitEpi f

If postcomposition with an isomorphism is a split epimorphism, the original morphism is also a split epimorphism.

theorem TauCeti.isSplitMono_of_isSplitMono_iso_comp {C : Type u} [CategoryTheory.Category.{v, u} C] {X' X Y : C} (e : X' ≅ X) (f : X ⟶ Y) [CategoryTheory.IsSplitMono (CategoryTheory.CategoryStruct.comp e.hom f)] : CategoryTheory.IsSplitMono f

If precomposition with an isomorphism is a split monomorphism, the original morphism is also a split monomorphism.

Irreducible morphisms

def TauCeti.IsIrreducibleMorphism {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) : Prop

An irreducible morphism: one that is neither a split monomorphism nor a split epimorphism, and admits only split factorizations: in every factorization f = g ≫ h, either g is a split mono or h is a split epi.

The two negative clauses are what makes the notion nonvacuous: without them every isomorphism would qualify. With them, an irreducible morphism is in particular not an isomorphism (TauCeti.IsIrreducibleMorphism.not_isIso) and not zero (TauCeti.IsIrreducibleMorphism.ne_zero).

Equations

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

theorem TauCeti.isIrreducibleMorphism_iff {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y} : IsIrreducibleMorphism f ↔ ¬CategoryTheory.IsSplitMono f ∧ ¬CategoryTheory.IsSplitEpi f ∧ ∀ (Z : C) (g : X ⟶ Z) (h : Z ⟶ Y), CategoryTheory.CategoryStruct.comp g h = f → CategoryTheory.IsSplitMono g ∨ CategoryTheory.IsSplitEpi h

The three clauses of irreducibility, spelled out. This is both the introduction rule — the body of TauCeti.IsIrreducibleMorphism is not exposed outside this module, so ⟨_, _, _⟩ does not establish it there — and the elimination rule in a single statement; the individual components are also available as TauCeti.IsIrreducibleMorphism.not_isSplitMono, TauCeti.IsIrreducibleMorphism.not_isSplitEpi and TauCeti.IsIrreducibleMorphism.factors.

theorem TauCeti.IsIrreducibleMorphism.not_isSplitMono {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y} (hf : IsIrreducibleMorphism f) : ¬CategoryTheory.IsSplitMono f

An irreducible morphism is not a split monomorphism.

theorem TauCeti.IsIrreducibleMorphism.not_isSplitEpi {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y} (hf : IsIrreducibleMorphism f) : ¬CategoryTheory.IsSplitEpi f

An irreducible morphism is not a split epimorphism.

theorem TauCeti.IsIrreducibleMorphism.factors {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y} (hf : IsIrreducibleMorphism f) {Z : C} (g : X ⟶ Z) (h : Z ⟶ Y) (hgh : CategoryTheory.CategoryStruct.comp g h = f) : CategoryTheory.IsSplitMono g ∨ CategoryTheory.IsSplitEpi h

The factorization property. In any factorization of an irreducible morphism, the first factor is a split mono or the second is a split epi.

theorem TauCeti.IsIrreducibleMorphism.isSplitMono_of_not_isSplitEpi {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y} (hf : IsIrreducibleMorphism f) {Z : C} {g : X ⟶ Z} {h : Z ⟶ Y} (hgh : CategoryTheory.CategoryStruct.comp g h = f) (hh : ¬CategoryTheory.IsSplitEpi h) : CategoryTheory.IsSplitMono g

In a factorization of an irreducible morphism, if the second factor is not a split epimorphism, the first is a split monomorphism.

theorem TauCeti.IsIrreducibleMorphism.isSplitEpi_of_not_isSplitMono {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y} (hf : IsIrreducibleMorphism f) {Z : C} {g : X ⟶ Z} {h : Z ⟶ Y} (hgh : CategoryTheory.CategoryStruct.comp g h = f) (hg : ¬CategoryTheory.IsSplitMono g) : CategoryTheory.IsSplitEpi h

In a factorization of an irreducible morphism, if the first factor is not a split monomorphism, the second is a split epimorphism.

theorem TauCeti.IsIrreducibleMorphism.not_isIso {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y} (hf : IsIrreducibleMorphism f) : ¬CategoryTheory.IsIso f

An irreducible morphism is not an isomorphism.

@[simp]

theorem TauCeti.not_isIrreducibleMorphism_id {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) : ¬IsIrreducibleMorphism (CategoryTheory.CategoryStruct.id X)

An identity is not irreducible.

Invariance under isomorphisms of the source and the target

theorem TauCeti.IsIrreducibleMorphism.comp_iso {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y} (hf : IsIrreducibleMorphism f) {Y' : C} (e : Y ≅ Y') : IsIrreducibleMorphism (CategoryTheory.CategoryStruct.comp f e.hom)

Postcomposing an irreducible morphism with an isomorphism keeps it irreducible.

theorem TauCeti.IsIrreducibleMorphism.iso_comp {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y} (hf : IsIrreducibleMorphism f) {X' : C} (e : X' ≅ X) : IsIrreducibleMorphism (CategoryTheory.CategoryStruct.comp e.hom f)

Precomposing an irreducible morphism with an isomorphism keeps it irreducible.

@[simp]

theorem TauCeti.isIrreducibleMorphism_comp_iso_iff {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y} {Y' : C} (e : Y ≅ Y') : IsIrreducibleMorphism (CategoryTheory.CategoryStruct.comp f e.hom) ↔ IsIrreducibleMorphism f

Irreducibility is invariant under an isomorphism of the target.

@[simp]

theorem TauCeti.isIrreducibleMorphism_iso_comp_iff {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y} {X' : C} (e : X' ≅ X) : IsIrreducibleMorphism (CategoryTheory.CategoryStruct.comp e.hom f) ↔ IsIrreducibleMorphism f

Irreducibility is invariant under an isomorphism of the source.

Zero morphisms

@[simp]

theorem TauCeti.not_isIrreducibleMorphism_zero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (X Y : C) : ¬IsIrreducibleMorphism 0

A zero morphism is never irreducible, in any category with zero morphisms.

theorem TauCeti.IsIrreducibleMorphism.ne_zero {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y} [CategoryTheory.Limits.HasZeroMorphisms C] (hf : IsIrreducibleMorphism f) : f ≠ 0

An irreducible morphism is nonzero.

The monomorphism/epimorphism dichotomy

theorem TauCeti.IsIrreducibleMorphism.not_mono_and_epi {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y} [CategoryTheory.Balanced C] (hf : IsIrreducibleMorphism f) : ¬(CategoryTheory.Mono f ∧ CategoryTheory.Epi f)

An irreducible morphism of a balanced category is not both a monomorphism and an epimorphism.

theorem TauCeti.IsIrreducibleMorphism.mono_or_epi {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y} [CategoryTheory.Limits.HasImage f] [CategoryTheory.Epi (CategoryTheory.Limits.factorThruImage f)] (hf : IsIrreducibleMorphism f) : CategoryTheory.Mono f ∨ CategoryTheory.Epi f

An irreducible morphism with an image whose factor map is epi is a monomorphism or an epimorphism.

theorem TauCeti.IsIrreducibleMorphism.mono_iff_not_epi {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y} [CategoryTheory.Balanced C] [CategoryTheory.Limits.HasImage f] [CategoryTheory.Epi (CategoryTheory.Limits.factorThruImage f)] (hf : IsIrreducibleMorphism f) : CategoryTheory.Mono f ↔ ¬CategoryTheory.Epi f

An irreducible morphism in a balanced category with an image whose factor map is epi is a monomorphism exactly when it fails to be an epimorphism.

theorem TauCeti.IsIrreducibleMorphism.epi_iff_not_mono {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y} [CategoryTheory.Balanced C] [CategoryTheory.Limits.HasImage f] [CategoryTheory.Epi (CategoryTheory.Limits.factorThruImage f)] (hf : IsIrreducibleMorphism f) : CategoryTheory.Epi f ↔ ¬CategoryTheory.Mono f

An irreducible morphism in a balanced category with an image whose factor map is epi is an epimorphism exactly when it fails to be a monomorphism.