The Coxeter functor

Reflecting a quiver at a sink reverses the arrows there, and the Bernstein-Gelfand-Ponomarev reflection functor C⁺ᵢ carries its representations to representations of the reflected quiver (TauCeti.reflectionFunctor). Reflecting at the successive entries of a sink-admissible list -- each entry a sink of the quiver its predecessors produce -- composes those functors, and along a sink-admissible ordering, a repetition-free list of all the vertices, the quiver comes back to itself (TauCeti.Quiver.reflectList_eq_self). The resulting endofunctor is the Coxeter functor of this file, TauCeti.coxeterFunctor, and on dimension vectors it realizes the Coxeter transformation TauCeti.vertexPreReflectionList of the ordering.

The identity dim (C⁺ M) = c · dim M is proved here for an indecomposable representation with finite-dimensional vertex spaces, with the zero representation as its alternative. The proof proceeds stagewise: away from the vertex simple at the current sink, reflection preserves indecomposability and transforms the dimension vector as predicted; at that vertex simple, reflection instead annihilates the representation (TauCeti.isZero_reflectRep). The corresponding dichotomy for indecomposables is supplied by TauCeti.incomingSum_surjective_or_forall_subsingleton.

Main definitions

• TauCeti.reflectionFunctorList: the composite of the reflection functors along a sink-admissible list, from the representations of q to those of TauCeti.Quiver.reflectList q l.
• TauCeti.coxeterFunctor: the Coxeter functor C⁺ of a sink-admissible ordering, an endofunctor of the representations of q.

Main results

• TauCeti.reflectionFunctorList_nil, TauCeti.reflectionFunctorList_cons and TauCeti.reflectionFunctorList_cons_obj: the composite is the identity on the empty list and peels off one reflection functor -- on objects, one TauCeti.reflectRep -- at a time.
• TauCeti.isZero_reflectionFunctorList_obj and TauCeti.isZero_coxeterFunctor_obj: the zero representation is carried to the zero representation.
• TauCeti.isFinDim_reflectionFunctorList_obj and TauCeti.isFinDim_coxeterFunctor_obj: pointwise finite-dimensional vertex spaces stay finite-dimensional.
• TauCeti.isZero_coxeterFunctor_obj_iff_isZero_reflectionFunctorList_obj and TauCeti.nonempty_iso_coxeterFunctor_obj_iff_nonempty_iso_reflectionFunctorList_obj: the Coxeter functor and the composite it transports annihilate the same representations and identify the same pairs of them, so a statement about the endofunctor may be proved one reflection at a time.
• TauCeti.indecomposable_and_dimVector_reflectionFunctorList_or_isZero and TauCeti.indecomposable_and_dimVector_coxeterFunctor_or_isZero: the dichotomy above, for a general sink-admissible list and for the Coxeter functor.
• TauCeti.titsForm_dimVector_coxeterFunctor_obj: the Coxeter functor preserves the Tits form of the dimension vector of an indecomposable representation it does not annihilate.

Implementation notes

The quiver structure is carried as an explicit argument rather than as an instance, because the recursion changes it: the vertex type is fixed and the arrows are reversed, so the recursion is on the Quiver structure TauCeti.Quiver.reflectAt, not on a type synonym like TauCeti.Quiver.Reflect, whose iteration would change the type at each step and so leave the range of structural recursion. The instance TauCeti.Quiver.instFintypeReflectHom carries arrow-finiteness along with it.

A consequence is that two Quiver structures on one vertex type occur in the same statement, and the one in scope as a local instance is not always the intended one. Every statement below therefore supplies the structure explicitly to TauCeti.dimVector, TauCeti.titsForm and TauCeti.vertexPreReflectionList; vanishing is stated as CategoryTheory.Limits.IsZero of the representation rather than vertexwise, since the vertexwise form would need the structure supplied to CategoryTheory.Functor.obj as well.

The Coxeter functor is the composite transported along TauCeti.Quiver.reflectList_eq_self, an equality of Quiver structures; TauCeti.coxeterFunctor_def exposes this characterization while the auxiliary transport construction remains private.

