The Euler and Tits forms under reflection of a quiver at a vertex

Reflecting a quiver at a vertex does not change its underlying graph, so it changes neither the Tits form (TauCeti.titsForm_reflect) nor its polarization (TauCeti.titsPolarForm_reflect), and hence not the simple reflections on dimension vectors either (TauCeti.vertexPreReflection_reflect_apply). The Euler form does change, since it records the orientation; what survives is the Bernstein-Gelfand-Ponomarev identity at a sink or source i: the Euler form of the reflected quiver, evaluated at the simple reflections sᵢ d and sᵢ e, is the Euler form of the original quiver evaluated at d and e.

Main results

• TauCeti.titsForm_reflect, TauCeti.titsPolarForm_reflect: the Tits form and its polarization are unchanged by reflection at a vertex.
• TauCeti.vertexPreReflection_reflect_apply: so is every simple reflection on dimension vectors.
• TauCeti.eulerForm_reflect_vertexPreReflection: at a sink, the Euler form is transported by the simple reflection at that vertex.
• TauCeti.eulerForm_reflect_vertexPreReflection_of_isSource: the corresponding identity at a source.

References

This is the dimension-vector shadow of the Layer 4 reflection-functor target dim (C⁺ᵢ M) = sᵢ · dim M of TauCetiRoadmap/RepresentationTheory/QuiverRepresentations/README.md. See Derksen--Weyman, An Introduction to Quiver Representations, and Bernstein--Gelfand--Ponomarev, Coxeter functors and Gabriel's theorem.

Two sum manipulations

The Tits form is unchanged

theorem TauCeti.titsForm_reflect {V : Type u} [Quiver V] [Fintype V] [(a b : V) → Fintype (a ⟶ b)] (i : V) (d : V → ℤ) : (titsForm (Quiver.Reflect V i)) d = (titsForm V) d

Reflecting at a vertex leaves the Tits form unchanged: the Tits form depends only on the underlying graph of the quiver, not on its orientation.

theorem TauCeti.titsPolarForm_reflect {V : Type u} [Quiver V] [Fintype V] [(a b : V) → Fintype (a ⟶ b)] (i : V) (d e : V → ℤ) : ((titsPolarForm (Quiver.Reflect V i)) d) e = ((titsPolarForm V) d) e

Reflecting at a vertex leaves the polarized Tits form unchanged.

theorem TauCeti.vertexPreReflection_reflect_apply {V : Type u} [Quiver V] [Fintype V] [(a b : V) → Fintype (a ⟶ b)] [DecidableEq V] (i j : V) (d : V → ℤ) (w : V) : (vertexPreReflection (Quiver.Reflect V i) j) d w = (vertexPreReflection V j) d w

Reflecting at a vertex leaves every simple reflection on dimension vectors unchanged, since these are built from the polarized Tits form, which reflection preserves.

The Euler form at a sink or source

theorem TauCeti.eulerForm_reflect_vertexPreReflection {V : Type u} [Quiver V] [Fintype V] [(a b : V) → Fintype (a ⟶ b)] [DecidableEq V] {i : V} (h : Quiver.IsSink i) (d e : V → ℤ) : ((eulerForm (Quiver.Reflect V i)) ((vertexPreReflection V i) d)) ((vertexPreReflection V i) e) = ((eulerForm V) d) e

At a sink i, the Euler form of the quiver reflected at i is carried to the Euler form of the original quiver by the simple reflection sᵢ on dimension vectors: ⟨sᵢ d, sᵢ e⟩ for Q.reflect i equals ⟨d, e⟩ for Q.

This is the numerical identity behind the Bernstein-Gelfand-Ponomarev reflection functor at a sink, which realizes sᵢ on dimension vectors.

theorem TauCeti.eulerForm_reflect_vertexPreReflection_of_isSource {V : Type u} [Quiver V] [Fintype V] [(a b : V) → Fintype (a ⟶ b)] [DecidableEq V] {i : V} (h : Quiver.IsSource i) (d e : V → ℤ) : ((eulerForm (Quiver.Reflect V i)) ((vertexPreReflection V i) d)) ((vertexPreReflection V i) e) = ((eulerForm V) d) e

At a source i, the Euler form of the quiver reflected at i is carried to the Euler form of the original quiver by the simple reflection sᵢ on dimension vectors: ⟨sᵢ d, sᵢ e⟩ for Q.reflect i equals ⟨d, e⟩ for Q.

This is the numerical identity behind the Bernstein-Gelfand-Ponomarev reflection functor at a source, which realizes sᵢ on dimension vectors.