Reflecting a representation at a sink #
For a sink i of a quiver Q -- a vertex no arrow leaves -- the Bernstein-Gelfand-Ponomarev
construction turns a representation M of Q into a representation of the reflected quiver
TauCeti.Quiver.Reflect Q i, in which every arrow at i points the other way. Away from i
nothing changes; at i the vector space Mᵢ is replaced by the kernel of the map
⨁_{a : b ⟶ i} M_b → Mᵢ
that sums the actions of the arrows into i, and each reversed arrow acts by the corresponding
coordinate projection out of that kernel. This file builds that representation and computes its
dimension vector, and bundles the construction as a functor on representations.
The content of the computation is that on dimension vectors the construction realizes the simple
reflection sᵢ of TauCeti.RepresentationTheory.Quiver.Reflection.DimensionVector, provided the
summing map is surjective: the reflected space at i then has dimension
∑_b #(b ⟶ i) · dim M_b - dim Mᵢ, which is exactly sᵢ applied to the dimension vector of M,
because a sink has no outgoing arrow. Surjectivity is the honest hypothesis here and it is not
automatic: it fails exactly the way TauCeti.incomingSum_not_surjective records, for a
representation concentrated at i whose space at i is nontrivial, of which the vertex simple
Sᵢ is the example. The reflection has zero vertex space at i in this boundary case, by
TauCeti.subsingleton_reflectRep_obj_self; in particular, it kills the vertex simple Sᵢ.
Main definitions #
TauCeti.incomingSum: the map⨁_{a : b ⟶ i} M_b → Mᵢsumming the arrows into a vertex, defined at every vertex of every representation, whose range contains the image of every arrow into that vertex (TauCeti.map_toPath_mem_range_incomingSum).TauCeti.reflectRep: the reflectionC⁺ᵢ Mof a representation at a sinki, a representation ofTauCeti.Quiver.Reflect Q i.TauCeti.reflectionFunctor: the BGP reflection functor at a sink.
Main results #
TauCeti.incomingSum_single: the incoming sum of a family supported at one arrow is the action of that arrow.TauCeti.incomingSum_naturality: the incoming sum is natural in the representation.TauCeti.reflectRep_obj_selfandTauCeti.reflectRep_obj_of_ne: the vertex spaces ofC⁺ᵢ M.TauCeti.reflectRep_map_reflectArrowandTauCeti.reflectRep_map_reflectArrowOfNeOfNe: the action of a reversed arrow, by a coordinate projection out of the kernel, and of an arrow away fromi, unchanged.TauCeti.reflectionFunctor_obj: the functor sendsMtoTauCeti.reflectRep M, so the wholereflectRepinterface computes its objects.TauCeti.reflectionFunctor_map_app_self_applyandTauCeti.reflectionFunctor_map_app_of_ne: the action of reflection on morphisms.TauCeti.reflectionFunctor_additive: the reflection functor is additive.TauCeti.dimVector_reflectRep_of_neandTauCeti.dimVector_reflectRep_self_add: the dimension vector ofC⁺ᵢ M, away fromiand ati.TauCeti.dimVector_reflectRep:dim (C⁺ᵢ M) = sᵢ (dim M)when the summing map is surjective.TauCeti.incomingSum_not_surjective: that surjectivity fails for a representation concentrated atiwith nontrivial space there, andTauCeti.subsingleton_reflectRep_obj_self: the reflected space ativanishes under the same source-vanishing hypothesis. Together they describe the vertex simpleSᵢ, the boundary case of the previous result.TauCeti.forall_subsingleton_reflectRep_objandTauCeti.isZero_reflectRep: a representation concentrated at the sink reflects to the zero representation, the same boundary case read at every vertex and on the whole reflection.TauCeti.finiteDimensional_reflectRep_obj: reflection preserves finite-dimensionality of the vertex spaces.TauCeti.nonempty_iso_of_isZero_away_of_linearEquivandTauCeti.nonempty_iso_of_dimVector_eq_of_forall_subsingleton: two representations concentrated at the same sink are isomorphic as soon as their vertex spaces there are, respectively as soon as their dimension vectors agree.
Implementation notes #
The vertex spaces branch on equality with i, so they are written with an if and decided
classically; no DecidableEq Q instance therefore appears in the interface of the construction,
exactly as for TauCeti.simpleRep. Only the statements naming TauCeti.vertexPreReflection assume
DecidableEq Q, because Pi.single needs one.
The vertex spaces, the prefunctor that TauCeti.reflectRep lifts, and the kernel maps underlying
the action on morphisms are private. The reflectRep_obj_*, reflectRep_map_*,
reflectionFunctor_obj, and reflectionFunctor_map_app_* theorems provide the interface
downstream files should use. The body of TauCeti.reflectionFunctor is not exposed outside this
module, so reflectionFunctor_obj cannot be proved by rfl where it is stated; it restates a
private unfolding lemma. A vertex space of a functor object is therefore computed by
reflectionFunctor_obj followed by the matching reflectRep_obj_* result, and that composite is
exactly the transport appearing in the reflectionFunctor_map_app_* statements.
The arrows of TauCeti.Quiver.Reflect Q i are given by TauCeti.Quiver.reflectHom, which is
again an if on equality with i, so an arrow of the reflected quiver is a cast of an arrow of
Q: TauCeti.Quiver.reflectArrow and TauCeti.Quiver.reflectArrowOfNeOfNe name the two casts, and
the computation rules for the action are stated on them. Both branches at i that a general vertex
would allow are impossible at a sink -- the reflected quiver has no arrow into i and i carries
no loop -- and the definition discharges them from TauCeti.Quiver.IsSink.
The universes are constrained the least the construction allows: the vertex spaces of M are
taken in max v w x for the vertex universe v, the arrow universe w and an arbitrary x,
because the reflected space at i is cut out of a product indexed by the arrows into i, which
lives in max v w together with the vertex spaces. The universe of the field is unconstrained.
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; as in the neighbouring files, the
CategoryTheory.Paths.of annotations record that identification where a proof needs it.
References #
This implements the reflection at a sink of the reflection functors of Layer 4 of
TauCetiRoadmap/RepresentationTheory/QuiverRepresentations/README.md. See
Bernstein--Gelfand--Ponomarev, Coxeter functors and Gabriel's theorem, and
Derksen--Weyman, An Introduction to Quiver Representations, Ch. 2.
The sum of the arrows into a vertex #
The sum of the arrows into a vertex. For a representation M of a finite quiver and a
vertex i, this is the linear map ⨁_{a : b ⟶ i} M_b → Mᵢ sending a family of vectors, indexed
by the arrows into i, to the sum of their images under the corresponding arrows. Its kernel is
the vector space that TauCeti.reflectRep puts at i. It is LinearMap.lsum applied to the
actions of the arrows into i; the decidable equality that combinator needs is supplied
classically, so none appears in the interface.
No hypothesis on i is imposed: the map is defined at every vertex, and it is the reflection that
needs i to be a sink.
Instances For
TauCeti.incomingSum sends a family of vectors indexed by the arrows into i to the sum,
over those arrows, of the images of its coordinates under the corresponding arrow actions.
The source of TauCeti.incomingSum has dimension ∑_b #(b ⟶ i) · dim M_b. Only the vertex
spaces at the sources of arrows into i need be finite-dimensional; they are the only ones the
domain is built from.
The reflected representation #
The reflection of a representation at a sink i: the representation C⁺ᵢ M of the
reflected quiver TauCeti.Quiver.Reflect Q i that agrees with M away from i, puts the kernel
of TauCeti.incomingSum at i, and lets each reversed arrow act by the matching coordinate
projection out of that kernel.
Instances For
The reflected representation at the reflected vertex is the kernel of the sum of the
arrows into i.
A reversed arrow acts by a coordinate projection. The arrow i ⟶ b of the reflected
quiver coming from an arrow e : b ⟶ i of Q sends an element of the kernel at i to its
coordinate at e. The source b of such an arrow is automatically distinct from i, since a
sink carries no loop.
An arrow away from the reflected vertex acts unchanged.
The sum of the arrows into a vertex is natural in the representation. Applying a morphism
η coordinatewise to a family indexed by the arrows into i and then summing is the same as
summing first and applying η at i; it is the naturality of η along those arrows, read off one
coordinate at a time.
The components of the reflected morphism are transports of components of the original one, so
every identity about them is an identity of the original conjugated by eqToHom. The general
transport API is in TauCeti.CategoryTheory.EqToHom, including the conjugation rules for the
identities, compositions, and sums used to construct the reflection functor.
The BGP reflection functor at a sink. It sends a representation to
TauCeti.reflectRep and a morphism to the induced map between the kernels at the reflected vertex,
while leaving its components away from that vertex unchanged.
Instances For
The BGP reflection functor is additive. Away from the reflected vertex its components are transports of the components of the given morphism, and at the reflected vertex the coordinatewise map between the two kernels; both are additive in the morphism.
The BGP reflection functor preserves scalar multiplication on morphisms.
The objects of the BGP reflection functor. The representation supplied by
TauCeti.reflectionFunctor is TauCeti.reflectRep, so the whole TauCeti.reflectRep interface --
its vertex spaces, the action of the reflected arrows, and its dimension vector -- describes it.
At the reflected vertex, reflection sends a morphism to the coordinatewise map between the
kernels of the incoming sums. The two vertex spaces are read off by TauCeti.reflectionFunctor_obj
followed by TauCeti.reflectRep_obj_self, which is the transport in the statement.
Away from the reflected vertex, reflection leaves the components of a morphism unchanged. The
two vertex spaces are read off by TauCeti.reflectionFunctor_obj followed by
TauCeti.reflectRep_obj_of_ne, which is the transport in the statement.
The dimension vector of the reflection #
The dimension of the reflected space at the sink. When the sum of the arrows into i is
onto, rank-nullity turns the kernel that the reflection puts at i into the arrow count
∑_b #(b ⟶ i) · dim M_b less the old dimension at i. Only the vertex spaces at the sources of
arrows into i need be assumed finite-dimensional; surjectivity exhibits Mᵢ as a quotient of
the resulting finite-dimensional domain.
The reflection acts on dimension vectors by the simple reflection at the sink. The
hypothesis is that the sum of the arrows into i is onto; it is exactly what makes the kernel at
i have the dimension the reflection sᵢ predicts, and it fails for the vertex simple Sᵢ. As
in TauCeti.dimVector_reflectRep_self_add, only the vertex spaces at the sources of arrows into
i need be finite-dimensional; away from i the dimension vector is unchanged.
The boundary case: a representation concentrated at the sink #
If every vertex space at the source of an arrow into i vanishes, then the sum of the arrows
into i is the zero map.
The sum of the arrows into i need not be onto. It fails to be whenever every vertex
space at the source of an arrow into i vanishes while the space at i does not, which is what
the vertex simple Sᵢ does at a sink: no arrow into a sink is a loop, so Sᵢ vanishes at every
source of such an arrow. This is why the surjectivity hypothesis of
TauCeti.dimVector_reflectRep cannot be dropped.
The reflected space at the sink vanishes when all incoming sources vanish. If every vertex
space at the source of an arrow into i vanishes, then the reflected space at i vanishes too.
In particular, this is the sink-vertex computation showing that reflection annihilates the vertex
simple Sᵢ.
Reflection annihilates a representation concentrated at the sink. If every vertex space of
M away from i vanishes, then the reflection is the zero representation: at i by
TauCeti.subsingleton_reflectRep_obj_self, since no arrow into a sink is a loop, and away from
i because the vertex space is unchanged there. This is the boundary case in which reflection
does not act by the simple reflection on dimension vectors -- for an indecomposable
representation it is the vertex simple Sᵢ, which TauCeti.incomingSum_not_surjective
describes -- and it is what makes a composite of reflections vanish once one of its stages
does.
Reflection annihilates a representation concentrated at the sink, read on the whole
reflection: TauCeti.forall_subsingleton_reflectRep_obj says every vertex space of the reflection
vanishes, and a representation with vanishing vertex spaces is a zero object.
Reflection preserves finite-dimensionality. The reflected space at the sink is a subspace
of a finite product of vertex spaces of M, and away from the sink the vertex spaces are those of
M. This is what carries the finite-dimensionality hypothesis of
TauCeti.dimVector_reflectRep through a sequence of reflections.
If every source of an arrow into the sink vanishes, the reflected dimension at the sink is zero.
Comparing two representations concentrated at the same sink #
Two representations vanishing away from a sink are isomorphic as soon as their vertex spaces
at that sink are. Every component away from i is a map between zero objects, and there is no
naturality condition to check at i, since no arrow leaves a sink.
A representation concentrated at a sink is isomorphic to every finite-dimensional
representation with the same dimension vector. Equality of dimension vectors makes the comparison
representation vanish wherever M does, and matches the two vertex spaces at the sink. Only the
vertex space of M at the sink is asked to be finite-dimensional, since M is a subsingleton
everywhere else; N is asked for it at every vertex, to read a vanishing dimension vector there as
a vanishing vertex space.