Representations of the generalized Kronecker quiver #
A representation of the generalized Kronecker quiver is a pair of vector spaces together with one
linear map between them for each arrow: no two arrows compose, so the only paths are the identities
and the arrows themselves. This file builds such a representation from that datum, as
TauCeti.kroneckerRep, computes its two vertex spaces and the action of each arrow, and identifies
the morphisms between two such representations with the pairs of linear maps making a commuting
square along every arrow. The same identification for representations that are not presented by
TauCeti.kroneckerRep is TauCeti.kroneckerHom, with its isomorphism version
TauCeti.kroneckerIso.
The representation type of the quiver -- infinite as soon as there are two arrows -- is
TauCeti.RepresentationTheory.Quiver.Kronecker.FiniteRepType, which builds its Jordan blocks with
the definition below.
Main definitions #
TauCeti.kroneckerRep: the representation of the generalized Kronecker quiver with prescribed vertex spaces and a prescribed linear map along each arrow.TauCeti.kroneckerRepHom: the morphism between two such representations attached to a pair of linear maps making a commuting square along every arrow.TauCeti.kroneckerHomandTauCeti.kroneckerIso: the same, for two arbitrary representations of the generalized Kronecker quiver rather than two presented byTauCeti.kroneckerRep, built from a linear map -- an isomorphism, forTauCeti.kroneckerIso-- at each vertex intertwining the action of every arrow.
Main results #
TauCeti.kroneckerRep_map_arrowPath: the arrow indexed byaacts by the prescribed map.TauCeti.kroneckerRep_hom_ext: a morphism of representations of the generalized Kronecker quiver is determined by its two components.TauCeti.kroneckerRepHom_eta: conversely, every morphism between two representations built byTauCeti.kroneckerRepis the one attached to its two components. Together withTauCeti.kroneckerRep_hom_extthis is the promised identification, mirroring the pairTauCeti.oneLoopRepHom_oneLoopRepScalar/TauCeti.oneLoopRep_hom_extof the loop quiver.TauCeti.kroneckerHom_eta: the same for two arbitrary representations, every morphism between them beingTauCeti.kroneckerHomof its two components.
Implementation notes #
TauCeti.kroneckerRep carries @[expose], for the reason the loop-quiver file
TauCeti.RepresentationTheory.Quiver.OneLoop.FiniteRepType records: a functor built by
CategoryTheory.Paths.lift reveals its value on objects only through its definition. The
obstruction is at the level of statements, not of proofs, so no characteristic lemma can remove
it: without @[expose], already kroneckerRep_map_arrowPath fails to elaborate, f a : M ⟶ N not
being accepted where (kroneckerRep k M N f).obj Quiver.Kronecker.src ⟶ (kroneckerRep k M N f).obj Quiver.Kronecker.tgt is expected.
References #
This is the representation-level part of the “Kronecker quiver” worked example of
TauCetiRoadmap/RepresentationTheory/QuiverRepresentations/README.md. See Derksen--Weyman, An
Introduction to Quiver Representations, and Assem--Simson--Skowroński, Elements of the
Representation Theory of Associative Algebras I, Ch. II.
A representation of the generalized Kronecker quiver: a vector space M at the source, a
vector space N at the target, and a linear map f a : M ⟶ N along the arrow indexed by a. No
two arrows compose, so the only paths are the identities and the arrows themselves, and this is the
whole datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The arrow indexed by a acts on TauCeti.kroneckerRep by f a.
A morphism of representations of the generalized Kronecker quiver is determined by its two components. The quiver has two vertices, so a natural transformation is a pair of linear maps.
The morphism of representations of the generalized Kronecker quiver attached to a commuting
square along every arrow: a linear map at each of the two vertices, intertwining the two actions
of each arrow. Together with TauCeti.kroneckerRep_hom_ext and TauCeti.kroneckerRepHom_eta this
identifies the morphisms kroneckerRep k M N f ⟶ kroneckerRep k M' N' f' with such pairs.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The two components of a morphism make a commuting square along every arrow, by naturality along the path of that arrow.
Every morphism between representations of the generalized Kronecker quiver is the one
attached to its two components. This is the converse of TauCeti.kroneckerRep_hom_ext: the two
together identify such morphisms with the commuting squares.
The morphism of representations of the generalized Kronecker quiver attached to a linear map
at each vertex intertwining the action of every arrow, the form of TauCeti.kroneckerRepHom for
representations that are not presented by TauCeti.kroneckerRep.
Equations
- One or more equations did not get rendered due to their size.
Instances For
At the source, TauCeti.kroneckerHom is the prescribed linear map.
At the target, TauCeti.kroneckerHom is the prescribed linear map.
Every morphism of representations of the generalized Kronecker quiver is the one attached to
its two components, the form of TauCeti.kroneckerRepHom_eta for representations that are not
presented by TauCeti.kroneckerRep: the commuting square along an arrow is naturality along the
path of that arrow.
Two representations of the generalized Kronecker quiver with isomorphic vertex spaces
intertwining every arrow are isomorphic, the isomorphism version of TauCeti.kroneckerHom.
Equations
- One or more equations did not get rendered due to their size.
Instances For
At the source, TauCeti.kroneckerIso is the prescribed isomorphism.
At the target, TauCeti.kroneckerIso is the prescribed isomorphism.
At the source, the inverse of TauCeti.kroneckerIso is the prescribed inverse.
At the target, the inverse of TauCeti.kroneckerIso is the prescribed inverse.