The loop-count grading of the two-dimensional Ginzburg path algebra

The Ginzburg quiver of a quiver Q consists of the doubled arrows and one additional loop t_i at every vertex. Its cohomological grading gives doubled arrows degree 0 and the loops degree -1. This file introduces the companion natural-number weight TauCeti.ginzburgLoopCount, which gives the same arrows weights 0 and 1 respectively.

The two path weights contain exactly the same information: the cohomological degree of a path is the negative of its loop count. Consequently the cohomological degree -n piece is literally the loop-count degree n piece, not merely isomorphic to it, and every positive cohomological piece vanishes. In particular, degree zero is spanned precisely by paths containing no adjoined loop. This is the path decomposition needed to identify the zeroth cohomology of the two-dimensional Ginzburg DG algebra with the additive preprojective algebra. The image of TauCeti.ginzburgMap is exactly cohomological degree zero, and TauCeti.ginzburgRetraction kills adjoined loops and inverts that map on degree zero.

Main results

• Quiver.Path.addWeight_ginzburgTwoDegree_eq_neg_addWeight_ginzburgLoopCount: the two weights of a Ginzburg path differ by sign.
• TauCeti.gradeBy_ginzburgTwoDegree_neg_eq_gradeBy_ginzburgLoopCount: the degree -n cohomological piece is the piece containing exactly n adjoined loops.
• TauCeti.gradeBy_ginzburgTwoDegree_eq_bot_of_pos: positive cohomological pieces vanish.
• TauCeti.ginzburgRetraction: the retraction onto the doubled path algebra.
• TauCeti.mem_gradeBy_ginzburgTwoDegree_zero_iff: degree zero is the image of the doubled path algebra.

References

• B. Keller, Deformed Calabi--Yau completions, Section 6.5.
• T. Etgü and Y. Lekili, Koszul duality patterns in Floer theory, Section 4.

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

The number of adjoined Ginzburg loops contributed by an arrow. A doubled arrow contributes zero and a loop t_i contributes one.

Equations

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

@[simp]

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

@[simp]

theorem TauCeti.ginzburgLoopCount_loop {Q : Type u} [Quiver Q] (i : Q) : ginzburgLoopCount (GinzburgHom.loop i) = 1

theorem TauCeti.ginzburgTwoDegree_eq_neg_ginzburgLoopCount {Q : Type u} [Quiver Q] {i j : GinzburgQuiver Q} (e : i ⟶ j) : ginzburgTwoDegree e = -↑(ginzburgLoopCount e)

On every Ginzburg arrow, cohomological degree is the negative of loop count.

theorem Quiver.Path.addWeight_ginzburgTwoDegree_eq_neg_addWeight_ginzburgLoopCount {Q : Type u} [Quiver Q] {i j : TauCeti.GinzburgQuiver Q} (p : Path i j) : addWeight (fun {i j : TauCeti.GinzburgQuiver Q} => TauCeti.ginzburgTwoDegree) p = -↑(addWeight (fun {i j : TauCeti.GinzburgQuiver Q} => TauCeti.ginzburgLoopCount) p)

The cohomological degree of a Ginzburg path is the negative of its number of adjoined loops.

@[simp]

theorem Quiver.Path.addWeight_ginzburgTwoDegree_eq_neg_iff {Q : Type u} [Quiver Q] {i j : TauCeti.GinzburgQuiver Q} (p : Path i j) (n : ℕ) : addWeight (fun {i j : TauCeti.GinzburgQuiver Q} => TauCeti.ginzburgTwoDegree) p = -↑n ↔ addWeight (fun {i j : TauCeti.GinzburgQuiver Q} => TauCeti.ginzburgLoopCount) p = n

A Ginzburg path has cohomological degree -n exactly when it contains n adjoined loops.

@[simp]

theorem Quiver.Path.addWeight_ginzburgTwoDegree_eq_zero_iff {Q : Type u} [Quiver Q] {i j : TauCeti.GinzburgQuiver Q} (p : Path i j) : addWeight (fun {i j : TauCeti.GinzburgQuiver Q} => TauCeti.ginzburgTwoDegree) p = 0 ↔ addWeight (fun {i j : TauCeti.GinzburgQuiver Q} => TauCeti.ginzburgLoopCount) p = 0

A Ginzburg path has cohomological degree zero exactly when it contains no adjoined loop.

theorem Quiver.Path.addWeight_ginzburgTwoDegree_nonpos {Q : Type u} [Quiver Q] {i j : TauCeti.GinzburgQuiver Q} (p : Path i j) : addWeight (fun {i j : TauCeti.GinzburgQuiver Q} => TauCeti.ginzburgTwoDegree) p ≤ 0

Every Ginzburg path has nonpositive cohomological degree.

@[simp]

theorem Quiver.Path.addWeight_ginzburgLoopCount_mapPath {Q : Type u} [Quiver Q] {i j : Symmetrify Q} (p : Path i j) : addWeight (fun {i j : TauCeti.GinzburgQuiver Q} => TauCeti.ginzburgLoopCount) (TauCeti.ginzburgOf.mapPath p) = 0

The inclusion of the doubled quiver contributes no adjoined loops to a path.

