The representation of a quiver carried by a module over its path algebra

TauCeti.RepresentationTheory.Quiver.ModuleDecomposition equips a left module M over the path algebra kQ of a finite quiver with the data of a representation of Q: the k-subspace eᵥ M = TauCeti.vertexComponent k M v at each vertex, the k-linear map TauCeti.pathMap along each path, and the restriction TauCeti.vertexComponentMap of a kQ-linear map to those subspaces. This file assembles that data into an object and a morphism of TauCeti.QuiverRep k Q, bundles the assignment as a functor ModuleCat (kQ) ⥤ TauCeti.QuiverRep k Q, and proves that functor fully faithful.

Main definitions

• TauCeti.quiverRepOfModule k Q M: the representation v ↦ eᵥ M of Q carried by a kQ-module.
• TauCeti.quiverRepHomOfModule k Q f: the morphism of representations carried by a kQ-linear map.
• TauCeti.quiverRepHomComponent k Q φ v: the component at v of a morphism between two such representations, retyped as a map eᵥ M →ₗ[k] eᵥ N.
• TauCeti.moduleHomOfQuiverRepHom k Q φ: the kQ-linear map glued from those components, inverse to TauCeti.quiverRepHomOfModule.
• TauCeti.quiverRepFunctor k Q: the two previous assignments bundled as a functor ModuleCat (kQ) ⥤ TauCeti.QuiverRep k Q, and TauCeti.quiverRepFunctorFullyFaithful: its full faithfulness.

Main results

• TauCeti.dimVector_quiverRepOfModule: the dimension vector of quiverRepOfModule k Q M is v ↦ dimₖ (eᵥ M), and TauCeti.finrank_eq_sum_dimVector_quiverRepOfModule: over a finite-dimensional module its coordinates sum to dimₖ M.
• TauCeti.quiverRepHomOfModule_id and TauCeti.quiverRepHomOfModule_comp: the assignment is functorial.
• TauCeti.quiverRepHomOfModule_injective and TauCeti.quiverRepHomOfModule_moduleHomOfQuiverRepHom: it is injective and surjective on Hom-sets, packaged as TauCeti.quiverRepHomOfModule_bijective and, on the bundled functor, as TauCeti.quiverRepFunctorFullyFaithful. The inverse laws for the explicit inverse are that surjectivity statement together with TauCeti.moduleHomOfQuiverRepHom_quiverRepHomOfModule.
• The functor is additive and k-linear, so that on Hom-sets it is an isomorphism of k-vector spaces and not merely a bijection; that is what makes a dimension computed for representations also one for kQ-modules.

Implementation notes

Both the module and the resulting representation are described through the subspaces eᵥ M of M, not through an abstract direct-sum carrier; that is what makes TauCeti.vertexProjection and the identity ∑ᵥ eᵥ • x = x (TauCeti.sum_coe_vertexProjection), both from TauCeti.RepresentationTheory.Quiver.ModuleDecomposition, available, and those two carry the whole content of full faithfulness: injectivity is the fact that a kQ-linear map is determined by its restrictions to the components, and surjectivity glues the components of a morphism back together, the naturality in the paths being exactly what makes the glued map kQ-linear.

The vertex set is finite throughout, as it must be: the unit 1 = ∑ᵥ eᵥ of kQ is a finite sum of vertex idempotents, and without it a module is not the sum of its vertex components at all. It is carried as [Finite Q], refined to [Fintype Q] only where a sum over the vertices is genuinely in a statement; elsewhere Fintype.ofFinite supplies the enumeration a proof or a body needs. The base is a field only because TauCeti.QuiverRep is; the underlying data of TauCeti.RepresentationTheory.Quiver.ModuleDecomposition needs no more than a commutative semiring. The k-linear structure carried on M alongside the kQ-action is asked for as [Module k M] with [IsScalarTower k (pathAlgebra k Q) M], not extracted from the algebra, exactly as in that file. The three modules of the morphism section share one universe, since ModuleCat k — and hence TauCeti.QuiverRep k Q — has objects in a single universe. Those two hypotheses are what forces the source category of TauCeti.quiverRepFunctor to be spelled with the scoped instances ModuleCat.moduleOfAlgebraModule and ModuleCat.isScalarTower_of_algebra_moduleCat of Mathlib.Algebra.Category.ModuleCat.Algebra, which restrict the scalars of an object of ModuleCat (kQ) along algebraMap k (kQ); a file stating anything about that functor must open scoped ModuleCat for the same reason.

