Reflecting a representation at a source

This file constructs the source-side Bernstein--Gelfand--Ponomarev reflection functor. For a source i, the linear map

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

collects the actions of all arrows leaving i. The reflected representation agrees with M away from i, replaces Mᵢ by the cokernel of this map, and lets a reversed arrow act by inserting its coordinate and passing to the quotient. The construction is functorial because a morphism of representations gives a commuting square of outgoing maps.

The target is the product over the arrows leaving i, not a direct sum: a linear map into a direct sum must produce finitely supported families, which need not hold when infinitely many arrows leave i, whereas the arrow actions always assemble into a map to the product. Over a finite quiver the product and direct sum agree by DirectSum.linearEquivFunOnFintype, so TauCeti.outgoingMap is then the direct-sum map Mᵢ → ⨁_{a : i ⟶ b} M_b of the BGP construction. The arrow-count and dimension-vector results below therefore carry the relevant finiteness hypotheses.

When the outgoing map is injective, the quotient dimension is the simple reflection of the old dimension vector. This is the dual of the surjectivity condition on TauCeti.incomingSum in the sink-side construction.

Main definitions

• TauCeti.outgoingMap: the map collecting all arrows out of a vertex.
• TauCeti.sourceReflectRep: reflection of a representation at a source.
• TauCeti.sourceReflectionFunctor: the BGP reflection functor at a source.

Main results

• TauCeti.sourceReflectRep_obj_self and TauCeti.sourceReflectRep_obj_of_ne compute the vertex spaces.
• TauCeti.sourceReflectRep_map_reflectArrowSource computes the action of a reversed arrow.
• TauCeti.sourceReflectionFunctor_map_app_self_mk computes reflection on morphisms at the reflected vertex.
• TauCeti.sourceReflectionFunctor_additive records that source reflection is additive.
• TauCeti.outgoingMap_not_injective shows that the injectivity hypothesis below is not automatic: it fails at the vertex simple.
• TauCeti.dimVector_sourceReflectRep identifies the new dimension vector with the simple reflection when the outgoing map is injective.
• TauCeti.finiteDimensional_sourceReflectRep_obj shows that source reflection preserves finite-dimensional vertex spaces.

References

See Bernstein--Gelfand--Ponomarev, Coxeter functors and Gabriel's theorem, and Derksen--Weyman, An Introduction to Quiver Representations, Ch. 2. The formal template for this dual construction is the sink-side API in TauCeti.RepresentationTheory.Quiver.Reflection.Representation, especially TauCeti.incomingSum, TauCeti.reflectRep, and TauCeti.reflectionFunctor.

The outgoing map

noncomputable def TauCeti.outgoingMap {k : Type u} {Q : Type v} [Field k] [Quiver Q] (M : QuiverRep k Q) (i : Q) : ↑(M.obj i) →ₗ[k] (e : (b : Q) × (i ⟶ b)) → ↑(M.obj e.fst)

The map collecting the arrows out of a vertex. Its coordinate at e : i ⟶ b is the action of e, so this is the product of the arrow actions over the arrows leaving i; for a finite quiver that product is the direct sum of the BGP construction. No hypothesis on i is imposed: the map is defined at every vertex, and it is the reflection that needs i to be a source. Its range is quotiented out in TauCeti.sourceReflectRep.

@[simp]

theorem TauCeti.outgoingMap_apply {k : Type u} {Q : Type v} [Field k] [Quiver Q] (M : QuiverRep k Q) (i : Q) (y : ↑(M.obj i)) (e : (b : Q) × (i ⟶ b)) : (outgoingMap M i) y e = (ModuleCat.Hom.hom (M.map e.snd.toPath)) y

The coordinate of TauCeti.outgoingMap at an arrow is the action of that arrow.

theorem TauCeti.outgoingMap_not_injective {k : Type u} {Q : Type v} [Field k] [Quiver Q] (M : QuiverRep k Q) (i : Q) (h : ∀ (b : Q) (a : i ⟶ b), Subsingleton ↑(M.obj b)) (hne : Nontrivial ↑(M.obj i)) : ¬Function.Injective ⇑(outgoingMap M i)

The map collecting the arrows out of i need not be injective. It fails to be whenever every vertex space at the target of an arrow out of i vanishes while the space at i does not, which is what the vertex simple Sᵢ does at a source: no arrow out of a source is a loop, so Sᵢ vanishes at every target of such an arrow. This is why the injectivity hypothesis of TauCeti.dimVector_sourceReflectRep cannot be dropped.

