The nonisolated zigzag quotient is an invariant of the graph

An isomorphism e : G ≃g H of simple graphs relabels the doubled quiver of G as the doubled quiver of H, hence relabels the path basis of k(DoubledQuiver G) as the path basis of k(DoubledQuiver H). This file carries that relabelling through the zigzag relations: it is an isomorphism of path algebras, it matches the two relation families, and it therefore descends to an isomorphism of the two TauCeti.nonisolatedZigzagQuotients.

That quotient is, as its own docstring records, the intended zigzag algebra only for a graph without an isolated vertex; the componentwise public algebra remains to be built, and its invariance is not established here.

Nothing here is specific to the uniform relation family beyond the fact that it is described by path lengths and by the endpoints of paths, both of which a relabelling preserves. That is exactly what the transport lemmas below say, one constructor at a time.

Main definitions

• TauCeti.DoubledQuiver.pathAlgebraEquiv: the isomorphism of doubled path algebras induced by a graph isomorphism.
• TauCeti.nonisolatedZigzagQuotientEquiv: the induced isomorphism of nonisolated zigzag quotients.

Main results

• TauCeti.DoubledQuiver.pathAlgebraEquiv_vertexIdempotent, TauCeti.DoubledQuiver.pathAlgebraEquiv_ofArrow and TauCeti.DoubledQuiver.pathAlgebraEquiv_backtrackElem: the relabelling on the three families of elements the zigzag relations are written in.
• TauCeti.isQuadraticZigzagRelator_pathAlgebraEquiv and TauCeti.isZigzagRelator_pathAlgebraEquiv: the relators are matched.
• TauCeti.nonisolatedZigzagQuotientEquiv_zigzagMk: the induced isomorphism of quotients sends the class of an element to the class of its relabelling.
• TauCeti.nonisolatedZigzagQuotientEquiv_refl and TauCeti.nonisolatedZigzagQuotientEquiv_trans: functoriality, the identity relabelling and a composite of relabellings behaving as they should.

References

This discharges the "functoriality under graph/quiver isomorphism" clause of Layer 0 of TauCetiRoadmap/ZigzagPreprojective/README.md. It covers the "invariance under graph isomorphism" clause of Layer 1 only in part: the uniform relation quotient is transported, while the skew-parameter statements of that clause — extension along a field homomorphism, the resulting scalar-extension comparison, and injectivity on units — are untouched. See Huerfano--Khovanov, A category for the adjoint representation, Section 3.

noncomputable def TauCeti.DoubledQuiver.pathAlgebraEquiv {V : Type u} {W : Type v} {G : SimpleGraph V} {H : SimpleGraph W} (k : Type w) [CommSemiring k] [Finite V] [Finite W] (e : G ≃g H) : pathAlgebra k (DoubledQuiver G) ≃ₐ[k] pathAlgebra k (DoubledQuiver H)

The isomorphism of doubled path algebras induced by a graph isomorphism: it relabels the basis path by path of the doubled quiver.

Equations

• TauCeti.DoubledQuiver.pathAlgebraEquiv k e = TauCeti.PathAlgebra.mapAlgEquiv k (TauCeti.DoubledQuiver.map e.toHom) (TauCeti.DoubledQuiver.map e.symm.toHom) ⋯ ⋯

@[simp]

theorem TauCeti.DoubledQuiver.pathAlgebraEquiv_ofPath {V : Type u} {W : Type v} {G : SimpleGraph V} {H : SimpleGraph W} (k : Type w) [CommSemiring k] [Finite V] [Finite W] (e : G ≃g H) (x : Quiver.TotalPath (DoubledQuiver G)) : (pathAlgebraEquiv k e) (PathAlgebra.ofPath x) = PathAlgebra.ofPath ((map e.toHom).mapTotalPath x)

The relabelling sends the basis element of a path of the doubled quiver of G to the basis element of the relabelled path of the doubled quiver of H.

@[simp]

theorem TauCeti.DoubledQuiver.pathAlgebraEquiv_vertexIdempotent {V : Type u} {W : Type v} {G : SimpleGraph V} {H : SimpleGraph W} (k : Type w) [CommSemiring k] [Finite V] [Finite W] (e : G ≃g H) (i : V) : (pathAlgebraEquiv k e) (PathAlgebra.vertexIdempotent k (vertex G i)) = PathAlgebra.vertexIdempotent k (vertex H (e i))

The relabelling carries the idempotent of a vertex of G to the idempotent of the image vertex of H.

