The componentwise zigzag algebra

The uniform path-algebra quotient TauCeti.nonisolatedZigzagQuotient gives the intended zigzag algebra on a connected graph with an edge, but gives only the coefficient ring on an isolated vertex. The Huerfano--Khovanov convention instead assigns the dual numbers to a one-vertex component. This file makes that distinction in the public definition: TauCeti.zigzagAlgebra is the product of the appropriate algebra over the connected components of the graph.

The component algebra is packaged in AlgCat because its carrier changes between the singleton and non-singleton cases. The public algebra is the product of those carriers, exposed through component projections and extensionality. For a connected nontrivial graph, the product has one factor and is canonically isomorphic to the landed relation quotient. For the one-vertex graph it is canonically the dual numbers from Mathlib. The relabelling isomorphism TauCeti.zigzagAlgebraEquiv is coherent: it takes identity relabellings to identities, composites to composites and inverses to inverses.

Main definitions

• TauCeti.zigzagComponentAlgebra: the algebra assigned to one connected component.
• TauCeti.zigzagAlgebra: the public zigzag algebra of an arbitrary finite simple graph.
• TauCeti.zigzagAlgebraEquivNonisolated: comparison with the relation quotient for a connected graph with at least two vertices.
• TauCeti.zigzagAlgebraEquivA1: the one-vertex zigzag algebra is the dual numbers.

References

The low-rank convention follows Huerfano--Khovanov, A category for the adjoint representation, Section 3. The dual-number implementation is Mathlib's DualNumber, rather than a duplicate polynomial-quotient model.

noncomputable def TauCeti.zigzagComponentAlgebra (k : Type w) [CommRing k] {V : Type u} [Finite V] (G : SimpleGraph V) (C : G.ConnectedComponent) : AlgCat k

The zigzag algebra assigned to one connected component. A singleton component carries the dual numbers; a component with more than one vertex carries the uniform zigzag relation quotient of its induced graph.

@[simp]

theorem TauCeti.zigzagComponentAlgebra_eq_nonisolated (k : Type w) [CommRing k] {V : Type u} [Finite V] (G : SimpleGraph V) (C : G.ConnectedComponent) [Nontrivial ↥C] : zigzagComponentAlgebra k G C = ↧(nonisolatedZigzagQuotient k C.toSimpleGraph)

On a nontrivial connected component, the component algebra is the uniform relation quotient.

@[simp]

theorem TauCeti.zigzagComponentAlgebra_eq_uliftDualNumber (k : Type w) [CommRing k] {V : Type u} [Finite V] (G : SimpleGraph V) (C : G.ConnectedComponent) [Subsingleton ↥C] : zigzagComponentAlgebra k G C = ↧(ULift.{u, w} (DualNumber k))

On a singleton connected component, the component algebra is a universe lift of the dual numbers.

noncomputable def TauCeti.zigzagComponentAlgebraEquivNonisolated (k : Type w) [CommRing k] {V : Type u} [Finite V] (G : SimpleGraph V) (C : G.ConnectedComponent) [Nontrivial ↥C] : ↑(zigzagComponentAlgebra k G C) ≃ₐ[k] nonisolatedZigzagQuotient k C.toSimpleGraph

The component algebra of a nontrivial component, as an algebra equivalence rather than an equality of bundled objects.

noncomputable def TauCeti.zigzagComponentAlgebraEquivULiftDualNumber (k : Type w) [CommRing k] {V : Type u} [Finite V] (G : SimpleGraph V) (C : G.ConnectedComponent) [Subsingleton ↥C] : ↑(zigzagComponentAlgebra k G C) ≃ₐ[k] ULift.{u, w} (DualNumber k)

The component algebra of a singleton component is a universe lift of the dual numbers.

noncomputable def TauCeti.zigzagAlgebra (k : Type w) [CommRing k] {V : Type u} [Finite V] (G : SimpleGraph V) : AlgCat k

The public zigzag algebra of a finite simple graph: the product of its component algebras, using dual numbers precisely on singleton components.

noncomputable def TauCeti.zigzagAlgebraMk (k : Type w) [CommRing k] {V : Type u} [Finite V] (G : SimpleGraph V) (x : (C : G.ConnectedComponent) → ↑(zigzagComponentAlgebra k G C)) : ↑(zigzagAlgebra k G)

Construct an element of the public zigzag algebra from one element in each connected-component factor.

noncomputable def TauCeti.zigzagComponentProjection (k : Type w) [CommRing k] {V : Type u} [Finite V] (G : SimpleGraph V) (C : G.ConnectedComponent) : ↑(zigzagAlgebra k G) →ₐ[k] ↑(zigzagComponentAlgebra k G C)

Projection from the public zigzag algebra to the factor indexed by a connected component.

@[simp]

