Documentation

TauCeti.RepresentationTheory.Quiver.FiniteRepType.Basic

Finite representation type #

A quiver has finite representation type when it has only finitely many isomorphism classes of finite-dimensional indecomposable representations. This file defines TauCeti.IsFiniteRepType, the finiteness of the skeleton of the full subcategory of finite-dimensional indecomposables, whose objects are the representations that are pointwise finite-dimensional (TauCeti.IsFinDim, from TauCeti.RepresentationTheory.Quiver.Representation.FiniteDimensional) and indecomposable; and it proves the criterion by which the property is refuted: an infinite family of pairwise non-isomorphic finite-dimensional indecomposables.

Both directions of that criterion are proved, because both are used. The refuting direction is what exhibits a quiver of infinite representation type; the affirming direction is what a quiver of finite representation type is for, namely that any family of pairwise non-isomorphic finite-dimensional indecomposables is finite, so that "the indecomposables" may be counted.

Main definitions #

Main results #

Implementation notes #

The definition does not carry [Finite Q]. The roadmap pins IsFiniteRepType with that instance binder, to record the intended setting, but nothing in the statement consumes it and an unused instance argument is a linter error here; a consumer that needs a finite vertex set -- Gabriel's dichotomy does -- states it where it is used. Dropping it costs nothing: the definition reads the same, and it stays meaningful over an infinite quiver.

The skeleton is Mathlib's CategoryTheory.Skeleton, so IsFiniteRepType is a finiteness statement about an honest type of isomorphism classes rather than about a hand-rolled quotient. The bridge in both proofs below is CategoryTheory.ObjectProperty.toSkeleton_eq_toSkeleton_iff_nonempty_iso, that two objects of a full subcategory have the same class in its skeleton exactly when they are isomorphic in the ambient category.

The two results are stated for a family M : α → QuiverRep k Q rather than for a set of representations: a family is what the worked examples produce -- the loop quiver's family is indexed by the base field -- and injectivity up to isomorphism is expressed directly on the index type.

References #

This implements the "finite representation type" item of Layer 5 of TauCetiRoadmap/RepresentationTheory/QuiverRepresentations/README.md, on which its Gabriel dichotomy and the loop-quiver and Kronecker worked examples are stated.

source
def TauCeti.IsFiniteRepType (k : Type u) (Q : Type v) [Field k] [Quiver Q] :
Prop

Finite representation type: the quiver Q has only finitely many isomorphism classes of finite-dimensional indecomposable representations over k. It is stated as the finiteness of the skeleton of the full subcategory they span, so that "isomorphism class" is Mathlib's.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem TauCeti.isFiniteRepType_iff {k : Type u} {Q : Type v} [Field k] [Quiver Q] :
    IsFiniteRepType k Q ↔ Finite (CategoryTheory.Skeleton (CategoryTheory.ObjectProperty.FullSubcategory fun (M : QuiverRep k Q) => IsFinDim k Q M ∧ CategoryTheory.Indecomposable M))

    The elimination and introduction rule for TauCeti.IsFiniteRepType: it is the finiteness of the skeleton of the full subcategory of finite-dimensional indecomposable representations.

    source
    theorem TauCeti.not_isFiniteRepType_of_infinite {k : Type u} {Q : Type v} [Field k] [Quiver Q] {α : Type u_1} {M : α → QuiverRep k Q} [Infinite α] (hfin : ∀ (a : α), IsFinDim k Q (M a)) (hind : ∀ (a : α), CategoryTheory.Indecomposable (M a)) (hne : ∀ (a b : α), a ≠ b → ¬Nonempty (M a ≅ M b)) :
    ¬IsFiniteRepType k Q

    An infinite family of pairwise non-isomorphic finite-dimensional indecomposables refutes finite representation type. This is how a quiver is shown to have infinite representation type: exhibit such a family.

    source
    theorem TauCeti.IsFiniteRepType.finite_of_pairwise_nonisomorphic {k : Type u} {Q : Type v} [Field k] [Quiver Q] {α : Type u_1} {M : α → QuiverRep k Q} (h : IsFiniteRepType k Q) (hfin : ∀ (a : α), IsFinDim k Q (M a)) (hind : ∀ (a : α), CategoryTheory.Indecomposable (M a)) (hne : ∀ (a b : α), a ≠ b → ¬Nonempty (M a ≅ M b)) :
    Finite α

    Under finite representation type a family of pairwise non-isomorphic finite-dimensional indecomposables is finite. This is the counting form of the property: only finitely many indecomposables are available to be listed.