A module over a path algebra is a representation of the quiver

A left module M over the path algebra kQ of a finite quiver carries one k-subspace for each vertex, Mᵥ = eᵥ M, and one k-linear map for each path, the action of that path. This file builds that data and proves the three facts that make it a representation of Q:

• the vertex subspaces are an internal direct sum, M = ⨁ᵥ eᵥ M (TauCeti.isInternal_vertexComponent);
• a path from a to b carries Mₐ into M_b and annihilates every other vertex subspace (TauCeti.ofPath_smul_mem_vertexComponent, TauCeti.ofPath_smul_eq_zero_of_ne_of_mem_vertexComponent);
• the resulting maps are functorial in the path (TauCeti.pathMap_nil, TauCeti.pathMap_comp) and in the module (TauCeti.vertexComponentMap_id, TauCeti.vertexComponentMap_comp), the two being compatible (TauCeti.vertexComponentMap_comp_pathMap).

This is the direction "module ↦ representation" of the equivalence between representations of Q and left kQ-modules; the vertex idempotents are what makes it work, and the finiteness of the vertex set is load-bearing, being what makes ∑ᵥ eᵥ = 1 a finite sum and kQ unital.

The orientation is fixed by the later factor first product of TauCeti.pathAlgebra: with it, e_b · p = p and p · eₐ = p for a path p from a to b, so left multiplication by p sends the component at the source to the component at the target, and the representations obtained here are the covariant ones. Reversing the product would transpose every statement below.

Implementation notes

Only the underlying data and its functoriality are built here: no object of TauCeti.QuiverRep k Q (Paths Q ⥤ ModuleCat k, in TauCeti.RepresentationTheory.Quiver.Representation.Basic) and no functor into it is assembled, and TauCeti.dimVector is not used. Two things are missing for that. First, QuiverRep is stated over a Field k while everything below needs only a CommSemiring k, so assembling the functor here would either restrict the results or duplicate them. Second, the assembly is the roadmap target quiverRepEquivalence itself, of which this file is the object-and-morphism half.

Main definitions

• TauCeti.vertexComponent k M v: the k-subspace eᵥ M of a kQ-module M.
• TauCeti.pathMap k M p: the k-linear map Mₐ → M_b given by the action of a path p from a to b.
• TauCeti.vertexComponentMap k f v: the restriction of a kQ-linear map to the components at v.
• TauCeti.vertexProjection k M v: the projection x ↦ eᵥ • x of M onto its component at v, the decomposition M = ⨁ᵥ eᵥ M read one vertex at a time.

Main results

• TauCeti.sum_coe_vertexProjection: the vertex projections of x sum back to x, the vertex idempotents summing to 1.
• TauCeti.isInternal_vertexComponent: M = ⨁ᵥ eᵥ M, with TauCeti.coe_ofBijective_coeLinearMap_symm_apply_vertexComponent reading off the component of x at v as eᵥ • x.
• TauCeti.finrank_eq_sum_finrank_vertexComponent: for a kQ-module finite-dimensional over a field k, the dimension of M is the sum of the dimensions of the vertex subspaces — the total dimension read off the dimension vector.
• TauCeti.pathMap_nil and TauCeti.pathMap_comp: the path maps are functorial, the trivial path acting as the identity and a concatenation as the composite.
• TauCeti.vertexComponentMap_comp_pathMap: the path maps are natural in the module.

References

Layer 1 of TauCetiRoadmap/RepresentationTheory/QuiverRepresentations/README.md, whose quiverRepEquivalence "sends a module M to the representation v ↦ eᵥ M, with an arrow acting by left multiplication, and inverts through the idempotent decomposition M = ⨁ᵥ eᵥ M (available because ∑ᵥ eᵥ = 1, hence the finiteness of the vertex set is load-bearing here)".

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.vertexComponent (k : Type w) {Q : Type u} [CommSemiring k] [Quiver Q] [Finite Q] (M : Type u_1) [AddCommMonoid M] [Module k M] [Module (pathAlgebra k Q) M] [IsScalarTower k (pathAlgebra k Q) M] (v : Q) : Submodule k M

