Scalar-labelled skew-zigzag relation quotients

A skew-zigzag relation quotient changes the ordinary relation identifying all backtracks at a vertex by allowing a unit-valued, hence invertible, scalar ratio between each ordered pair of incident edges. A parameter therefore assigns a unit ratio h h' to two adjacencies with a common source, subject to the reflexive, inverse, and cocycle identities for these ratios. The quotient imposes

backtrack(h) = ratio(h,h') • backtrack(h').

As for the ordinary relation quotient, non-returning length-two paths and paths of length at least three vanish. At the constant parameter, all of whose ratios are one, the relation ideal is the ordinary zigzag relation ideal, so the two presentations agree there.

Main definitions

• TauCeti.SkewZigzagParameter: a unit-valued backtrack-ratio labelling.
• the One instance on TauCeti.SkewZigzagParameter: the constant parameter, all of whose ratios are one.
• the CommGroup instance on TauCeti.SkewZigzagParameter: over a commutative monoid, parameters multiply ratio by ratio.
• TauCeti.IsSkewZigzagRelator and TauCeti.skewZigzagIdeal: the uniform skew relation family and the two-sided ideal it generates, with TauCeti.skewZigzagIdeal_eq_span reading it as a two-sided span.
• TauCeti.skewZigzagQuotient and TauCeti.skewZigzagMk: the relation quotient and quotient map.
• TauCeti.skewZigzagQuotientOneEquiv: the identification of the constant-parameter quotient with the ordinary zigzag relation quotient.

Main results

• TauCeti.skewZigzagMk_backtrackElem_eq_smul: the defining scalar backtrack relation in the quotient.
• TauCeti.skewZigzagLift and TauCeti.skewZigzagLift_unique: the quotient universal property.
• TauCeti.skewZigzagIdeal_one_eq_zigzagIdeal: the constant parameter spans the ordinary zigzag relation ideal.

References

See C. Couture, Skew-Zigzag Algebras, Definition 3.1 and Definition 3.2, https://arxiv.org/abs/1509.08405.

structure TauCeti.SkewZigzagParameter (k : Type w) [Monoid k] {V : Type u} (G : SimpleGraph V) : Type (max u w)

A skew-zigzag parameter assigns a unit-valued, hence invertible, scalar ratio to every ordered pair of adjacencies with a common source. The units make invertibility part of the type, and the fields below record the coefficient identities. Gauge equivalence of parameters is intentionally not imposed by this presentation.

• ratio ⦃i j j' : V⦄ : G.Adj i j → G.Adj i j' → kˣ

  The ratio from the backtrack indexed by h to the one indexed by h'.

• ratio_self ⦃i j : V⦄ (h : G.Adj i j) : self.ratio h h = 1

  A backtrack has ratio one with itself.

• ratio_inv ⦃i j j' : V⦄ (h : G.Adj i j) (h' : G.Adj i j') : self.ratio h h' * self.ratio h' h = 1

  Reversing an ordered pair of backtracks inverts its ratio.

• ratio_cocycle ⦃i j j' j'' : V⦄ (h : G.Adj i j) (h' : G.Adj i j') (h'' : G.Adj i j'') : self.ratio h h' * self.ratio h' h'' * self.ratio h'' h = 1

  Ratios between three backtracks satisfy the multiplicative cocycle identity.

theorem TauCeti.SkewZigzagParameter.ext_iff {k : Type w} {inst✝ : Monoid k} {V : Type u} {G : SimpleGraph V} {x y : SkewZigzagParameter k G} : x = y ↔ x.ratio = y.ratio

theorem TauCeti.SkewZigzagParameter.ext {k : Type w} {inst✝ : Monoid k} {V : Type u} {G : SimpleGraph V} {x y : SkewZigzagParameter k G} (ratio : x.ratio = y.ratio) : x = y

@[simp]

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

Skew-zigzag ratios compose along incident edges.

@[instance_reducible]

instance TauCeti.SkewZigzagParameter.instOne {k : Type w} [Monoid k] {V : Type u} {G : SimpleGraph V} : One (SkewZigzagParameter k G)

The constant skew-zigzag parameter, all of whose ratios are one: it imposes that all backtracks at a vertex are equal, which is the ordinary zigzag relation.

@[simp]

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

@[instance_reducible]

instance TauCeti.SkewZigzagParameter.instMul {k : Type w} [CommMonoid k] {V : Type u} {G : SimpleGraph V} : Mul (SkewZigzagParameter k G)

The ratio-by-ratio product of two skew-zigzag parameters.

@[instance_reducible]