theorem TauCeti.zigzagComponentProjection_zigzagAlgebraMk (k : Type w) [CommRing k] {V : Type u} [Finite V] (G : SimpleGraph V) (x : (C : G.ConnectedComponent) → ↑(zigzagComponentAlgebra k G C)) (C : G.ConnectedComponent) : (zigzagComponentProjection k G C) (zigzagAlgebraMk k G x) = x C

Projecting a componentwise-constructed element recovers the specified component.

theorem TauCeti.zigzagAlgebra.ext (k : Type w) [CommRing k] {V : Type u} [Finite V] (G : SimpleGraph V) {x y : ↑(zigzagAlgebra k G)} (h : ∀ (C : G.ConnectedComponent), (zigzagComponentProjection k G C) x = (zigzagComponentProjection k G C) y) : x = y

Elements of the public zigzag algebra are equal when all their component projections agree.

theorem TauCeti.zigzagAlgebra.ext_iff {k : Type w} [CommRing k] {V : Type u} [Finite V] {G : SimpleGraph V} {x y : ↑(zigzagAlgebra k G)} : x = y ↔ ∀ (C : G.ConnectedComponent), (zigzagComponentProjection k G C) x = (zigzagComponentProjection k G C) y

@[simp]

theorem TauCeti.zigzagAlgebra.mk_projections (k : Type w) [CommRing k] {V : Type u} [Finite V] (G : SimpleGraph V) (x : ↑(zigzagAlgebra k G)) : (zigzagAlgebraMk k G fun (C : G.ConnectedComponent) => (zigzagComponentProjection k G C) x) = x

Reconstructing a public zigzag-algebra element from its component projections returns the original element.

noncomputable def TauCeti.zigzagAlgebraPiAlgEquiv (k : Type w) [CommRing k] {V : Type u} [Finite V] (G : SimpleGraph V) : ↑(zigzagAlgebra k G) ≃ₐ[k] (C : G.ConnectedComponent) → ↑(zigzagComponentAlgebra k G C)

The public zigzag algebra as the product of its connected-component factors.

@[simp]

theorem TauCeti.zigzagAlgebraPiAlgEquiv_apply (k : Type w) [CommRing k] {V : Type u} [Finite V] (G : SimpleGraph V) (x : ↑(zigzagAlgebra k G)) (C : G.ConnectedComponent) : (zigzagAlgebraPiAlgEquiv k G) x C = (zigzagComponentProjection k G C) x

@[simp]

theorem TauCeti.zigzagAlgebraPiAlgEquiv_symm_apply (k : Type w) [CommRing k] {V : Type u} [Finite V] (G : SimpleGraph V) (x : (C : G.ConnectedComponent) → ↑(zigzagComponentAlgebra k G C)) : (zigzagAlgebraPiAlgEquiv k G).symm x = zigzagAlgebraMk k G x

noncomputable def TauCeti.connectedComponentGraphIso {V : Type u} (G : SimpleGraph V) (hconn : G.Connected) (C : G.ConnectedComponent) : C.toSimpleGraph ≃g G

For a connected graph, the induced graph on any one of its connected components is canonically isomorphic to the original graph by forgetting the membership proof.

theorem TauCeti.nontrivial_connectedComponent {V : Type u} (G : SimpleGraph V) (hconn : G.Connected) [Nontrivial V] (C : G.ConnectedComponent) : Nontrivial ↥C

Every connected component of a connected graph on a nontrivial vertex type is nontrivial.

Invariance under graph isomorphism

noncomputable def TauCeti.zigzagComponentAlgebraEquiv (k : Type w) [CommRing k] {V : Type u} [Finite V] (G : SimpleGraph V) {W : Type v} [Finite W] {H : SimpleGraph W} (e : G ≃g H) (C : G.ConnectedComponent) : ↑(zigzagComponentAlgebra k G C) ≃ₐ[k] ↑(zigzagComponentAlgebra k H (e.connectedComponentEquiv C))

The algebras attached to corresponding connected components are invariant under graph isomorphism. In the nontrivial case this is the landed invariance of the relation quotient; in the singleton case both sides are universe lifts of Mathlib's dual numbers.

noncomputable def TauCeti.zigzagAlgebraEquiv (k : Type w) [CommRing k] {V : Type u} [Finite V] (G : SimpleGraph V) {W : Type v} [Finite W] {H : SimpleGraph W} (e : G ≃g H) : ↑(zigzagAlgebra k G) ≃ₐ[k] ↑(zigzagAlgebra k H)

The public zigzag algebra is invariant under graph isomorphism. The isomorphism relabels the connected-component factors and applies the corresponding component-algebra isomorphism in each factor.

@[simp]

theorem TauCeti.zigzagAlgebraEquiv_apply_component (k : Type w) [CommRing k] {V : Type u} [Finite V] (G : SimpleGraph V) {W : Type v} [Finite W] {H : SimpleGraph W} (e : G ≃g H) (x : ↑(zigzagAlgebra k G)) (C : G.ConnectedComponent) : (zigzagComponentProjection k H (e.connectedComponentEquiv C)) ((zigzagAlgebraEquiv k G e) x) = (zigzagComponentAlgebraEquiv k G e C) ((zigzagComponentProjection k G C) x)

