The two-dimensional Ginzburg differential graded algebra of a quiver

Let Q be a finite quiver. The Ginzburg quiver TauCeti.GinzburgQuiver Q has the vertices of Q, the arrows of the doubled quiver Quiver.Symmetrify Q, and one further loop t_i at every vertex i. Its path algebra carries two gradings: a cohomological one in which doubled arrows have degree 0 and the loops degree -1, and an Adams (path) grading in which doubled arrows have degree 1 and the loops degree 2.

The two-dimensional Ginzburg differential is the degree +1 graded derivation which kills every doubled arrow and sends t_i to the local preprojective relator

ρ_i = ∑_{head a = i} a a* - ∑_{tail a = i} a* a

of TauCeti.localPreprojectiveRelator, read inside the Ginzburg path algebra. The resulting differential graded algebra is the non-completed two-dimensional Ginzburg algebra Π₂(Q); its differential has bidegree (1, 0), raising the cohomological degree by one and preserving the Adams degree.

Main definitions

• TauCeti.GinzburgQuiver: the Ginzburg quiver of Q, with arrows TauCeti.GinzburgHom.
• TauCeti.ginzburgOf: the inclusion of the doubled quiver, and TauCeti.ginzburgMap the induced homomorphism of path algebras.
• TauCeti.ginzburgOriginalMap: the inclusion of the path algebra of Q in the Ginzburg path algebra, as the original arrows.
• TauCeti.ginzburgTwoArrowRelator: the prescribed values of the differential on the arrows.
• TauCeti.ginzburgTwoDegree and TauCeti.ginzburgTwoAdamsDegree: the two arrow weights.
• TauCeti.ginzburgTwoDifferential: the two-dimensional Ginzburg differential.

Main results

• TauCeti.ginzburgTwoDifferential_ofArrow_loop: the differential of the loop at i is the local preprojective relator at i, while TauCeti.ginzburgTwoDifferential_ginzburgMap says that the whole doubled path algebra consists of cycles.
• TauCeti.isDGAlgebra_ginzburgTwoDifferential: the two-dimensional Ginzburg differential graded algebra, for the cohomological grading, with TauCeti.ginzburgTwoDifferential_mul and TauCeti.ginzburgTwoDifferential_sq_zero its Leibniz rule and vanishing square.
• TauCeti.ginzburgTwoDifferential_mem_gradeBy_ginzburgTwoAdamsDegree: the differential preserves the Adams grading, so that together with the previous result it has bidegree (1, 0).

References

• V. Ginzburg, Calabi--Yau algebras, Section 4.2.
• B. Keller, Deformed Calabi--Yau completions, Section 6.5.
• T. Etgü and Y. Lekili, Koszul duality patterns in Floer theory, Section 4, for the bigraded, non-completed two-dimensional model used here.

inductive TauCeti.GinzburgHom (Q : Type u) [Quiver Q] : Q → Q → Type (max u v)

The arrows of the Ginzburg quiver of Q: the arrows of the doubled quiver Quiver.Symmetrify Q, together with one extra loop at every vertex.

• double {Q : Type u} [Quiver Q] {i j : Q} (a : (i ⟶ j) ⊕ (j ⟶ i)) : GinzburgHom Q i j

  An arrow of the doubled quiver, whose arrows i ⟶ j are by definition the arrows of Q in either direction. TauCeti.ginzburgOf is the resulting inclusion of Quiver.Symmetrify Q.

• loop {Q : Type u} [Quiver Q] (i : Q) : GinzburgHom Q i i

  The extra loop at a vertex.

def TauCeti.GinzburgQuiver (Q : Type u) : Type u

The Ginzburg quiver of Q: the doubled quiver with one extra loop adjoined at every vertex. Its vertices are those of Q, and its arrows are TauCeti.GinzburgHom.

Equations

• TauCeti.GinzburgQuiver Q = Q

@[instance_reducible]

instance TauCeti.instQuiverGinzburgQuiver {Q : Type u} [Quiver Q] : Quiver (GinzburgQuiver Q)