A representation is a functor out of CategoryTheory.Paths Q, whose objects are the vertices of Q only after unfolding the semireducible CategoryTheory.Paths. Two devices from the neighbouring files handle that: change Q at v restates a quantified object as a vertex, and the functorial equations of quiverRepOfModule are proved by first naming the intended identity with the vertex-indexed TauCeti.pathMap_nil and TauCeti.pathMap_comp, whose statements are then matched definitionally. The morphism-level API is stated on ModuleCat homomorphisms rather than on elements for the same reason: an element of (quiverRepOfModule k Q M).obj v is an element of eᵥ M only up to unfolding, so a coercion of it to M does not elaborate. That is what TauCeti.quiverRepHomComponent is for: it names the component of a morphism at the vertex-indexed type eᵥ M →ₗ[k] eᵥ N once and for all, and everything about the gluing is stated through it.

References

This is the fully faithful half of quiverRepEquivalence, Layer 1 of TauCetiRoadmap/RepresentationTheory/QuiverRepresentations/README.md, which asks for the equivalence "sending a module M to the representation v ↦ eᵥ M, with an arrow acting by left multiplication, and inverting through the idempotent decomposition M = ⨁ᵥ eᵥ M". Full faithfulness is proved here; the essential surjectivity that completes the equivalence — a kQ-module structure on ⨁ᵥ Mᵥ for a given representation — is TauCeti.RepresentationTheory.Quiver.Representation.AsModule, where the two halves are assembled into TauCeti.quiverRepEquivalence.

The equivalence itself is classical; see Assem--Simson--Skowroński, Elements of the Representation Theory of Associative Algebras I, Ch. III, or Schiffler, Quiver Representations, Ch. 5.

noncomputable def TauCeti.quiverRepOfModule (k : Type u) (Q : Type v) [Field k] [Quiver Q] [Finite Q] (M : Type t) [AddCommGroup M] [Module k M] [Module (pathAlgebra k Q) M] [IsScalarTower k (pathAlgebra k Q) M] : QuiverRep k Q

The representation of Q carried by a module over its path algebra: the vector space at a vertex v is the component eᵥ M, and a path acts by left multiplication, carrying the component at its source to the component at its target.

@[expose] is load-bearing rather than a leak: the statements of TauCeti.quiverRepOfModule_map and of TauCeti.quiverRepHomOfModule speak of maps between the objects (quiverRepOfModule k Q M).obj v, which only typecheck against ModuleCat.of k (eᵥ M) once this body is unfolded.

Equations

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

@[simp]

theorem TauCeti.quiverRepOfModule_obj (k : Type u) (Q : Type v) [Field k] [Quiver Q] [Finite Q] (M : Type t) [AddCommGroup M] [Module k M] [Module (pathAlgebra k Q) M] [IsScalarTower k (pathAlgebra k Q) M] (v : Q) : (quiverRepOfModule k Q M).obj v = ↧↥(vertexComponent k M v)

The vector space of quiverRepOfModule k Q M at a vertex is the component of M there.

@[simp]

theorem TauCeti.quiverRepOfModule_map (k : Type u) (Q : Type v) [Field k] [Quiver Q] [Finite Q] (M : Type t) [AddCommGroup M] [Module k M] [Module (pathAlgebra k Q) M] [IsScalarTower k (pathAlgebra k Q) M] {a b : Q} (p : Quiver.Path a b) : (quiverRepOfModule k Q M).map p = ModuleCat.ofHom (pathMap k M p)

A path acts on quiverRepOfModule k Q M by left multiplication.

theorem TauCeti.dimVector_quiverRepOfModule (k : Type u) (Q : Type v) [Field k] [Quiver Q] [Finite Q] (M : Type t) [AddCommGroup M] [Module k M] [Module (pathAlgebra k Q) M] [IsScalarTower k (pathAlgebra k Q) M] (v : Q) : dimVector (quiverRepOfModule k Q M) v = Module.finrank k ↥(vertexComponent k M v)