theorem TauCeti.DoubledQuiver.pathAlgebraEquiv_ofArrow {V : Type u} {W : Type v} {G : SimpleGraph V} {H : SimpleGraph W} (k : Type w) [CommSemiring k] [Finite V] [Finite W] (e : G ≃g H) {i j : V} (h : G.Adj i j) : (pathAlgebraEquiv k e) (PathAlgebra.ofArrow (arrow G h)) = PathAlgebra.ofArrow (arrow H ⋯)

The relabelling carries an arrow along an edge of G to the arrow along the image edge of H. Deliberately not a simp lemma, TauCeti.PathAlgebra.ofArrow_eq_ofPath already rewriting its left-hand side.

@[simp]

theorem TauCeti.DoubledQuiver.pathAlgebraEquiv_backtrackElem {V : Type u} {W : Type v} {G : SimpleGraph V} {H : SimpleGraph W} (k : Type w) [CommSemiring k] [Finite V] [Finite W] (e : G ≃g H) {i j : V} (h : G.Adj i j) : (pathAlgebraEquiv k e) (backtrackElem G k h) = backtrackElem H k ⋯

The relabelling carries the backtrack element along an edge of G to the backtrack element along the image edge of H: it traverses the image edge and returns along it.

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

The relabelling is functorial: composing two graph isomorphisms composes the induced isomorphisms of path algebras.

@[simp]

theorem TauCeti.DoubledQuiver.pathAlgebraEquiv_refl {V : Type u} {G : SimpleGraph V} (k : Type w) [CommSemiring k] [Finite V] : pathAlgebraEquiv k SimpleGraph.Iso.refl = AlgEquiv.refl

The identity relabelling induces the identity.

@[simp]

theorem TauCeti.DoubledQuiver.pathAlgebraEquiv_symm {V : Type u} {W : Type v} {G : SimpleGraph V} {H : SimpleGraph W} (k : Type w) [CommSemiring k] [Finite V] [Finite W] (e : G ≃g H) : (pathAlgebraEquiv k e).symm = pathAlgebraEquiv k e.symm

The inverse of the induced isomorphism is the isomorphism induced by the inverse relabelling.

The relators are matched

theorem TauCeti.isQuadraticZigzagRelator_pathAlgebraEquiv (k : Type w) [CommRing k] {V : Type u} {W : Type v} [Finite V] [Finite W] {G : SimpleGraph V} {H : SimpleGraph W} (e : G ≃g H) {x : pathAlgebra k (DoubledQuiver G)} (hx : IsQuadraticZigzagRelator k G x) : IsQuadraticZigzagRelator k H ((DoubledQuiver.pathAlgebraEquiv k e) x)

A graph isomorphism carries the quadratic zigzag relators of G to those of H: it preserves the length of a path and, being injective on vertices, whether its endpoints agree.

theorem TauCeti.isZigzagRelator_pathAlgebraEquiv (k : Type w) [CommRing k] {V : Type u} {W : Type v} [Finite V] [Finite W] {G : SimpleGraph V} {H : SimpleGraph W} (e : G ≃g H) {x : pathAlgebra k (DoubledQuiver G)} (hx : IsZigzagRelator k G x) : IsZigzagRelator k H ((DoubledQuiver.pathAlgebraEquiv k e) x)

A graph isomorphism carries the uniform zigzag relators of G to those of H.

The quotients are isomorphic

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

The nonisolated zigzag quotient is an invariant of the graph: an isomorphism of simple graphs induces an isomorphism of the uniform relation quotients of their doubled path algebras. This is invariance of TauCeti.nonisolatedZigzagQuotient, which is the intended zigzag algebra only for a graph without an isolated vertex; the componentwise public algebra is not treated here.

Equations

• TauCeti.nonisolatedZigzagQuotientEquiv k e = AlgEquiv.ofAlgHom (TauCeti.nonisolatedZigzagQuotientHom✝ k e) (TauCeti.nonisolatedZigzagQuotientHom✝ k e.symm) ⋯ ⋯

@[simp]

theorem TauCeti.nonisolatedZigzagQuotientEquiv_zigzagMk (k : Type w) [CommRing k] {V : Type u} {W : Type v} [Finite V] [Finite W] {G : SimpleGraph V} {H : SimpleGraph W} (e : G ≃g H) (x : pathAlgebra k (DoubledQuiver G)) : (nonisolatedZigzagQuotientEquiv k e) ((zigzagMk k G) x) = (zigzagMk k H) ((DoubledQuiver.pathAlgebraEquiv k e) x)

The induced isomorphism of quotients sends the class of an element to the class of its relabelling.

@[simp]

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

The inverse quotient isomorphism is induced by the inverse graph relabelling.

@[simp]

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

The identity relabelling induces the identity of quotients.

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

The isomorphism of quotients is functorial: composing two graph isomorphisms composes the induced isomorphisms of nonisolated zigzag quotients.