Equations

• TauCeti.instQuiverGinzburgQuiver = { Hom := TauCeti.GinzburgHom Q }

instance TauCeti.instFiniteGinzburgQuiver {Q : Type u} [Finite Q] : Finite (GinzburgQuiver Q)

def TauCeti.ginzburgOf {Q : Type u} [Quiver Q] : Quiver.Symmetrify Q ⥤q GinzburgQuiver Q

The inclusion of the doubled quiver in the Ginzburg quiver, the identity on vertices.

Equations

• TauCeti.ginzburgOf = { obj := fun (v : Quiver.Symmetrify Q) => v, map := fun {X Y : Quiver.Symmetrify Q} (a : X ⟶ Y) => TauCeti.GinzburgHom.double a }

@[simp]

theorem TauCeti.ginzburgOf_map {Q : Type u} [Quiver Q] {i j : Quiver.Symmetrify Q} (a : i ⟶ j) : ginzburgOf.map a = GinzburgHom.double a

@[simp]

theorem TauCeti.ginzburgOf_obj {Q : Type u} [Quiver Q] (v : Quiver.Symmetrify Q) : ginzburgOf.obj v = v

The doubled-quiver inclusion is the identity on vertices.

theorem TauCeti.ginzburgOf_obj_bijective {Q : Type u} [Quiver Q] : Function.Bijective ginzburgOf.obj

The inclusion of the doubled quiver in the Ginzburg quiver is bijective on vertices.

def TauCeti.ginzburgTwoDegree {Q : Type u} [Quiver Q] {i j : GinzburgQuiver Q} : (i ⟶ j) → ℤ

The cohomological degree of an arrow of the Ginzburg quiver: the doubled arrows sit in degree 0 and the adjoined loops in degree -1.

Equations

• TauCeti.ginzburgTwoDegree (TauCeti.GinzburgHom.double a) = 0
• TauCeti.ginzburgTwoDegree (TauCeti.GinzburgHom.loop x✝) = -1

def TauCeti.ginzburgTwoAdamsDegree {Q : Type u} [Quiver Q] {i j : GinzburgQuiver Q} : (i ⟶ j) → ℕ

The Adams degree of an arrow of the Ginzburg quiver: the doubled arrows sit in degree 1 and the adjoined loops in degree 2, the degrees for which the differential below is homogeneous of degree 0.

Equations

• TauCeti.ginzburgTwoAdamsDegree (TauCeti.GinzburgHom.double a) = 1
• TauCeti.ginzburgTwoAdamsDegree (TauCeti.GinzburgHom.loop x✝) = 2

@[simp]

theorem TauCeti.ginzburgTwoDegree_double {Q : Type u} [Quiver Q] {i j : Q} (a : (i ⟶ j) ⊕ (j ⟶ i)) : ginzburgTwoDegree (GinzburgHom.double a) = 0

@[simp]

theorem TauCeti.ginzburgTwoDegree_loop {Q : Type u} [Quiver Q] (i : Q) : ginzburgTwoDegree (GinzburgHom.loop i) = -1

@[simp]

theorem TauCeti.ginzburgTwoAdamsDegree_double {Q : Type u} [Quiver Q] {i j : Q} (a : (i ⟶ j) ⊕ (j ⟶ i)) : ginzburgTwoAdamsDegree (GinzburgHom.double a) = 1

@[simp]

theorem TauCeti.ginzburgTwoAdamsDegree_loop {Q : Type u} [Quiver Q] (i : Q) : ginzburgTwoAdamsDegree (GinzburgHom.loop i) = 2

noncomputable def TauCeti.ginzburgMap {Q : Type u} [Quiver Q] (k : Type w) [CommSemiring k] [Finite Q] : pathAlgebra k (Quiver.Symmetrify Q) →ₐ[k] pathAlgebra k (GinzburgQuiver Q)

The homomorphism from the doubled path algebra to the Ginzburg path algebra induced by TauCeti.ginzburgOf.

Equations

