Zigzag, preprojective, and Ginzburg algebras

The declarations the status of Tau Ceti's roadmap names as Tau Ceti has them at commit ace60277.

TheoremThe Koszulity dichotomy for zigzag algebras#

for a connected finite simple graph G on at least two vertices, every graded vertex simple of ZigzagAlgebra k G admits a linear graded projective resolution if and only if G is not isomorphic to the diagram of any valid Dynkin type.

TauCeti.forall_exists_isLinear_zigzagGradedSimple_iff.{u, w} (k : Type w) [Field k] {V : Type u}
  {G : SimpleGraph V} [Finite V] [Nontrivial V] (hG : G.Connected) :
  (∀ (v : V), ∃ r, r.IsLinear) ↔ ¬∃ t, t.Valid ∧ Nonempty (G ≃g TauCeti.diagramGraph t.cartanMatrix)
Lean

Formalized in Tau Ceti as TauCeti.forall_exists_isLinear_zigzagGradedSimple_iff.

Sources
LeanTauCeti.forall_exists_isLinear_zigzagGradedSimple_iff
Uses 3
Statement usesTauCeti.GradedProjectiveResolution.IsLinear
Proof usesThe entrywise graded Cartan formula · The Koszul defect formula

TheoremThe finite/infinite dichotomy for preprojective algebras of oriented graphs#

for a connected finite simple graph G and any orientation o of G, the preprojective algebra Π_k(OrientedQuiver G o) is finite-dimensional over k if and only if G is isomorphic to the diagram of a valid Dynkin type.

TauCeti.finiteDimensional_preprojectiveAlgebra_orientedQuiver_iff.{u_1, u_2} (k : Type u_1)
  [Field k] {V : Type u_2} [Finite V] {G : SimpleGraph V} (hG : G.Connected)
  (o : TauCeti.DoubledQuiver.Orientation G) :
  FiniteDimensional k (TauCeti.preprojectiveAlgebra k (TauCeti.DoubledQuiver.OrientedQuiver G o)) ↔
    ∃ t, t.Valid ∧ Nonempty (G ≃g TauCeti.diagramGraph t.cartanMatrix)
Lean

Formalized in Tau Ceti as TauCeti.finiteDimensional_preprojectiveAlgebra_orientedQuiver_iff.

Sources
LeanTauCeti.finiteDimensional_preprojectiveAlgebra_orientedQuiver_iff

TheoremThe Koszulity dichotomy for preprojective algebras of oriented graphs#

for a connected finite simple graph G and any orientation o of G, the left Koszul differential of Π_k(OrientedQuiver G o) is injective at every vertex if and only if G is not isomorphic to the diagram of any valid Dynkin type.

TauCeti.forall_preprojectiveKoszulLeft_injective_iff.{u, w} (k : Type w) [Field k] {V : Type u}
  {G : SimpleGraph V} [Finite V] (hG : G.Connected) (o : TauCeti.DoubledQuiver.Orientation G) :
  (∀ (v : TauCeti.DoubledQuiver.OrientedQuiver G o),
      Function.Injective ⇑(TauCeti.preprojectiveKoszulLeft k v)) ↔
    ¬∃ t, t.Valid ∧ Nonempty (G ≃g TauCeti.diagramGraph t.cartanMatrix)
Lean

Formalized in Tau Ceti as TauCeti.forall_preprojectiveKoszulLeft_injective_iff.

Sources
LeanTauCeti.forall_preprojectiveKoszulLeft_injective_iff
Uses 1
Proof usesThe Koszul defect formula

DefinitionThe braid group action of a zigzag algebra#

The Artin group of the graph G acts on the homotopy category of graded Z-modules, by sending the standard generator at a vertex i to the class of tensoring with the braid complex Bᵢ.

