Composites of source reflection functors

A list is source-admissible when each vertex is a source after reflecting at the preceding vertices. Source reflection functors therefore compose along such a list. This file constructs that composite and proves that it preserves finite-dimensional indecomposables whenever the successive reflected dimension vectors stay nonnegative.

The reverse of a sink-admissible list is source-admissible for the quiver obtained after the sink reflections. This is the direction needed to reconstruct a quiver representation from a simple representation in the reflection induction for Gabriel's theorem.

Main definition

• TauCeti.sourceReflectionFunctorList: the composite of source reflection functors along a source-admissible list.

Main results

• TauCeti.sourceReflectionFunctorList_nil, TauCeti.sourceReflectionFunctorList_cons and TauCeti.sourceReflectionFunctorList_cons_obj: the composite is the identity on the empty list and peels off one source reflection at a time.
• TauCeti.isFinDim_sourceReflectionFunctorList_obj: the composite preserves pointwise finite-dimensionality, without a nonnegativity hypothesis.
• TauCeti.indecomposable_and_dimVector_sourceReflectionFunctorList: if all successive reflected dimension vectors are nonnegative, the composite preserves indecomposability and realizes the corresponding product of simple reflections on dimension vectors.

References

See Bernstein--Gelfand--Ponomarev, Coxeter functors and Gabriel's theorem, and Derksen--Weyman, An Introduction to Quiver Representations, Ch. 2. The source-reflection construction here is dual to the sink-reflection composite TauCeti.reflectionFunctorList in TauCeti.RepresentationTheory.Quiver.Reflection.Composite.

The composite along a source-admissible list

noncomputable def TauCeti.sourceReflectionFunctorList (k : Type u) {V : Type v} [fld : Field k] (l : List V) (q : Quiver V) : Quiver.IsSourceAdmissible q l → CategoryTheory.Functor (QuiverRep k V) (QuiverRep k V)

The composite of the source reflection functors along a source-admissible list. It sends representations of q to representations of the quiver obtained by reflecting successively at the entries of l.

@[simp]

theorem TauCeti.sourceReflectionFunctorList_nil {k : Type u} {V : Type v} [fld : Field k] (q : Quiver V) (hl : Quiver.IsSourceAdmissible q []) : sourceReflectionFunctorList k [] q hl = CategoryTheory.Functor.id (QuiverRep k V)

@[simp]

theorem TauCeti.sourceReflectionFunctorList_cons {k : Type u} {V : Type v} [fld : Field k] (i : V) (l : List V) (q : Quiver V) (hl : Quiver.IsSourceAdmissible q (i :: l)) : sourceReflectionFunctorList k (i :: l) q hl = (sourceReflectionFunctor i ⋯).comp (sourceReflectionFunctorList k l (Quiver.reflectAt q i) ⋯)

theorem TauCeti.sourceReflectionFunctorList_cons_obj {k : Type u} {V : Type v} [fld : Field k] (i : V) (l : List V) (q : Quiver V) (hl : Quiver.IsSourceAdmissible q (i :: l)) (M : QuiverRep k V) : (sourceReflectionFunctorList k (i :: l) q hl).obj M = (sourceReflectionFunctorList k l (Quiver.reflectAt q i) ⋯).obj (sourceReflectRep M ⋯)

The composite along a nonempty source-admissible list first source-reflects at its head.

theorem TauCeti.isFinDim_sourceReflectionFunctorList_obj {k : Type u} {V : Type v} [fld : Field k] [Finite V] (l : List V) (q : Quiver V) (_hq : (a b : V) → Fintype (a ⟶ b)) (hl : Quiver.IsSourceAdmissible q l) (M : QuiverRep k V) : IsFinDim k V M → IsFinDim k V ((sourceReflectionFunctorList k l q hl).obj M)

Source-reflection composites preserve pointwise finite-dimensionality.

Indecomposability and dimension vectors

theorem TauCeti.indecomposable_and_dimVector_sourceReflectionFunctorList {K : Type u} {W : Type v} [fldK : Field K] [fW : Fintype W] [DecidableEq W] (l : List W) (q : Quiver W) (hq : (a b : W) → Fintype (a ⟶ b)) (hl : Quiver.IsSourceAdmissible q l) (M : QuiverRep K W) : CategoryTheory.Indecomposable M → (∀ (a : W), FiniteDimensional K ↑(M.obj a)) → (∀ r < l.length, 0 ≤ (vertexPreReflectionList W (List.take (r + 1) l)) fun (j : W) => ↑(dimVector M j)) → CategoryTheory.Indecomposable ((sourceReflectionFunctorList K l q hl).obj M) ∧ (fun (j : W) => ↑(dimVector ((sourceReflectionFunctorList K l q hl).obj M) j)) = (vertexPreReflectionList W l) fun (j : W) => ↑(dimVector M j)

A source-reflection composite reconstructs an indecomposable along a nonnegative reflection word. If M is an indecomposable with finite-dimensional vertex spaces and the image of its dimension vector after every nonempty prefix of the source-admissible word is nonnegative, then the final representation is indecomposable and its dimension vector is the product of the simple reflections along the word applied to dimVector M.