• TauCeti.ginzburgMap k = TauCeti.PathAlgebra.mapAlgHom k TauCeti.ginzburgOf ⋯

theorem TauCeti.ginzburgMap_ofArrow {Q : Type u} [Quiver Q] (k : Type w) [CommSemiring k] [Finite Q] {i j : Quiver.Symmetrify Q} (a : i ⟶ j) : (ginzburgMap k) (PathAlgebra.ofArrow a) = PathAlgebra.ofArrow (GinzburgHom.double a)

The induced homomorphism sends a doubled-quiver arrow to the corresponding doubled arrow of the Ginzburg quiver.

@[simp]

theorem TauCeti.ginzburgMap_ofPath {Q : Type u} [Quiver Q] (k : Type w) [CommSemiring k] [Finite Q] (x : Quiver.TotalPath (Quiver.Symmetrify Q)) : (ginzburgMap k) (PathAlgebra.ofPath x) = PathAlgebra.ofPath (ginzburgOf.mapTotalPath x)

The induced homomorphism sends a doubled-quiver path to its image in the Ginzburg quiver.

@[simp]

theorem TauCeti.ginzburgMap_doubledVertexIdempotent {Q : Type u} [Quiver Q] (k : Type w) [CommSemiring k] [Finite Q] (v : Q) : (ginzburgMap k) (doubledVertexIdempotent k v) = PathAlgebra.vertexIdempotent k v

noncomputable def TauCeti.ginzburgOriginalMap {Q : Type u} [Quiver Q] (k : Type w) [CommSemiring k] [Finite Q] : pathAlgebra k Q →ₐ[k] pathAlgebra k (GinzburgQuiver Q)

The inclusion of the path algebra of Q in the path algebra of the Ginzburg quiver, sending every arrow of Q to the corresponding original arrow.

Equations

• TauCeti.ginzburgOriginalMap k = (TauCeti.ginzburgMap k).comp (TauCeti.PathAlgebra.mapAlgHom k Quiver.Symmetrify.of ⋯)

theorem TauCeti.ginzburgOriginalMap_ofArrow {Q : Type u} [Quiver Q] (k : Type w) [CommSemiring k] [Finite Q] {i j : Q} (a : i ⟶ j) : (ginzburgOriginalMap k) (PathAlgebra.ofArrow a) = PathAlgebra.ofArrow (GinzburgHom.double (Sum.inl a))

The inclusion sends an arrow of Q to the corresponding original arrow of the Ginzburg quiver. Deliberately not a simp lemma: TauCeti.PathAlgebra.ofArrow_eq_ofPath already normalizes its left-hand side, and TauCeti.ginzburgOriginalMap_ofPath_toPath is the simp form.

@[simp]

theorem TauCeti.ginzburgOriginalMap_ofPath_toPath {Q : Type u} [Quiver Q] (k : Type w) [CommSemiring k] [Finite Q] {i j : Q} (a : i ⟶ j) : (ginzburgOriginalMap k) (PathAlgebra.ofPath ⟨i, ⟨j, a.toPath⟩⟩) = PathAlgebra.ofArrow (GinzburgHom.double (Sum.inl a))

The inclusion sends the one-arrow path to the corresponding original arrow.

@[simp]

theorem TauCeti.ginzburgOriginalMap_vertexIdempotent {Q : Type u} [Quiver Q] (k : Type w) [CommSemiring k] [Finite Q] (v : Q) : (ginzburgOriginalMap k) (PathAlgebra.vertexIdempotent k v) = PathAlgebra.vertexIdempotent k v

The doubled path algebra mapped to the Ginzburg path algebra

theorem TauCeti.ginzburgMap_mem_gradeBy_ginzburgTwoDegree {Q : Type u} [Quiver Q] (k : Type w) [CommSemiring k] [Finite Q] (x : pathAlgebra k (Quiver.Symmetrify Q)) : (ginzburgMap k) x ∈ PathAlgebra.gradeBy k (fun {a b : GinzburgQuiver Q} => ginzburgTwoDegree) 0

