Transition factors of a skew-zigzag parameter and their integration

A skew-zigzag parameter records ratios between backtracks along edges incident to the same vertex. Choosing a reference edge at every vertex turns these ratios into local edge coordinates, and comparing the two ends of an edge gives a transition factor across it. Multiplying transition factors along the darts of a walk gives the transition factor of the walk.

When the transition factor of a path depends only on its endpoints, multiplying transition factors along paths from a chosen root in every connected component gives a vertex potential, a unit at every vertex changing by the transition factor across every edge. The local ratios then integrate to a global scale on the unoriented edges, and rescaling one orientation of every edge by it trivializes the parameter.

Main definitions

• TauCeti.SkewZigzagParameter.localCoordinate: the ratio from an incident edge to a chosen reference edge at its source.
• TauCeti.SkewZigzagParameter.transition: the change of local edge coordinates across an oriented edge.
• TauCeti.SkewZigzagParameter.walkTransition: the product of the transition factors along a walk.

Main results

• TauCeti.SkewZigzagParameter.ratio_eq_localCoordinate_div: every ratio is a quotient of local edge coordinates.
• TauCeti.SkewZigzagParameter.localCoordinate_map: local coordinates are carried by the monoid homomorphism mapping a parameter.
• TauCeti.SkewZigzagParameter.transition_map: transition factors are carried by the monoid homomorphism mapping a parameter.
• TauCeti.SkewZigzagParameter.walkTransition_map: transition factors along a walk are carried by the monoid homomorphism mapping a parameter.
• TauCeti.SkewZigzagParameter.transition_mul: transition factors are multiplicative in the parameter.
• TauCeti.SkewZigzagParameter.isGaugeEquivalent_one_of_potential: a vertex potential for the transition factors trivializes the parameter.
• TauCeti.SkewZigzagParameter.isGaugeEquivalent_one_of_walkTransition_eq: a parameter whose transition factor along a path depends only on its endpoints is gauge trivial.

References

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

Local edge coordinates

noncomputable def TauCeti.SkewZigzagParameter.localCoordinate {k : Type w} {V : Type u} {G : SimpleGraph V} [Monoid k] (c : SkewZigzagParameter k G) {v w : V} (h : G.Adj v w) : kˣ

The local coordinate of an incident edge: its ratio to a chosen reference edge at its source.

noncomputable def TauCeti.SkewZigzagParameter.transition {k : Type w} {V : Type u} {G : SimpleGraph V} [Monoid k] (c : SkewZigzagParameter k G) {v w : V} (h : G.Adj v w) : kˣ

The transition factor across an oriented edge: the change of local edge coordinates from its source to its target.

theorem TauCeti.SkewZigzagParameter.transition_def {k : Type w} {V : Type u} {G : SimpleGraph V} [Monoid k] (c : SkewZigzagParameter k G) {v w : V} (h : G.Adj v w) : c.transition h = c.localCoordinate h / c.localCoordinate ⋯

The transition factor is the quotient of the local coordinates at the two ends of an edge.