TauCeti.zigzagBraidArtinAction.{u, w} (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V)
  [Finite V] :
  TauCeti.ArtinGroup G.coxeterMatrix →*
    TauCeti.AutoequivalenceClass
      (HomotopyCategory
        (TauCeti.GradedModuleCat ((TauCeti.zigzagAlgebraInternalGrading k G).piece ℤ))
        (ComplexShape.up ℤ))
Lean

Formalized in Tau Ceti as TauCeti.zigzagBraidArtinAction.

Sources
LeanTauCeti.zigzagBraidArtinAction

DefinitionThe action of the graph's Artin group on K₀^gr(proj Z)#

The standard generator at i acts by the deformed simple reflection at q, in the basis of vertex-projective classes; by TauCeti.zigzagBraidK0Action_gen_zigzagAlgebraGradedProjectiveClass it sends [P_j] to the Euler class of the braid complex B_i ⊗_Z P_j.

TauCeti.zigzagBraidK0Action.{u, w} (k : Type w) {V : Type u} [Finite V] (G : SimpleGraph V)
  [Field k] [Fintype V] [DecidableEq V] :
  TauCeti.ArtinGroup G.coxeterMatrix →*
    TauCeti.LaurentK0
        (TauCeti.gradedFiniteProjectiveModulesExactStructure
          (TauCeti.zigzagAlgebraIntegerGrade k G)) ≃ₗ[LaurentPolynomial ℤ]
      TauCeti.LaurentK0
        (TauCeti.gradedFiniteProjectiveModulesExactStructure
          (TauCeti.zigzagAlgebraIntegerGrade k G))
Lean

Formalized in Tau Ceti as TauCeti.zigzagBraidK0Action.

Sources
LeanTauCeti.zigzagBraidK0Action
Uses 4
Proof usesThe dual Noether isomorphism · Jacobson's lemma · The Noether isomorphism for exact categories · TauCeti.isLocalRing_end_of_indecomposable

TheoremLiu--Wang's A∞ algebra is formal, for every scalar c#

the displayed quartic operation m₄ is a Hochschild coboundary of the strict zigzag algebra, so it defines the trivial A∞ deformation.

TauCeti.isFormal_liuWangAffineD4AInfinityAlgebra.{w} {k : Type w} [CommRing k] (c : k) :
  (TauCeti.liuWangAffineD4AInfinityAlgebra k c).IsFormal
Lean

Formalized in Tau Ceti as TauCeti.isFormal_liuWangAffineD4AInfinityAlgebra.

Sources
LeanTauCeti.isFormal_liuWangAffineD4AInfinityAlgebra

TheoremThe quartic Hochschild cohomology HH^{4, -2} of a zigzag algebra is nonzero#

The quartic Hochschild cohomology HH^{4, -2} of a zigzag algebra is nonzero when four distinct darts of G have a common head, that is when some vertex has four distinct neighbours, over every nontrivial commutative ring: some Hochschild cocycle of the strict zigzag algebra of suspended degree one, concentrated on words of length four, is not the Hochschild differential of a cochain of degree zero.

TauCeti.not_hochschildVanishesAt_four_zigzagStrictAInfinityAlgebra.{u, w} {k : Type w} [CommRing k]
  {V : Type u} {G : SimpleGraph V} [Finite V] {hns : ∀ (i : V), ∃ j, G.Adj i j} [Nontrivial k]
  {δ : Fin 4 → G.Dart} (hδ : Function.Injective δ) {v : V}
  (hv : ∀ (i : Fin 4), (δ i).toProd.2 = v) :
  ¬(TauCeti.zigzagStrictAInfinityAlgebra k hns).HochschildVanishesAt
      ⟨4, TauCeti.not_hochschildVanishesAt_four_zigzagStrictAInfinityAlgebra._proof_1⟩
Lean

Formalized in Tau Ceti as TauCeti.not_hochschildVanishesAt_four_zigzagStrictAInfinityAlgebra.