theorem TauCeti.gradeBy_ginzburgTwoDegree_neg_eq_gradeBy_ginzburgLoopCount {Q : Type u} [Quiver Q] (k : Type w) [Semiring k] (n : ℕ) : PathAlgebra.gradeBy k (fun {a b : GinzburgQuiver Q} => ginzburgTwoDegree) (-↑n) = PathAlgebra.gradeBy k (fun {a b : GinzburgQuiver Q} => ginzburgLoopCount) n

The cohomological degree -n part of the Ginzburg path algebra is exactly its loop-count degree n part.

theorem TauCeti.gradeBy_ginzburgTwoDegree_zero_eq_gradeBy_ginzburgLoopCount_zero {Q : Type u} [Quiver Q] (k : Type w) [Semiring k] : PathAlgebra.gradeBy k (fun {a b : GinzburgQuiver Q} => ginzburgTwoDegree) 0 = PathAlgebra.gradeBy k (fun {a b : GinzburgQuiver Q} => ginzburgLoopCount) 0

The degree-zero cohomological piece consists exactly of linear combinations of paths with no adjoined loop.

theorem TauCeti.gradeBy_ginzburgTwoDegree_eq_bot_of_pos {Q : Type u} [Quiver Q] (k : Type w) [Semiring k] {m : ℤ} (hm : 0 < m) : PathAlgebra.gradeBy k (fun {a b : GinzburgQuiver Q} => ginzburgTwoDegree) m = ⊥

Every positive cohomological piece of the two-dimensional Ginzburg path algebra vanishes.

theorem TauCeti.ginzburgMap_mem_gradeBy_ginzburgLoopCount_zero {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} => ginzburgLoopCount) 0

The doubled path algebra lands in loop-count degree zero inside the Ginzburg path algebra.

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

Every cohomological degree-zero element is a cycle in the two-dimensional Ginzburg DG algebra.

Killing the adjoined loops

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

The algebra homomorphism from the Ginzburg path algebra to the doubled path algebra which fixes the vertex idempotents and the doubled arrows and kills every adjoined loop t_i. It follows the construction of TauCeti.PathAlgebra.symmetrifyRetraction: a Ginzburg path goes to itself when it uses no loop, and to zero otherwise.

Equations

• TauCeti.ginzburgRetraction k = TauCeti.PathAlgebra.liftAlgHom k (fun (x : TauCeti.Quiver.TotalPath (TauCeti.GinzburgQuiver Q)) => TauCeti.ginzburgRetractPath✝ k x.snd.snd) ⋯ ⋯ ⋯

@[simp]

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

The retraction fixes every vertex idempotent.

@[simp]

theorem TauCeti.ginzburgRetraction_ofArrow_loop (k : Type w) {Q : Type u} [CommSemiring k] [Quiver Q] [Finite Q] (i : Q) : (ginzburgRetraction k) (PathAlgebra.ofArrow (GinzburgHom.loop i)) = 0

The retraction kills every adjoined loop.

@[simp]

theorem TauCeti.ginzburgRetraction_comp_ginzburgMap (k : Type w) {Q : Type u} [CommSemiring k] [Quiver Q] [Finite Q] : (ginzburgRetraction k).comp (ginzburgMap k) = AlgHom.id k (pathAlgebra k (Quiver.Symmetrify Q))

The retraction is a left inverse of the inclusion of the doubled path algebra.

@[simp]

theorem TauCeti.ginzburgRetraction_ginzburgMap (k : Type w) {Q : Type u} [CommSemiring k] [Quiver Q] [Finite Q] (x : pathAlgebra k (Quiver.Symmetrify Q)) : (ginzburgRetraction k) ((ginzburgMap k) x) = x

The retraction undoes the inclusion of the doubled path algebra.

@[simp]

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

The retraction fixes every doubled arrow.

@[simp]

theorem TauCeti.ginzburgRetraction_ofPath_loop (k : Type w) {Q : Type u} [CommSemiring k] [Quiver Q] [Finite Q] (i : Q) : (ginzburgRetraction k) (PathAlgebra.ofPath ⟨i, ⟨i, Quiver.Hom.toPath (GinzburgHom.loop i)⟩⟩) = 0

The retraction kills an adjoined loop in the path basis.

@[simp]

theorem TauCeti.ginzburgRetraction_ofPath_double (k : Type w) {Q : Type u} [CommSemiring k] [Quiver Q] [Finite Q] {i j : Q} (a : (i ⟶ j) ⊕ (j ⟶ i)) : (ginzburgRetraction k) (PathAlgebra.ofPath ⟨i, ⟨j, Quiver.Hom.toPath (GinzburgHom.double a)⟩⟩) = PathAlgebra.ofPath ⟨i, ⟨j, Quiver.Hom.toPath a⟩⟩

The retraction sends a doubled arrow to the corresponding doubled path.

theorem TauCeti.ginzburgMap_injective (k : Type w) {Q : Type u} [CommSemiring k] [Quiver Q] [Finite Q] : Function.Injective ⇑(ginzburgMap k)

The inclusion of the doubled path algebra in the Ginzburg path algebra is injective.

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

The retraction is a right inverse of the inclusion on cohomological degree 0.

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

Cohomological degree 0 of the Ginzburg path algebra is the doubled path algebra: an element has degree 0 exactly when it is the image of an element of the doubled path algebra.