Extension by zero along an embedding of quivers #
An embedding of quivers φ : Q' → Q (TauCeti.QuiverEmbedding) is a prefunctor injective on
vertices and on the arrows between each pair of vertices; it exhibits Q' as a subquiver of Q,
not necessarily full. A representation M of Q' then extends by zero to a representation of Q
(TauCeti.QuiverEmbedding.extendByZeroRep): it carries M u at φ u and the zero space at every
vertex outside the image, the image of an arrow a of Q' acts as a, and every other arrow of
Q acts by zero.
The point of the construction is that it loses nothing: extension by zero is a fully faithful
functor (TauCeti.QuiverEmbedding.fullyFaithfulExtendByZeroFunctor). A morphism between two
extensions by zero is determined by its components over the image, and those commute with the
arrows of Q' because the image of an arrow of Q' is not the image of any other. Hence extension
by zero preserves finite-dimensionality and indecomposability, and it reflects isomorphism. This is
how a representation-theoretic property of a subquiver is transported to the ambient quiver; in
particular a subquiver with infinitely many indecomposables forces the ambient quiver to have
infinitely many, the reduction by which the non-Dynkin half of Gabriel's theorem is proved.
Main definitions #
TauCeti.QuiverEmbedding.extendByZeroRep: the extension by zero of a representation.TauCeti.QuiverEmbedding.extendByZeroFunctor: extension by zero as a functor.
Main results #
TauCeti.QuiverEmbedding.extendByZeroRepFiberEquiv_map_apply: arrow action on the actual extended vertex spaces, expressed through the fiber equivalences.TauCeti.QuiverEmbedding.extendByZeroMap_map_apply: the image of an arrow ofQ'acts on the extension by zero as the arrow itself.TauCeti.QuiverEmbedding.extendByZeroMap_apply_of_not_exists: an arrow ofQthat is not in the image acts by zero.TauCeti.QuiverEmbedding.extendByZeroRepVertexSpaceEquiv: the vertex space over an image vertex is linearly equivalent to the original space.TauCeti.QuiverEmbedding.isZero_extendByZeroRep_obj_of_not_mem_range: the vertex space outside the image is zero.TauCeti.QuiverEmbedding.fullyFaithfulExtendByZeroFunctor: extension by zero is fully faithful.TauCeti.QuiverEmbedding.nonempty_extendByZeroRep_iso_iff,TauCeti.QuiverEmbedding.isFinDim_extendByZeroRepandTauCeti.QuiverEmbedding.indecomposable_extendByZeroRep: extension by zero reflects and preserves isomorphism, and preserves finite-dimensionality and indecomposability.
Implementation notes #
The space over a vertex v of Q is the product of the spaces of M over the fiber of φ at
v (TauCeti.QuiverEmbedding.Fiber), which has at most one point. This names the space without
choosing a preimage of v, and without transporting M along an equality of vertices: over
φ u the fiber is the single point ⟨u, rfl⟩, whose component is M u on the nose. The price is
a universe: the vertices of Q' are in v', so the product is in max v' t when the spaces of
M are in t. For the quivers the theory is applied to, whose vertices form a Type, that is
t again.
An arrow α : v ⟶ w of Q acts on the component over u' through the arrow of Q' over α
ending at u', when there is one; that arrow is picked by choice, and it is unique by injectivity,
which is what TauCeti.QuiverEmbedding.extendByZeroMap_apply_of_cast_eq records.
References #
- I. Assem, D. Simson, A. Skowroński, Elements of the Representation Theory of Associative Algebras, Volume I, Chapter VII.
- H. Derksen, J. Weyman, An Introduction to Quiver Representations, Chapter 4.
The action of an arrow α : v ⟶ w of Q on the extension by zero of M: the component over
u' is the action of the arrow of Q' over α ending at u', applied to the component at its
source, if there is such an arrow, and zero otherwise.
Instances For
On a component over which α has a lift a, the extension by zero acts by a.
The image of an arrow acts on the extension by zero as the arrow itself, from the component at its source to the component at its target.
On a component over which α has no lift, the extension by zero acts by zero.
The extension by zero of a representation M of Q' along an embedding φ into Q: the
representation of Q with M u at φ u and the zero space at every vertex outside the image,
on which the image of an arrow a of Q' acts as a and every other arrow of Q acts by zero.
The space over a vertex v is the product of the spaces of M over the fiber of φ at v,
which has at most one point; this names it without choosing a preimage of v.
Instances For
The space of the extension by zero over a vertex is the product of the spaces of M over the
fiber there.
The actual vertex space of the extension by zero is linearly equivalent to the product of the original vertex spaces over the fiber.
Instances For
Over an image vertex, the actual vertex space of the extension by zero is linearly equivalent to the original vertex space by evaluation at the unique point of the fiber.
Instances For
The vertex-space equivalence over an image vertex evaluates at the unique fiber point.
The inverse vertex-space equivalence returns the original element at the unique fiber point.
Outside the vertex image of an embedding, extension by zero has a zero vertex space.
An arrow of Q acts on the extension by zero by TauCeti.QuiverEmbedding.extendByZeroMap,
transported from the fiber products to the actual vertex spaces.
Through the fiber equivalences, the action on actual vertex spaces is the extension-by-zero arrow map. Together with the evaluation lemmas, this describes image arrows and arrows with no lift.
The component over a vertex of the extension by zero of a morphism f: f over the fiber.
Instances For
The component of the extension by zero of f over the point u of a fiber is f at u.
The extension by zero of a morphism commutes with the action of every arrow of Q: over the
image of an arrow of Q' this is naturality of f, and elsewhere both sides vanish.
Extension by zero along an embedding of quivers, as a functor from the representations of
Q' to those of Q; on a morphism it acts by that morphism over the image and by zero
elsewhere.
Instances For
The extension by zero functor sends a representation to its extension by zero.
The component of an extended morphism is its action on the fiber products, transported to the actual vertex spaces of the functor objects.
Through the vertex-space equivalences, an extended morphism acts as the original component over each image vertex.
Extension by zero is additive: it acts on morphisms componentwise.
Full faithfulness #
Extension by zero along an embedding of quivers is fully faithful. A morphism between two
extensions by zero is the extension by zero of its components over the image, which form a morphism
of representations of Q' because the embedding is injective on arrows.
Instances For
What extension by zero preserves #
Extension by zero reflects and preserves isomorphism: two representations of Q' are
isomorphic exactly when their extensions by zero are.
The extension by zero of a finite-dimensional representation is finite-dimensional: each
of its spaces is a product of at most one space of M.
The extension by zero of an indecomposable representation is indecomposable: extension by
zero is fully faithful, so it matches the idempotent endomorphisms of M with those of its
extension.