The completed two-dimensional Ginzburg differential graded algebra

Let Q be a finite quiver and Π₂(Q) its non-completed two-dimensional Ginzburg differential graded algebra, the path algebra of the Ginzburg quiver with the differential TauCeti.ginzburgTwoDifferential (TauCeti.isDGAlgebra_ginzburgTwoDifferential). Besides its cohomological grading it carries the Adams grading TauCeti.ginzburgTwoAdamsDegree, in which the doubled arrows have degree 1 and the adjoined loops degree 2, and the differential has bidegree (1, 0).

The completed two-dimensional Ginzburg algebra Π̂₂(Q) is the length-adic completion of Π₂(Q) along this Adams grading, taken in the category of graded modules: in each cohomological degree, the finite sums of paths are replaced by formal series of paths of unbounded Adams degree. It is the Adams completion TauCeti.adamsCompletion of Π₂(Q), a subalgebra of the formal power series over the Ginzburg path algebra whose coefficient of index n is Adams-homogeneous of degree n, with the coefficientwise differential. The two gradings of the Ginzburg path algebra are compatible because every path is homogeneous for both at once.

The comparison morphism TauCeti.ginzburgTwoToCompleted from Π₂(Q) to Π̂₂(Q) is an injective morphism of differential graded algebras whose image consists of the series with finitely many nonzero coefficients. The ordinary and the completed algebra are distinct objects and are not interchanged: which of the two a derived Koszul duality statement produces depends on whether the Adams grading is retained or forgotten.

Main definitions

• TauCeti.completedGinzburgTwo: the completed two-dimensional Ginzburg algebra Π̂₂(Q).
• TauCeti.completedGinzburgTwoGrading and TauCeti.completedGinzburgTwoDifferential: its cohomological grading and its differential.
• TauCeti.ginzburgTwoToCompleted: the comparison morphism of differential graded algebras Π₂(Q) → Π̂₂(Q).

Main results

• TauCeti.isHomogeneous_gradeBy_ginzburgTwoAdamsDegree and TauCeti.isHomogeneous_gradeBy_ginzburgTwoDegree: the cohomological and Adams gradings of the Ginzburg path algebra are compatible.
• TauCeti.isDGAlgebra_completedGinzburgTwoDifferential: Π̂₂(Q) is a differential graded algebra.
• TauCeti.mem_completedGinzburgTwo_iff: its elements are the series of Adams-homogeneous coefficients with uniformly bounded cohomological degree.
• TauCeti.ginzburgTwoToCompleted_injective and TauCeti.mem_range_ginzburgTwoToCompleted_iff: Π₂(Q) is the finite-support part of Π̂₂(Q).
• TauCeti.completedGinzburgTwoDifferential_ginzburgTwoToCompleted_loop: in the completion the differential of the adjoined loop t_i is still the local preprojective relator ρ_i.

References

• B. Keller, Deformed Calabi--Yau completions, Section 6, for the completed Ginzburg algebra.
• T. Etgü and Y. Lekili, Koszul duality patterns in Floer theory, Section 4, for the completed and the non-completed two-dimensional Ginzburg algebra.

Compatibility of the two gradings

theorem TauCeti.isHomogeneous_gradeBy_ginzburgTwoAdamsDegree (k : Type w) {Q : Type u} [CommRing k] [Quiver Q] [Finite Q] (p : ℤ) : DirectSum.SetLike.IsHomogeneous (PathAlgebra.gradeBy k fun {a b : GinzburgQuiver Q} => ginzburgTwoAdamsDegree) (PathAlgebra.gradeBy k (fun {a b : GinzburgQuiver Q} => ginzburgTwoDegree) p)

The Adams components of a cohomologically homogeneous element of the Ginzburg path algebra are cohomologically homogeneous.

theorem TauCeti.isHomogeneous_gradeBy_ginzburgTwoDegree (k : Type w) {Q : Type u} [CommRing k] [Quiver Q] [Finite Q] (n : ℕ) : DirectSum.SetLike.IsHomogeneous (PathAlgebra.gradeBy k fun {a b : GinzburgQuiver Q} => ginzburgTwoDegree) (PathAlgebra.gradeBy k (fun {a b : GinzburgQuiver Q} => ginzburgTwoAdamsDegree) n)

The cohomological components of an Adams-homogeneous element of the Ginzburg path algebra are Adams-homogeneous.

The completed algebra

@[reducible, inline]

noncomputable abbrev TauCeti.completedGinzburgTwo (k : Type w) (Q : Type u) [CommRing k] [Quiver Q] [Finite Q] : Subalgebra k (PowerSeries (pathAlgebra k (GinzburgQuiver Q)))

The completed two-dimensional Ginzburg algebra Π̂₂(Q): the length-adic completion of Π₂(Q) along its Adams grading, in each cohomological degree. Its elements are the formal power series over the Ginzburg path algebra whose coefficient of index n is a combination of paths of Adams degree n, with uniformly bounded cohomological degree.