The sink-admissible ordering is an argument of TauCeti.coxeterFunctor rather than something chosen from TauCeti.Quiver.IsAcyclic.exists_isSinkAdmissible: the Coxeter transformation the functor realizes depends on the ordering, so a consumer that needs to name it must be able to name the ordering too.

References

See Bernstein--Gelfand--Ponomarev, Coxeter functors and Gabriel's theorem, and Assem--Simson--Skowroński, Elements of the Representation Theory of Associative Algebras I, VII.5.

The composite of the reflection functors along a sink-admissible list

noncomputable def TauCeti.reflectionFunctorList (k : Type u) {V : Type v} [fld : Field k] [fV : Fintype V] (l : List V) (q : Quiver V) (_hq : (a b : V) → Fintype (a ⟶ b)) : Quiver.IsSinkAdmissible q l → CategoryTheory.Functor (QuiverRep k V) (QuiverRep k V)

The composite of the reflection functors along a sink-admissible list. Each entry of the list is a sink of the quiver its predecessors produce, so the reflection functors at the successive entries compose; the result carries the representations of q to those of TauCeti.Quiver.reflectList q l.

The quiver structure is an explicit argument rather than an instance because it is what the recursion moves: the vertex type stays fixed while the arrows are reversed.

@[simp]

theorem TauCeti.reflectionFunctorList_nil {k : Type u} {V : Type v} [fld : Field k] [fV : Fintype V] (q : Quiver V) (hq : (a b : V) → Fintype (a ⟶ b)) (hl : Quiver.IsSinkAdmissible q []) : reflectionFunctorList k [] q hq hl = CategoryTheory.Functor.id (QuiverRep k V)

@[simp]

theorem TauCeti.reflectionFunctorList_cons {k : Type u} {V : Type v} [fld : Field k] [fV : Fintype V] (i : V) (l : List V) (q : Quiver V) (hq : (a b : V) → Fintype (a ⟶ b)) (hl : Quiver.IsSinkAdmissible q (i :: l)) : reflectionFunctorList k (i :: l) q hq hl = (reflectionFunctor i ⋯).comp (reflectionFunctorList k l (Quiver.reflectAt q i) (Quiver.instFintypeReflectHom i) ⋯)

theorem TauCeti.reflectionFunctorList_cons_obj {k : Type u} {V : Type v} [fld : Field k] [fV : Fintype V] (i : V) (l : List V) (q : Quiver V) (hq : (a b : V) → Fintype (a ⟶ b)) (hl : Quiver.IsSinkAdmissible q (i :: l)) (M : QuiverRep k V) : (reflectionFunctorList k (i :: l) q hq hl).obj M = (reflectionFunctorList k l (Quiver.reflectAt q i) (Quiver.instFintypeReflectHom i) ⋯).obj (reflectRep M ⋯)

The composite along a cons, on objects. The first stage is TauCeti.reflectRep by TauCeti.reflectionFunctor_obj, so the composite along i :: l is the composite along l evaluated at the reflected representation. This is the step every stagewise induction along a sink-admissible list opens with.

theorem TauCeti.isZero_reflectionFunctorList_obj {k : Type u} {V : Type v} [fld : Field k] [fV : Fintype V] (l : List V) (q : Quiver V) (hq : (a b : V) → Fintype (a ⟶ b)) (hl : Quiver.IsSinkAdmissible q l) (M : QuiverRep k V) : CategoryTheory.Limits.IsZero M → CategoryTheory.Limits.IsZero ((reflectionFunctorList k l q hq hl).obj M)

A composite of reflections annihilates the zero representation. Only the vanishing of the vertex spaces is used at each stage, through TauCeti.isZero_reflectRep.

theorem TauCeti.isFinDim_reflectionFunctorList_obj {k : Type u} {V : Type v} [fld : Field k] [fV : Fintype V] (l : List V) (q : Quiver V) (hq : (a b : V) → Fintype (a ⟶ b)) (hl : Quiver.IsSinkAdmissible q l) (M : QuiverRep k V) : IsFinDim k V M → IsFinDim k V ((reflectionFunctorList k l q hq hl).obj M)

