Deformed simple reflections of a finite graph

For a unit q in a commutative ring, the graph Cartan rows have diagonal coefficient 1 + q² and edge coefficient q. Subtracting the value of a row times its vertex vector gives a linear automorphism. Its inverse subtracts q⁻² times the same row.

These transformations satisfy the graph's Artin relations. At q = -1 the Cartan rows are the rows of SimpleGraph.graphCartanMatrix, and the transformations are the standard simple reflections. The construction uses the existing rank-one matrix calculus TauCeti.oneSubVecMulVecGL and its commutation and braid theorems. The ordinary specialization uses Module.reflection.

The vertex module and its operators are defined algebraically; identifying them with graded Grothendieck classes requires a separate comparison.

References

• Huerfano--Khovanov, A category for the adjoint representation, Section 2.2, equation (11), for the Cartan coefficients, and Section 4.6 for the evaluation-complex braid action. The identity-minus-row sign here corresponds to placing the evaluation term in degree -1.
• Khovanov--Seidel, Quivers, Floer cohomology, and braid group actions, Section 2e.1 and Proposition 2.8, for the type-A reduced Burau formulas. Replace the grading parameter by q²; rescaling the vertex vector at j by qʲ gives the symmetric edge coefficient used here.

noncomputable def SimpleGraph.deformedCartanEntry {V : Type u} [DecidableEq V] {R : Type v} [CommRing R] (G : SimpleGraph V) (q : R) (i j : V) : R

The diagonal and edge coefficients of the deformed graph Cartan matrix.

@[simp]

theorem SimpleGraph.deformedCartanEntry_self {V : Type u} [DecidableEq V] {R : Type v} [CommRing R] (G : SimpleGraph V) (q : R) (i : V) : G.deformedCartanEntry q i i = 1 + q ^ 2

The diagonal coefficient of a deformed Cartan row.

@[simp]

theorem SimpleGraph.deformedCartanEntry_of_adj {V : Type u} [DecidableEq V] {R : Type v} [CommRing R] (G : SimpleGraph V) (q : R) {i j : V} (h : G.Adj i j) : G.deformedCartanEntry q i j = q

The coefficient at an adjacent vertex.

@[simp]

theorem SimpleGraph.deformedCartanEntry_of_not_adj {V : Type u} [DecidableEq V] {R : Type v} [CommRing R] (G : SimpleGraph V) (q : R) {i j : V} (hne : i ≠ j) (h : ¬G.Adj i j) : G.deformedCartanEntry q i j = 0

The coefficient at a distinct nonadjacent vertex.

noncomputable def SimpleGraph.deformedCartanRow {V : Type u} [DecidableEq V] {R : Type v} [CommRing R] (G : SimpleGraph V) [Fintype V] (q : R) (i : V) : Module.Dual R (V → R)

A row of the deformed graph Cartan matrix as a linear functional on vertex coordinates.

theorem SimpleGraph.deformedCartanRow_apply {V : Type u} [DecidableEq V] {R : Type v} [CommRing R] (G : SimpleGraph V) [Fintype V] (q : R) (i : V) (x : V → R) : (G.deformedCartanRow q i) x = ∑ j : V, G.deformedCartanEntry q i j * x j

A Cartan row is the sum of its coefficients times the vertex coordinates.

@[simp]

theorem SimpleGraph.deformedCartanRow_single {V : Type u} [DecidableEq V] {R : Type v} [CommRing R] (G : SimpleGraph V) [Fintype V] (q : R) (i j : V) : (G.deformedCartanRow q i) (Pi.single j 1) = G.deformedCartanEntry q i j

noncomputable def SimpleGraph.deformedReflection {V : Type u} [DecidableEq V] {R : Type v} [CommRing R] (G : SimpleGraph V) [Fintype V] (q : Rˣ) (i : V) : (V → R) ≃ₗ[R] V → R

The deformed simple reflection at a vertex, in functional composition order.

theorem SimpleGraph.deformedReflection_apply {V : Type u} [DecidableEq V] {R : Type v} [CommRing R] (G : SimpleGraph V) [Fintype V] (q : Rˣ) (i : V) (x : V → R) : (G.deformedReflection q i) x = x - (G.deformedCartanRow (↑q) i) x • Pi.single i 1

A deformed reflection subtracts its Cartan-row value in the vertex direction.