The doubled path algebra lands in cohomological degree 0: it is generated by the arrows of the doubled quiver, all of which are of degree 0.

theorem TauCeti.ginzburgMap_mem_gradeBy_ginzburgTwoAdamsDegree {Q : Type u} [Quiver Q] (k : Type w) [CommSemiring k] [Finite Q] {n : ℕ} {x : pathAlgebra k (Quiver.Symmetrify Q)} (hx : x ∈ PathAlgebra.grade k (Quiver.Symmetrify Q) n) : (ginzburgMap k) x ∈ PathAlgebra.gradeBy k (fun {a b : GinzburgQuiver Q} => ginzburgTwoAdamsDegree) n

The doubled path algebra keeps its length grading as the Adams grading.

noncomputable def TauCeti.ginzburgTwoArrowRelator {Q : Type u} [Quiver Q] (k : Type w) [CommRing k] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] {i j : GinzburgQuiver Q} : (i ⟶ j) → pathAlgebra k (GinzburgQuiver Q)

The relator assigned to an arrow in the two-dimensional Ginzburg differential: it is zero on doubled arrows and the local preprojective relator at the vertex of an adjoined loop.

Equations

• TauCeti.ginzburgTwoArrowRelator k (TauCeti.GinzburgHom.double a) = 0
• TauCeti.ginzburgTwoArrowRelator k (TauCeti.GinzburgHom.loop x✝) = (TauCeti.ginzburgMap k) (TauCeti.localPreprojectiveRelator k x✝)

@[simp]

theorem TauCeti.ginzburgTwoArrowRelator_double {Q : Type u} [Quiver Q] (k : Type w) [CommRing k] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] {i j : Q} (a : (i ⟶ j) ⊕ (j ⟶ i)) : ginzburgTwoArrowRelator k (GinzburgHom.double a) = 0

@[simp]

theorem TauCeti.ginzburgTwoArrowRelator_loop {Q : Type u} [Quiver Q] (k : Type w) [CommRing k] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] (i : Q) : ginzburgTwoArrowRelator k (GinzburgHom.loop i) = (ginzburgMap k) (localPreprojectiveRelator k i)

noncomputable def TauCeti.ginzburgTwoDifferential {Q : Type u} [Quiver Q] (k : Type w) [CommRing k] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] : pathAlgebra k (GinzburgQuiver Q) →ₗ[k] pathAlgebra k (GinzburgQuiver Q)

The two-dimensional Ginzburg differential of Q: the degree +1 graded derivation which kills the doubled arrows and sends the loop t_i to the local preprojective relator ρ_i.

Equations

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

@[simp]

theorem TauCeti.ginzburgTwoDifferential_vertexIdempotent {Q : Type u} [Quiver Q] (k : Type w) [CommRing k] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] (v : GinzburgQuiver Q) : (ginzburgTwoDifferential k) (PathAlgebra.vertexIdempotent k v) = 0

theorem TauCeti.ginzburgTwoDifferential_ofArrow {Q : Type u} [Quiver Q] (k : Type w) [CommRing k] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] {i j : GinzburgQuiver Q} (e : i ⟶ j) : (ginzburgTwoDifferential k) (PathAlgebra.ofArrow e) = ginzburgTwoArrowRelator k e

The differential of an arrow is the value prescribed by TauCeti.ginzburgTwoArrowRelator.

theorem TauCeti.ginzburgTwoDifferential_ofArrow_mul {Q : Type u} [Quiver Q] (k : Type w) [CommRing k] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] {i j : GinzburgQuiver Q} (e : i ⟶ j) (z : pathAlgebra k (GinzburgQuiver Q)) : (ginzburgTwoDifferential k) (PathAlgebra.ofArrow e * z) = ginzburgTwoArrowRelator k e * z + (ginzburgTwoDegree e).negOnePow • (PathAlgebra.ofArrow e * (ginzburgTwoDifferential k) z)

The two-dimensional Ginzburg Leibniz rule against an arrow.