A composite of reflections preserves pointwise finite-dimensionality. Each stage is TauCeti.finiteDimensional_reflectRep_obj; carrying this along the composite is what lets a later stage apply the dimension-vector identities, which need finite-dimensional vertex spaces.

The action on an indecomposable representation

theorem TauCeti.indecomposable_and_dimVector_reflectionFunctorList_or_isZero {k : Type u} {V : Type v} [fld : Field k] [fV : Fintype V] [DecidableEq V] (l : List V) (q : Quiver V) (hq : (a b : V) → Fintype (a ⟶ b)) (hl : Quiver.IsSinkAdmissible q l) (M : QuiverRep k V) : CategoryTheory.Indecomposable M → (∀ (a : V), FiniteDimensional k ↑(M.obj a)) → (CategoryTheory.Indecomposable ((reflectionFunctorList k l q hq hl).obj M) ∧ (fun (j : V) => ↑(dimVector ((reflectionFunctorList k l q hq hl).obj M) j)) = (vertexPreReflectionList V l) fun (j : V) => ↑(dimVector M j)) ∨ CategoryTheory.Limits.IsZero ((reflectionFunctorList k l q hq hl).obj M)

A composite of reflection functors on an indecomposable representation. Either the composite is again indecomposable, and then its dimension vector is the corresponding product of simple reflections applied to the dimension vector of M, or the composite is the zero representation.

The proof runs the dichotomy TauCeti.incomingSum_surjective_or_forall_subsingleton at each stage: a stage meeting the vertex simple at its own sink annihilates the representation (TauCeti.isZero_reflectRep), which is what lands in the second branch, while every other stage preserves indecomposability and reflects the dimension vector. Both branches occur -- the vertex simple at the first entry falls into the second. The simple reflections on the right are those of the original quiver, by TauCeti.vertexPreReflectionList_reflectAt, even though the successive stages act on successively reflected quivers.

The Coxeter functor

noncomputable def TauCeti.coxeterFunctor (k : Type u) {V : Type v} [fld : Field k] [Fintype V] (q : Quiver V) (hq : (a b : V) → Fintype (a ⟶ b)) {l : List V} (hnd : l.Nodup) (hall : ∀ (v : V), v ∈ l) (hl : Quiver.IsSinkAdmissible q l) : CategoryTheory.Functor (QuiverRep k V) (QuiverRep k V)

The Coxeter functor C⁺: the composite of the Bernstein-Gelfand-Ponomarev reflection functors at the successive vertices of a sink-admissible ordering of the vertices -- a sink-admissible list that repeats no vertex and contains every one of them. Reflecting once at every vertex restores the quiver structure (TauCeti.Quiver.reflectList_eq_self), so unlike a general composite of reflection functors this is an endofunctor of the representations of q.

Every finite acyclic quiver has such an ordering, by TauCeti.Quiver.IsAcyclic.exists_isSinkAdmissible; the ordering is an argument rather than a choice, since the Coxeter transformation it realizes on dimension vectors, TauCeti.vertexPreReflectionList, depends on it.

theorem TauCeti.coxeterFunctor_def {k : Type u} {V : Type v} [fld : Field k] [fV : Fintype V] (q : Quiver V) (hq : (a b : V) → Fintype (a ⟶ b)) {l : List V} (hnd : l.Nodup) (hall : ∀ (v : V), v ∈ l) (hl : Quiver.IsSinkAdmissible q l) : coxeterFunctor k q hq hnd hall hl = ⋯.mp (reflectionFunctorList k l q hq hl)

The Coxeter functor is the reflection-functor composite transported along the equality between the iteratively reflected quiver and the original quiver.

