Gauge equivalence of skew-zigzag parameters

A skew-zigzag parameter labels each ordered pair of incident edges of a simple graph G by the unit-valued ratio between the two backtracks they carry, and the associated relation quotient imposes backtrack(h) = ratio(h,h') • backtrack(h'). Rescaling every arrow of the doubled quiver by a unit is an automorphism of the doubled path algebra which fixes the vertex idempotents, so it carries one skew presentation to another. This file identifies the induced change of parameters and proves that it does not change the presented algebra.

Rescaling by a labelling u multiplies the backtrack along an edge by the backtrack scale u(h) * u(h*), the product of the labels of the two orientations of that edge; the scale is therefore a function of the underlying unoriented edge. The parameter is changed by

(c.gauge u).ratio h h' = c.ratio h h' * (backtrackScale u h' / backtrackScale u h),

which is again reflexive, inverse-symmetric, and a multiplicative cocycle. Two parameters related this way present isomorphic algebras, the isomorphism being the arrow rescaling itself, so gauge equivalence is a genuine equivalence relation on parameters through which the presented algebra factors. Specializing to the constant parameter 1, which presents the ordinary zigzag relation quotient, a gauge-trivial parameter presents the ordinary zigzag algebra.

Main definitions

• TauCeti.DoubledQuiver.backtrackScale: the factor by which an arrow rescaling multiplies the backtrack along an edge.
• TauCeti.SkewZigzagParameter.gauge: the gauge transform of a skew-zigzag parameter.
• the MulAction instance on TauCeti.SkewZigzagParameter: gauge transforms as an action of the pointwise group of unit-valued arrow labellings.
• TauCeti.SkewZigzagParameter.IsGaugeEquivalent: the gauge equivalence relation on parameters, the orbit relation of that action.

Main results

• TauCeti.DoubledQuiver.backtrackScale_symm: the backtrack scale depends only on the unoriented edge.
• TauCeti.SkewZigzagParameter.isGaugeEquivalent_iff: gauge equivalence in existential form.
• TauCeti.SkewZigzagParameter.IsGaugeEquivalent.equivalence: gauge equivalence is an equivalence relation.
• TauCeti.SkewZigzagParameter.gauge_eq_mul_gauge_one: a gauge transform multiplies a parameter by the gauge transform of the constant parameter.
• TauCeti.SkewZigzagParameter.isGaugeEquivalent_iff_isGaugeEquivalent_one_div: two parameters are gauge equivalent exactly when their quotient is gauge trivial.
• TauCeti.SkewZigzagParameter.isGaugeEquivalent_one_iff_exists_ratio_eq_div: a parameter is gauge trivial exactly when its ratios are quotients of a symmetric edge scale.
• TauCeti.skewZigzagQuotientGaugeEquiv: gauge independence, a gauge transform of a parameter presents an isomorphic algebra.
• TauCeti.nonempty_algEquiv_nonisolatedZigzagQuotient_of_isGaugeEquivalent_one: a gauge-trivial parameter presents the ordinary zigzag relation quotient.

References

C. Couture, Skew-Zigzag Algebras, Section 4, https://arxiv.org/abs/1509.08405, which sets up the gauge relation on skew parameters and its cohomological classification.

The gauge isomorphism of relation quotients follows TauCeti.RepresentationTheory.Quiver.Preprojective.Gauge.

The backtrack scale of an arrow labelling

def TauCeti.DoubledQuiver.backtrackScale {V : Type u} (G : SimpleGraph V) {M : Type u_1} [Mul M] (u : ⦃x y : DoubledQuiver G⦄ → (x ⟶ y) → M) {i j : V} (h : G.Adj i j) : M

The backtrack scale of a labelling u of the arrows of a doubled quiver along an edge: the product of the labels of the two orientations of that edge. Rescaling by u multiplies the backtrack along the edge by this factor.

@[simp]

theorem TauCeti.DoubledQuiver.backtrackScale_apply {V : Type u} (G : SimpleGraph V) {M : Type u_1} [Mul M] (u : ⦃x y : DoubledQuiver G⦄ → (x ⟶ y) → M) {i j : V} (h : G.Adj i j) : backtrackScale G u h = u (arrow G h) * u (arrow G ⋯)

The backtrack scale is the product of the labels on the two orientations of an edge.

theorem TauCeti.DoubledQuiver.val_backtrackScale {V : Type u} (G : SimpleGraph V) {k : Type w} [Monoid k] (u : ⦃x y : DoubledQuiver G⦄ → (x ⟶ y) → kˣ) {i j : V} (h : G.Adj i j) : ↑(backtrackScale G u h) = backtrackScale G (fun (x x_1 : DoubledQuiver G) (e : x ⟶ x_1) => ↑(u e)) h

The backtrack scale of a unit-valued labelling is the backtrack scale of its underlying scalar labelling.

theorem TauCeti.DoubledQuiver.backtrackScale_symm {V : Type u} (G : SimpleGraph V) {M : Type u_1} [CommMonoid M] (u : ⦃x y : DoubledQuiver G⦄ → (x ⟶ y) → M) {i j : V} (h : G.Adj i j) : backtrackScale G u ⋯ = backtrackScale G u h

The backtrack scale is a function of the unoriented edge: it is unchanged by reversing the adjacency indexing it.

Rescaling a backtrack element

theorem TauCeti.DoubledQuiver.rescale_backtrackElem {V : Type u} (G : SimpleGraph V) (k : Type w) [CommSemiring k] [Finite V] (u : ⦃x y : DoubledQuiver G⦄ → (x ⟶ y) → k) {i j : V} (h : G.Adj i j) : (PathAlgebra.rescale u) (backtrackElem G k h) = backtrackScale G u h • backtrackElem G k h

Rescaling multiplies a backtrack element by its backtrack scale: the backtrack element is the product of an arrow with its reverse, and rescaling multiplies each of the two by its own label.

The gauge transform of a parameter

def TauCeti.SkewZigzagParameter.gauge {k : Type w} [CommMonoid k] {V : Type u} {G : SimpleGraph V} (c : SkewZigzagParameter k G) (u : ⦃x y : DoubledQuiver G⦄ → (x ⟶ y) → kˣ) : SkewZigzagParameter k G

The gauge transform of a skew-zigzag parameter by a unit-valued labelling u of the arrows of the doubled quiver: each ratio is multiplied by the ratio of the two backtrack scales it compares. This is exactly the change of parameters produced by rescaling the arrows by u.

@[simp]

theorem TauCeti.SkewZigzagParameter.gauge_ratio {k : Type w} [CommMonoid k] {V : Type u} {G : SimpleGraph V} (c : SkewZigzagParameter k G) (u : ⦃x y : DoubledQuiver G⦄ → (x ⟶ y) → kˣ) {i j j' : V} (h : G.Adj i j) (h' : G.Adj i j') : (c.gauge u).ratio h h' = c.ratio h h' * (DoubledQuiver.backtrackScale G u h' / DoubledQuiver.backtrackScale G u h)

theorem TauCeti.SkewZigzagParameter.gauge_congr {k : Type w} [CommMonoid k] {V : Type u} {G : SimpleGraph V} (c : SkewZigzagParameter k G) {u u' : ⦃x y : DoubledQuiver G⦄ → (x ⟶ y) → kˣ} (hu : ∀ ⦃x y : DoubledQuiver G⦄ (e : x ⟶ y), u e = u' e) : c.gauge u = c.gauge u'

Gauging by pointwise equal labellings gives the same parameter.

@[simp]

theorem TauCeti.SkewZigzagParameter.gauge_one {k : Type w} [CommMonoid k] {V : Type u} {G : SimpleGraph V} (c : SkewZigzagParameter k G) : (c.gauge fun (x x_1 : DoubledQuiver G) (x_2 : x ⟶ x_1) => 1) = c

Gauging by the constant labelling one changes nothing.

theorem TauCeti.SkewZigzagParameter.gauge_gauge {k : Type w} [CommMonoid k] {V : Type u} {G : SimpleGraph V} (c : SkewZigzagParameter k G) (u u' : ⦃x y : DoubledQuiver G⦄ → (x ⟶ y) → kˣ) : (c.gauge u).gauge u' = c.gauge fun (x x_1 : DoubledQuiver G) (e : x ⟶ x_1) => u e * u' e

Gauge transforms compose by multiplying labellings.

theorem TauCeti.SkewZigzagParameter.backtrackScale_mul_gauge_ratio {k : Type w} [CommMonoid k] {V : Type u} {G : SimpleGraph V} (c : SkewZigzagParameter k G) (u : ⦃x y : DoubledQuiver G⦄ → (x ⟶ y) → kˣ) {i j j' : V} (h : G.Adj i j) (h' : G.Adj i j') : DoubledQuiver.backtrackScale G u h * (c.gauge u).ratio h h' = c.ratio h h' * DoubledQuiver.backtrackScale G u h'

The defining identity of the gauge transform: multiplying a gauged ratio by the backtrack scale of its first edge gives the original ratio times the backtrack scale of its second edge. This is the scalar identity behind gauge independence of the presented algebra: it equates the two ways of rescaling the backtrack relator of a pair of incident edges.

@[simp]

theorem TauCeti.SkewZigzagParameter.gauge_gauge_inv {k : Type w} [CommMonoid k] {V : Type u} {G : SimpleGraph V} (c : SkewZigzagParameter k G) (u : ⦃x y : DoubledQuiver G⦄ → (x ⟶ y) → kˣ) : ((c.gauge u).gauge fun (x x_1 : DoubledQuiver G) (e : x ⟶ x_1) => (u e)⁻¹) = c

Gauging by the pointwise inverse labelling undoes a gauge transform.

The gauge action and gauge equivalence

@[instance_reducible]

instance TauCeti.SkewZigzagParameter.instMulActionForallForallForallHomDoubledQuiverUnits {k : Type w} [CommMonoid k] {V : Type u} {G : SimpleGraph V} : MulAction (⦃x y : DoubledQuiver G⦄ → (x ⟶ y) → kˣ) (SkewZigzagParameter k G)

Gauge transforms are an action of the pointwise group of unit-valued arrow labellings on skew-zigzag parameters: gauge_one and gauge_gauge are its two axioms. Gauge equivalence is the orbit relation of this action.

@[simp]

theorem TauCeti.SkewZigzagParameter.smul_eq_gauge {k : Type w} [CommMonoid k] {V : Type u} {G : SimpleGraph V} (u : ⦃x y : DoubledQuiver G⦄ → (x ⟶ y) → kˣ) (c : SkewZigzagParameter k G) : u • c = c.gauge u

The gauge action is the gauge transform.

def TauCeti.SkewZigzagParameter.IsGaugeEquivalent {k : Type w} [CommMonoid k] {V : Type u} {G : SimpleGraph V} (c c' : SkewZigzagParameter k G) : Prop

Two skew-zigzag parameters are gauge equivalent when one is a gauge transform of the other, that is, when rescaling the arrows of the doubled quiver by units carries the first presentation to the second. This is the orbit relation of the gauge action.

theorem TauCeti.SkewZigzagParameter.isGaugeEquivalent_iff {k : Type w} [CommMonoid k] {V : Type u} {G : SimpleGraph V} {c c' : SkewZigzagParameter k G} : c.IsGaugeEquivalent c' ↔ ∃ (u : ⦃x y : DoubledQuiver G⦄ → (x ⟶ y) → kˣ), c' = c.gauge u

Gauge equivalence in existential form: a gauging labelling carrying the first parameter to the second.

theorem TauCeti.SkewZigzagParameter.IsGaugeEquivalent.refl {k : Type w} [CommMonoid k] {V : Type u} {G : SimpleGraph V} (c : SkewZigzagParameter k G) : c.IsGaugeEquivalent c

Every parameter is gauge equivalent to itself, by the constant labelling one.

theorem TauCeti.SkewZigzagParameter.IsGaugeEquivalent.symm {k : Type w} [CommMonoid k] {V : Type u} {G : SimpleGraph V} {c c' : SkewZigzagParameter k G} (h : c.IsGaugeEquivalent c') : c'.IsGaugeEquivalent c

Gauge equivalence is symmetric: the pointwise inverse labelling gauges back.

theorem TauCeti.SkewZigzagParameter.IsGaugeEquivalent.trans {k : Type w} [CommMonoid k] {V : Type u} {G : SimpleGraph V} {c c' c'' : SkewZigzagParameter k G} (h : c.IsGaugeEquivalent c') (h' : c'.IsGaugeEquivalent c'') : c.IsGaugeEquivalent c''

Gauge equivalence is transitive: the pointwise product labelling gauges across.

theorem TauCeti.SkewZigzagParameter.IsGaugeEquivalent.equivalence {k : Type w} [CommMonoid k] {V : Type u} {G : SimpleGraph V} : Equivalence IsGaugeEquivalent

Gauge equivalence of skew-zigzag parameters is an equivalence relation.

theorem TauCeti.SkewZigzagParameter.gauge_eq_mul_gauge_one {k : Type w} [CommMonoid k] {V : Type u} {G : SimpleGraph V} (c : SkewZigzagParameter k G) (u : ⦃x y : DoubledQuiver G⦄ → (x ⟶ y) → kˣ) : c.gauge u = c * gauge 1 u

A gauge transform multiplies a parameter by the gauge transform of the constant parameter.

theorem TauCeti.SkewZigzagParameter.isGaugeEquivalent_iff_isGaugeEquivalent_one_div {k : Type w} [CommMonoid k] {V : Type u} {G : SimpleGraph V} {c c' : SkewZigzagParameter k G} : c.IsGaugeEquivalent c' ↔ IsGaugeEquivalent 1 (c' / c)

Two parameters are gauge equivalent exactly when their quotient is gauge trivial.

Gauge triviality through edge scales

theorem TauCeti.SkewZigzagParameter.isGaugeEquivalent_one_iff_exists_ratio_eq_div {k : Type w} [CommMonoid k] {V : Type u} {G : SimpleGraph V} {c : SkewZigzagParameter k G} : IsGaugeEquivalent 1 c ↔ ∃ (s : ⦃i j : V⦄ → G.Adj i j → kˣ), (∀ ⦃i j : V⦄ (h : G.Adj i j), s ⋯ = s h) ∧ ∀ ⦃i j j' : V⦄ (h : G.Adj i j) (h' : G.Adj i j'), c.ratio h h' = s h / s h'

A parameter is gauge trivial exactly when its ratios are quotients of a symmetric edge scale: a unit s on each edge, independent of its orientation, with ratio(h, h') = s h / s h' for every two edges h, h' at a common vertex.

@[simp]

theorem TauCeti.SkewZigzagParameter.map_gauge {k : Type w} [CommMonoid k] {V : Type u} {G : SimpleGraph V} {l : Type z} [CommMonoid l] (f : k →* l) (c : SkewZigzagParameter k G) (a : ⦃x y : DoubledQuiver G⦄ → (x ⟶ y) → kˣ) : map f (c.gauge a) = (map f c).gauge fun (x x_1 : DoubledQuiver G) (b : x ⟶ x_1) => (Units.map f) (a b)

Mapping parameters along a monoid homomorphism commutes with gauge transforms when the arrow labels are mapped by the same homomorphism.

theorem TauCeti.SkewZigzagParameter.IsGaugeEquivalent.map {k : Type w} [CommMonoid k] {V : Type u} {G : SimpleGraph V} {l : Type z} [CommMonoid l] {c c' : SkewZigzagParameter k G} (h : c.IsGaugeEquivalent c') (f : k →* l) : (SkewZigzagParameter.map f c).IsGaugeEquivalent (SkewZigzagParameter.map f c')

Mapping along a monoid homomorphism preserves gauge equivalence of skew-zigzag parameters.

Gauge independence of the presented algebra

noncomputable def TauCeti.skewZigzagQuotientGaugeEquiv (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (c c' : SkewZigzagParameter k G) (u : ⦃x y : DoubledQuiver G⦄ → (x ⟶ y) → kˣ) (hc : c' = c.gauge u) : skewZigzagQuotient k G c ≃ₐ[k] skewZigzagQuotient k G c'

Gauge independence of the skew-zigzag relation quotient. A parameter and its gauge transform present isomorphic algebras: the isomorphism is the arrow rescaling by the gauging units, which fixes every vertex idempotent and multiplies each oriented edge by its unit.

@[simp]

theorem TauCeti.skewZigzagQuotientGaugeEquiv_skewZigzagMk (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (c c' : SkewZigzagParameter k G) (u : ⦃x y : DoubledQuiver G⦄ → (x ⟶ y) → kˣ) (hc : c' = c.gauge u) (x : pathAlgebra k (DoubledQuiver G)) : (skewZigzagQuotientGaugeEquiv k G c c' u hc) ((skewZigzagMk k G c) x) = (skewZigzagMk k G c') ((PathAlgebra.rescale fun (x x_1 : DoubledQuiver G) (e : x ⟶ x_1) => ↑(u e)) x)

The gauge isomorphism is the arrow rescaling: on an arbitrary quotient representative it rescales and then takes the class in the gauged quotient.

@[simp]

theorem TauCeti.skewZigzagQuotientGaugeEquiv_symm_skewZigzagMk (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (c c' : SkewZigzagParameter k G) (u : ⦃x y : DoubledQuiver G⦄ → (x ⟶ y) → kˣ) (hc : c' = c.gauge u) (x : pathAlgebra k (DoubledQuiver G)) : (skewZigzagQuotientGaugeEquiv k G c c' u hc).symm ((skewZigzagMk k G c') x) = (skewZigzagMk k G c) ((PathAlgebra.rescale fun (x x_1 : DoubledQuiver G) (e : x ⟶ x_1) => ↑(u e)⁻¹) x)

The inverse gauge isomorphism is rescaling by the pointwise inverse units.

theorem TauCeti.nonempty_algEquiv_skewZigzagQuotient_of_isGaugeEquivalent (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] {c c' : SkewZigzagParameter k G} (h : c.IsGaugeEquivalent c') : Nonempty (skewZigzagQuotient k G c ≃ₐ[k] skewZigzagQuotient k G c')

Gauge equivalent parameters present isomorphic algebras.

Gauge-trivial parameters

theorem TauCeti.nonempty_algEquiv_nonisolatedZigzagQuotient_of_isGaugeEquivalent_one (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] {c : SkewZigzagParameter k G} (h : SkewZigzagParameter.IsGaugeEquivalent 1 c) : Nonempty (skewZigzagQuotient k G c ≃ₐ[k] nonisolatedZigzagQuotient k G)

A gauge-trivial skew-zigzag parameter presents the ordinary zigzag algebra. Gauge equivalence is symmetric, so this is the comparison for every parameter in the gauge class of the constant one.