theorem TauCeti.finrank_pi_outgoing {k : Type u} {Q : Type v} [Field k] [Quiver Q] [Fintype Q] [(a b : Q) → Fintype (a ⟶ b)] (M : QuiverRep k Q) (i : Q) (hM : ∀ (e : (b : Q) × (i ⟶ b)), FiniteDimensional k ↑(M.obj e.fst)) : Module.finrank k ((e : (b : Q) × (i ⟶ b)) → ↑(M.obj e.fst)) = ∑ b : Q, Fintype.card (i ⟶ b) * Module.finrank k ↑(M.obj b)

The target of TauCeti.outgoingMap has dimension ∑_b #(i ⟶ b) · dim M_b.

The reflected representation and functor

noncomputable def TauCeti.sourceReflectRep {k : Type u} {Q : Type v} [Field k] [Quiver Q] (M : QuiverRep k Q) {i : Q} (hi : Quiver.IsSource i) : QuiverRep k (Quiver.Reflect Q i)

The reflection of a representation at a source i. It agrees with M away from i and puts the cokernel of TauCeti.outgoingMap M i at i.

@[simp]

theorem TauCeti.sourceReflectRep_obj_self {k : Type u} {Q : Type v} [Field k] [Quiver Q] (M : QuiverRep k Q) {i : Q} (hi : Quiver.IsSource i) : (sourceReflectRep M hi).obj i = ↧(((e : (b : Q) × (i ⟶ b)) → ↑(M.obj e.fst)) ⧸ (outgoingMap M i).range)

At the reflected vertex, source reflection is the quotient by the outgoing map's range.

@[simp]

theorem TauCeti.sourceReflectRep_obj_of_ne {k : Type u} {Q : Type v} [Field k] [Quiver Q] (M : QuiverRep k Q) {i : Q} (hi : Quiver.IsSource i) {j : Q} (h : j ≠ i) : (sourceReflectRep M hi).obj j = M.obj j

Away from the source, the reflected representation is unchanged.

@[simp]

theorem TauCeti.sourceReflectRep_map_reflectArrowSource {k : Type u} {Q : Type v} [Field k] [Quiver Q] (M : QuiverRep k Q) {i : Q} (hi : Quiver.IsSource i) {b : Q} (e : i ⟶ b) : (sourceReflectRep M hi).map (Quiver.reflectArrowSource i e).toPath = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (ModuleCat.ofHom ((outgoingMap M i).range.mkQ ∘ₗ LinearMap.single k (fun (e : (b : Q) × (i ⟶ b)) => ↑(M.obj e.fst)) ⟨b, e⟩)) (CategoryTheory.eqToHom ⋯))

A source-side reversed arrow acts by insertion followed by the quotient map.

@[simp]

theorem TauCeti.sourceReflectRep_map_reflectArrowOfNeOfNe {k : Type u} {Q : Type v} [Field k] [Quiver Q] (M : QuiverRep k Q) {i : Q} (hi : Quiver.IsSource i) {a b : Q} (ha : a ≠ i) (hb : b ≠ i) (e : a ⟶ b) : (sourceReflectRep M hi).map (Quiver.reflectArrowOfNeOfNe ha hb e).toPath = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (M.map e.toPath) (CategoryTheory.eqToHom ⋯))

An arrow away from the reflected vertex acts unchanged.

theorem TauCeti.outgoingMap_naturality {k : Type u} {Q : Type v} [Field k] [Quiver Q] {M N : QuiverRep k Q} (η : M ⟶ N) (i : Q) (y : ↑(M.obj i)) : (fun (e : (b : Q) × (i ⟶ b)) => (CategoryTheory.ConcreteCategory.hom (η.app e.fst)) ((outgoingMap M i) y e)) = (outgoingMap N i) ((CategoryTheory.ConcreteCategory.hom (η.app i)) y)

The outgoing map is natural in the representation.

noncomputable def TauCeti.sourceReflectionFunctor {k : Type u} {Q : Type v} [Field k] [Quiver Q] (i : Q) (hi : Quiver.IsSource i) : CategoryTheory.Functor (QuiverRep k Q) (QuiverRep k (Quiver.Reflect Q i))

The BGP reflection functor at a source. It uses the quotient map induced by each morphism at the reflected vertex and leaves all other components unchanged.

@[simp]