theorem TauCeti.ginzburgTwoDifferential_ofArrow_double {Q : Type u} [Quiver Q] (k : Type w) [CommRing k] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] {i j : Q} (a : (i ⟶ j) ⊕ (j ⟶ i)) : (ginzburgTwoDifferential k) (PathAlgebra.ofArrow (GinzburgHom.double a)) = 0

The doubled arrows are cycles of the two-dimensional Ginzburg differential graded algebra. Deliberately not a simp lemma: TauCeti.PathAlgebra.ofArrow_eq_ofPath already normalizes its left-hand side.

theorem TauCeti.ginzburgTwoDifferential_ofArrow_loop {Q : Type u} [Quiver Q] (k : Type w) [CommRing k] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] (i : Q) : (ginzburgTwoDifferential k) (PathAlgebra.ofArrow (GinzburgHom.loop i)) = (ginzburgMap k) (localPreprojectiveRelator k i)

The differential of the adjoined loop t_i is the local preprojective relator ρ_i, the defining equation of the two-dimensional Ginzburg differential graded algebra. Deliberately not a simp lemma: TauCeti.PathAlgebra.ofArrow_eq_ofPath already normalizes its left-hand side.

The differential graded algebra

@[simp]

theorem TauCeti.ginzburgTwoDifferential_ginzburgMap {Q : Type u} [Quiver Q] (k : Type w) [CommRing k] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] (x : pathAlgebra k (Quiver.Symmetrify Q)) : (ginzburgTwoDifferential k) ((ginzburgMap k) x) = 0

The doubled path algebra consists of cycles: the differential kills every doubled arrow, hence every path in them.

theorem TauCeti.isDGAlgebra_ginzburgTwoDifferential {Q : Type u} [Quiver Q] (k : Type w) [CommRing k] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] : IsDGAlgebra (PathAlgebra.gradeBy k fun {a b : GinzburgQuiver Q} => ginzburgTwoDegree) (ginzburgTwoDifferential k)

The two-dimensional Ginzburg differential graded algebra Π₂(Q): the path algebra of the Ginzburg quiver, graded by the cohomological degree, with the Ginzburg differential.

theorem TauCeti.ginzburgTwoDifferential_mul {Q : Type u} [Quiver Q] (k : Type w) [CommRing k] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] {m : ℤ} {x : pathAlgebra k (GinzburgQuiver Q)} (hx : x ∈ PathAlgebra.gradeBy k (fun {a b : GinzburgQuiver Q} => ginzburgTwoDegree) m) (y : pathAlgebra k (GinzburgQuiver Q)) : (ginzburgTwoDifferential k) (x * y) = (ginzburgTwoDifferential k) x * y + m.negOnePow • (x * (ginzburgTwoDifferential k) y)

The Leibniz rule for the Ginzburg differential on a left factor homogeneous of cohomological degree m.

@[simp]

theorem TauCeti.ginzburgTwoDifferential_sq_zero {Q : Type u} [Quiver Q] (k : Type w) [CommRing k] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] (x : pathAlgebra k (GinzburgQuiver Q)) : (ginzburgTwoDifferential k) ((ginzburgTwoDifferential k) x) = 0

The square of the Ginzburg differential vanishes.

The Adams grading

theorem TauCeti.ginzburgTwoDifferential_mem_gradeBy_ginzburgTwoAdamsDegree {Q : Type u} [Quiver Q] (k : Type w) [CommRing k] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] {n : ℕ} {x : pathAlgebra k (GinzburgQuiver Q)} (hx : x ∈ PathAlgebra.gradeBy k (fun {a b : GinzburgQuiver Q} => ginzburgTwoAdamsDegree) n) : (ginzburgTwoDifferential k) x ∈ PathAlgebra.gradeBy k (fun {a b : GinzburgQuiver Q} => ginzburgTwoAdamsDegree) n

The Ginzburg differential preserves the Adams grading. Together with TauCeti.isDGAlgebra_ginzburgTwoDifferential this says that it has bidegree (1, 0).