The dimension vector of the representation carried by a module is the vertexwise dimension of its components.

theorem TauCeti.finrank_eq_sum_dimVector_quiverRepOfModule (k : Type u) (Q : Type v) [Field k] [Quiver Q] [Finite Q] (M : Type t) [AddCommGroup M] [Module k M] [Module (pathAlgebra k Q) M] [IsScalarTower k (pathAlgebra k Q) M] [Fintype Q] [Module.Finite k M] : Module.finrank k M = ∑ v : Q, dimVector (quiverRepOfModule k Q M) v

The dimension vector of a finite-dimensional module sums to its dimension: this is TauCeti.finrank_eq_sum_finrank_vertexComponent read on the associated representation.

noncomputable def TauCeti.quiverRepHomOfModule (k : Type u) (Q : Type v) [Field k] [Quiver Q] [Finite Q] {M N : Type t} [AddCommGroup M] [Module k M] [Module (pathAlgebra k Q) M] [IsScalarTower k (pathAlgebra k Q) M] [AddCommGroup N] [Module k N] [Module (pathAlgebra k Q) N] [IsScalarTower k (pathAlgebra k Q) N] (f : M →ₗ[pathAlgebra k Q] N) : quiverRepOfModule k Q M ⟶ quiverRepOfModule k Q N

The morphism of representations carried by a kQ-linear map: at each vertex it is the restriction of the map to the components there, natural in the path by TauCeti.vertexComponentMap_comp_pathMap.

Equations

• TauCeti.quiverRepHomOfModule k Q f = { app := fun (v : CategoryTheory.Paths Q) => ModuleCat.ofHom (TauCeti.vertexComponentMap k f v), naturality := ⋯ }

@[simp]

theorem TauCeti.quiverRepHomOfModule_app (k : Type u) (Q : Type v) [Field k] [Quiver Q] [Finite Q] {M N : Type t} [AddCommGroup M] [Module k M] [Module (pathAlgebra k Q) M] [IsScalarTower k (pathAlgebra k Q) M] [AddCommGroup N] [Module k N] [Module (pathAlgebra k Q) N] [IsScalarTower k (pathAlgebra k Q) N] (f : M →ₗ[pathAlgebra k Q] N) (v : Q) : (quiverRepHomOfModule k Q f).app v = ModuleCat.ofHom (vertexComponentMap k f v)

@[simp]

theorem TauCeti.quiverRepHomOfModule_id (k : Type u) (Q : Type v) [Field k] [Quiver Q] [Finite Q] {M : Type t} [AddCommGroup M] [Module k M] [Module (pathAlgebra k Q) M] [IsScalarTower k (pathAlgebra k Q) M] : quiverRepHomOfModule k Q LinearMap.id = CategoryTheory.CategoryStruct.id (quiverRepOfModule k Q M)

The assignment is functorial: the identity map goes to the identity morphism.

@[simp]

theorem TauCeti.quiverRepHomOfModule_comp (k : Type u) (Q : Type v) [Field k] [Quiver Q] [Finite Q] {M N P : Type t} [AddCommGroup M] [Module k M] [Module (pathAlgebra k Q) M] [IsScalarTower k (pathAlgebra k Q) M] [AddCommGroup N] [Module k N] [Module (pathAlgebra k Q) N] [IsScalarTower k (pathAlgebra k Q) N] [AddCommGroup P] [Module k P] [Module (pathAlgebra k Q) P] [IsScalarTower k (pathAlgebra k Q) P] (f : M →ₗ[pathAlgebra k Q] N) (g : N →ₗ[pathAlgebra k Q] P) : quiverRepHomOfModule k Q (g ∘ₗ f) = CategoryTheory.CategoryStruct.comp (quiverRepHomOfModule k Q f) (quiverRepHomOfModule k Q g)

The assignment is functorial: a composite goes to the composite.

theorem TauCeti.quiverRepHomOfModule_injective (k : Type u) (Q : Type v) [Field k] [Quiver Q] [Finite Q] {M N : Type t} [AddCommGroup M] [Module k M] [Module (pathAlgebra k Q) M] [IsScalarTower k (pathAlgebra k Q) M] [AddCommGroup N] [Module k N] [Module (pathAlgebra k Q) N] [IsScalarTower k (pathAlgebra k Q) N] : Function.Injective (quiverRepHomOfModule k Q)

