Relabelling skew-zigzag algebras

An isomorphism of simple graphs transports a skew-zigzag parameter by relabelling its incident edges. The induced isomorphism of doubled path algebras then carries each skew relation to the corresponding transported relation, and hence descends to an algebra isomorphism of the relation quotients.

Identity relabellings act as identities, composites act by composites, and reversing a graph isomorphism undoes parameter relabelling. This makes graph automorphisms available for comparing arbitrary, rather than vertex-fixing, isomorphism classes of skew-zigzag algebras.

Main definitions

• TauCeti.SkewZigzagParameter.relabel: transport a parameter along a graph isomorphism.
• TauCeti.SkewZigzagParameter.relabelEquiv: relabelling is an equivalence on parameters.
• TauCeti.skewZigzagQuotientEquiv: the induced isomorphism of skew-zigzag relation quotients.

Main results

• TauCeti.SkewZigzagParameter.relabel_ratio_map: relabelling preserves the ratio attached to a pair of incident edges.
• TauCeti.isSkewZigzagRelator_pathAlgebraEquiv: graph relabelling carries skew relators to skew relators for the transported parameter.
• TauCeti.skewZigzagQuotientEquiv_skewZigzagMk: the quotient isomorphism sends a class to the class of its relabelled path-algebra representative.
• TauCeti.skewZigzagQuotientEquiv_refl, TauCeti.skewZigzagQuotientEquiv_trans, and TauCeti.skewZigzagQuotientEquiv_symm: quotient relabelling is coherent with graph-isomorphism identities, composition, and inverses.

References

C. Couture, Skew-Zigzag Algebras, Section 4, https://arxiv.org/abs/1509.08405.

def TauCeti.SkewZigzagParameter.relabel {k : Type w} [Monoid k] {V : Type u} {W : Type v} {G : SimpleGraph V} {H : SimpleGraph W} (e : G ≃g H) (c : SkewZigzagParameter k G) : SkewZigzagParameter k H

Transport a skew-zigzag parameter along an isomorphism of simple graphs. The ratio at two incident edges of the target is the ratio at their inverse images.

@[simp]