The vertex component eᵥ M of a module over the path algebra: the k-subspace on which the vertex idempotent at v acts as the identity. It is the value at v of the representation of Q attached to M.

Equations

• TauCeti.vertexComponent k M v = TauCeti.PathAlgebra.vertexIdempotent k v • ⊤

theorem TauCeti.vertexComponent_def (k : Type w) {Q : Type u} [CommSemiring k] [Quiver Q] [Finite Q] (M : Type u_1) [AddCommMonoid M] [Module k M] [Module (pathAlgebra k Q) M] [IsScalarTower k (pathAlgebra k Q) M] (v : Q) : vertexComponent k M v = PathAlgebra.vertexIdempotent k v • ⊤

The defining equation of the vertex component: it is the piece eᵥ • (⊤ : Submodule k M) cut out by the vertex idempotent. This is the bridge to the general theory: through it both Mathlib's pointwise API and the general lemmas about such a piece — IsIdempotentElem.mem_smul_top_iff_smul_eq_self, TauCeti.isInternal_smul_top, … — apply to TauCeti.vertexComponent, without its body being exposed.

Not @[simp]: rewriting with it would unfold the abstraction everywhere and take TauCeti.mem_vertexComponent_iff_smul_eq_self and the results below out of simp normal form.

@[simp]

theorem TauCeti.mem_vertexComponent_iff_smul_eq_self {k : Type w} {Q : Type u} [CommSemiring k] [Quiver Q] [Finite Q] {M : Type u_1} [AddCommMonoid M] [Module k M] [Module (pathAlgebra k Q) M] [IsScalarTower k (pathAlgebra k Q) M] {v : Q} {x : M} : x ∈ vertexComponent k M v ↔ PathAlgebra.vertexIdempotent k v • x = x

Membership in eᵥ M is the fixed-point condition for the vertex idempotent.

@[simp]

theorem TauCeti.vertexIdempotent_smul_eq_self_of_mem_vertexComponent {k : Type w} {Q : Type u} [CommSemiring k] [Quiver Q] [Finite Q] {M : Type u_1} [AddCommMonoid M] [Module k M] [Module (pathAlgebra k Q) M] [IsScalarTower k (pathAlgebra k Q) M] {v : Q} {x : M} (hx : x ∈ vertexComponent k M v) : PathAlgebra.vertexIdempotent k v • x = x

The vertex idempotent fixes its own component.

theorem TauCeti.ofPath_smul_mem_vertexComponent {k : Type w} {Q : Type u} [CommSemiring k] [Quiver Q] [Finite Q] {M : Type u_1} [AddCommMonoid M] [Module k M] [Module (pathAlgebra k Q) M] [IsScalarTower k (pathAlgebra k Q) M] {a b : Q} (p : Quiver.Path a b) (x : M) : PathAlgebra.ofPath ⟨a, ⟨b, p⟩⟩ • x ∈ vertexComponent k M b

A path lands in the component of its target. Together with TauCeti.ofPath_smul_eq_zero_of_ne_of_mem_vertexComponent this says that a path from a to b acts as a map from the component at its source to the component at its target, which is the orientation the later factor first product of the path algebra was chosen to produce.

theorem TauCeti.ofPath_smul_eq_zero_of_ne_of_mem_vertexComponent {k : Type w} {Q : Type u} [CommSemiring k] [Quiver Q] [Finite Q] {M : Type u_1} [AddCommMonoid M] [Module k M] [Module (pathAlgebra k Q) M] [IsScalarTower k (pathAlgebra k Q) M] {a b c : Q} (p : Quiver.Path a b) (h : c ≠ a) {x : M} (hx : x ∈ vertexComponent k M c) : PathAlgebra.ofPath ⟨a, ⟨b, p⟩⟩ • x = 0

A path annihilates every vertex component but that of its source.