instance TauCeti.SkewZigzagParameter.instInv {k : Type w} [CommMonoid k] {V : Type u} {G : SimpleGraph V} : Inv (SkewZigzagParameter k G)

The ratio-by-ratio inverse of a skew-zigzag parameter.

@[simp]

theorem TauCeti.SkewZigzagParameter.mul_ratio {k : Type w} [CommMonoid k] {V : Type u} {G : SimpleGraph V} (c c' : SkewZigzagParameter k G) {i j j' : V} (h : G.Adj i j) (h' : G.Adj i j') : (c * c').ratio h h' = c.ratio h h' * c'.ratio h h'

The ratios of a product of parameters are the products of their ratios.

@[simp]

theorem TauCeti.SkewZigzagParameter.inv_ratio {k : Type w} [CommMonoid k] {V : Type u} {G : SimpleGraph V} (c : SkewZigzagParameter k G) {i j j' : V} (h : G.Adj i j) (h' : G.Adj i j') : c⁻¹.ratio h h' = (c.ratio h h')⁻¹

The ratios of an inverse parameter are the inverses of its ratios.

@[instance_reducible]

instance TauCeti.SkewZigzagParameter.instCommGroup {k : Type w} [CommMonoid k] {V : Type u} {G : SimpleGraph V} : CommGroup (SkewZigzagParameter k G)

Over a commutative monoid, skew-zigzag parameters form a commutative group under the ratio-by-ratio product, with the constant parameter as identity.

@[simp]

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

The ratios of a quotient of parameters are the quotients of their ratios.

def TauCeti.SkewZigzagParameter.map {k : Type w} {l : Type z} [Monoid k] [Monoid l] {V : Type u} {G : SimpleGraph V} (f : k →* l) (c : SkewZigzagParameter k G) : SkewZigzagParameter l G

Apply a monoid homomorphism to every ratio of a skew-zigzag parameter.

@[simp]

theorem TauCeti.SkewZigzagParameter.map_ratio {k : Type w} {l : Type z} [Monoid k] [Monoid l] {V : Type u} {G : SimpleGraph V} (f : k →* l) (c : SkewZigzagParameter k G) {i j j' : V} (h : G.Adj i j) (h' : G.Adj i j') : (map f c).ratio h h' = (Units.map f) (c.ratio h h')

Mapping a parameter applies the monoid homomorphism to each ratio.

@[simp]

theorem TauCeti.SkewZigzagParameter.map_one {k : Type w} {l : Type z} [Monoid k] [Monoid l] {V : Type u} {G : SimpleGraph V} (f : k →* l) : map f 1 = 1

The constant parameter remains constant after mapping along a monoid homomorphism.

@[simp]

theorem TauCeti.SkewZigzagParameter.map_id {k : Type w} [Monoid k] {V : Type u} {G : SimpleGraph V} (c : SkewZigzagParameter k G) : map (MonoidHom.id k) c = c

Mapping a parameter along the identity homomorphism changes nothing.

@[simp]

theorem TauCeti.SkewZigzagParameter.map_comp {k : Type w} {l : Type z} [Monoid k] [Monoid l] {V : Type u} {G : SimpleGraph V} {m : Type u_1} [Monoid m] (f : k →* l) (g : l →* m) (c : SkewZigzagParameter k G) : map (g.comp f) c = map g (map f c)

Mapping a parameter along a composite is the same as successive mapping.

theorem TauCeti.SkewZigzagParameter.map_injective {k : Type w} {l : Type z} [Monoid k] [Monoid l] {V : Type u} {G : SimpleGraph V} (f : k →* l) (hf : Function.Injective ⇑(Units.map f)) : Function.Injective (map f)

Injectivity on units induces an injective map on skew-zigzag parameters.

theorem TauCeti.SkewZigzagParameter.ratio_ne_zero {k : Type w} [MonoidWithZero k] [Nontrivial k] {V : Type u} {G : SimpleGraph V} (c : SkewZigzagParameter k G) {i j j' : V} (h : G.Adj i j) (h' : G.Adj i j') : ↑(c.ratio h h') ≠ 0

The scalar ratio attached to two incident edges is nonzero.

inductive TauCeti.IsSkewZigzagRelator (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) (c : SkewZigzagParameter k G) : pathAlgebra k (DoubledQuiver G) → Prop

The uniform skew-zigzag relators: non-returning quadratic paths, scalar ratios between backtracks based at one vertex, and all paths of length at least three.

• nonreturn {k : Type w} [CommRing k] {V : Type u} {G : SimpleGraph V} {c : SkewZigzagParameter k G} {i j : DoubledQuiver G} (p : Quiver.Path i j) (length_eq : p.length = 2) (different_endpoints : i ≠ j) : IsSkewZigzagRelator k G c (PathAlgebra.ofPath ⟨i, ⟨j, p⟩⟩)
• backtrack_ratio {k : Type w} [CommRing k] {V : Type u} {G : SimpleGraph V} {c : SkewZigzagParameter k G} {i j j' : V} (h : G.Adj i j) (h' : G.Adj i j') : IsSkewZigzagRelator k G c (DoubledQuiver.backtrackElem G k h - ↑(c.ratio h h') • DoubledQuiver.backtrackElem G k h')
• long_path {k : Type w} [CommRing k] {V : Type u} {G : SimpleGraph V} {c : SkewZigzagParameter k G} (x : Quiver.TotalPath (DoubledQuiver G)) (three_le : 3 ≤ x.snd.snd.length) : IsSkewZigzagRelator k G c (PathAlgebra.ofPath x)

noncomputable def TauCeti.skewZigzagIdeal (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) (c : SkewZigzagParameter k G) : TwoSidedIdeal (pathAlgebra k (DoubledQuiver G))

The two-sided ideal generated by the uniform skew-zigzag relation family.

theorem TauCeti.skewZigzagIdeal_eq_span (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) (c : SkewZigzagParameter k G) : skewZigzagIdeal k G c = TwoSidedIdeal.span {x : pathAlgebra k (DoubledQuiver G) | IsSkewZigzagRelator k G c x}

The skew-zigzag relation ideal is the two-sided span of the relation family.

theorem TauCeti.mem_skewZigzagIdeal_of_isSkewZigzagRelator (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) (c : SkewZigzagParameter k G) {x : pathAlgebra k (DoubledQuiver G)} (hx : IsSkewZigzagRelator k G c x) : x ∈ skewZigzagIdeal k G c

Every skew-zigzag relator belongs to the relation ideal it generates.

The relation quotient

@[reducible, inline]

noncomputable abbrev TauCeti.skewZigzagQuotient (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (c : SkewZigzagParameter k G) : Type (max (max u w) w u)

The scalar-labelled skew-zigzag relation quotient of a doubled simple graph. As with nonisolatedZigzagQuotient, this is a relation quotient rather than the eventual componentwise public zigzag algebra.

noncomputable def TauCeti.skewZigzagMk (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (c : SkewZigzagParameter k G) : pathAlgebra k (DoubledQuiver G) →ₐ[k] skewZigzagQuotient k G c

The quotient map onto the skew-zigzag relation quotient.

theorem TauCeti.skewZigzagMk_apply (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (c : SkewZigzagParameter k G) (x : pathAlgebra k (DoubledQuiver G)) : (skewZigzagMk k G c) x = (Ideal.Quotient.mk (TwoSidedIdeal.asIdeal (skewZigzagIdeal k G c))) x

The quotient map is the ring-theoretic quotient map of the skew relation ideal.

theorem TauCeti.skewZigzagMk_surjective (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (c : SkewZigzagParameter k G) : Function.Surjective ⇑(skewZigzagMk k G c)

The skew-zigzag quotient map is surjective.

@[simp]

theorem TauCeti.skewZigzagMk_eq_zero_iff (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (c : SkewZigzagParameter k G) {x : pathAlgebra k (DoubledQuiver G)} : (skewZigzagMk k G c) x = 0 ↔ x ∈ skewZigzagIdeal k G c

The kernel of the skew-zigzag quotient map is its relation ideal.

theorem TauCeti.skewZigzagMk_eq_zero_of_isSkewZigzagRelator (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (c : SkewZigzagParameter k G) {x : pathAlgebra k (DoubledQuiver G)} (hx : IsSkewZigzagRelator k G c x) : (skewZigzagMk k G c) x = 0

Every skew-zigzag relator dies in the quotient.

@[simp]

theorem TauCeti.skewZigzagMk_ofPath_eq_zero_of_ne (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (c : SkewZigzagParameter k G) {i j : DoubledQuiver G} (p : Quiver.Path i j) (hp : p.length = 2) (hij : i ≠ j) : (skewZigzagMk k G c) (PathAlgebra.ofPath ⟨i, ⟨j, p⟩⟩) = 0

A length-two path whose endpoints differ dies in the skew-zigzag quotient.

@[simp]

theorem TauCeti.skewZigzagMk_ofPath_eq_zero_of_three_le (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (c : SkewZigzagParameter k G) (x : Quiver.TotalPath (DoubledQuiver G)) (hx : 3 ≤ x.snd.snd.length) : (skewZigzagMk k G c) (PathAlgebra.ofPath x) = 0

A path of length at least three dies in the skew-zigzag quotient.

theorem TauCeti.skewZigzagMk_backtrackElem_eq_smul (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (c : SkewZigzagParameter k G) {i j j' : V} (h : G.Adj i j) (h' : G.Adj i j') : (skewZigzagMk k G c) (DoubledQuiver.backtrackElem G k h) = ↑(c.ratio h h') • (skewZigzagMk k G c) (DoubledQuiver.backtrackElem G k h')

The defining skew relation: backtracks at one vertex differ by the prescribed unit-valued, hence invertible, scalar ratio.

The universal property

theorem TauCeti.skewZigzagIdeal_le_ker (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (c : SkewZigzagParameter k G) {B : Type u_1} [Ring B] [Algebra k B] (f : pathAlgebra k (DoubledQuiver G) →ₐ[k] B) (hf : ∀ (x : pathAlgebra k (DoubledQuiver G)), IsSkewZigzagRelator k G c x → f x = 0) : skewZigzagIdeal k G c ≤ TwoSidedIdeal.ker f

An algebra map which kills the skew relators kills the two-sided ideal they generate.

noncomputable def TauCeti.skewZigzagLift (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (c : SkewZigzagParameter k G) {B : Type u_1} [Ring B] [Algebra k B] (f : pathAlgebra k (DoubledQuiver G) →ₐ[k] B) (hf : ∀ (x : pathAlgebra k (DoubledQuiver G)), IsSkewZigzagRelator k G c x → f x = 0) : skewZigzagQuotient k G c →ₐ[k] B

An algebra map which kills every skew-zigzag relator factors through the skew relation quotient.

@[simp]

theorem TauCeti.skewZigzagLift_skewZigzagMk (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (c : SkewZigzagParameter k G) {B : Type u_1} [Ring B] [Algebra k B] (f : pathAlgebra k (DoubledQuiver G) →ₐ[k] B) (hf : ∀ (x : pathAlgebra k (DoubledQuiver G)), IsSkewZigzagRelator k G c x → f x = 0) (x : pathAlgebra k (DoubledQuiver G)) : (skewZigzagLift k G c f hf) ((skewZigzagMk k G c) x) = f x

The skew-zigzag lift agrees with its defining map on quotient representatives.

theorem TauCeti.skewZigzagLift_unique (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (c : SkewZigzagParameter k G) {B : Type u_1} [Ring B] [Algebra k B] (f : pathAlgebra k (DoubledQuiver G) →ₐ[k] B) (hf : ∀ (x : pathAlgebra k (DoubledQuiver G)), IsSkewZigzagRelator k G c x → f x = 0) (g : skewZigzagQuotient k G c →ₐ[k] B) (hg : ∀ (x : pathAlgebra k (DoubledQuiver G)), g ((skewZigzagMk k G c) x) = f x) : g = skewZigzagLift k G c f hf

The skew-zigzag lift is the unique algebra map whose composite with the quotient map is its defining map.

The constant parameter and the ordinary zigzag relations

theorem TauCeti.skewZigzagIdeal_one_eq_zigzagIdeal (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) : skewZigzagIdeal k G 1 = zigzagIdeal k G

The constant parameter imposes exactly the ordinary zigzag relations. Its backtrack relators say that two backtracks at a vertex are equal, which is the ordinary quadratic relator, and the non-returning and long-path families of the two presentations agree.

noncomputable def TauCeti.skewZigzagQuotientOneEquiv (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] : skewZigzagQuotient k G 1 ≃ₐ[k] nonisolatedZigzagQuotient k G

The constant parameter presents the ordinary zigzag algebra: its skew relation is that all backtracks at a vertex are equal, which is the ordinary zigzag relation.

@[simp]

theorem TauCeti.skewZigzagQuotientOneEquiv_skewZigzagMk (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (x : pathAlgebra k (DoubledQuiver G)) : (skewZigzagQuotientOneEquiv k G) ((skewZigzagMk k G 1) x) = (zigzagMk k G) x

The comparison with the ordinary zigzag quotient sends the class of an element to its ordinary class.

@[simp]

theorem TauCeti.skewZigzagQuotientOneEquiv_symm_zigzagMk (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (x : pathAlgebra k (DoubledQuiver G)) : (skewZigzagQuotientOneEquiv k G).symm ((zigzagMk k G) x) = (skewZigzagMk k G 1) x

The inverse comparison with the ordinary zigzag quotient sends the class of an element to its skew class at the constant parameter.