theorem TauCeti.SkewZigzagParameter.relabel_ratio {k : Type w} [Monoid k] {V : Type u} {W : Type v} {G : SimpleGraph V} {H : SimpleGraph W} (e : G ≃g H) (c : SkewZigzagParameter k G) {i j j' : W} (h : H.Adj i j) (h' : H.Adj i j') : (relabel e c).ratio h h' = c.ratio ⋯ ⋯

The ratio of a relabelled parameter is the ratio at the inverse-image edges.

theorem TauCeti.SkewZigzagParameter.relabel_ratio_map {k : Type w} [Monoid k] {V : Type u} {W : Type v} {G : SimpleGraph V} {H : SimpleGraph W} (e : G ≃g H) (c : SkewZigzagParameter k G) {i j j' : V} (h : G.Adj i j) (h' : G.Adj i j') : (relabel e c).ratio ⋯ ⋯ = c.ratio h h'

Relabelling preserves the ratio attached to two incident edges.

@[simp]

theorem TauCeti.SkewZigzagParameter.relabel_refl {k : Type w} [Monoid k] {V : Type u} {G : SimpleGraph V} (c : SkewZigzagParameter k G) : relabel SimpleGraph.Iso.refl c = c

Relabelling by the identity graph isomorphism changes no parameter.

@[simp]

theorem TauCeti.SkewZigzagParameter.relabel_trans {k : Type w} [Monoid k] {V : Type u} {W : Type v} {G : SimpleGraph V} {H : SimpleGraph W} {X : Type x} {K : SimpleGraph X} (e : G ≃g H) (f : H ≃g K) (c : SkewZigzagParameter k G) : relabel (RelIso.trans e f) c = relabel f (relabel e c)

Relabelling along a composite graph isomorphism is successive relabelling.

@[simp]

theorem TauCeti.SkewZigzagParameter.relabel_symm_relabel {k : Type w} [Monoid k] {V : Type u} {W : Type v} {G : SimpleGraph V} {H : SimpleGraph W} (e : G ≃g H) (c : SkewZigzagParameter k G) : relabel e.symm (relabel e c) = c

Relabelling by an isomorphism and then its inverse changes no parameter.

@[simp]

theorem TauCeti.SkewZigzagParameter.relabel_relabel_symm {k : Type w} [Monoid k] {V : Type u} {W : Type v} {G : SimpleGraph V} {H : SimpleGraph W} (e : G ≃g H) (c : SkewZigzagParameter k H) : relabel e (relabel e.symm c) = c

Relabelling by an inverse isomorphism and then by the original isomorphism changes no parameter.

def TauCeti.SkewZigzagParameter.relabelEquiv (k : Type w) [Monoid k] {V : Type u} {W : Type v} {G : SimpleGraph V} {H : SimpleGraph W} (e : G ≃g H) : SkewZigzagParameter k G ≃ SkewZigzagParameter k H

A graph isomorphism induces an equivalence between the skew-zigzag parameters on the two graphs, by relabelling incident edges.

@[simp]

theorem TauCeti.SkewZigzagParameter.relabelEquiv_apply {k : Type w} [Monoid k] {V : Type u} {W : Type v} {G : SimpleGraph V} {H : SimpleGraph W} (e : G ≃g H) (c : SkewZigzagParameter k G) : (relabelEquiv k e) c = relabel e c

The parameter equivalence induced by a graph isomorphism acts by relabelling.

@[simp]

theorem TauCeti.SkewZigzagParameter.relabelEquiv_symm_apply {k : Type w} [Monoid k] {V : Type u} {W : Type v} {G : SimpleGraph V} {H : SimpleGraph W} (e : G ≃g H) (c : SkewZigzagParameter k H) : (relabelEquiv k e).symm c = relabel e.symm c

The inverse parameter equivalence acts by relabelling along the inverse graph isomorphism.

The relators are matched

theorem TauCeti.isSkewZigzagRelator_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) (c : SkewZigzagParameter k G) {z : pathAlgebra k (DoubledQuiver G)} (hz : IsSkewZigzagRelator k G c z) : IsSkewZigzagRelator k H (SkewZigzagParameter.relabel e c) ((DoubledQuiver.pathAlgebraEquiv k e) z)

An isomorphism of graphs carries each skew-zigzag relator to the corresponding relator for the transported parameter.

The quotient isomorphism

noncomputable def TauCeti.skewZigzagQuotientEquiv (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) (c : SkewZigzagParameter k G) : skewZigzagQuotient k G c ≃ₐ[k] skewZigzagQuotient k H (SkewZigzagParameter.relabel e c)

A graph isomorphism induces an algebra isomorphism from a skew-zigzag quotient to the quotient for the relabelled parameter.

@[simp]

theorem TauCeti.skewZigzagQuotientEquiv_skewZigzagMk (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) (c : SkewZigzagParameter k G) (z : pathAlgebra k (DoubledQuiver G)) : (skewZigzagQuotientEquiv k e c) ((skewZigzagMk k G c) z) = (skewZigzagMk k H (SkewZigzagParameter.relabel e c)) ((DoubledQuiver.pathAlgebraEquiv k e) z)

The induced quotient isomorphism sends a class to the class of its relabelled representative.

@[simp]

theorem TauCeti.skewZigzagQuotientEquiv_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) (c : SkewZigzagParameter k G) : (skewZigzagQuotientEquiv k e c).symm = (skewZigzagQuotientEquiv k e.symm (SkewZigzagParameter.relabel e c)).trans (AlgEquiv.cast ⋯)

The inverse quotient isomorphism is induced by inverse graph relabelling, after identifying the twice-relabelled parameter with the original parameter.

@[simp]

theorem TauCeti.skewZigzagQuotientEquiv_refl (k : Type w) [CommRing k] {V : Type u} [Finite V] {G : SimpleGraph V} (c : SkewZigzagParameter k G) : (skewZigzagQuotientEquiv k SimpleGraph.Iso.refl c).trans (AlgEquiv.cast ⋯) = AlgEquiv.refl

Relabelling by the identity graph isomorphism induces the identity quotient isomorphism, after identifying the relabelled parameter with the original parameter.

theorem TauCeti.skewZigzagQuotientEquiv_trans (k : Type w) [CommRing k] {V : Type u} {W : Type v} [Finite V] [Finite W] {G : SimpleGraph V} {H : SimpleGraph W} {X : Type x} [Finite X] {K : SimpleGraph X} (e : G ≃g H) (f : H ≃g K) (c : SkewZigzagParameter k G) : (skewZigzagQuotientEquiv k (RelIso.trans e f) c).trans (AlgEquiv.cast ⋯) = (skewZigzagQuotientEquiv k e c).trans (skewZigzagQuotientEquiv k f (SkewZigzagParameter.relabel e c))

Relabelling along a composite graph isomorphism agrees with successive quotient relabellings, after identifying the two relabelled parameters.