The graph-isomorphism comparison acts on a corresponding component through the component algebra isomorphism.

@[simp]

theorem TauCeti.zigzagAlgebraEquiv_refl (k : Type w) [CommRing k] {V : Type u} [Finite V] (G : SimpleGraph V) : zigzagAlgebraEquiv k G SimpleGraph.Iso.refl = AlgEquiv.refl

The identity relabelling induces the identity of the public zigzag algebra.

theorem TauCeti.zigzagAlgebraEquiv_trans (k : Type w) [CommRing k] {V : Type u} [Finite V] (G : SimpleGraph V) {W : Type v} [Finite W] {H : SimpleGraph W} {X : Type u_1} [Finite X] {K : SimpleGraph X} (e : G ≃g H) (f : H ≃g K) : zigzagAlgebraEquiv k G (RelIso.trans e f) = (zigzagAlgebraEquiv k G e).trans (zigzagAlgebraEquiv k H f)

The public zigzag algebra is functorial in the graph: composing two relabellings composes the induced isomorphisms of public zigzag algebras.

@[simp]

theorem TauCeti.zigzagAlgebraEquiv_symm (k : Type w) [CommRing k] {V : Type u} [Finite V] (G : SimpleGraph V) {W : Type v} [Finite W] {H : SimpleGraph W} (e : G ≃g H) : (zigzagAlgebraEquiv k G e).symm = zigzagAlgebraEquiv k H e.symm

The inverse relabelling induces the inverse isomorphism of public zigzag algebras.

noncomputable def TauCeti.zigzagAlgebraEquivNonisolated (k : Type w) [CommRing k] {V : Type u} [Finite V] (G : SimpleGraph V) (hconn : G.Connected) [Nontrivial V] : ↑(zigzagAlgebra k G) ≃ₐ[k] nonisolatedZigzagQuotient k G

On a connected graph with at least two vertices, the public componentwise zigzag algebra is canonically isomorphic to the uniform relation quotient.

theorem TauCeti.zigzagAlgebraEquivNonisolated_apply (k : Type w) [CommRing k] {V : Type u} [Finite V] (G : SimpleGraph V) (hconn : G.Connected) [Nontrivial V] (x : ↑(zigzagAlgebra k G)) (C : G.ConnectedComponent) : (zigzagAlgebraEquivNonisolated k G hconn) x = have x_1 := ⋯; (nonisolatedZigzagQuotientEquiv k (connectedComponentGraphIso G hconn C)) ((zigzagComponentAlgebraEquivNonisolated k G C) ((zigzagComponentProjection k G C) x))

The connected nonisolated comparison evaluates through any connected-component factor and the canonical graph isomorphism from that factor to the original graph.

@[simp]

theorem TauCeti.zigzagAlgebraEquivNonisolated_symm_apply_component (k : Type w) [CommRing k] {V : Type u} [Finite V] (G : SimpleGraph V) (hconn : G.Connected) [Nontrivial V] (x : nonisolatedZigzagQuotient k G) (C : G.ConnectedComponent) : (zigzagComponentProjection k G C) ((zigzagAlgebraEquivNonisolated k G hconn).symm x) = have x_1 := ⋯; (zigzagComponentAlgebraEquivNonisolated k G C).symm ((nonisolatedZigzagQuotientEquiv k (connectedComponentGraphIso G hconn C)).symm x)

The inverse connected nonisolated comparison is computed componentwise by the inverse graph and component equivalences.

noncomputable def TauCeti.zigzagAlgebraEquivA1 (k : Type w) [CommRing k] : ↑(zigzagAlgebra k ⊥) ≃ₐ[k] DualNumber k

The public zigzag algebra of the one-vertex graph is the algebra of dual numbers.

@[simp]

theorem TauCeti.zigzagAlgebraEquivA1_apply (k : Type w) [CommRing k] (x : ↑(zigzagAlgebra k ⊥)) : (zigzagAlgebraEquivA1 k) x = ((zigzagComponentAlgebraEquivULiftDualNumber k ⊥ default) ((zigzagComponentProjection k ⊥ default) x)).down

The rank-one comparison evaluates the unique component and then lowers the universe lift.

@[simp]

theorem TauCeti.zigzagAlgebraEquivA1_symm_apply_component (k : Type w) [CommRing k] (x : DualNumber k) (C : ⊥.ConnectedComponent) : (zigzagComponentProjection k ⊥ C) ((zigzagAlgebraEquivA1 k).symm x) = (zigzagComponentAlgebraEquivULiftDualNumber k ⊥ C).symm { down := x }

The inverse rank-one comparison inserts a dual number into the unique lifted component.