Equations

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

@[reducible, inline]

noncomputable abbrev TauCeti.completedGinzburgTwoGrading (k : Type w) (Q : Type u) [CommRing k] [Quiver Q] [Finite Q] : ℤ → Submodule k ↥(completedGinzburgTwo k Q)

The cohomological grading of the completed two-dimensional Ginzburg algebra.

Equations

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

theorem TauCeti.mem_completedGinzburgTwo_iff (k : Type w) (Q : Type u) [CommRing k] [Quiver Q] [Finite Q] {f : PowerSeries (pathAlgebra k (GinzburgQuiver Q))} : f ∈ completedGinzburgTwo k Q ↔ (∀ (n : ℕ), (PowerSeries.coeff n) f ∈ PathAlgebra.gradeBy k (fun {a b : GinzburgQuiver Q} => ginzburgTwoAdamsDegree) n) ∧ ∃ (s : Finset ℤ), ∀ (n : ℕ), ∀ p ∉ s, ↑(((DirectSum.decompose (PathAlgebra.gradeBy k fun {a b : GinzburgQuiver Q} => ginzburgTwoDegree)) ((PowerSeries.coeff n) f)) p) = 0

The elements of Π̂₂(Q) are the power series whose coefficient of index n is a combination of paths of Adams degree n, and whose cohomological components vanish outside a finite set of degrees.

The differential

@[reducible, inline]

noncomputable abbrev TauCeti.completedGinzburgTwoDifferential (k : Type w) (Q : Type u) [CommRing k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] : ↥(completedGinzburgTwo k Q) →ₗ[k] ↥(completedGinzburgTwo k Q)

The differential of the completed two-dimensional Ginzburg algebra: the Ginzburg differential applied coefficientwise.

Equations

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

theorem TauCeti.isDGAlgebra_completedGinzburgTwoDifferential (k : Type w) (Q : Type u) [CommRing k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] : IsDGAlgebra (completedGinzburgTwoGrading k Q) (completedGinzburgTwoDifferential k Q)

The completed two-dimensional Ginzburg differential graded algebra Π̂₂(Q).

The comparison morphism

noncomputable def TauCeti.ginzburgTwoToCompleted (k : Type w) (Q : Type u) [CommRing k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] : DGAlgHom ⋯ ⋯

The comparison morphism Π₂(Q) → Π̂₂(Q) of differential graded algebras, sending an element of the Ginzburg path algebra to the series of its Adams-homogeneous components.

Equations

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

@[simp]

theorem TauCeti.coe_ginzburgTwoToCompleted_apply (k : Type w) (Q : Type u) [CommRing k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] (x : pathAlgebra k (GinzburgQuiver Q)) : ↑((ginzburgTwoToCompleted k Q) x) = (gradedComponentSeries (PathAlgebra.gradeBy k fun {a b : GinzburgQuiver Q} => ginzburgTwoAdamsDegree)) x

theorem TauCeti.coeff_ginzburgTwoToCompleted (k : Type w) (Q : Type u) [CommRing k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] (x : pathAlgebra k (GinzburgQuiver Q)) (n : ℕ) : (PowerSeries.coeff n) ↑((ginzburgTwoToCompleted k Q) x) = ↑(((DirectSum.decompose (PathAlgebra.gradeBy k fun {a b : GinzburgQuiver Q} => ginzburgTwoAdamsDegree)) x) n)

The coefficient of index n of the image of an element of Π₂(Q) is its component of Adams degree n.

theorem TauCeti.ginzburgTwoToCompleted_injective (k : Type w) (Q : Type u) [CommRing k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] : Function.Injective ⇑(ginzburgTwoToCompleted k Q)

Π₂(Q) embeds in Π̂₂(Q).

theorem TauCeti.mem_range_ginzburgTwoToCompleted_iff (k : Type w) (Q : Type u) [CommRing k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] {f : ↥(completedGinzburgTwo k Q)} : f ∈ Set.range ⇑(ginzburgTwoToCompleted k Q) ↔ (Function.support fun (n : ℕ) => (PowerSeries.coeff n) ↑f).Finite

Π₂(Q) is the finite-support part of Π̂₂(Q): an element of the completion comes from the non-completed algebra exactly when only finitely many of its coefficients are nonzero.

theorem TauCeti.completedGinzburgTwoDifferential_ginzburgTwoToCompleted_loop (k : Type w) (Q : Type u) [CommRing k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] (i : Q) : (completedGinzburgTwoDifferential k Q) ((ginzburgTwoToCompleted k Q) (PathAlgebra.ofArrow (GinzburgHom.loop i))) = (ginzburgTwoToCompleted k Q) ((ginzburgMap k) (localPreprojectiveRelator k i))

In the completion, the differential of the adjoined loop t_i is the local preprojective relator ρ_i, the defining equation of the two-dimensional Ginzburg differential.