theorem TauCeti.sourceReflectionFunctor_obj {k : Type u} {Q : Type v} [Field k] [Quiver Q] (i : Q) (hi : Quiver.IsSource i) (M : QuiverRep k Q) : (sourceReflectionFunctor i hi).obj M = sourceReflectRep M hi

The source reflection functor sends M to TauCeti.sourceReflectRep M hi.

instance TauCeti.sourceReflectionFunctor_additive {k : Type u} {Q : Type v} [Field k] [Quiver Q] (i : Q) (hi : Quiver.IsSource i) : (sourceReflectionFunctor i hi).Additive

The source reflection functor is additive. The map induced on the quotient is additive in the original morphism, coordinate by coordinate.

@[simp]

theorem TauCeti.sourceReflectionFunctor_map_app_self_mk {k : Type u} {Q : Type v} [Field k] [Quiver Q] {M N : QuiverRep k Q} (η : M ⟶ N) {i : Q} (hi : Quiver.IsSource i) (f : (e : (b : Q) × (i ⟶ b)) → ↑(M.obj e.fst)) : (ModuleCat.Hom.hom (CategoryTheory.eqToHom ⋯)) ((ModuleCat.Hom.hom (((sourceReflectionFunctor i hi).map η).app i)) ((ModuleCat.Hom.hom (CategoryTheory.eqToHom ⋯)) (Submodule.Quotient.mk f))) = (outgoingMap N i).range.mkQ fun (e : (b : Q) × (i ⟶ b)) => (CategoryTheory.ConcreteCategory.hom (η.app e.fst)) (f e)

At the reflected vertex, source reflection sends a morphism to the induced map on quotient classes, computed here on a representative.

@[simp]

theorem TauCeti.sourceReflectionFunctor_map_app_of_ne {k : Type u} {Q : Type v} [Field k] [Quiver Q] {M N : QuiverRep k Q} (η : M ⟶ N) {i : Q} (hi : Quiver.IsSource i) {j : Q} (hj : j ≠ i) : ((sourceReflectionFunctor i hi).map η).app j = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (η.app j) (CategoryTheory.eqToHom ⋯))

Away from the reflected vertex, source reflection leaves morphism components unchanged.

The dimension vector

@[simp]

theorem TauCeti.dimVector_sourceReflectRep_of_ne {k : Type u} {Q : Type v} [Field k] [Quiver Q] (M : QuiverRep k Q) {i : Q} (hi : Quiver.IsSource i) {j : Q} (h : j ≠ i) : dimVector (sourceReflectRep M hi) j = dimVector M j

Away from the source, the dimension vector is unchanged.

theorem TauCeti.dimVector_sourceReflectRep_self_add {k : Type u} {Q : Type v} [Field k] [Quiver Q] [Fintype Q] [(a b : Q) → Fintype (a ⟶ b)] (M : QuiverRep k Q) {i : Q} (hi : Quiver.IsSource i) (hM : ∀ (e : (b : Q) × (i ⟶ b)), FiniteDimensional k ↑(M.obj e.fst)) (hinj : Function.Injective ⇑(outgoingMap M i)) : dimVector (sourceReflectRep M hi) i + dimVector M i = ∑ b : Q, Fintype.card (i ⟶ b) * dimVector M b

The dimension of the reflected space at the source. If the outgoing map is injective, the dimension of its cokernel plus the old source dimension is the total dimension at the targets of outgoing arrows.

theorem TauCeti.dimVector_sourceReflectRep {k : Type u} {Q : Type v} [Field k] [Quiver Q] [Fintype Q] [(a b : Q) → Fintype (a ⟶ b)] (M : QuiverRep k Q) {i : Q} (hi : Quiver.IsSource i) [DecidableEq Q] (hM : ∀ (e : (b : Q) × (i ⟶ b)), FiniteDimensional k ↑(M.obj e.fst)) (hinj : Function.Injective ⇑(outgoingMap M i)) : (fun (j : Q) => ↑(dimVector (sourceReflectRep M hi) j)) = (vertexPreReflection Q i) fun (j : Q) => ↑(dimVector M j)

Source reflection acts on dimension vectors by the simple reflection.

theorem TauCeti.finiteDimensional_sourceReflectRep_obj {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))] (h : ∀ (a : Q), FiniteDimensional k ↑(M.obj a)) (j : Q) : FiniteDimensional k ↑((sourceReflectRep M hi).obj j)

Source reflection preserves finite-dimensionality of every vertex space.