Source reflection preserves indecomposability

The Bernstein--Gelfand--Ponomarev reflection C⁻ᵢ at a source i replaces Mᵢ by the cokernel of the outgoing map

Mᵢ → ∏_{a : i ⟶ b} M_b.

This file proves that source reflection is fully faithful on morphisms whose target has injective outgoing map. Faithfulness follows directly from naturality of the outgoing map. For fullness, a morphism of reflected representations determines the components away from i. Naturality along the reversed arrows says that their product map carries the range of the outgoing map of the source into the range for the target. A linear retraction of the target's injective outgoing map then recovers the missing component at i.

The finite-arrow hypothesis is essential to this argument: it lets a vector in the product be written as the sum of its coordinate vectors, so naturality along each reversed arrow determines the induced map on the whole quotient. This is automatic for the finite quivers used in Gabriel's theorem.

As a consequence, source reflection preserves indecomposability whenever the outgoing map is injective. This is the source-side reverse step needed to reconstruct indecomposables along an admissible reflection sequence.

Main results

• TauCeti.sourceReflectionFunctor_map_injective, TauCeti.sourceReflectionFunctor_map_surjective, and TauCeti.sourceReflectionFunctor_map_bijective: source reflection is fully faithful when the outgoing map of the target is injective.
• TauCeti.nonempty_iso_of_nonempty_iso_sourceReflectRep: source reflection reflects isomorphisms under injectivity of both outgoing maps.
• TauCeti.indecomposable_sourceReflectRep: source reflection preserves indecomposability when the outgoing map is injective.

Implementation notes

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, so a goal mentioning both is not type-correct at the transparency rw and simp build motives with. Every step that strips a conjugation by eqToHom is therefore factored through the general transport lemmas TauCeti.eq_of_eqToHom_conjugate and TauCeti.eqToHom_conjugate_vertical_square_of_horizontal_square of TauCeti.CategoryTheory.EqToHom, which subst the object equalities away in an abstract category, where no such identification is in play.

References

See Bernstein--Gelfand--Ponomarev, Coxeter functors and Gabriel's theorem, and Derksen--Weyman, An Introduction to Quiver Representations, Ch. 2. The formal template is the sink-side argument in TauCeti.RepresentationTheory.Quiver.Reflection.FullyFaithful.

Transport helpers

Faithfulness

theorem TauCeti.sourceReflectionFunctor_map_injective {k : Type u} {Q : Type v} [Field k] [Quiver Q] {M N : QuiverRep k Q} {i : Q} (hi : Quiver.IsSource i) (hinj : Function.Injective ⇑(outgoingMap N i)) : Function.Injective fun (η : M ⟶ N) => (sourceReflectionFunctor i hi).map η

Source reflection is faithful on morphisms whose target has injective outgoing map.

Fullness

Full faithfulness and indecomposability

theorem TauCeti.sourceReflectionFunctor_map_surjective {k : Type u} {Q : Type v} [Field k] [Quiver Q] {M N : QuiverRep k Q} {i : Q} (hi : Quiver.IsSource i) [Finite ((b : Q) × (i ⟶ b))] (hinj : Function.Injective ⇑(outgoingMap N i)) : Function.Surjective fun (η : M ⟶ N) => (sourceReflectionFunctor i hi).map η

Source reflection is full on morphisms whose target has injective outgoing map.

theorem TauCeti.sourceReflectionFunctor_map_bijective {k : Type u} {Q : Type v} [Field k] [Quiver Q] {M N : QuiverRep k Q} {i : Q} (hi : Quiver.IsSource i) [Finite ((b : Q) × (i ⟶ b))] (hinj : Function.Injective ⇑(outgoingMap N i)) : Function.Bijective fun (η : M ⟶ N) => (sourceReflectionFunctor i hi).map η

Source reflection is fully faithful on morphisms whose target has injective outgoing map.

theorem TauCeti.nonempty_iso_of_nonempty_iso_sourceReflectRep {k : Type u} {Q : Type v} [Field k] [Quiver Q] {M N : QuiverRep k Q} {i : Q} (hi : Quiver.IsSource i) [Finite ((b : Q) × (i ⟶ b))] (hinjM : Function.Injective ⇑(outgoingMap M i)) (hinjN : Function.Injective ⇑(outgoingMap N i)) (h : Nonempty (sourceReflectRep M hi ≅ sourceReflectRep N hi)) : Nonempty (M ≅ N)

Source reflection reflects isomorphisms when both outgoing maps are injective.

theorem TauCeti.indecomposable_sourceReflectRep {k : Type u} {Q : Type v} [Field k] [Quiver Q] {M : QuiverRep k Q} {i : Q} (hi : Quiver.IsSource i) [Finite ((b : Q) × (i ⟶ b))] (hM : CategoryTheory.Indecomposable M) (hinj : Function.Injective ⇑(outgoingMap M i)) : CategoryTheory.Indecomposable (sourceReflectRep M hi)

Reflection at a source preserves indecomposability when the outgoing map is injective.