Faithfulness: a kQ-linear map is determined by the morphism of representations it carries, a module being the sum of its vertex components.

noncomputable def TauCeti.quiverRepHomComponent (k : Type u) (Q : Type v) [Field k] [Quiver Q] [Finite Q] {M N : Type t} [AddCommGroup M] [Module k M] [Module (pathAlgebra k Q) M] [IsScalarTower k (pathAlgebra k Q) M] [AddCommGroup N] [Module k N] [Module (pathAlgebra k Q) N] [IsScalarTower k (pathAlgebra k Q) N] (φ : quiverRepOfModule k Q M ⟶ quiverRepOfModule k Q N) (v : Q) : ↥(vertexComponent k M v) →ₗ[k] ↥(vertexComponent k N v)

The component at a vertex of a morphism between representations carried by modules, named at the vertex-indexed type eᵥ M →ₗ[k] eᵥ N. It is the component of φ as a ModuleCat homomorphism, retyped: that is what lets its values be spoken of as elements of eᵥ N, which the object type of TauCeti.quiverRepOfModule otherwise hides.

Equations

• TauCeti.quiverRepHomComponent k Q φ v = ModuleCat.Hom.hom (φ.app v)

theorem TauCeti.quiverRepHomComponent_comp_pathMap (k : Type u) (Q : Type v) [Field k] [Quiver Q] [Finite Q] {M N : Type t} [AddCommGroup M] [Module k M] [Module (pathAlgebra k Q) M] [IsScalarTower k (pathAlgebra k Q) M] [AddCommGroup N] [Module k N] [Module (pathAlgebra k Q) N] [IsScalarTower k (pathAlgebra k Q) N] (φ : quiverRepOfModule k Q M ⟶ quiverRepOfModule k Q N) {a b : Q} (p : Quiver.Path a b) : quiverRepHomComponent k Q φ b ∘ₗ pathMap k M p = pathMap k N p ∘ₗ quiverRepHomComponent k Q φ a

The components of a morphism commute with the action of a path. This is the naturality of φ, read at the vertex-indexed types.

@[simp]

theorem TauCeti.quiverRepHomComponent_quiverRepHomOfModule (k : Type u) (Q : Type v) [Field k] [Quiver Q] [Finite Q] {M N : Type t} [AddCommGroup M] [Module k M] [Module (pathAlgebra k Q) M] [IsScalarTower k (pathAlgebra k Q) M] [AddCommGroup N] [Module k N] [Module (pathAlgebra k Q) N] [IsScalarTower k (pathAlgebra k Q) N] (f : M →ₗ[pathAlgebra k Q] N) (v : Q) : quiverRepHomComponent k Q (quiverRepHomOfModule k Q f) v = vertexComponentMap k f v

The component of the morphism carried by a kQ-linear map is the restriction of that map.

noncomputable def TauCeti.moduleHomOfQuiverRepHom (k : Type u) (Q : Type v) [Field k] [Quiver Q] [Finite Q] {M N : Type t} [AddCommGroup M] [Module k M] [Module (pathAlgebra k Q) M] [IsScalarTower k (pathAlgebra k Q) M] [AddCommGroup N] [Module k N] [Module (pathAlgebra k Q) N] [IsScalarTower k (pathAlgebra k Q) N] (φ : quiverRepOfModule k Q M ⟶ quiverRepOfModule k Q N) : M →ₗ[pathAlgebra k Q] N

The kQ-linear map recovered from a morphism of the associated representations. It glues the components of φ along the decomposition M = ⨁ᵥ eᵥ M; the naturality of φ in the paths is exactly what makes the glued map commute with the action of the path algebra.

Only [Finite Q] is asked for: the gluing needs an enumeration of the vertices, but no sum over them occurs in the type, so Fintype.ofFinite supplies one in the body.

Equations

• TauCeti.moduleHomOfQuiverRepHom k Q φ = { toFun := ⇑(TauCeti.moduleHomAux✝ k Q φ), map_add' := ⋯, map_smul' := ⋯ }

