Documentation

TauCeti.Algebra.Category.ModuleCat.RepresentationFinite

Representation-finite rings #

A ring A is representation-finite (TauCeti.IsRepresentationFinite) if it has only finitely many isomorphism classes of finitely generated indecomposable modules. As for quivers (TauCeti.IsFiniteRepType), this is stated as the finiteness of the skeleton of the full subcategory these modules span, so that "isomorphism class" is Mathlib's. The modules are taken in a universe w, which is a parameter of the predicate.

The predicate is used for the module category of a finite-dimensional algebra, where it says that the quiver of irreducible morphisms has finitely many vertices (TauCeti.IrreducibleMorphismQuiver.finite_iff_isRepresentationFinite), and for path algebras, where it agrees with finite representation type of the quiver (TauCeti.isFiniteRepType_iff_isRepresentationFinite_pathAlgebra).

References #

source
def TauCeti.IsRepresentationFinite (A : Type v) [Ring A] :
Prop

Representation-finite rings: A has only finitely many isomorphism classes of finitely generated indecomposable modules (in the universe w). It is stated as the finiteness of the skeleton of the full subcategory they span.

Instances For
    source
    @[simp]
    theorem TauCeti.isRepresentationFinite_iff (A : Type v) [Ring A] :
    IsRepresentationFinite A ↔ Finite (CategoryTheory.Skeleton (CategoryTheory.ObjectProperty.FullSubcategory fun (M : ModuleCat A) => Module.Finite A ↑M ∧ CategoryTheory.Indecomposable M))

    Unfolding TauCeti.IsRepresentationFinite in modules where its body is not exposed.

    source
    theorem TauCeti.isRepresentationFinite_of_forall_exists_iso {A : Type v} [Ring A] {S : Set (ModuleCat A)} (hS : S.Finite) (h : ∀ (M : ModuleCat A), Module.Finite A ↑M → CategoryTheory.Indecomposable M → ∃ Q ∈ S, Nonempty (M ≅ Q)) :
    IsRepresentationFinite A

    A ring is representation-finite as soon as every finitely generated indecomposable module is isomorphic to a member of a fixed finite set of modules.