theorem TauCeti.SkewZigzagParameter.ratio_eq_localCoordinate_div {k : Type w} {V : Type u} {G : SimpleGraph V} [Monoid k] (c : SkewZigzagParameter k G) {i j j' : V} (h : G.Adj i j) (h' : G.Adj i j') : c.ratio h h' = c.localCoordinate h / c.localCoordinate h'

Every ratio is a quotient of local edge coordinates.

@[simp]

theorem TauCeti.SkewZigzagParameter.transition_symm {k : Type w} {V : Type u} {G : SimpleGraph V} [Monoid k] (c : SkewZigzagParameter k G) {v w : V} (h : G.Adj v w) : c.transition ⋯ = (c.transition h)⁻¹

Reversing an edge inverts its transition factor.

Transition factors under a coefficient homomorphism

@[simp]

theorem TauCeti.SkewZigzagParameter.localCoordinate_map {k : Type w} {V : Type u} {G : SimpleGraph V} [Monoid k] {l : Type z} [Monoid l] (f : k →* l) (c : SkewZigzagParameter k G) {v w : V} (h : G.Adj v w) : (map f c).localCoordinate h = (Units.map f) (c.localCoordinate h)

The local coordinates of a mapped parameter are the images of the local coordinates.

@[simp]

theorem TauCeti.SkewZigzagParameter.transition_map {k : Type w} {V : Type u} {G : SimpleGraph V} [Monoid k] {l : Type z} [Monoid l] (f : k →* l) (c : SkewZigzagParameter k G) {v w : V} (h : G.Adj v w) : (map f c).transition h = (Units.map f) (c.transition h)

The transition factors of a mapped parameter are the images of the transition factors.

Products of parameters

@[simp]

theorem TauCeti.SkewZigzagParameter.localCoordinate_mul {k : Type w} {V : Type u} {G : SimpleGraph V} [CommMonoid k] (c c' : SkewZigzagParameter k G) {v w : V} (h : G.Adj v w) : (c * c').localCoordinate h = c.localCoordinate h * c'.localCoordinate h

The local coordinates of a product of parameters are the products of their local coordinates.

@[simp]

theorem TauCeti.SkewZigzagParameter.transition_mul {k : Type w} {V : Type u} {G : SimpleGraph V} [CommMonoid k] (c c' : SkewZigzagParameter k G) {v w : V} (h : G.Adj v w) : (c * c').transition h = c.transition h * c'.transition h

The transition factors of a product of parameters are the products of their transition factors.

Transition factors along walks

noncomputable def TauCeti.SkewZigzagParameter.walkTransition {k : Type w} {V : Type u} {G : SimpleGraph V} [Monoid k] (c : SkewZigzagParameter k G) {v w : V} (q : G.Walk v w) : kˣ

The transition factor of a walk: the product of the transition factors along its darts.

theorem TauCeti.SkewZigzagParameter.walkTransition_def {k : Type w} {V : Type u} {G : SimpleGraph V} [Monoid k] (c : SkewZigzagParameter k G) {v w : V} (q : G.Walk v w) : c.walkTransition q = (List.map (fun (d : G.Dart) => c.transition ⋯) q.darts).prod

The transition factor of a walk is the product of the transition factors along its darts.

@[simp]

theorem TauCeti.SkewZigzagParameter.walkTransition_nil {k : Type w} {V : Type u} {G : SimpleGraph V} [Monoid k] (c : SkewZigzagParameter k G) (v : V) : c.walkTransition SimpleGraph.Walk.nil = 1

The transition factor of the empty walk is one.

@[simp]

theorem TauCeti.SkewZigzagParameter.walkTransition_toWalk {k : Type w} {V : Type u} {G : SimpleGraph V} [Monoid k] (c : SkewZigzagParameter k G) {v w : V} (h : G.Adj v w) : c.walkTransition h.toWalk = c.transition h

The transition factor of a one-edge walk is the transition factor of that edge.

@[simp]

theorem TauCeti.SkewZigzagParameter.walkTransition_concat {k : Type w} {V : Type u} {G : SimpleGraph V} [Monoid k] (c : SkewZigzagParameter k G) {r v w : V} (q : G.Walk r v) (h : G.Adj v w) : c.walkTransition (q.concat h) = c.walkTransition q * c.transition h

Extending a walk by an edge multiplies its transition factor by that of the edge.

@[simp]

theorem TauCeti.SkewZigzagParameter.walkTransition_append {k : Type w} {V : Type u} {G : SimpleGraph V} [Monoid k] (c : SkewZigzagParameter k G) {u v w : V} (p : G.Walk u v) (q : G.Walk v w) : c.walkTransition (p.append q) = c.walkTransition p * c.walkTransition q

The transition factor of a concatenation of walks is the product of theirs.

@[simp]

theorem TauCeti.SkewZigzagParameter.walkTransition_map {k : Type w} {V : Type u} {G : SimpleGraph V} [Monoid k] {l : Type z} [Monoid l] (f : k →* l) (c : SkewZigzagParameter k G) {v w : V} (q : G.Walk v w) : (map f c).walkTransition q = (Units.map f) (c.walkTransition q)

The transition factor of a walk is carried by the monoid homomorphism mapping a parameter.

@[simp]

theorem TauCeti.SkewZigzagParameter.walkTransition_reverse {k : Type w} {V : Type u} {G : SimpleGraph V} [Monoid k] (c : SkewZigzagParameter k G) {u v : V} (p : G.Walk u v) : c.walkTransition p.reverse = (c.walkTransition p)⁻¹

Reversing a walk inverts its transition factor. Reversing a walk reverses its darts and replaces each of them by the reverse dart, whose transition factor is the inverse. Its transition factor is therefore the reverse of the list of inverses of the original factors, which is the inverse of the original product in any monoid.

Trivializing a parameter from a vertex potential

theorem TauCeti.SkewZigzagParameter.isGaugeEquivalent_one_of_potential {k : Type w} {V : Type u} {G : SimpleGraph V} [CommMonoid k] (c : SkewZigzagParameter k G) (a : V → kˣ) (ha : ∀ ⦃v w : V⦄ (h : G.Adj v w), a w = a v * c.transition h) : IsGaugeEquivalent 1 c

A vertex potential for the transition factors, a unit at every vertex changing by the transition factor across every edge, trivializes the parameter: the resulting edge scales are symmetric and the ratios are their quotients.

The potential along paths from a root

theorem TauCeti.SkewZigzagParameter.isGaugeEquivalent_one_of_walkTransition_eq {k : Type w} {V : Type u} {G : SimpleGraph V} [CommMonoid k] (c : SkewZigzagParameter k G) (hc : ∀ ⦃u v : V⦄ (p q : G.Walk u v), p.IsPath → q.IsPath → c.walkTransition p = c.walkTransition q) : IsGaugeEquivalent 1 c

A parameter whose transition factor along a path depends only on its endpoints is gauge equivalent to the constant parameter. The transition factors along paths from a root in every connected component form a vertex potential, which trivializes the parameter.