Graded derivations of a path algebra, freely determined by the arrows

Give every arrow e of a finite quiver Q an integer degree wt e. The path algebra kQ is then ℤ-graded by TauCeti.PathAlgebra.gradeBy k wt, and a degree +1 graded derivation of kQ is a k-linear endomorphism d obeying the signed Leibniz rule

d (x * y) = d x * y + (-1) ^ p • (x * d y)

for a left factor x homogeneous of degree p.

Such a derivation is free on the arrows. An assignment f sending an arrow e : a ⟶ b into the corner e_b (kQ) e_a extends to the graded derivation TauCeti.PathAlgebra.liftDerivation, which kills every vertex idempotent and takes the value f e on e, and it is the only one. Its value on a path is read off from the recursion

d (e ⬝ p) = f e ⬝ p + (-1) ^ (wt e) • (e ⬝ d p),

which the later-factor-first multiplication of Tau Ceti turns into an induction along cons.

The derivation is graded for every arrow weight at once: if a second weight g, valued in any additive commutative monoid, gives f e the degree g e + δ for one fixed shift δ, then d raises the g-degree by δ. Taking g = wt and δ = 1 is the cohomological statement, and a second weight with δ = 0 is the Adams grading of a differential graded path algebra.

Finally, d ∘ d is again a derivation, an unsigned one, so it vanishes as soon as it vanishes on the arrows; together with the two previous paragraphs this packages d as the differential of a differential graded algebra.

Main definitions

• TauCeti.PathAlgebra.liftDerivation: the graded derivation of kQ extending an assignment f of a corner element to each arrow.

Main results

• TauCeti.PathAlgebra.liftDerivation_ofArrow: the derivation extends the assignment.
• TauCeti.PathAlgebra.liftDerivation_mul: the graded Leibniz rule.
• TauCeti.PathAlgebra.liftDerivation_unique: a graded derivation is determined by its values on the arrows and its vanishing on the vertex idempotents.
• TauCeti.PathAlgebra.liftDerivation_mem_gradeBy: the derivation shifts the grading by an arbitrary arrow weight by a fixed amount, provided the assignment does.
• TauCeti.PathAlgebra.liftDerivation_sq_zero: the square of the derivation vanishes as soon as it vanishes on the arrows.
• TauCeti.PathAlgebra.isDGAlgebra_liftDerivation: the resulting differential graded algebra.

References

• B. Keller, Deformed Calabi--Yau completions, Section 6.5, and T. Etgü and Y. Lekili, Koszul duality patterns in Floer theory, Section 4, where the differential of a Ginzburg differential graded algebra is prescribed on the arrows of a quiver and extended by the Leibniz rule.

noncomputable def TauCeti.PathAlgebra.liftDerivation (k : Type w) [CommRing k] {Q : Type u} [Quiver Q] (wt : {a b : Q} → (a ⟶ b) → ℤ) (f : {a b : Q} → (a ⟶ b) → pathAlgebra k Q) : pathAlgebra k Q →ₗ[k] pathAlgebra k Q

The graded derivation of a path algebra extending an assignment on arrows. Arrows are given the integer degrees wt, and f e is the value of the derivation on the arrow e; for the Leibniz rule to hold, f e must lie in the corner of kQ cut out by the endpoints of e.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.PathAlgebra.liftDerivation_vertexIdempotent (k : Type w) [CommRing k] {Q : Type u} [Quiver Q] [Finite Q] (wt : {a b : Q} → (a ⟶ b) → ℤ) (f : {a b : Q} → (a ⟶ b) → pathAlgebra k Q) (v : Q) : (liftDerivation k (fun {a b : Q} => wt) fun {a b : Q} => f) (vertexIdempotent k v) = 0

theorem TauCeti.PathAlgebra.liftDerivation_ofArrow (k : Type w) [CommRing k] {Q : Type u} [Quiver Q] [Finite Q] (wt : {a b : Q} → (a ⟶ b) → ℤ) (f : {a b : Q} → (a ⟶ b) → pathAlgebra k Q) (hfr : ∀ {a b : Q} (e : a ⟶ b), f e * vertexIdempotent k a = f e) {a b : Q} (e : a ⟶ b) : (liftDerivation k (fun {a b : Q} => wt) fun {a b : Q} => f) (ofArrow e) = f e

The derivation extends the assignment on arrows. Deliberately not a simp lemma: TauCeti.PathAlgebra.ofArrow_eq_ofPath already normalizes its left-hand side.

theorem TauCeti.PathAlgebra.liftDerivation_ofArrow_mul (k : Type w) [CommRing k] {Q : Type u} [Quiver Q] [Finite Q] (wt : {a b : Q} → (a ⟶ b) → ℤ) (f : {a b : Q} → (a ⟶ b) → pathAlgebra k Q) (hfl : ∀ {a b : Q} (e : a ⟶ b), vertexIdempotent k b * f e = f e) (hfr : ∀ {a b : Q} (e : a ⟶ b), f e * vertexIdempotent k a = f e) {b c : Q} (e : b ⟶ c) (z : pathAlgebra k Q) : (liftDerivation k (fun {a b : Q} => wt) fun {a b : Q} => f) (ofArrow e * z) = f e * z + (wt e).negOnePow • (ofArrow e * (liftDerivation k (fun {a b : Q} => wt) fun {a b : Q} => f) z)

The Leibniz rule against an arrow.

