The injective representation at a vertex of a quiver #
For a vertex i of a quiver Q, the representation Iᵢ puts the space of all k-valued
functions on the paths j → i at the vertex j, a path p acting by precomposition,
(p · x) q = x (p.comp q). Under the identification of representations with left modules over the
path algebra it is the k-dual D(eᵢ · kQ) of the right ideal spanned by the paths ending at i.
Main definitions #
TauCeti.indecInjRep k Q i: the representationIᵢ.TauCeti.indecInjRepHom: the morphismM ⟶ Iᵢdetermined by a linear functional onMati.
Main results #
TauCeti.indecInjRepHomEquiv:Iᵢrepresents the dual of evaluation ati, by thek-linear isomorphism(M ⟶ Iᵢ) ≃ₗ[k] Module.Dual k Mᵢsending a morphism to the functional reading off its value on the trivial path. This is the universal property from which everything else here follows, and it is dual toTauCeti.indecProjRepHomEquiv.TauCeti.isSplitMono_of_indecInjRep_app_injective: a morphism out ofIᵢthat is injective atiis a split monomorphism.TauCeti.injective_indecInjRep:Iᵢis an injective object ofTauCeti.QuiverRep k Q.TauCeti.dimVector_indecInjRep: the dimension vector ofIᵢcounts the paths intoi, andTauCeti.not_isZero_indecInjRep:Iᵢis nonzero.TauCeti.finrank_hom_indecInjRep_indecInjRep:dim Hom(Iᵢ, Iⱼ)is the number of pathsj → i, the same path count asTauCeti.finrank_hom_indecProjRep_indecProjRep.
Implementation notes #
The name indecInjRep is the one the roadmap pins for this object. As with the projectives,
indecomposability is not proved here: it needs the Krull-Schmidt theory of Layer 2, which is not
yet available. What is proved is injectivity, and the universal property that makes Iᵢ the
representing object of the contravariant functor M ↦ Module.Dual k Mᵢ; both are independent of any
finiteness assumption on Q, so no such assumption is made.
Iᵢ puts the product Quiver.Path j i → k at j, not the free module on the paths j → i.
The two agree exactly when there are finitely many paths j → i, and the product is the right
choice: it is the full k-dual of the span of the paths ending at i, and only the product
corepresents Module.Dual k Mᵢ on representations with infinite-dimensional vertex spaces. The
dimension count TauCeti.dimVector_indecInjRep is nevertheless unconditional, because
Module.finrank of an infinite-dimensional space and Nat.card of an infinite type are both 0.
Because the vertex spaces are function types rather than Finsupps, no basis is needed to name
their elements: every lemma below is stated on the value of a function at a path, and Iᵢ admits a
uniform description of the action of a path, TauCeti.indecInjRep_map_apply, which
TauCeti.indecProjRep_map_basis can only give on basis vectors.
Iᵢ is built by CategoryTheory.Paths.lift, so only its value on arrows is written down and
Mathlib supplies functoriality along path concatenation. indecInjRep is the one definition here
that exposes its body: that is what makes (Iᵢ)_j definitionally the function type
Quiver.Path j i → k, so an element of it can be applied to a path with no transport in the way,
which is the point of choosing a function type over a Finsupp here. The morphism it receives and
the universal-property equivalence keep their bodies sealed; their characteristic lemmas
TauCeti.indecInjRepHom_app_apply, TauCeti.indecInjRepHomEquiv_apply and
TauCeti.indecInjRepHomEquiv_symm_apply are the whole public interface.
A vertex i : Q is used below as an object of the free category CategoryTheory.Paths Q, and
(Iᵢ)_j is the function type Quiver.Path j i → k only by unfolding indecInjRep and
CategoryTheory.Paths.lift. Goals that cross that identification are therefore not reached by
ModuleCat.hom_ofHom, LinearMap.pi_apply or LinearMap.proj_apply, which have nothing to match
on; the two proofs inside TauCeti.indecInjRepHom and TauCeti.indecInjRepHomEquiv that have to
cross it do so by change, and each says in a comment which definitional equality it is recording.
The vector space (Iᵢ)_j lives in the universe of Quiver.Path j i → 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 embedding
Sᵢ ↪ Iᵢ is therefore not stated here, exactly as the surjection Pᵢ ↠ Sᵢ is not stated in
TauCeti.RepresentationTheory.Quiver.Representation.Projective.Basic; both are stated in
TauCeti.RepresentationTheory.Quiver.Representation.Comparison, where those universes are aligned.
References #
This implements the indecomposable injectives 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 injective representation at a vertex Iᵢ: the k-valued functions on the paths
j → i at the vertex j, an arrow acting by prepending itself to a path. Under the identification
of representations with left modules over the path algebra this is the k-dual D(eᵢ · kQ) of the
right ideal spanned by the paths ending at i.
Equations
- One or more equations did not get rendered due to their size.
Instances For
A path acts on Iᵢ by precomposition: the value of p · x on a path q : b → i is the
value of x on the concatenation p.comp q.
The dimension of the vector space Iᵢ puts at j is the number of paths j → i. With
infinitely many such paths both sides are 0, by the conventions for Module.finrank and
Nat.card.
The dimension vector of Iᵢ counts, at each vertex, the paths from it to i. Together with
TauCeti.dimVector_indecProjRep this says that the dimension vectors of the injectives are the
transposes of the dimension vectors of the projectives.
The dimension vector of Iᵢ is the transpose of the dimension vector of Pⱼ: both count the
paths j → i.
The universal property #
The morphism M ⟶ Iᵢ determined by a linear functional φ on M at the vertex i: at the
vertex j it sends x to the function reading off φ of the action of a path j → i on x.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The morphism attached to φ : Module.Dual k Mᵢ sends x at the vertex j to the function
whose value on a path q : j → i is φ of the action of q on x.
A morphism into Iᵢ is determined by its value on the trivial path at i: naturality
propagates that single functional to every vertex.
A morphism into Iᵢ is recovered from the functional it induces at i.
Iᵢ represents the dual of evaluation at i. A morphism into Iᵢ is determined by, and
can be prescribed by, the linear functional reading off its value on the trivial path at i; the
bijection is k-linear. This is the exact dual of TauCeti.indecProjRepHomEquiv.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The universal property is natural in the source: precomposition with g corresponds to
precomposition of functionals with g at i.
A morphism out of Iᵢ that is injective at i is a split monomorphism. The retraction is
obtained by extending the functional corresponding to the identity of Iᵢ across that injective
component.
The representations Iᵢ are injective. A morphism into Iᵢ is a single linear functional
on the source at i, a monomorphism of representations is injective there, and a linear functional
extends along an injective linear map of vector spaces.
The path-counting form of the Cartan matrix, read on injectives: the dimension of
Hom(Iᵢ, Iⱼ) is the number of paths j → i, the same count as for Hom(Pⱼ, Pᵢ).
The representation Iᵢ is nonzero: the function that is 1 on every path is a nonzero element
of (Iᵢ)_i, since the trivial path is one of them.