Reflecting an indecomposable representation at a source

The Bernstein--Gelfand--Ponomarev reflection at a source i replaces the vertex space Mᵢ by the cokernel of the map TauCeti.outgoingMap collecting the arrows out of i. It acts on dimension vectors by the simple reflection sᵢ, and preserves indecomposability, whenever that map is injective (TauCeti.dimVector_sourceReflectRep, TauCeti.indecomposable_sourceReflectRep). This file discharges that hypothesis: the map out of a source is injective for every indecomposable representation except the vertex simple Sᵢ, which is the representation the reflection annihilates.

This is the mirror of the sink-side argument in TauCeti.RepresentationTheory.Quiver.Reflection.Indecomposable, and it reuses that file's construction rather than repeating it. A linear endomorphism π of Mᵢ extends by the identity at the other vertices to an endomorphism TauCeti.vertexEnd of M as soon as the paths through i do not see it; at a source, no path arrives at i from elsewhere, so only the condition on the paths leaving i has content, and it follows from the condition on the arrows leaving i because such a path begins with one. An indecomposable representation admits no idempotent endomorphism but 0 and the identity, so an idempotent π of this kind is 0 or the identity (TauCeti.sourceIdempotent_eq_id_or_eq_zero_of_indecomposable). Applied to the projection onto a complement of the kernel of the outgoing map, this says the kernel vanishes unless M vanishes away from i, in which case M is Sᵢ.

Main results

• TauCeti.sourceIdempotent_eq_id_or_eq_zero_of_indecomposable: an idempotent of Mᵢ that every arrow out of a source i of an indecomposable M does not see is the identity, or is zero and M vanishes away from i.
• TauCeti.outgoingMap_injective_or_forall_subsingleton: hence the map collecting the arrows out of a source is injective, unless the representation is concentrated there.
• TauCeti.outgoingMap_injective_of_vertexPreReflection_nonneg: nonnegativity of the reflected dimension vector forces that outgoing map to be injective.
• TauCeti.outgoingMap_injective_of_indecomposable: the map collecting the arrows out of a source is injective for every indecomposable representation not isomorphic to the vertex simple there.
• TauCeti.not_nonempty_iso_simpleRep_of_vertexPreReflection_nonneg: the exceptional case is detected numerically, by the simple reflection driving the dimension vector negative.
• TauCeti.dimVector_sourceReflectRep_of_indecomposable and TauCeti.indecomposable_sourceReflectRep_of_not_nonempty_iso_simpleRep: consequently reflection at a source carries such a representation to an indecomposable one, whose dimension vector is the simple reflection of the old one.

Implementation notes

As in the sink-side file, 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: the vertex spaces of a reflected representation are cut out of a product indexed by the arrows, while Sᵢ puts the field itself at i.

References

See Bernstein--Gelfand--Ponomarev, Coxeter functors and Gabriel's theorem, and Derksen--Weyman, An Introduction to Quiver Representations, Ch. 2.

Idempotents at a source of an indecomposable representation

theorem TauCeti.sourceIdempotent_eq_id_or_eq_zero_of_indecomposable {k : Type u} {Q : Type v} [Field k] [Quiver Q] {M : QuiverRep k Q} {i : Q} (hi : Quiver.IsSource i) (hM : CategoryTheory.Indecomposable M) (π : ↑(M.obj i) →ₗ[k] ↑(M.obj i)) (hπ : ∀ (b : Q) (e : i ⟶ b) (y : ↑(M.obj i)), (ModuleCat.Hom.hom (M.map e.toPath)) (π y) = (ModuleCat.Hom.hom (M.map e.toPath)) y) (hidem : IsIdempotentElem π) : π = LinearMap.id ∨ π = 0 ∧ ∀ (a : Q), a ≠ i → Subsingleton ↑(M.obj a)

An idempotent at a source of an indecomposable representation is trivial. Let i be a source of Q and M an indecomposable representation. An idempotent endomorphism of Mᵢ that every arrow out of i composes away is either the identity, or zero; in the second case M vanishes away from i.

The injectivity of the outgoing map

theorem TauCeti.outgoingMap_injective_or_forall_subsingleton {k : Type u} {Q : Type v} [Field k] [Quiver Q] {M : QuiverRep k Q} {i : Q} (hi : Quiver.IsSource i) (hM : CategoryTheory.Indecomposable M) : Function.Injective ⇑(outgoingMap M i) ∨ ∀ (a : Q), a ≠ i → Subsingleton ↑(M.obj a)