theorem TauCeti.PathAlgebra.liftDerivation_mul (k : Type w) [CommRing k] {Q : Type u} [Quiver Q] [Finite Q] (wt : {a b : Q} → (a ⟶ b) → ℤ) (f : {a b : Q} → (a ⟶ b) → pathAlgebra k Q) (hfl : ∀ {a b : Q} (e : a ⟶ b), vertexIdempotent k b * f e = f e) (hfr : ∀ {a b : Q} (e : a ⟶ b), f e * vertexIdempotent k a = f e) {m : ℤ} {x : pathAlgebra k Q} (hx : x ∈ gradeBy k (fun {a b : Q} => wt) m) (y : pathAlgebra k Q) : (liftDerivation k (fun {a b : Q} => wt) fun {a b : Q} => f) (x * y) = (liftDerivation k (fun {a b : Q} => wt) fun {a b : Q} => f) x * y + m.negOnePow • (x * (liftDerivation k (fun {a b : Q} => wt) fun {a b : Q} => f) y)

The graded Leibniz rule: on a homogeneous left factor of degree m, the derivation obeys the Koszul sign rule.

Gradings, uniqueness, and the differential graded algebra

theorem TauCeti.PathAlgebra.liftDerivation_mem_gradeBy (k : Type w) [CommRing k] {Q : Type u} [Quiver Q] [Finite Q] (wt : {a b : Q} → (a ⟶ b) → ℤ) (f : {a b : Q} → (a ⟶ b) → pathAlgebra k Q) {M : Type u_1} [AddCommMonoid M] (g : {a b : Q} → (a ⟶ b) → M) (δ : M) (hg : ∀ {a b : Q} (e : a ⟶ b), f e ∈ gradeBy k (fun {a b : Q} => g) (g e + δ)) {m : M} {x : pathAlgebra k Q} (hx : x ∈ gradeBy k (fun {a b : Q} => g) m) : (liftDerivation k (fun {a b : Q} => wt) fun {a b : Q} => f) x ∈ gradeBy k (fun {a b : Q} => g) (m + δ)

The derivation shifts every arrow grading by a fixed amount, provided the assignment does: if f e is homogeneous of degree g e + δ for the arrow weight g, then the derivation raises the g-degree by δ. With g = wt and δ = 1 this is the cohomological degree of a differential; with a second weight and δ = 0 it is the invariance of an Adams grading.

theorem TauCeti.PathAlgebra.liftDerivation_unique (k : Type w) [CommRing k] {Q : Type u} [Quiver Q] [Finite Q] (wt : {a b : Q} → (a ⟶ b) → ℤ) (f : {a b : Q} → (a ⟶ b) → pathAlgebra k Q) (hfl : ∀ {a b : Q} (e : a ⟶ b), vertexIdempotent k b * f e = f e) (hfr : ∀ {a b : Q} (e : a ⟶ b), f e * vertexIdempotent k a = f e) (D : pathAlgebra k Q →ₗ[k] pathAlgebra k Q) (hvertex : ∀ (v : Q), D (vertexIdempotent k v) = 0) (hleibniz : ∀ {m : ℤ} {x : pathAlgebra k Q}, x ∈ gradeBy k (fun {a b : Q} => wt) m → ∀ (y : pathAlgebra k Q), D (x * y) = D x * y + m.negOnePow • (x * D y)) (harrow : ∀ {a b : Q} (e : a ⟶ b), D (ofArrow e) = f e) : D = liftDerivation k (fun {a b : Q} => wt) fun {a b : Q} => f

A graded derivation is determined by vanishing on the vertex idempotents together with its values on the arrows.

theorem TauCeti.PathAlgebra.liftDerivation_sq_zero (k : Type w) [CommRing k] {Q : Type u} [Quiver Q] [Finite Q] (wt : {a b : Q} → (a ⟶ b) → ℤ) (f : {a b : Q} → (a ⟶ b) → pathAlgebra k Q) (hfl : ∀ {a b : Q} (e : a ⟶ b), vertexIdempotent k b * f e = f e) (hfr : ∀ {a b : Q} (e : a ⟶ b), f e * vertexIdempotent k a = f e) (hf : ∀ {a b : Q} (e : a ⟶ b), f e ∈ gradeBy k (fun {a b : Q} => wt) (wt e + 1)) (hsq : ∀ {a b : Q} (e : a ⟶ b), (liftDerivation k (fun {a b : Q} => wt) fun {a b : Q} => f) (f e) = 0) (z : pathAlgebra k Q) : (liftDerivation k (fun {a b : Q} => wt) fun {a b : Q} => f) ((liftDerivation k (fun {a b : Q} => wt) fun {a b : Q} => f) z) = 0

The square of the derivation vanishes as soon as it vanishes on the arrows.

theorem TauCeti.PathAlgebra.isDGAlgebra_liftDerivation (k : Type w) [CommRing k] {Q : Type u} [Quiver Q] [Finite Q] (wt : {a b : Q} → (a ⟶ b) → ℤ) (f : {a b : Q} → (a ⟶ b) → pathAlgebra k Q) (hfl : ∀ {a b : Q} (e : a ⟶ b), vertexIdempotent k b * f e = f e) (hfr : ∀ {a b : Q} (e : a ⟶ b), f e * vertexIdempotent k a = f e) (hf : ∀ {a b : Q} (e : a ⟶ b), f e ∈ gradeBy k (fun {a b : Q} => wt) (wt e + 1)) (hsq : ∀ {a b : Q} (e : a ⟶ b), (liftDerivation k (fun {a b : Q} => wt) fun {a b : Q} => f) (f e) = 0) : IsDGAlgebra (gradeBy k fun {a b : Q} => wt) (liftDerivation k (fun {a b : Q} => wt) fun {a b : Q} => f)

The path algebra, graded by the arrow degrees wt, is a differential graded algebra with differential TauCeti.PathAlgebra.liftDerivation.