Documentation

TauCeti.RepresentationTheory.Quiver.Representation.FiniteDimensional

Finite-dimensional quiver representations #

A representation of a quiver is pointwise finite-dimensional when the vector space it puts at every vertex is finite-dimensional. This file defines that property, TauCeti.IsFinDim, proves that it transports along an isomorphism, equips its full subcategory with an exact structure, proves essential smallness for a finite vertex set, and shows that a path algebra module finite-dimensional over the base field gives such a representation.

Main definitions #

Main results #

Implementation notes #

IsFinDim is stated vertex by vertex rather than as a single finiteness of the total space: the category of representations is a functor category, with no ambient module to be finite over, and over an infinite vertex set the two conditions genuinely differ. Over a finite quiver they agree, and that is the setting the theory is meant for.

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

Pointwise finite-dimensionality of a quiver representation: the vector space at every vertex is finite-dimensional. Over a finite quiver this is total finite-dimensionality, and it is the finiteness condition under which the indecomposables can be counted; the functor category itself contains infinite-dimensional objects.

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.isFinDim_iff {k : Type u} {Q : Type v} [Field k] [Quiver Q] {M : QuiverRep k Q} :
    IsFinDim k Q M ↔ ∀ (v : CategoryTheory.Paths Q), FiniteDimensional k ↑(M.obj v)

    The elimination and introduction rule for TauCeti.IsFinDim: it is finite-dimensionality at every vertex.

    source
    theorem TauCeti.IsFinDim.of_iso {k : Type u} {Q : Type v} [Field k] [Quiver Q] {M N : QuiverRep k Q} (h : IsFinDim k Q M) (e : M ≅ N) :
    IsFinDim k Q N

    Finite-dimensionality at each vertex transports along an isomorphism of representations.

    source
    theorem TauCeti.IsFinDim.of_mono {k : Type u} {Q : Type v} [Field k] [Quiver Q] {M N : QuiverRep k Q} (hM : IsFinDim k Q M) (f : N ⟶ M) [CategoryTheory.Mono f] :
    IsFinDim k Q N

    A subobject of a pointwise finite-dimensional representation is pointwise finite-dimensional. A monomorphism of representations is a monomorphism at every vertex, hence an injective linear map into a finite-dimensional space. The intended instance is a biproduct summand, CategoryTheory.Limits.biproduct.ι being a split monomorphism.

    source
    instance TauCeti.instIsClosedUnderIsomorphismsQuiverRepIsFinDim (k : Type u) (Q : Type v) [Field k] [Quiver Q] :
    CategoryTheory.ObjectProperty.IsClosedUnderIsomorphisms (IsFinDim k Q)

    Isomorphism closure makes pointwise finite-dimensionality a replete object property.

    source
    instance TauCeti.instContainsZeroQuiverRepIsFinDim (k : Type u) (Q : Type v) [Field k] [Quiver Q] :
    CategoryTheory.ObjectProperty.ContainsZero (IsFinDim k Q)

    The zero representation belongs to the finite-dimensional full subcategory.

    source
    theorem TauCeti.isExtensionClosed_pointwiseFiniteDimensionalQuiverRepresentations (k : Type u) (Q : Type v) [Field k] [Quiver Q] :
    (ExactStructure.abelian (QuiverRep k Q)).IsExtensionClosed (IsFinDim k Q)

    Pointwise finite-dimensional representations are closed under extensions.

    source
    instance TauCeti.instIsClosedUnderBinaryProductsQuiverRepIsFinDim (k : Type u) (Q : Type v) [Field k] [Quiver Q] :
    CategoryTheory.ObjectProperty.IsClosedUnderBinaryProducts (IsFinDim k Q)

    Binary products keep the finite-dimensional full subcategory additive, as required by its induced exact structure.

    source
    noncomputable def TauCeti.pointwiseFiniteDimensionalQuiverRepresentationsExactStructure (k : Type u) (Q : Type v) [Field k] [Quiver Q] :
    ExactStructure (CategoryTheory.ObjectProperty.FullSubcategory (IsFinDim k Q))

    The exact structure on pointwise finite-dimensional quiver representations.

    Equations
    Instances For
      source
      @[simp]
      theorem TauCeti.pointwiseFiniteDimensionalQuiverRepresentationsExactStructure_conflation_iff (k : Type u) (Q : Type v) [Field k] [Quiver Q] (S : CategoryTheory.ShortComplex (CategoryTheory.ObjectProperty.FullSubcategory (IsFinDim k Q))) :
      (pointwiseFiniteDimensionalQuiverRepresentationsExactStructure k Q).Conflation S ↔ (S.map (CategoryTheory.ObjectProperty.ι (IsFinDim k Q))).ShortExact

      Conflations of pointwise finite-dimensional quiver representations are exactly their short exact sequences in the ambient functor category.

      source
      theorem TauCeti.module_finite_asModule_of_isFinDim (k : Type u) (Q : Type v) [Field k] [Quiver Q] [Finite Q] [DecidableEq Q] (M : QuiverRep k Q) (hM : IsFinDim k Q M) :
      Module.Finite (pathAlgebra k Q) (QuiverRep.asModule k Q M)

      A pointwise finite-dimensional representation of a finite quiver gives a finite module over the path algebra under QuiverRep.asModule.

      source
      theorem TauCeti.module_finite_quiverRepEquivalenceFunctorObj_of_isFinDim (k : Type u) (Q : Type v) [Field k] [Quiver Q] [Finite Q] (M : QuiverRep k Q) (hM : IsFinDim k Q M) :
      Module.Finite k ↑((quiverRepEquivalence k Q).functor.obj M)

      A pointwise finite-dimensional representation of a finite quiver is carried to a finite-dimensional module by TauCeti.quiverRepEquivalence. That module is the direct sum of the vertex spaces, so finite-dimensionality at every vertex is finite-dimensionality of the module. Finite-dimensionality over k is what makes the module Artinian and Noetherian over kQ, by isArtinian_of_tower and isNoetherian_of_tower, and so is the route by which a theorem about modules of finite length reaches a finite-dimensional representation.

      source
      instance TauCeti.instEssentiallySmallFullSubcategoryQuiverRepIsFinDim (k : Type u) (Q : Type v) [Field k] [Quiver Q] [Finite Q] :
      CategoryTheory.EssentiallySmall.{max (max u v) w, max t v, max (max (max (t + 1) u) v) w} (CategoryTheory.ObjectProperty.FullSubcategory (IsFinDim k Q))

      Pointwise finite-dimensional representations of a finite quiver form an essentially small category, via their finitely generated modules over the path algebra.

      source
      theorem TauCeti.isFinDim_quiverRepFunctor_obj (k : Type u) (Q : Type v) [Field k] [Quiver Q] [Finite Q] (M : ModuleCat (pathAlgebra k Q)) (hM : FiniteDimensional k ↑M) :
      IsFinDim k Q ((quiverRepFunctor k Q).obj M)

      A path algebra module finite-dimensional over the base field gives a representation with finite-dimensional vertex spaces.