theorem TauCeti.moduleHomOfQuiverRepHom_apply (k : Type u) (Q : Type v) [Field k] [Quiver Q] [Finite Q] {M N : Type t} [AddCommGroup M] [Module k M] [Module (pathAlgebra k Q) M] [IsScalarTower k (pathAlgebra k Q) M] [AddCommGroup N] [Module k N] [Module (pathAlgebra k Q) N] [IsScalarTower k (pathAlgebra k Q) N] [Fintype Q] (φ : quiverRepOfModule k Q M ⟶ quiverRepOfModule k Q N) (x : M) : (moduleHomOfQuiverRepHom k Q φ) x = ∑ v : Q, ↑((quiverRepHomComponent k Q φ v) ((vertexProjection k M v) x))

The recovered map, spelled out: glue the components of φ along the vertex projections.

theorem TauCeti.moduleHomOfQuiverRepHom_apply_of_mem (k : Type u) (Q : Type v) [Field k] [Quiver Q] [Finite Q] {M N : Type t} [AddCommGroup M] [Module k M] [Module (pathAlgebra k Q) M] [IsScalarTower k (pathAlgebra k Q) M] [AddCommGroup N] [Module k N] [Module (pathAlgebra k Q) N] [IsScalarTower k (pathAlgebra k Q) N] (φ : quiverRepOfModule k Q M ⟶ quiverRepOfModule k Q N) {v : Q} (x : ↥(vertexComponent k M v)) : (moduleHomOfQuiverRepHom k Q φ) ↑x = ↑((quiverRepHomComponent k Q φ v) x)

On a vertex component the recovered map is the component of φ there.

@[simp]

theorem TauCeti.quiverRepHomOfModule_moduleHomOfQuiverRepHom (k : Type u) (Q : Type v) [Field k] [Quiver Q] [Finite Q] {M N : Type t} [AddCommGroup M] [Module k M] [Module (pathAlgebra k Q) M] [IsScalarTower k (pathAlgebra k Q) M] [AddCommGroup N] [Module k N] [Module (pathAlgebra k Q) N] [IsScalarTower k (pathAlgebra k Q) N] (φ : quiverRepOfModule k Q M ⟶ quiverRepOfModule k Q N) : quiverRepHomOfModule k Q (moduleHomOfQuiverRepHom k Q φ) = φ

Fullness: every morphism of the associated representations is carried by a kQ-linear map, namely TauCeti.moduleHomOfQuiverRepHom.

@[simp]

theorem TauCeti.moduleHomOfQuiverRepHom_quiverRepHomOfModule (k : Type u) (Q : Type v) [Field k] [Quiver Q] [Finite Q] {M N : Type t} [AddCommGroup M] [Module k M] [Module (pathAlgebra k Q) M] [IsScalarTower k (pathAlgebra k Q) M] [AddCommGroup N] [Module k N] [Module (pathAlgebra k Q) N] [IsScalarTower k (pathAlgebra k Q) N] (f : M →ₗ[pathAlgebra k Q] N) : moduleHomOfQuiverRepHom k Q (quiverRepHomOfModule k Q f) = f

Faithfulness, in inverse form: gluing the components of the morphism carried by a kQ-linear map returns that map.

theorem TauCeti.exists_quiverRepHomOfModule_eq (k : Type u) (Q : Type v) [Field k] [Quiver Q] [Finite Q] {M N : Type t} [AddCommGroup M] [Module k M] [Module (pathAlgebra k Q) M] [IsScalarTower k (pathAlgebra k Q) M] [AddCommGroup N] [Module k N] [Module (pathAlgebra k Q) N] [IsScalarTower k (pathAlgebra k Q) N] (φ : quiverRepOfModule k Q M ⟶ quiverRepOfModule k Q N) : ∃ (f : M →ₗ[pathAlgebra k Q] N), quiverRepHomOfModule k Q f = φ

Fullness, in existential form.

theorem TauCeti.quiverRepHomOfModule_bijective (k : Type u) (Q : Type v) [Field k] [Quiver Q] [Finite Q] {M N : Type t} [AddCommGroup M] [Module k M] [Module (pathAlgebra k Q) M] [IsScalarTower k (pathAlgebra k Q) M] [AddCommGroup N] [Module k N] [Module (pathAlgebra k Q) N] [IsScalarTower k (pathAlgebra k Q) N] : Function.Bijective (quiverRepHomOfModule k Q)

