Documentation

TauCeti.Algebra.Homology.Ginzburg.ThreeDimensional

The three-dimensional Ginzburg differential graded algebra of a quiver with potential #

Let Q be a finite quiver and W ∈ kQ a potential, typically a linear combination of cycles; only its cycles matter, since the cyclic derivative of a path which is not a cycle vanishes. The three-dimensional Ginzburg differential graded algebra Γ₃(Q, W) is the path algebra of the Ginzburg quiver TauCeti.GinzburgQuiver Q (the doubled quiver of Q with one extra loop t_i at every vertex), graded cohomologically by putting

with the degree +1 graded derivation d given on the arrows by

d a = 0,    d a* = ∂_a W,    d t_i = ρ_i = ∑_{head a = i} a a* - ∑_{tail a = i} a* a,

where ∂_a is the cyclic derivative TauCeti.PathAlgebra.cyclicDerivative and ρ_i the local preprojective relator TauCeti.localPreprojectiveRelator. The words a a* and a* a are read in Tau Ceti's later-factor-first convention, as in the two-dimensional Ginzburg algebra of TauCeti.Algebra.Homology.Ginzburg.Basic.

The quiver is the one of the two-dimensional Ginzburg algebra Π₂(Q), but the grading and the differential differ, so the two differential graded algebras are distinct. The square of d vanishes on a and on a* because the path algebra of Q consists of cycles of d; on t_i,

d (d t_i) = ∑_{head a = i} a ∂_a W - ∑_{tail a = i} ∂_a W a,

which vanishes by the local cyclic identity TauCeti.PathAlgebra.sum_ofArrow_mul_cyclicDerivative_eq_sum_cyclicDerivative_mul_ofArrow.

Main definitions #

Main results #

References #

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

