The reflection functor is fully faithful where the incoming sum is onto #
The Bernstein-Gelfand-Ponomarev reflection C⁺ᵢ at a sink i replaces the vertex space Mᵢ by
the kernel of the sum TauCeti.incomingSum of the arrows into i. It annihilates the vertex
simple Sᵢ, so it cannot be an equivalence; what it is, is fully faithful on the representations
whose incoming sum at i is onto. This file proves that: whenever the sum of the arrows into i
is onto for M, the map (M ⟶ N) → (C⁺ᵢ M ⟶ C⁺ᵢ N) supplied by TauCeti.reflectionFunctor is a
bijection. Only the source M needs the hypothesis; the target N is arbitrary.
Surjectivity of the incoming sum is the hypothesis throughout; it is not equivalent to avoiding
Sᵢ. It is TauCeti.incomingSum_surjective_of_indecomposable that ties the two together, and only
for an indecomposable M: such an M has its incoming sum at i onto as soon as it is not
isomorphic to Sᵢ. So the vertex simple names the exceptional case only among indecomposables, and
that is the only place below where it is mentioned.
Both halves are elementary once the incoming sum is available. Faithfulness is the surjectivity
of that sum: a morphism reflecting to zero has vanishing components away from i, hence, by
TauCeti.incomingSum_naturality, its component at i kills the range of the incoming sum, which
is everything. Fullness is the first isomorphism theorem: a morphism θ of the reflected
representations carries the kernel at i for M into the kernel for N, so the composite
⨁_{a : b ⟶ i} M_b → ⨁_{a : b ⟶ i} N_b → Nᵢ factors through the incoming sum of M, and the
resulting map Mᵢ → Nᵢ completes the components of θ away from i to a morphism M ⟶ N
reflecting back to θ.
The consequence is that reflection at a sink preserves indecomposability. The reflection functor
is additive, so a bijection on endomorphisms matches idempotents with idempotents; an indecomposable
M other than Sᵢ therefore reflects to an indecomposable representation of the reflected quiver.
No finite-dimensionality is needed for that. It is needed for the other half of the induction step:
TauCeti.dimVector_reflectRep_of_indecomposable computes the dimension vector of the reflection as
sᵢ · dim M when the vertex spaces at the sources of the arrows into i are finite-dimensional.
Main results #
TauCeti.reflectionFunctor_map_injective,TauCeti.reflectionFunctor_map_surjectiveandTauCeti.reflectionFunctor_map_bijective: the reflection functor at a sink is fully faithful on the representations whose incoming sum there is onto.TauCeti.nonempty_iso_of_nonempty_iso_reflectRep: the reflection functor at a sink reflects isomorphisms between representations whose incoming sums there are onto.TauCeti.indecomposable_reflectRep: reflection at a sink preserves indecomposability, under the same hypothesis.TauCeti.indecomposable_reflectRep_of_not_nonempty_iso_simpleRep: the same statement with the hypothesis discharged, for an indecomposable representation other than the vertex simpleSᵢ.
Implementation notes #
The reflection functor's object (reflectionFunctor i hi).obj M is only propositionally equal to
TauCeti.reflectRep M hi, because the body of the functor is not exposed outside the module
defining it. The statements below therefore speak of the functor's map, whose type mentions only
the functor, and the vertex spaces of its objects are named by the two private transports
reflectObj_self and reflectObj_of_ne, which are exactly the composites appearing in
TauCeti.reflectionFunctor_map_app_self_apply and TauCeti.reflectionFunctor_map_app_of_ne.
Proof irrelevance makes them interchangeable with the transports written inline there.
As in the neighbouring files, a vertex i : Q is used both as an object of CategoryTheory.Paths
and as a vertex of TauCeti.Quiver.Reflect Q i, identifications that hold only by unfolding
semireducible definitions. Goals mentioning both are therefore not type-correct at the transparency
rw and simp build motives with, so every step that strips a conjugation by eqToHom is
factored through the general transport lemmas in TauCeti.CategoryTheory.EqToHom, which subst
the object equalities away before doing anything.
The linear section of the incoming sum used to build the preimage exists because a vector space is
projective; the private sinkSection is a choice of one. Nothing downstream depends on which
section is chosen: the private homSink_incomingSum pins the resulting map on the whole of Mᵢ,
and it is the only property of that map the proofs use.
References #
See Bernstein--Gelfand--Ponomarev, Coxeter functors and Gabriel's theorem, and Derksen--Weyman, An Introduction to Quiver Representations, Ch. 2.
Faithfulness #
The reflection functor at a sink is faithful on the representations whose incoming sum
there is onto. Two morphisms with the same reflection agree away from the sink, because reflection
leaves those components alone; at the sink they then agree on the range of the incoming sum, by
TauCeti.incomingSum_naturality, and that range is everything.
Fullness #
A morphism θ of reflected representations is taken apart into its components away from the sink
and the map it induces between the two kernels there, and those pieces are reassembled into a
morphism of the original representations.
Full faithfulness, and indecomposability #
The reflection functor at a sink is full on the representations whose incoming sum there is onto.
The reflection functor at a sink is fully faithful on the representations whose incoming
sum there is onto, a class that by TauCeti.incomingSum_surjective_of_indecomposable contains
every indecomposable representation other than the vertex simple Sᵢ.
Reflection preserves the dimension of the endomorphism space when the incoming sum at the sink is surjective.
The reflection functor at a sink reflects isomorphisms, between representations whose
incoming sums there are onto. Fullness produces morphisms f : M ⟶ N and g : N ⟶ M reflecting
to the two halves of the given isomorphism, and faithfulness turns the two triangle identities
downstairs into the two upstairs.
The reflection functor is not fully faithful on all of TauCeti.QuiverRep k Q -- it annihilates
the vertex simple at i -- so CategoryTheory.Functor.ReflectsIsomorphisms and the machinery
around it, which ask for Full and Faithful instances, do not apply, and the argument is made
directly from TauCeti.reflectionFunctor_map_surjective and
TauCeti.reflectionFunctor_map_injective.
Reflection at a sink preserves indecomposability, as soon as the sum of the arrows into the
sink is onto. Reflection is additive and bijective on the endomorphisms of M, so it matches the
idempotents of M with those of its reflection; an indecomposable has only the trivial ones, and
the reflection of the identity is the identity while the reflection of 0 is 0.
The vertex simple as the exceptional case #
As in TauCeti.RepresentationTheory.Quiver.Reflection.Indecomposable, a statement naming both a
reflected representation and the vertex simple has to put the quiver, its arrows and the field in
one universe.
Reflection at a sink carries an indecomposable representation other than the vertex simple
there to an indecomposable representation of the reflected quiver. The vertex simple Sᵢ is
genuinely excluded: reflection sends it to the zero representation, by
TauCeti.subsingleton_reflectRep_obj_self. Together with
TauCeti.dimVector_reflectRep_of_indecomposable, which computes the dimension vector of the result
as sᵢ · dim M under the additional hypothesis that the vertex spaces at the sources of the arrows
into i are finite-dimensional, this is the inductive step of the reflection-functor proof of
Gabriel's theorem.