Full faithfulness on a Hom-set: the kQ-linear maps M → N are exactly the morphisms quiverRepOfModule k Q M ⟶ quiverRepOfModule k Q N. With TauCeti.quiverRepHomOfModule_id and TauCeti.quiverRepHomOfModule_comp this is one half of the roadmap's quiverRepEquivalence; the other half is essential surjectivity.

noncomputable def TauCeti.quiverRepFunctor (k : Type u) (Q : Type v) [Field k] [Quiver Q] [Finite Q] : CategoryTheory.Functor (ModuleCat (pathAlgebra k Q)) (QuiverRep k Q)

The functor from kQ-modules to representations of Q: it carries a module to TauCeti.quiverRepOfModule and a kQ-linear map to TauCeti.quiverRepHomOfModule, the functoriality being TauCeti.quiverRepHomOfModule_id and TauCeti.quiverRepHomOfModule_comp. This is the module-to-representation half of the roadmap's quiverRepEquivalence, and TauCeti.quiverRepFunctorFullyFaithful is its full faithfulness.

@[expose] here is load-bearing for the same reason as on TauCeti.quiverRepOfModule: the statement of TauCeti.quiverRepFunctor_map speaks of a morphism between the objects (quiverRepFunctor k Q).obj M, which only typechecks against a morphism of TauCeti.quiverRepOfModule once this body is unfolded.

Equations

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

@[simp]

theorem TauCeti.quiverRepFunctor_obj (k : Type u) (Q : Type v) [Field k] [Quiver Q] [Finite Q] (M : ModuleCat (pathAlgebra k Q)) : (quiverRepFunctor k Q).obj M = quiverRepOfModule k Q ↑M

The functor carries a module to the representation it carries.

@[simp]

theorem TauCeti.quiverRepFunctor_map (k : Type u) (Q : Type v) [Field k] [Quiver Q] [Finite Q] {M N : ModuleCat (pathAlgebra k Q)} (f : M ⟶ N) : (quiverRepFunctor k Q).map f = quiverRepHomOfModule k Q (ModuleCat.Hom.hom f)

The functor carries a kQ-linear map to the morphism of representations it carries.

noncomputable def TauCeti.quiverRepFunctorFullyFaithful (k : Type u) (Q : Type v) [Field k] [Quiver Q] [Finite Q] : (quiverRepFunctor k Q).FullyFaithful

The functor from kQ-modules to representations of Q is fully faithful: this is TauCeti.quiverRepHomOfModule_bijective, with TauCeti.moduleHomOfQuiverRepHom as the explicit preimage. It is one half of the roadmap's quiverRepEquivalence; the other half is essential surjectivity, proved in TauCeti.RepresentationTheory.Quiver.Representation.AsModule.

Equations

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

instance TauCeti.instFullModuleCatPathAlgebraQuiverRepQuiverRepFunctor (k : Type u) (Q : Type v) [Field k] [Quiver Q] [Finite Q] : (quiverRepFunctor k Q).Full

instance TauCeti.instFaithfulModuleCatPathAlgebraQuiverRepQuiverRepFunctor (k : Type u) (Q : Type v) [Field k] [Quiver Q] [Finite Q] : (quiverRepFunctor k Q).Faithful

instance TauCeti.instAdditiveModuleCatPathAlgebraQuiverRepQuiverRepFunctor (k : Type u) (Q : Type v) [Field k] [Quiver Q] [Finite Q] : (quiverRepFunctor k Q).Additive

The functor is additive: a kQ-linear map restricts to the vertex components additively.

instance TauCeti.instLinearModuleCatPathAlgebraQuiverRepQuiverRepFunctor (k : Type u) (Q : Type v) [Field k] [Quiver Q] [Finite Q] : CategoryTheory.Functor.Linear k (quiverRepFunctor k Q)

The functor is k-linear: the vertex components of a kQ-module are k-subspaces, and restricting a kQ-linear map to them is k-linear in the map. This is what makes the functor compare k-dimensions of morphism spaces.