Documentation

TauCeti.RepresentationTheory.Quiver.PathAlgebra.CyclicDerivative

Cyclic derivatives in a path algebra #

Let a : i ⟶ j be an arrow of a quiver Q. The cyclic derivative ∂_a is the linear endomorphism of the path algebra kQ which, on a cycle, deletes one occurrence of a and reads the rest of the cycle starting just after it, summed over all occurrences of a: if the cycle traverses v, then a, then u, the occurrence contributes the path traversing u and then v, a path from j back to i. In Tau Ceti's later-factor-first convention this contribution is the product ofPath v * ofPath u. A path which is not a cycle has no such rearrangement and has cyclic derivative 0. Cyclic derivatives of a potential W, a linear combination of cycles, are the relations of the Jacobian algebra of (Q, W) and the differentials of the reverse arrows in its three-dimensional Ginzburg differential graded algebra.

The basic identity satisfied by cyclic derivatives is

∑_a a ∂_a(x) = ∑_a ∂_a(x) a,

the sums running over all arrows of Q, for every x ∈ kQ when Q has finitely many vertices and arrows. On a cycle both sides are the sum of all its rotations, one for each of its arrows. The identity holds vertex by vertex as well: the arrows a with head v on the left and those with tail v on the right give equal sums. This is what makes the square of the three-dimensional Ginzburg differential vanish on the adjoined loops.

Main definitions #

Main results #

References #

source
noncomputable def TauCeti.PathAlgebra.cyclicDerivative (k : Type w) [Semiring k] {Q : Type u} [Quiver Q] {i j : Q} (a : i ⟶ j) :
pathAlgebra k Q →ₗ[k] pathAlgebra k Q

The cyclic derivative ∂_a with respect to an arrow a : i ⟶ j. On a cycle which traverses a path v, then a, then a path u, each such occurrence of a contributes the path u followed by v, which is ofPath v * ofPath u in the later-factor-first convention; paths which are not cycles have cyclic derivative 0.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem TauCeti.PathAlgebra.cyclicDerivative_mul_vertexIdempotent {k : Type w} [Semiring k] {Q : Type u} [Quiver Q] {i j : Q} (a : i ⟶ j) (z : pathAlgebra k Q) :
    (cyclicDerivative k a) z * vertexIdempotent k j = (cyclicDerivative k a) z

    The cyclic derivative with respect to a : i ⟶ j lies in the right corner of j.

    source
    @[simp]
    theorem TauCeti.PathAlgebra.cyclicDerivative_ofPath_of_ne {k : Type w} [Semiring k] {Q : Type u} [Quiver Q] {i j : Q} (a : i ⟶ j) {s t : Q} (p : Quiver.Path s t) (h : s ≠ t) :
    (cyclicDerivative k a) (ofPath ⟨s, ⟨t, p⟩⟩) = 0

    A path which is not a cycle has cyclic derivative 0.

    source
    theorem TauCeti.PathAlgebra.cyclicDerivative_ofPath {k : Type w} [Semiring k] {Q : Type u} [Quiver Q] {i j : Q} (a : i ⟶ j) {s : Q} (c : Quiver.Path s s) :
    (cyclicDerivative k a) (ofPath ⟨s, ⟨s, c⟩⟩) = ∑ᶠ (d : Quiver.Path s i × Quiver.Path j s) (_ : d ∈ {d : Quiver.Path s i × Quiver.Path j s | d.1.comp (a.toPath.comp d.2) = c}), ofPath ⟨j, ⟨i, d.2.comp d.1⟩⟩

    The cyclic derivative of a cycle: the cyclic derivative with respect to a : i ⟶ j of a cycle c is the sum, over the ways of writing c as a path v, then a, then a path u, of the rotated remainder, the path traversing u and then v.

    source
    @[simp]
    theorem TauCeti.PathAlgebra.cyclicDerivative_vertexIdempotent {k : Type w} [Semiring k] {Q : Type u} [Quiver Q] {i j : Q} (a : i ⟶ j) (v : Q) :
    (cyclicDerivative k a) (vertexIdempotent k v) = 0

    The cyclic derivative kills the vertex idempotents, which are paths of length 0.

    source
    @[simp]
    theorem TauCeti.PathAlgebra.cyclicDerivative_ofArrow_self {k : Type w} [Semiring k] {Q : Type u} [Quiver Q] {i : Q} (a : i ⟶ i) :
    (cyclicDerivative k a) (ofPath ⟨i, ⟨i, a.toPath⟩⟩) = vertexIdempotent k i

    The cyclic derivative of a loop with respect to itself is the vertex idempotent at its vertex.

    source
    @[simp]
    theorem TauCeti.PathAlgebra.cyclicDerivative_ofArrow_of_ne {k : Type w} [Semiring k] {Q : Type u} [Quiver Q] {i j : Q} (a : i ⟶ j) {m t : Q} (b : m ⟶ t) (h : ⟨m, ⟨t, b⟩⟩ ≠ ⟨i, ⟨j, a⟩⟩) :
    (cyclicDerivative k a) (ofPath ⟨m, ⟨t, b.toPath⟩⟩) = 0

    The cyclic derivative of an arrow with respect to a different arrow vanishes.

    source
    @[simp]
    theorem TauCeti.PathAlgebra.vertexIdempotent_mul_cyclicDerivative {k : Type w} [CommSemiring k] {Q : Type u} [Quiver Q] {i j : Q} (a : i ⟶ j) (z : pathAlgebra k Q) :
    vertexIdempotent k i * (cyclicDerivative k a) z = (cyclicDerivative k a) z

    The cyclic derivative with respect to a : i ⟶ j lies in the left corner of i.

    source
    theorem TauCeti.PathAlgebra.cyclicDerivative_mul_comm {k : Type w} [CommSemiring k] {Q : Type u} [Quiver Q] {i j : Q} (a : i ⟶ j) (x y : pathAlgebra k Q) :
    (cyclicDerivative k a) (x * y) = (cyclicDerivative k a) (y * x)

    The cyclic derivative is invariant under cyclic permutation: it takes the same value on x * y and on y * x, so that it vanishes on commutators and only depends on a potential up to cyclic equivalence.

    source
    theorem TauCeti.PathAlgebra.sum_ofArrow_mul_cyclicDerivative_eq_sum_cyclicDerivative_mul_ofArrow {k : Type w} [CommSemiring k] {Q : Type u} [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] (x : pathAlgebra k Q) (v : Q) :
    ∑ i : Q, ∑ a : i ⟶ v, ofArrow a * (cyclicDerivative k a) x = ∑ j : Q, ∑ a : v ⟶ j, (cyclicDerivative k a) x * ofArrow a

    The local cyclic identity: at every vertex v, the arrows a with head v and those with tail v give ∑_{head a = v} a ∂_a(x) = ∑_{tail a = v} ∂_a(x) a.

    source
    theorem TauCeti.PathAlgebra.sum_sum_sum_ofArrow_mul_cyclicDerivative_comm {k : Type w} [CommSemiring k] {Q : Type u} [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] (x : pathAlgebra k Q) :
    ∑ i : Q, ∑ j : Q, ∑ a : i ⟶ j, ofArrow a * (cyclicDerivative k a) x = ∑ i : Q, ∑ j : Q, ∑ a : i ⟶ j, (cyclicDerivative k a) x * ofArrow a

    The global cyclic identity ∑_a a ∂_a(x) = ∑_a ∂_a(x) a, the sums running over all arrows of Q.