The cohomological degree of an arrow of the Ginzburg quiver in the three-dimensional Ginzburg algebra: the original arrows of Q sit in degree 0, their formal reverses in degree -1, and the adjoined loops in degree -2.

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.ginzburgThreeDegree_double_inl {Q : Type u} [Quiver Q] {i j : Q} (a : i ⟶ j) :
    ginzburgThreeDegree (GinzburgHom.double (Sum.inl a)) = 0
    source
    @[simp]
    theorem TauCeti.ginzburgThreeDegree_double_inr {Q : Type u} [Quiver Q] {i j : Q} (a : j ⟶ i) :
    ginzburgThreeDegree (GinzburgHom.double (Sum.inr a)) = -1
    source
    @[simp]
    theorem TauCeti.ginzburgThreeDegree_loop {Q : Type u} [Quiver Q] (i : Q) :
    ginzburgThreeDegree (GinzburgHom.loop i) = -2
    source
    theorem TauCeti.ginzburgOriginalMap_mem_gradeBy_ginzburgThreeDegree {Q : Type u} [Quiver Q] {k : Type w} [CommSemiring k] [Finite Q] (x : pathAlgebra k Q) :
    (ginzburgOriginalMap k) x ∈ PathAlgebra.gradeBy k (fun {a b : GinzburgQuiver Q} => ginzburgThreeDegree) 0

    The path algebra of Q lands in cohomological degree 0: it is generated by the original arrows, all of which have degree 0.

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

    The relator assigned to an arrow in the three-dimensional Ginzburg differential of (Q, W): zero on the original arrows, the cyclic derivative ∂_a W on the reverse a* of an arrow a, and the local preprojective relator at the vertex of an adjoined loop.

    Equations
    Instances For
      source
      @[simp]
      theorem TauCeti.ginzburgThreeArrowRelator_double_inl {Q : Type u} [Quiver Q] (k : Type w) [CommRing k] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] (W : pathAlgebra k Q) {i j : Q} (a : i ⟶ j) :
      ginzburgThreeArrowRelator k W (GinzburgHom.double (Sum.inl a)) = 0
      source
      @[simp]
      theorem TauCeti.ginzburgThreeArrowRelator_double_inr {Q : Type u} [Quiver Q] (k : Type w) [CommRing k] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] (W : pathAlgebra k Q) {i j : Q} (a : j ⟶ i) :
      ginzburgThreeArrowRelator k W (GinzburgHom.double (Sum.inr a)) = (ginzburgOriginalMap k) ((PathAlgebra.cyclicDerivative k a) W)
      source
      @[simp]
      theorem TauCeti.ginzburgThreeArrowRelator_loop {Q : Type u} [Quiver Q] (k : Type w) [CommRing k] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] (W : pathAlgebra k Q) (i : Q) :
      ginzburgThreeArrowRelator k W (GinzburgHom.loop i) = (ginzburgMap k) (localPreprojectiveRelator k i)
      source
      noncomputable def TauCeti.ginzburgThreeDifferential {Q : Type u} [Quiver Q] (k : Type w) [CommRing k] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] (W : pathAlgebra k Q) :
      pathAlgebra k (GinzburgQuiver Q) →ₗ[k] pathAlgebra k (GinzburgQuiver Q)

      The three-dimensional Ginzburg differential of (Q, W): the degree +1 graded derivation which kills the original arrows, sends the reverse a* of an arrow a to the cyclic derivative ∂_a W, 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.
      Instances For
        source
        @[simp]
        theorem TauCeti.ginzburgThreeDifferential_vertexIdempotent {Q : Type u} [Quiver Q] (k : Type w) [CommRing k] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] (W : pathAlgebra k Q) (v : GinzburgQuiver Q) :
        (ginzburgThreeDifferential k W) (PathAlgebra.vertexIdempotent k v) = 0
        source
        theorem TauCeti.ginzburgThreeDifferential_ofArrow {Q : Type u} [Quiver Q] (k : Type w) [CommRing k] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] (W : pathAlgebra k Q) {i j : GinzburgQuiver Q} (e : i ⟶ j) :
        (ginzburgThreeDifferential k W) (PathAlgebra.ofArrow e) = ginzburgThreeArrowRelator k W e

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

        source
        theorem TauCeti.ginzburgThreeDifferential_ofArrow_mul {Q : Type u} [Quiver Q] (k : Type w) [CommRing k] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] (W : pathAlgebra k Q) {i j : GinzburgQuiver Q} (e : i ⟶ j) (z : pathAlgebra k (GinzburgQuiver Q)) :
        (ginzburgThreeDifferential k W) (PathAlgebra.ofArrow e * z) = ginzburgThreeArrowRelator k W e * z + (ginzburgThreeDegree e).negOnePow • (PathAlgebra.ofArrow e * (ginzburgThreeDifferential k W) z)

        The three-dimensional Ginzburg Leibniz rule against an arrow.

        source
        @[simp]
        theorem TauCeti.ginzburgThreeDifferential_ofArrow_original {Q : Type u} [Quiver Q] (k : Type w) [CommRing k] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] (W : pathAlgebra k Q) {i j : Q} (a : i ⟶ j) :
        (ginzburgThreeDifferential k W) (PathAlgebra.ofArrow (GinzburgHom.double (Sum.inl a))) = 0

        The original arrows are cycles of the three-dimensional Ginzburg differential.

        source
        @[simp]
        theorem TauCeti.ginzburgThreeDifferential_ofArrow_reverse {Q : Type u} [Quiver Q] (k : Type w) [CommRing k] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] (W : pathAlgebra k Q) {i j : Q} (a : j ⟶ i) :
        (ginzburgThreeDifferential k W) (PathAlgebra.ofArrow (GinzburgHom.double (Sum.inr a))) = (ginzburgOriginalMap k) ((PathAlgebra.cyclicDerivative k a) W)

        The differential of the reverse a* of an arrow a is the cyclic derivative ∂_a W.

        source
        @[simp]
        theorem TauCeti.ginzburgThreeDifferential_ofArrow_loop {Q : Type u} [Quiver Q] (k : Type w) [CommRing k] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] (W : pathAlgebra k Q) (i : Q) :
        (ginzburgThreeDifferential k W) (PathAlgebra.ofArrow (GinzburgHom.loop i)) = (ginzburgMap k) (localPreprojectiveRelator k i)

        The differential of the adjoined loop t_i is the local preprojective relator ρ_i.

        source
        @[simp]
        theorem TauCeti.ginzburgThreeDifferential_ginzburgOriginalMap {Q : Type u} [Quiver Q] (k : Type w) [CommRing k] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] (W x : pathAlgebra k Q) :
        (ginzburgThreeDifferential k W) ((ginzburgOriginalMap k) x) = 0

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

        The differential graded algebra #

        source
        theorem TauCeti.isDGAlgebra_ginzburgThreeDifferential {Q : Type u} [Quiver Q] (k : Type w) [CommRing k] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] (W : pathAlgebra k Q) :
        IsDGAlgebra (PathAlgebra.gradeBy k fun {a b : GinzburgQuiver Q} => ginzburgThreeDegree) (ginzburgThreeDifferential k W)

        The three-dimensional Ginzburg differential graded algebra Γ₃(Q, W): the path algebra of the Ginzburg quiver, graded by TauCeti.ginzburgThreeDegree, with the Ginzburg differential of the potential W.

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

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

        source
        @[simp]
        theorem TauCeti.ginzburgThreeDifferential_sq_zero {Q : Type u} [Quiver Q] (k : Type w) [CommRing k] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] (W : pathAlgebra k Q) (x : pathAlgebra k (GinzburgQuiver Q)) :
        (ginzburgThreeDifferential k W) ((ginzburgThreeDifferential k W) x) = 0

        The square of the three-dimensional Ginzburg differential vanishes.

        source
        theorem TauCeti.ginzburgThreeDifferential_add_mul_sub_mul {Q : Type u} [Quiver Q] (k : Type w) [CommRing k] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] (W x y : pathAlgebra k Q) :
        ginzburgThreeDifferential k (W + (x * y - y * x)) = ginzburgThreeDifferential k W

        The three-dimensional Ginzburg differential only depends on the potential up to cyclic equivalence: adding a commutator x y - y x to W does not change it.