noncomputable def TauCeti.pathMap (k : Type w) {Q : Type u} [CommSemiring k] [Quiver Q] [Finite Q] (M : Type u_1) [AddCommMonoid M] [Module k M] [Module (pathAlgebra k Q) M] [IsScalarTower k (pathAlgebra k Q) M] {a b : Q} (p : Quiver.Path a b) : ↥(vertexComponent k M a) →ₗ[k] ↥(vertexComponent k M b)

The k-linear map eₐ M → e_b M given by the action of a path from a to b. These are the structure maps of the representation of Q attached to M.

Equations

• TauCeti.pathMap k M p = { toFun := fun (x : ↥(TauCeti.vertexComponent k M a)) => ⟨TauCeti.PathAlgebra.ofPath ⟨a, ⟨b, p⟩⟩ • ↑x, ⋯⟩, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem TauCeti.coe_pathMap_apply (k : Type w) {Q : Type u} [CommSemiring k] [Quiver Q] [Finite Q] (M : Type u_1) [AddCommMonoid M] [Module k M] [Module (pathAlgebra k Q) M] [IsScalarTower k (pathAlgebra k Q) M] {a b : Q} (p : Quiver.Path a b) (x : ↥(vertexComponent k M a)) : ↑((pathMap k M p) x) = PathAlgebra.ofPath ⟨a, ⟨b, p⟩⟩ • ↑x

@[simp]

theorem TauCeti.pathMap_nil (k : Type w) {Q : Type u} [CommSemiring k] [Quiver Q] [Finite Q] (M : Type u_1) [AddCommMonoid M] [Module k M] [Module (pathAlgebra k Q) M] [IsScalarTower k (pathAlgebra k Q) M] (a : Q) : pathMap k M Quiver.Path.nil = LinearMap.id

The trivial path acts as the identity.

@[simp]

theorem TauCeti.pathMap_comp (k : Type w) {Q : Type u} [CommSemiring k] [Quiver Q] [Finite Q] (M : Type u_1) [AddCommMonoid M] [Module k M] [Module (pathAlgebra k Q) M] [IsScalarTower k (pathAlgebra k Q) M] {a b c : Q} (p : Quiver.Path a b) (q : Quiver.Path b c) : pathMap k M (p.comp q) = pathMap k M q ∘ₗ pathMap k M p

Concatenation of paths is composition of the maps they act by. Together with TauCeti.pathMap_nil this says that the assignment v ↦ eᵥ M is functorial in the path.

@[simp]

theorem TauCeti.pathMap_cons (k : Type w) {Q : Type u} [CommSemiring k] [Quiver Q] [Finite Q] (M : Type u_1) [AddCommMonoid M] [Module k M] [Module (pathAlgebra k Q) M] [IsScalarTower k (pathAlgebra k Q) M] {a b c : Q} (p : Quiver.Path a b) (f : b ⟶ c) : pathMap k M (p.cons f) = pathMap k M f.toPath ∘ₗ pathMap k M p

The composition law in the form paths are destructured: extending p by an arrow f composes the map of p with that of f.

noncomputable def TauCeti.vertexProjection (k : Type w) {Q : Type u} [CommSemiring k] [Quiver Q] [Finite Q] (M : Type u_1) [AddCommMonoid M] [Module k M] [Module (pathAlgebra k Q) M] [IsScalarTower k (pathAlgebra k Q) M] (v : Q) : M →ₗ[k] ↥(vertexComponent k M v)

The projection of a module onto a vertex component, x ↦ eᵥ • x. It reads the decomposition M = ⨁ᵥ eᵥ M (TauCeti.isInternal_vertexComponent) one vertex at a time; the facts about it that matter are that its values sum to the identity (TauCeti.sum_coe_vertexProjection) and that it is the identity on the component at v and zero on the component at any other vertex.

Equations

• TauCeti.vertexProjection k M v = { toFun := fun (x : M) => ⟨TauCeti.PathAlgebra.vertexIdempotent k v • x, ⋯⟩, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem TauCeti.coe_vertexProjection_apply (k : Type w) {Q : Type u} [CommSemiring k] [Quiver Q] [Finite Q] (M : Type u_1) [AddCommMonoid M] [Module k M] [Module (pathAlgebra k Q) M] [IsScalarTower k (pathAlgebra k Q) M] (v : Q) (x : M) : ↑((vertexProjection k M v) x) = PathAlgebra.vertexIdempotent k v • x

theorem TauCeti.sum_coe_vertexProjection {k : Type w} {Q : Type u} [CommSemiring k] [Quiver Q] [Finite Q] {M : Type u_1} [AddCommMonoid M] [Module k M] [Module (pathAlgebra k Q) M] [IsScalarTower k (pathAlgebra k Q) M] [Fintype Q] (x : M) : ∑ v : Q, ↑((vertexProjection k M v) x) = x

The vertex projections sum to the identity, because the vertex idempotents sum to 1.

theorem TauCeti.coe_vertexProjection_apply_of_mem {k : Type w} {Q : Type u} [CommSemiring k] [Quiver Q] [Finite Q] {M : Type u_1} [AddCommMonoid M] [Module k M] [Module (pathAlgebra k Q) M] [IsScalarTower k (pathAlgebra k Q) M] {v : Q} {x : M} (hx : x ∈ vertexComponent k M v) : ↑((vertexProjection k M v) x) = x

The projection at v fixes the component at v.

theorem TauCeti.coe_vertexProjection_apply_eq_zero_of_ne {k : Type w} {Q : Type u} [CommSemiring k] [Quiver Q] [Finite Q] {M : Type u_1} [AddCommMonoid M] [Module k M] [Module (pathAlgebra k Q) M] [IsScalarTower k (pathAlgebra k Q) M] {u v : Q} (h : u ≠ v) {x : M} (hx : x ∈ vertexComponent k M v) : ↑((vertexProjection k M u) x) = 0

The projection at u kills the component at any other vertex.

noncomputable def TauCeti.vertexComponentMap (k : Type w) {Q : Type u} [CommSemiring k] [Quiver Q] [Finite Q] {M : Type u_1} {N : Type u_2} [AddCommMonoid M] [Module k M] [Module (pathAlgebra k Q) M] [IsScalarTower k (pathAlgebra k Q) M] [AddCommMonoid N] [Module k N] [Module (pathAlgebra k Q) N] [IsScalarTower k (pathAlgebra k Q) N] (f : M →ₗ[pathAlgebra k Q] N) (v : Q) : ↥(vertexComponent k M v) →ₗ[k] ↥(vertexComponent k N v)

A kQ-linear map restricts to a k-linear map between the components at each vertex: it commutes with the action of eᵥ, so it preserves the fixed points of eᵥ. This is TauCeti.smulTopMap at the vertex idempotent.

Equations

• TauCeti.vertexComponentMap k f v = TauCeti.smulTopMap k (TauCeti.PathAlgebra.vertexIdempotent k v) f

@[simp]

theorem TauCeti.coe_vertexComponentMap_apply (k : Type w) {Q : Type u} [CommSemiring k] [Quiver Q] [Finite Q] {M : Type u_1} {N : Type u_2} [AddCommMonoid M] [Module k M] [Module (pathAlgebra k Q) M] [IsScalarTower k (pathAlgebra k Q) M] [AddCommMonoid N] [Module k N] [Module (pathAlgebra k Q) N] [IsScalarTower k (pathAlgebra k Q) N] (f : M →ₗ[pathAlgebra k Q] N) (v : Q) (x : ↥(vertexComponent k M v)) : ↑((vertexComponentMap k f v) x) = f ↑x

@[simp]

theorem TauCeti.vertexComponentMap_id (k : Type w) {Q : Type u} [CommSemiring k] [Quiver Q] [Finite Q] {M : Type u_1} [AddCommMonoid M] [Module k M] [Module (pathAlgebra k Q) M] [IsScalarTower k (pathAlgebra k Q) M] (v : Q) : vertexComponentMap k LinearMap.id v = LinearMap.id

The restriction to the components is functorial: the identity restricts to the identity. This is TauCeti.smulTopMap_id at the vertex idempotent.

@[simp]

theorem TauCeti.vertexComponentMap_comp (k : Type w) {Q : Type u} [CommSemiring k] [Quiver Q] [Finite Q] {M : Type u_1} {N : Type u_2} {P : Type u_3} [AddCommMonoid M] [Module k M] [Module (pathAlgebra k Q) M] [IsScalarTower k (pathAlgebra k Q) M] [AddCommMonoid N] [Module k N] [Module (pathAlgebra k Q) N] [IsScalarTower k (pathAlgebra k Q) N] [AddCommMonoid P] [Module k P] [Module (pathAlgebra k Q) P] [IsScalarTower k (pathAlgebra k Q) P] (g : N →ₗ[pathAlgebra k Q] P) (f : M →ₗ[pathAlgebra k Q] N) (v : Q) : vertexComponentMap k (g ∘ₗ f) v = vertexComponentMap k g v ∘ₗ vertexComponentMap k f v

The restriction to the components is functorial: a composite restricts to the composite of the restrictions. This is TauCeti.smulTopMap_comp at the vertex idempotent.

@[simp]

theorem TauCeti.vertexComponentMap_comp_pathMap (k : Type w) {Q : Type u} [CommSemiring k] [Quiver Q] [Finite Q] {M : Type u_1} {N : Type u_2} [AddCommMonoid M] [Module k M] [Module (pathAlgebra k Q) M] [IsScalarTower k (pathAlgebra k Q) M] [AddCommMonoid N] [Module k N] [Module (pathAlgebra k Q) N] [IsScalarTower k (pathAlgebra k Q) N] (f : M →ₗ[pathAlgebra k Q] N) {a b : Q} (p : Quiver.Path a b) : vertexComponentMap k f b ∘ₗ pathMap k M p = pathMap k N p ∘ₗ vertexComponentMap k f a

The path maps are natural in the module: restricting a kQ-linear map to the vertex components commutes with the action of every path. This is the morphism half of the passage from kQ-modules to representations of Q.

theorem TauCeti.isInternal_vertexComponent (k : Type w) {Q : Type u} [CommSemiring k] [Quiver Q] [Finite Q] [DecidableEq Q] (M : Type u_1) [AddCommMonoid M] [Module k M] [Module (pathAlgebra k Q) M] [IsScalarTower k (pathAlgebra k Q) M] : DirectSum.IsInternal fun (v : Q) => vertexComponent k M v

A module over the path algebra is the direct sum of its vertex components, M = ⨁ᵥ eᵥ M. The component of x at v is eᵥ • x, and the decomposition is the one the identity ∑ᵥ eᵥ = 1 provides.

@[simp]

theorem TauCeti.coe_ofBijective_coeLinearMap_symm_apply_vertexComponent (k : Type w) {Q : Type u} [CommSemiring k] [Quiver Q] [Finite Q] [DecidableEq Q] (M : Type u_1) [AddCommMonoid M] [Module k M] [Module (pathAlgebra k Q) M] [IsScalarTower k (pathAlgebra k Q) M] (x : M) (v : Q) : ↑(((LinearEquiv.ofBijective (DirectSum.coeLinearMap fun (w : Q) => vertexComponent k M w) ⋯).symm x) v) = PathAlgebra.vertexIdempotent k v • x

The component of x at v is eᵥ • x: the inverse of the decomposition, read off one vertex at a time. This is the fact the roadmap's inversion of quiverRepEquivalence runs on.

theorem TauCeti.finrank_eq_sum_finrank_vertexComponent (k : Type w) {Q : Type u} [Field k] [Quiver Q] [Fintype Q] (M : Type u_1) [AddCommGroup M] [Module k M] [Module (pathAlgebra k Q) M] [IsScalarTower k (pathAlgebra k Q) M] [Module.Finite k M] : Module.finrank k M = ∑ v : Q, Module.finrank k ↥(vertexComponent k M v)

The dimension of a finite-dimensional kQ-module is the sum of the dimensions of its vertex components: the total dimension is read off the dimension vector v ↦ dim (eᵥ M).