The projective representation at a vertex of a quiver #
For a vertex i of a quiver Q, the representation Pᵢ puts the free k-module on the paths
i → j at the vertex j, an arrow e : a ⟶ b acting by appending e to a path. Under the
identification of representations with left modules over the path algebra it is the left ideal
kQ · eᵢ, whose basis is the paths starting at i.
Main definitions #
TauCeti.indecProjRep k Q i: the representationPᵢ.TauCeti.indecProjRepBasis: the pathsi → jas ak-basis of(Pᵢ)_j.TauCeti.indecProjRepHom: the morphismPᵢ ⟶ Mdetermined by an element ofMati.
Main results #
TauCeti.indecProjRepHomEquiv:Pᵢrepresents evaluation ati, by thek-linear isomorphism(Pᵢ ⟶ M) ≃ₗ[k] Mᵢsending a morphism to the image of the trivial path. This is the universal property from which everything else here follows.TauCeti.projective_indecProjRep:Pᵢis a projective object ofTauCeti.QuiverRep k Q.TauCeti.dimVector_indecProjRep: the dimension vector ofPᵢcounts the paths out ofi, andTauCeti.not_isZero_indecProjRep:Pᵢis nonzero.TauCeti.finrank_hom_indecProjRep_indecProjRep:dim Hom(Pᵢ, Pⱼ)is the number of pathsj → i, the path-counting form of the Cartan matrix of a path algebra. Its acyclic consequence, thatPᵢis then a brick, is inTauCeti.RepresentationTheory.Quiver.Representation.Projective.Acyclic.TauCeti.isSplitEpi_of_app_eq_indecProjRepBasis_nil:Pᵢis generated by the basis vector of the trivial path, so a morphism intoPᵢhitting that vector is a split epimorphism, andTauCeti.eq_id_of_app_indecProjRepBasis_nil_eq_self: an endomorphism ofPᵢfixing it is the identity.TauCeti.exists_eq_smul_indecProjRepBasis_nil: when the trivial path is the only pathi → i, the vertex space(Pᵢ)ᵢis the line that vector spans. These are thePᵢ-side ingredients of the projective coverPᵢ ↠ SᵢinTauCeti.RepresentationTheory.Quiver.Representation.Projective.Cover.
Implementation notes #
The name indecProjRep is the one the roadmap pins for this object. Indecomposability is not
proved here: it needs the Krull-Schmidt theory of Layer 2, which is not yet available. What is
proved is projectivity, and the universal property that makes Pᵢ the representable functor at
i; both are independent of any finiteness assumption on Q, so no such assumption is made.
Pᵢ is built by CategoryTheory.Paths.lift: a representation of Q is a functor out of the free
category on Q, so a module at each vertex and a map along each arrow suffice, and Mathlib
supplies functoriality along path concatenation. No definition here exposes its body. Downstream
names an element of (Pᵢ)_j through the basis indecProjRepBasis, indexed by the paths i → j,
and every public lemma — on the action of a path, on the morphism attached to an element of the
target, on the universal property — is stated on those basis vectors; anyone who wants the
underlying free module has the explicit transport (indecProjRepBasis k i j).repr. The lemmas that
name finitely supported functions directly are private to this file.
Read as a functor composite, Pᵢ is the free-module image of the covariant representable at i,
CategoryTheory.coyoneda.obj (Opposite.op i) ⋙ ModuleCat.free k. That composite is not what is
written below, for a universe reason: ModuleCat.free exists only as Type u ⥤ ModuleCat.{u} k for
k : Type u, so composing it with the representable Paths Q ⥤ Type (max v w) forces
max v w = u, collapsing the vertex and arrow universes into the universe of the field, and
interposing CategoryTheory.uliftFunctor only weakens that to max v w ≤ u while re-indexing the
basis by ULift (Quiver.Path i j). The Finsupp API underlying that composite is reused directly
instead, at the level where it is universe-polymorphic: ModuleCat.free acts by
Finsupp.lmapDomain, which is the map below, and its adjunction bijection is the Finsupp.sum map
Finsupp.linearCombination used for indecProjRepHom.
A vertex i : Q is used below as an object of the free category CategoryTheory.Paths Q, which is
Q itself only by unfolding a semireducible definition. Goals about the action of a path are
therefore not type-correct at instances transparency, where rw and simp build their motives;
the one proof that has to reach the underlying statement about finitely supported functions does so
by change, and says so in a comment.
The vector space (Pᵢ)_j lives in the universe of Quiver.Path i j →₀ k, which is larger than
the universe of k unless the vertex and arrow types are small. The vertex simple Sᵢ of
TauCeti.RepresentationTheory.Quiver.Representation.Simple is built on k itself, so the two
objects sit in a common category only when those universes agree, and the surjection
Pᵢ ↠ Sᵢ is therefore not stated here, but in
TauCeti.RepresentationTheory.Quiver.Representation.Comparison, where those universes are aligned.
References #
This implements the indecomposable projectives of Layer 1 of
TauCetiRoadmap/RepresentationTheory/QuiverRepresentations/README.md. See Assem--Simson--
Skowroński, Elements of the Representation Theory of Associative Algebras I, Ch. III.
The projective representation at a vertex Pᵢ: the free k-module on the paths i → j
at the vertex j, an arrow acting by appending itself to a path. Under the identification of
representations with left modules over the path algebra this is the left ideal kQ · eᵢ.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The paths i → j are a k-basis of the vector space that Pᵢ puts at j. This is the handle
on (Pᵢ)_j: the construction of Pᵢ is opaque, and the lemmas below name the elements of (Pᵢ)_j
through this basis.
Equations
Instances For
A path acts on Pᵢ by concatenation: it carries the basis vector of a path q : i → a to
the basis vector of the concatenation q.comp p.
The dimension vector of Pᵢ counts, at each vertex, the paths from i to it. With infinitely
many paths i → j both sides are 0, by the conventions for Module.finrank and Nat.card.
The universal property #
The morphism Pᵢ ⟶ M determined by an element x of M at the vertex i: it sends the basis
element of a path p : i → j to the image of x under the action of p.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The morphism attached to x : Mᵢ sends the basis vector of a path p to the action of p
on x.
The morphism attached to x : Mᵢ sends the basis vector of the trivial path back to x.
A morphism out of Pᵢ is determined by the image of the basis vector of the trivial path
at i.
Pᵢ represents evaluation at i. A morphism out of Pᵢ is determined by, and can be
prescribed by, the image of the basis vector of the trivial path at i; the bijection is
k-linear.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The basis vector of the trivial path is the element of Pᵢ at i that the universal property
picks out.
The universal property is natural in the target: postcomposition with g corresponds to
applying g at i.
Generation by the basis vector of the trivial path #
(Pᵢ)ᵢ is a line when the trivial path is the only path i → i: it is then spanned by
the basis vector of that path. This is the hypothesis on Q that makes Pᵢ ↠ Sᵢ a projective
cover in TauCeti.RepresentationTheory.Quiver.Representation.Projective.Cover, and it fails for
the one-loop quiver, where (Pᵢ)ᵢ is k[X]. Only closed paths at i matter, so an acyclic Q
supplies the hypothesis as hQ.eq_nil.
An endomorphism of Pᵢ fixing the basis vector of the trivial path is the identity. A
morphism out of Pᵢ is determined by the image of that basis vector
(TauCeti.indecProjRepHom_app_nil_self), and the identity is the morphism attached to the basis
vector itself.
Pᵢ is generated by the basis vector of the trivial path: a morphism into Pᵢ whose
image at i contains that basis vector is a split epimorphism. The splitting is the morphism
that the universal property of Pᵢ attaches to a preimage, and the composite is the identity by
TauCeti.eq_id_of_app_indecProjRepBasis_nil_eq_self. No hypothesis on the quiver is needed.
The representations Pᵢ are projective. A morphism out of Pᵢ lifts along any
epimorphism, because it is determined by a single element of the target at i and an epimorphism
of representations is surjective there.
The path-counting form of the Cartan matrix of a path algebra: the dimension of
Hom(Pᵢ, Pⱼ) is the number of paths j → i.
The representation Pᵢ is nonzero: the basis vector of the trivial path at i is a nonzero
element of (Pᵢ)_i.