theorem SimpleGraph.deformedReflection_symm_apply {V : Type u} [DecidableEq V] {R : Type v} [CommRing R] (G : SimpleGraph V) [Fintype V] (q : Rˣ) (i : V) (x : V → R) : (G.deformedReflection q i).symm x = x - (↑q⁻¹ ^ 2 * (G.deformedCartanRow (↑q) i) x) • Pi.single i 1

The inverse subtracts q⁻² times the same Cartan-row value.

theorem SimpleGraph.deformedReflection_commute {V : Type u} [DecidableEq V] {R : Type v} [CommRing R] (G : SimpleGraph V) [Fintype V] (q : Rˣ) {i j : V} (hne : i ≠ j) (h : ¬G.Adj i j) : G.deformedReflection q i * G.deformedReflection q j = G.deformedReflection q j * G.deformedReflection q i

Distinct nonadjacent vertex operators commute.

theorem SimpleGraph.deformedReflection_braid {V : Type u} [DecidableEq V] {R : Type v} [CommRing R] (G : SimpleGraph V) [Fintype V] (q : Rˣ) {i j : V} (h : G.Adj i j) : G.deformedReflection q i * G.deformedReflection q j * G.deformedReflection q i = G.deformedReflection q j * G.deformedReflection q i * G.deformedReflection q j

Adjacent vertex operators satisfy the length-three braid relation.

noncomputable def SimpleGraph.deformedReflectionRepresentation {V : Type u} [DecidableEq V] {R : Type v} [CommRing R] (G : SimpleGraph V) [Fintype V] (q : Rˣ) : TauCeti.ArtinGroup G.coxeterMatrix →* (V → R) ≃ₗ[R] V → R

The deformed reflections define a linear representation of the graph's Artin group.

@[simp]

theorem SimpleGraph.deformedReflectionRepresentation_gen {V : Type u} [DecidableEq V] {R : Type v} [CommRing R] (G : SimpleGraph V) [Fintype V] (q : Rˣ) (i : V) : (G.deformedReflectionRepresentation q) (TauCeti.ArtinGroup.gen G.coxeterMatrix i) = G.deformedReflection q i

The representation sends each Artin generator to its vertex operator.

@[simp]

theorem SimpleGraph.deformedReflectionRepresentation_gen_inv {V : Type u} [DecidableEq V] {R : Type v} [CommRing R] (G : SimpleGraph V) [Fintype V] (q : Rˣ) (i : V) : (G.deformedReflectionRepresentation q) (TauCeti.ArtinGroup.gen G.coxeterMatrix i)⁻¹ = (G.deformedReflection q i).symm

An inverse Artin generator acts by the inverse vertex operator.

@[simp]

theorem SimpleGraph.deformedReflection_single_self {V : Type u} [DecidableEq V] {R : Type v} [CommRing R] (G : SimpleGraph V) [Fintype V] (q : Rˣ) (i : V) : (G.deformedReflection q i) (Pi.single i 1) = -↑q ^ 2 • Pi.single i 1

The vertex direction is multiplied by -q².

@[simp]

theorem SimpleGraph.deformedReflection_single_of_adj {V : Type u} [DecidableEq V] {R : Type v} [CommRing R] (G : SimpleGraph V) [Fintype V] (q : Rˣ) {i j : V} (h : G.Adj i j) : (G.deformedReflection q i) (Pi.single j 1) = Pi.single j 1 - ↑q • Pi.single i 1

An adjacent vertex direction acquires -q times the reflecting direction.

@[simp]

theorem SimpleGraph.deformedReflection_single_of_not_adj {V : Type u} [DecidableEq V] {R : Type v} [CommRing R] (G : SimpleGraph V) [Fintype V] (q : Rˣ) {i j : V} (hne : i ≠ j) (h : ¬G.Adj i j) : (G.deformedReflection q i) (Pi.single j 1) = Pi.single j 1

A distinct nonadjacent vertex direction is fixed.

theorem SimpleGraph.deformedReflection_neg_one {V : Type u} [DecidableEq V] {R : Type v} [CommRing R] (G : SimpleGraph V) [Fintype V] (i : V) : G.deformedReflection (-1) i = Module.reflection ⋯

At q = -1, a deformed reflection is Mathlib's ordinary simple reflection.

theorem SimpleGraph.deformedCartanRow_neg_one_single {V : Type u} [DecidableEq V] {R : Type v} [CommRing R] (G : SimpleGraph V) [Fintype V] [DecidableRel G.Adj] (i j : V) : (G.deformedCartanRow (-1) i) (Pi.single j 1) = G.graphCartanMatrix R i j

The specialized Cartan row has the entries of the canonical graph Cartan matrix.