theorem TauCeti.finrank_end_coxeterFunctor_obj {k : Type u} {V : Type v} [fld : Field k] [fV : Fintype V] (q : Quiver V) (hq : (a b : V) → Fintype (a ⟶ b)) {l : List V} (hnd : l.Nodup) (hall : ∀ (v : V), v ∈ l) (hl : Quiver.IsSinkAdmissible q l) (M : QuiverRep k V) : Module.finrank k (CategoryTheory.End ((coxeterFunctor k q hq hnd hall hl).obj M)) = Module.finrank k (CategoryTheory.End ((reflectionFunctorList k l q hq hl).obj M))

Transporting the reflection-functor composite back to the original quiver preserves the dimension of its endomorphism space.

theorem TauCeti.dimVector_coxeterFunctor_obj {k : Type u} {V : Type v} [fld : Field k] [fV : Fintype V] (q : Quiver V) (hq : (a b : V) → Fintype (a ⟶ b)) {l : List V} (hnd : l.Nodup) (hall : ∀ (v : V), v ∈ l) (hl : Quiver.IsSinkAdmissible q l) (M : QuiverRep k V) : dimVector ((coxeterFunctor k q hq hnd hall hl).obj M) = dimVector ((reflectionFunctorList k l q hq hl).obj M)

Transporting the reflection-functor composite back to the original quiver does not change its dimension vector.

theorem TauCeti.intCast_dimVector_coxeterFunctor_obj {k : Type u} {V : Type v} [fld : Field k] [fV : Fintype V] (q : Quiver V) (hq : (a b : V) → Fintype (a ⟶ b)) {l : List V} (hnd : l.Nodup) (hall : ∀ (v : V), v ∈ l) (hl : Quiver.IsSinkAdmissible q l) (M : QuiverRep k V) : (fun (j : V) => ↑(dimVector ((coxeterFunctor k q hq hnd hall hl).obj M) j)) = fun (j : V) => ↑(dimVector ((reflectionFunctorList k l q hq hl).obj M) j)

Transporting the reflection-functor composite back to the original quiver does not change its dimension vector after coercion to integers.

theorem TauCeti.isFinDim_coxeterFunctor_obj {k : Type u} {V : Type v} [fld : Field k] [fV : Fintype V] (q : Quiver V) (hq : (a b : V) → Fintype (a ⟶ b)) {l : List V} (hnd : l.Nodup) (hall : ∀ (v : V), v ∈ l) (hl : Quiver.IsSinkAdmissible q l) (M : QuiverRep k V) (hfd : IsFinDim k V M) : IsFinDim k V ((coxeterFunctor k q hq hnd hall hl).obj M)

The Coxeter functor preserves pointwise finite-dimensionality, since the composite of the reflection functors it transports does.

theorem TauCeti.isZero_coxeterFunctor_obj_iff_isZero_reflectionFunctorList_obj {k : Type u} {V : Type v} [fld : Field k] [fV : Fintype V] (q : Quiver V) (hq : (a b : V) → Fintype (a ⟶ b)) {l : List V} (hnd : l.Nodup) (hall : ∀ (v : V), v ∈ l) (hl : Quiver.IsSinkAdmissible q l) (M : QuiverRep k V) : CategoryTheory.Limits.IsZero ((coxeterFunctor k q hq hnd hall hl).obj M) ↔ CategoryTheory.Limits.IsZero ((reflectionFunctorList k l q hq hl).obj M)

The Coxeter functor annihilates a representation exactly when the reflection-functor composite along the ordering does. The two differ only by the transport of the codomain along TauCeti.Quiver.reflectList_eq_self, so this is what lets a statement about the endofunctor be proved one reflection at a time.

theorem TauCeti.nonempty_iso_coxeterFunctor_obj_iff_nonempty_iso_reflectionFunctorList_obj {k : Type u} {V : Type v} [fld : Field k] [fV : Fintype V] (q : Quiver V) (hq : (a b : V) → Fintype (a ⟶ b)) {l : List V} (hnd : l.Nodup) (hall : ∀ (v : V), v ∈ l) (hl : Quiver.IsSinkAdmissible q l) (M N : QuiverRep k V) : Nonempty ((coxeterFunctor k q hq hnd hall hl).obj M ≅ (coxeterFunctor k q hq hnd hall hl).obj N) ↔ Nonempty ((reflectionFunctorList k l q hq hl).obj M ≅ (reflectionFunctorList k l q hq hl).obj N)

