Reflecting an indecomposable representation at a sink #
The Bernstein-Gelfand-Ponomarev reflection at a sink i replaces the vertex space Mᵢ by the
kernel of the sum TauCeti.incomingSum of the arrows into i, and it acts on dimension vectors by
the simple reflection sᵢ whenever that sum is onto (TauCeti.dimVector_reflectRep). This file
discharges that hypothesis: the sum of the arrows into a sink is onto for every indecomposable
representation except the vertex simple Sᵢ, which is the representation the reflection
annihilates.
One construction does the work. A linear endomorphism π of Mᵢ that the paths through i do
not see extends by the identity at the other vertices to an endomorphism TauCeti.vertexEnd of
the whole representation, idempotent as soon as π is. The category of representations is
abelian, hence idempotent complete, so an indecomposable object carries no idempotent endomorphism
besides 0 and the identity (TauCeti.idempotent_eq_zero_or_id_of_indecomposable), and therefore
π itself is 0 or the identity. Applied to the projection onto the range of the incoming sum
along a complement, this says the range is all of Mᵢ unless M vanishes away from i; applied
to the projection onto a line, it says a representation concentrated at i is a line there, hence
is Sᵢ, provided i carries no nontrivial closed path.
TauCeti.vertexEnd is stated at a vertex, not at a sink: naturality needs only that no path from
elsewhere into i sees π before it, that no path from i to elsewhere sees π after it, and
that π commutes with the maps of closed paths at i. At a sink the second condition is vacuous
and all closed paths are trivial; the dual construction at a source, in
TauCeti.RepresentationTheory.Quiver.Reflection.Source.Indecomposable, is the same theorem with
the first condition vacuous instead.
Main definitions #
TauCeti.vertexEnd: the endomorphism ofMacting by a given endomorphism ofMᵢat a vertexiand by the identity elsewhere, withTauCeti.vertexEnd_eq_id_iffandTauCeti.vertexEnd_eq_zero_iffrecognizing when it is trivial.
Main results #
TauCeti.vertexIdempotent_eq_id_or_eq_zero_of_indecomposable: an idempotent ofMᵢinvisible to the paths throughiis the identity, or is zero andMvanishes away fromi, withTauCeti.sinkIdempotent_eq_id_or_eq_zero_of_indecomposableits form at a sink, where the hypothesis reads "πfixes the image of every arrow intoi".TauCeti.exists_ne_zero_span_eq_top_of_forall_subsingleton,TauCeti.dimVector_eq_single_of_forall_subsingletonandTauCeti.nonempty_iso_simpleRep_of_forall_subsingleton: an indecomposable representation concentrated at a vertex with no nontrivial closed path is a line there, hence isomorphic to the vertex simple.TauCeti.nonempty_iso_of_forall_subsingleton: two such representations concentrated at the same vertex are isomorphic; unlike the comparison with the vertex simple, this needs no restriction on universes.TauCeti.incomingSum_surjective_of_indecomposable: the sum of the arrows into a sink is onto for every indecomposable representation not isomorphic to the vertex simple there.TauCeti.dimVector_reflectRep_of_indecomposable: consequently the reflection at a sink acts on the dimension vector of such a representation by the simple reflection at that vertex.
Implementation notes #
TauCeti.sinkIdempotent_eq_id_or_eq_zero_of_indecomposable takes its hypothesis on π in the form
"π fixes the image of each arrow into i" rather than "π fixes the range of
TauCeti.incomingSum". The two agree on a finite quiver, by
TauCeti.map_toPath_mem_range_incomingSum, but the arrow form needs no finiteness, and neither
then do the construction, its recognition lemmas, or the statement that an indecomposable
representation concentrated at a sink is a line there. Finiteness enters only where
TauCeti.incomingSum does.
The results comparing M with TauCeti.simpleRep k Q i are stated in the last section, where the
quiver, its arrows and the field all live in one universe. This is forced, not chosen: the vertex
spaces of a reflected representation are cut out of a product indexed by the arrows, so
TauCeti.reflectRep needs them in max v w x, while Sᵢ puts the field itself at i and so
needs them in the universe of the field. A statement mentioning both therefore has to identify the
two, and the general statements above -- which name no vertex simple -- are proved in the wider
setting and specialize to it.
As in the neighbouring files, a vertex i : Q is used as an object of the free category
CategoryTheory.Paths Q, which is Q only by unfolding a semireducible definition. Rewriting
cannot see through that identification, so every step that branches on equality of vertices is
factored through a lemma quantified over Q, and the components of TauCeti.vertexEnd are
supplied by the private vertexEndApp; TauCeti.vertexEnd_app_self and
TauCeti.vertexEnd_app_of_ne are the interface.
References #
This is the identity dim (C⁺ᵢ M) = sᵢ · dim M with its hypothesis discharged. See
Bernstein--Gelfand--Ponomarev, Coxeter functors and Gabriel's theorem, and Derksen--Weyman, An
Introduction to Quiver Representations, Ch. 2.
The endomorphism attached to an idempotent at a vertex #
The endomorphism of M given by an endomorphism at one vertex. For a linear endomorphism
π of Mᵢ that no path into i from elsewhere sees before it (hin), that no path out of i
to elsewhere sees after it (hout), and that commutes with every closed-path map at i (hcomm),
this is the endomorphism of M acting by π at i and by the identity at every other vertex.
The three hypotheses hold at a sink and, dually, at a source; they are what naturality asks for,
one case of the square for each of the four positions of i relative to the ends of a path.
Instances For
At its vertex, TauCeti.vertexEnd acts by the given endomorphism.
Away from its vertex, TauCeti.vertexEnd acts by the identity.
TauCeti.vertexEnd is idempotent as soon as the endomorphism it is built from is.
TauCeti.vertexEnd is the identity exactly when the endomorphism it is built from is.
TauCeti.vertexEnd vanishes exactly when the endomorphism it is built from vanishes and the
representation is concentrated at its vertex: elsewhere it acts by the identity, which is zero only
on a vanishing vertex space.
Idempotents at a vertex of an indecomposable representation #
An idempotent at a vertex of an indecomposable representation is trivial. Let M be an
indecomposable representation. An idempotent endomorphism of Mᵢ invisible to the paths through
i, in the sense of
TauCeti.vertexEnd, is either the identity, or zero — and in the second case M vanishes away
from i.
An idempotent at a sink of an indecomposable representation is trivial. Let i be a sink
of Q and M an indecomposable representation. An idempotent endomorphism of Mᵢ fixing the
image of every arrow into i is either the identity, or zero — and in the second case M vanishes
away from i.
An indecomposable representation concentrated at one vertex is a line there: if M
vanishes away from a vertex i carrying no closed path but the trivial one, its vertex space at
i is spanned by a single nonzero vector.
An indecomposable representation concentrated at a vertex with no nontrivial closed path has a one-dimensional endomorphism space.
An indecomposable representation concentrated at a vertex carrying no nontrivial closed path has the corresponding simple dimension vector.
Two indecomposable representations concentrated at the same vertex are isomorphic, provided that vertex carries no closed path but the trivial one. Each is a line at that vertex and zero elsewhere, and no arrow joins the vertex to itself, so any linear isomorphism of the two lines is an isomorphism of representations.
The surjectivity of the incoming sum #
The sum of the arrows into a sink of an indecomposable representation is onto, unless the
representation is concentrated at that sink. This is the surjectivity hypothesis of
TauCeti.dimVector_reflectRep, discharged: the range of the incoming sum is a direct summand of
Mᵢ, so a proper range would split M, and the only splitting an indecomposable representation
admits leaves nothing outside the sink.
The vertex simple as the exceptional case #
An indecomposable representation concentrated at one vertex is the vertex simple there, provided that vertex carries no closed path but the trivial one.
The sum of the arrows into a sink is onto for every indecomposable representation other than
the vertex simple there. The vertex simple Sᵢ is genuinely excluded, by
TauCeti.incomingSum_not_surjective.
The reflection at a sink acts on the dimension vector of an indecomposable representation by
the simple reflection there, unless that representation is the vertex simple at the sink, which
the reflection annihilates instead. This is the identity dim (C⁺ᵢ M) = sᵢ · dim M with its
hypothesis discharged.