The map collecting the arrows out of a source of an indecomposable representation is injective, unless the representation is concentrated at that source. This is the injectivity hypothesis of TauCeti.dimVector_sourceReflectRep, discharged: the kernel of the outgoing map is a direct summand of Mᵢ, so a nonzero kernel would split M, and the only splitting an indecomposable representation admits leaves nothing outside the source.

Injectivity from a nonnegative reflected dimension vector

theorem TauCeti.outgoingMap_injective_of_vertexPreReflection_nonneg {k : Type u} {Q : Type v} [Field k] [Quiver Q] {M : QuiverRep k Q} {i : Q} [Fintype Q] [(a b : Q) → Fintype (a ⟶ b)] [DecidableEq Q] (hi : Quiver.IsSource i) (hM : CategoryTheory.Indecomposable M) (h : 0 ≤ (vertexPreReflection Q i) fun (j : Q) => ↑(dimVector M j)) : Function.Injective ⇑(outgoingMap M i)

A nonnegative reflected dimension vector forces the outgoing map to be injective. For an indecomposable representation M and a source i, if the dimension vector of M reflected at i is nonnegative, then the outgoing map of M at i is injective.

The vertex simple as the exceptional case

theorem TauCeti.outgoingMap_injective_of_indecomposable {k Q : Type u} [Field k] [Quiver Q] {M : QuiverRep k Q} {i : Q} (hi : Quiver.IsSource i) (hM : CategoryTheory.Indecomposable M) (hne : ¬Nonempty (M ≅ simpleRep k Q i)) : Function.Injective ⇑(outgoingMap M i)

The map collecting the arrows out of a source is injective for every indecomposable representation other than the vertex simple there. The vertex simple Sᵢ is genuinely excluded, by TauCeti.outgoingMap_not_injective.

theorem TauCeti.indecomposable_sourceReflectRep_of_not_nonempty_iso_simpleRep {k Q : Type u} [Field k] [Quiver Q] {M : QuiverRep k Q} {i : Q} [Finite ((b : Q) × (i ⟶ b))] (hi : Quiver.IsSource i) (hM : CategoryTheory.Indecomposable M) (hne : ¬Nonempty (M ≅ simpleRep k Q i)) : CategoryTheory.Indecomposable (sourceReflectRep M hi)

Reflection at a source carries an indecomposable representation other than the vertex simple there to an indecomposable representation of the reflected quiver. Together with TauCeti.dimVector_sourceReflectRep_of_indecomposable, which computes the dimension vector of the result as sᵢ · dim M under the additional hypothesis that the vertex spaces at the targets of the arrows out of i are finite-dimensional, this is the step that rebuilds an indecomposable along a reflection sequence, dual to TauCeti.indecomposable_reflectRep_of_not_nonempty_iso_simpleRep.

theorem TauCeti.dimVector_sourceReflectRep_of_indecomposable {k Q : Type u} [Field k] [Quiver Q] {M : QuiverRep k Q} {i : Q} [Fintype Q] [(a b : Q) → Fintype (a ⟶ b)] [DecidableEq Q] (hi : Quiver.IsSource i) (hM : CategoryTheory.Indecomposable M) (hne : ¬Nonempty (M ≅ simpleRep k Q i)) (hfin : ∀ (e : (b : Q) × (i ⟶ b)), FiniteDimensional k ↑(M.obj e.fst)) : (fun (j : Q) => ↑(dimVector (sourceReflectRep M hi) j)) = (vertexPreReflection Q i) fun (j : Q) => ↑(dimVector M j)

Reflection at a source acts on the dimension vector of an indecomposable representation by the simple reflection there, unless that representation is the vertex simple at the source.

theorem TauCeti.not_nonempty_iso_simpleRep_of_vertexPreReflection_nonneg {k Q : Type u} [Field k] [Quiver Q] {M : QuiverRep k Q} {i : Q} [Fintype Q] [(a b : Q) → Fintype (a ⟶ b)] [DecidableEq Q] (hloop : IsEmpty (i ⟶ i)) (h : 0 ≤ (vertexPreReflection Q i) fun (j : Q) => ↑(dimVector M j)) : ¬Nonempty (M ≅ simpleRep k Q i)

A representation whose dimension vector the simple reflection keeps nonnegative is not the vertex simple. The dimension vector of Sᵢ is the simple dimension vector αᵢ, which the reflection at a loopless vertex i negates. This universe-aligned comparison with Sᵢ complements TauCeti.outgoingMap_injective_of_vertexPreReflection_nonneg, the general-universe injectivity result used by the reflection induction.