The Coxeter functor identifies two representations exactly when the reflection-functor composite along the ordering does. Like TauCeti.isZero_coxeterFunctor_obj_iff_isZero_reflectionFunctorList_obj, this only undoes the transport of the codomain, so that an isomorphism of Coxeter images may be descended one reflection at a time.

theorem TauCeti.isZero_coxeterFunctor_obj {k : Type u} {V : Type v} [fld : Field k] [fV : Fintype V] (q : Quiver V) (hq : (a b : V) → Fintype (a ⟶ b)) {l : List V} (hnd : l.Nodup) (hall : ∀ (v : V), v ∈ l) (hl : Quiver.IsSinkAdmissible q l) (M : QuiverRep k V) (hM : CategoryTheory.Limits.IsZero M) : CategoryTheory.Limits.IsZero ((coxeterFunctor k q hq hnd hall hl).obj M)

The Coxeter functor annihilates the zero representation.

theorem TauCeti.indecomposable_and_dimVector_coxeterFunctor_or_isZero {k : Type u} {V : Type v} [fld : Field k] [fV : Fintype V] [DecidableEq V] (q : Quiver V) (hq : (a b : V) → Fintype (a ⟶ b)) {l : List V} (hnd : l.Nodup) (hall : ∀ (v : V), v ∈ l) (hl : Quiver.IsSinkAdmissible q l) (M : QuiverRep k V) (hM : CategoryTheory.Indecomposable M) (hfd : ∀ (a : V), FiniteDimensional k ↑(M.obj a)) : (CategoryTheory.Indecomposable ((coxeterFunctor k q hq hnd hall hl).obj M) ∧ (fun (j : V) => ↑(dimVector ((coxeterFunctor k q hq hnd hall hl).obj M) j)) = (vertexPreReflectionList V l) fun (j : V) => ↑(dimVector M j)) ∨ CategoryTheory.Limits.IsZero ((coxeterFunctor k q hq hnd hall hl).obj M)

The Coxeter functor on an indecomposable representation. Either it is again indecomposable, with dimension vector the Coxeter transformation TauCeti.vertexPreReflectionList of the ordering applied to the dimension vector of M, or it is the zero representation. This is the statement dim (C⁺ M) = c · dim M for the Coxeter element c, with the boundary case named.

theorem TauCeti.titsForm_dimVector_coxeterFunctor_obj {k : Type u} {V : Type v} [fld : Field k] [fV : Fintype V] (q : Quiver V) (hq : (a b : V) → Fintype (a ⟶ b)) {l : List V} (hnd : l.Nodup) (hall : ∀ (v : V), v ∈ l) (hl : Quiver.IsSinkAdmissible q l) (M : QuiverRep k V) (hM : CategoryTheory.Indecomposable M) (hfd : ∀ (a : V), FiniteDimensional k ↑(M.obj a)) (hne : ¬CategoryTheory.Limits.IsZero ((coxeterFunctor k q hq hnd hall hl).obj M)) : ((titsForm V) fun (j : V) => ↑(dimVector ((coxeterFunctor k q hq hnd hall hl).obj M) j)) = (titsForm V) fun (j : V) => ↑(dimVector M j)

The Coxeter functor preserves the Tits form of the dimension vector. The Tits form is unchanged by a simple reflection at a loopless vertex, hence by the whole Coxeter transformation (TauCeti.titsForm_vertexPreReflectionList), and no vertex of a repetition-free sink-admissible list carries a loop (TauCeti.Quiver.IsSinkAdmissible.isEmpty_hom_self). So on an indecomposable representation the Coxeter functor either annihilates it or leaves the Tits form of its dimension vector alone. This preserved invariant feeds the finite-orbit descent theorem TauCeti.exists_vertexPreReflectionList_pow_apply_neg, which forces a nonzero dimension vector out of the nonnegative cone after finitely many Coxeter passes.