Sources
LeanTauCeti.not_hochschildVanishesAt_four_zigzagStrictAInfinityAlgebra

TheoremCouture's classification#

over a commutative ring, two skew-zigzag parameters of a finite graph have the same cohomology class in H¹(G, kˣ) exactly when their relation quotients are isomorphic by an algebra isomorphism fixing every vertex idempotent.

TauCeti.SkewZigzagParameter.cohomologyClass_eq_iff_exists_vertexFixing_algEquiv.{u, w} {V : Type u}
  {G : SimpleGraph V} {k : Type w} [CommRing k] [Finite V]
  {c c' : TauCeti.SkewZigzagParameter k G} :
  (TauCeti.SkewZigzagParameter.cohomologyClass k G) c =
      (TauCeti.SkewZigzagParameter.cohomologyClass k G) c' ↔
    ∃ φ,
      ∀ (i : V),
        φ
            ((TauCeti.skewZigzagMk k G c)
              (TauCeti.PathAlgebra.vertexIdempotent k (TauCeti.DoubledQuiver.vertex G i))) =
          (TauCeti.skewZigzagMk k G c')
            (TauCeti.PathAlgebra.vertexIdempotent k (TauCeti.DoubledQuiver.vertex G i))
Lean

Formalized in Tau Ceti as TauCeti.SkewZigzagParameter.cohomologyClass_eq_iff_exists_vertexFixing_algEquiv.

Other forms

Couture's classification up to graph automorphisms. Formalized in Tau Ceti as TauCeti.SkewZigzagParameter.exists_firstCohomologyRelabel_eq_iff_exists_algEquiv_mem_span.

TauCeti.SkewZigzagParameter.exists_firstCohomologyRelabel_eq_iff_exists_algEquiv_mem_span.{u, w}
  {k : Type w} [CommRing k] {V : Type u} {G : SimpleGraph V} [Finite V]
  {c c' : TauCeti.SkewZigzagParameter k G} [Nontrivial k]
  (hidempotents : ∀ (e : k), IsIdempotentElem e → e = 0 ∨ e = 1) :
  (∃ τ,
      (SimpleGraph.firstCohomologyRelabel kˣ τ)
          ((TauCeti.SkewZigzagParameter.cohomologyClass k G) c) =
        (TauCeti.SkewZigzagParameter.cohomologyClass k G) c') ↔
    ∃ φ,
      ∀ (i : V),
        φ
            ((TauCeti.skewZigzagMk k G c)
              (TauCeti.PathAlgebra.vertexIdempotent k (TauCeti.DoubledQuiver.vertex G i))) ∈
          Submodule.span k
            (Set.range fun j =>
              (TauCeti.skewZigzagMk k G c')
                (TauCeti.PathAlgebra.vertexIdempotent k (TauCeti.DoubledQuiver.vertex G j)))

Couture's classification up to graph automorphisms, permuting form. Formalized in Tau Ceti as TauCeti.SkewZigzagParameter.exists_firstCohomologyRelabel_eq_iff_exists_vertexPermuting_algEquiv.

TauCeti.SkewZigzagParameter.exists_firstCohomologyRelabel_eq_iff_exists_vertexPermuting_algEquiv.{u,
    w}
  {k : Type w} [CommRing k] {V : Type u} {G : SimpleGraph V} [Finite V]
  {c c' : TauCeti.SkewZigzagParameter k G} [Nontrivial k] :
  (∃ τ,
      (SimpleGraph.firstCohomologyRelabel kˣ τ)
          ((TauCeti.SkewZigzagParameter.cohomologyClass k G) c) =
        (TauCeti.SkewZigzagParameter.cohomologyClass k G) c') ↔
    ∃ φ σ,
      ∀ (i : V),
        φ
            ((TauCeti.skewZigzagMk k G c)
              (TauCeti.PathAlgebra.vertexIdempotent k (TauCeti.DoubledQuiver.vertex G i))) =
          (TauCeti.skewZigzagMk k G c')
            (TauCeti.PathAlgebra.vertexIdempotent k (TauCeti.DoubledQuiver.vertex G (σ i)))
Sources
LeanTauCeti.SkewZigzagParameter.cohomologyClass_eq_iff_exists_vertexFixing_algEquiv · TauCeti.SkewZigzagParameter.exists_firstCohomologyRelabel_eq_iff_exists_algEquiv_mem_span · TauCeti.SkewZigzagParameter.exists_firstCohomologyRelabel_eq_iff_exists_vertexPermuting_algEquiv

TheoremTauCeti.gradedCartanMatrix_zigzagAlgebra#

The categorical graded Cartan map of the public algebra has matrix (1 + q²) I + q A_G in the vertex-projective and vertex-head class bases, including isolated vertices.

TauCeti.gradedCartanMatrix_zigzagAlgebra.{u, w} (k : Type w) [Field k] {V : Type u} [Finite V]
  (G : SimpleGraph V) [Fintype V] [DecidableEq V] [DecidableRel G.Adj] :
  TauCeti.gradedCartanMatrix (TauCeti.zigzagAlgebraIntegerGrade k G)
      (TauCeti.zigzagAlgebraGradedProjectiveClassBasis k G)
      (TauCeti.zigzagAlgebraGradedSimpleClassBasis k G) =
    (1 + LaurentPolynomial.T 2) • 1 +
      LaurentPolynomial.T 1 • SimpleGraph.adjMatrix (LaurentPolynomial ℤ) G
Lean

Formalized in Tau Ceti as TauCeti.gradedCartanMatrix_zigzagAlgebra.

Sources
LeanTauCeti.gradedCartanMatrix_zigzagAlgebra
Uses 5
Statement usesThe graded Cartan matrix in a projective basis bP and a module basis bM
Proof usesThe dual Noether isomorphism · Jacobson's lemma · The Noether isomorphism for exact categories · TauCeti.isLocalRing_end_of_indecomposable

DefinitionTauCeti.zigzagBraidTensorLocalizerMorphism#

The positive braid tensor functor defines a morphism of the quasi-isomorphism localizer.

TauCeti.zigzagBraidTensorLocalizerMorphism.{u, v, w} (k : Type w) [CommRing k] {V : Type u}
  (G : SimpleGraph V) [Finite V] (i : V) :
  CategoryTheory.LocalizerMorphism
    (HomologicalComplex.quasiIso
      (TauCeti.GradedModuleCat ((TauCeti.zigzagAlgebraInternalGrading k G).piece ℤ))
      (ComplexShape.up ℤ))
    (HomologicalComplex.quasiIso
      (TauCeti.GradedModuleCat ((TauCeti.zigzagAlgebraInternalGrading k G).piece ℤ))
      (ComplexShape.up ℤ))
Lean

Formalized in Tau Ceti as TauCeti.zigzagBraidTensorLocalizerMorphism.

Sources
LeanTauCeti.zigzagBraidTensorLocalizerMorphism

TheoremTauCeti.zigzagAlgebraGradedProjectiveHomTracePairing_isPerfPair#

Complementary shifted Hom spaces of actual componentwise vertex projectives are in perfect trace pairing over every commutative coefficient ring.

TauCeti.zigzagAlgebraGradedProjectiveHomTracePairing_isPerfPair.{u, w} (k : Type w) [CommRing k]
  {V : Type u} [Finite V] (G : SimpleGraph V) (i j : V) (s : ℤ) :
  (TauCeti.zigzagAlgebraGradedProjectiveHomTracePairing k G i j s).IsPerfPair
Lean

Formalized in Tau Ceti as TauCeti.zigzagAlgebraGradedProjectiveHomTracePairing_isPerfPair.

Sources
LeanTauCeti.zigzagAlgebraGradedProjectiveHomTracePairing_isPerfPair

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.