The repetition ℤΔ of a tree and the signed preprojective category Π(Δ)

scalar-normalization.tex and periodic-mesh-calculations.tex.

We use the height coordinates of Proposition 4.1(2) (periodic-mesh-calculations.tex). Fix a finite graph Δ with a proper two-colouring par. A vertex of ℤΔ is a pair (v, t) with t ≡ par v (mod 2), its height being t; there is an arrow (u, t) → (v, t + 1) for every edge u — v. Translation is (v, t) ↦ (v, t - 2). For an orientation of Δ with d_v - d_u = 1 along every arrow u → v, this is the repetition quiver of Subsection 4.1 under v_j ↦ (v, 2j + d_v).

Π(Δ) is the path category of the doubled quiver modulo the vertex relations ∑_{a : x → y} a a* - ∑_{a : y → x} a* a, i.e. ρ_x = ∑_{y — x} ε(x, y) (x → y → x) with ε(x, y) = 1 if the edge is oriented x → y and -1 otherwise. The signed mesh coefficients of ℤΔ are c_{(x,t), (y,t-1)} = ε(x, y), so forgetting heights sends the mesh relation at (x, t) to ρ_x.

structure MultiplicativeBasisDeformations.OrientedTree (D : Type v) : Type v

A finite graph with a proper two-colouring and an orientation of its edges.

• G : SimpleGraph D
• par : D → ZMod 2
• par_adj {u w : D} : self.G.Adj u w → self.par w = self.par u + 1
• orient : D → D → Prop
• orient_adj {u w : D} : self.orient u w → self.G.Adj u w
• orient_or {u w : D} : self.G.Adj u w → (self.orient u w ↔ ¬self.orient w u)

structure MultiplicativeBasisDeformations.OrientedTree.ZVert {D : Type v} (T : OrientedTree D) : Type v

A vertex of the repetition ℤΔ, in height coordinates.

• v : D
• t : ℤ
• ht : ↑self.t = T.par self.v

theorem MultiplicativeBasisDeformations.OrientedTree.ZVert.ext {D : Type v} {T : OrientedTree D} {x y : T.ZVert} (v : x.v = y.v) (t : x.t = y.t) : x = y

theorem MultiplicativeBasisDeformations.OrientedTree.ZVert.ext_iff {D : Type v} {T : OrientedTree D} {x y : T.ZVert} : x = y ↔ x.v = y.v ∧ x.t = y.t

@[instance_reducible]

instance MultiplicativeBasisDeformations.OrientedTree.instQuiverZVert {D : Type v} (T : OrientedTree D) : Quiver T.ZVert

instance MultiplicativeBasisDeformations.OrientedTree.instSubsingletonHomZVert {D : Type v} (T : OrientedTree D) (X Y : T.ZVert) : Subsingleton (X ⟶ Y)

def MultiplicativeBasisDeformations.OrientedTree.ztau {D : Type v} (T : OrientedTree D) (X : T.ZVert) : T.ZVert

Translation on ℤΔ.

def MultiplicativeBasisDeformations.OrientedTree.ztauInv {D : Type v} (T : OrientedTree D) (X : T.ZVert) : T.ZVert

Inverse translation on ℤΔ.

def MultiplicativeBasisDeformations.OrientedTree.zQuiver {D : Type v} (T : OrientedTree D) : TranslationQuiver T.ZVert

ℤΔ as a stable translation quiver.

theorem MultiplicativeBasisDeformations.OrientedTree.zQuiver_isStable {D : Type v} (T : OrientedTree D) : T.zQuiver.IsStable

@[simp]

theorem MultiplicativeBasisDeformations.OrientedTree.zQuiver_tau_v {D : Type v} (T : OrientedTree D) (X : ↑T.zQuiver.nonprojective) : (↑(T.zQuiver.tau X)).v = (↑X).v

@[simp]

theorem MultiplicativeBasisDeformations.OrientedTree.zQuiver_tau_t {D : Type v} (T : OrientedTree D) (X : ↑T.zQuiver.nonprojective) : (↑(T.zQuiver.tau X)).t = (↑X).t - 2

@[instance_reducible]

noncomputable instance MultiplicativeBasisDeformations.OrientedTree.instFintypeCostar {D : Type v} (T : OrientedTree D) [Fintype D] (X : T.ZVert) : Fintype ((Y : T.ZVert) × (Y ⟶ X))

def MultiplicativeBasisDeformations.OrientedTree.sgn {D : Type v} (T : OrientedTree D) (k : Type u) [CommRing k] [DecidableRel T.orient] (u w : D) : kˣ

The sign ε(u, w) of an edge: 1 if it is oriented u → w, else -1.

theorem MultiplicativeBasisDeformations.OrientedTree.sgn_swap {D : Type v} (T : OrientedTree D) [Fintype D] [DecidableEq D] (k : Type u) [CommRing k] [DecidableRel T.orient] {u w : D} (h : T.G.Adj u w) : T.sgn k w u = -T.sgn k u w

def MultiplicativeBasisDeformations.OrientedTree.zSigned {D : Type v} (T : OrientedTree D) (k : Type u) [CommRing k] [DecidableRel T.orient] : MeshCoefficients k T.zQuiver

The signed preprojective mesh coefficients on ℤΔ.

def MultiplicativeBasisDeformations.OrientedTree.Dbl {D : Type v} (_T : OrientedTree D) : Type v

The doubled quiver of Δ: an arrow each way along every edge.

@[instance_reducible]

instance MultiplicativeBasisDeformations.OrientedTree.instQuiverDbl {D : Type v} (T : OrientedTree D) : Quiver T.Dbl

instance MultiplicativeBasisDeformations.OrientedTree.instSubsingletonHomDbl {D : Type v} (T : OrientedTree D) (u w : T.Dbl) : Subsingleton (u ⟶ w)

@[instance_reducible]

instance MultiplicativeBasisDeformations.OrientedTree.instFintypeDbl {D : Type v} (T : OrientedTree D) [Fintype D] : Fintype T.Dbl

@[instance_reducible]

instance MultiplicativeBasisDeformations.OrientedTree.instDecidableEqDbl {D : Type v} (T : OrientedTree D) [DecidableEq D] : DecidableEq T.Dbl

@[instance_reducible]

noncomputable instance MultiplicativeBasisDeformations.OrientedTree.instFintypeDblStar {D : Type v} (T : OrientedTree D) [Fintype D] (x : T.Dbl) : Fintype ((y : T.Dbl) × (x ⟶ y))

noncomputable def MultiplicativeBasisDeformations.OrientedTree.preprojRel {D : Type v} (T : OrientedTree D) [Fintype D] (k : Type u) [CommRing k] [DecidableRel T.orient] (x : T.Dbl) : LinearPaths.obj x ⟶ LinearPaths.obj x

The relation ρ_x = ∑_{y — x} ε(x, y) (x → y → x) of Π(Δ).

noncomputable def MultiplicativeBasisDeformations.OrientedTree.preproj {D : Type v} (T : OrientedTree D) [Fintype D] (k : Type u) [CommRing k] [DecidableRel T.orient] : RelSystem k T.Dbl

The relations of Π(Δ).

def MultiplicativeBasisDeformations.OrientedTree.forget {D : Type v} (T : OrientedTree D) : T.ZVert ⥤q T.Dbl

Forgetting heights, ℤΔ → Δ̄.

theorem MultiplicativeBasisDeformations.OrientedTree.forget_isCovering {D : Type v} (T : OrientedTree D) [Fintype D] [DecidableEq D] : T.forget.IsCovering

def MultiplicativeBasisDeformations.OrientedTree.toDbl {D : Type v} (T : OrientedTree D) (v : D) : T.Dbl

A vertex of Δ, as a vertex of the doubled quiver.

def MultiplicativeBasisDeformations.OrientedTree.costarEquiv {D : Type v} (T : OrientedTree D) (X : T.ZVert) : (Y : T.ZVert) × (Y ⟶ X) ≃ (y : T.Dbl) × (T.toDbl X.v ⟶ y)

The arrows into X correspond to the edges at X.v.

theorem MultiplicativeBasisDeformations.OrientedTree.mapPaths_forget_meshRelation {D : Type v} (T : OrientedTree D) [Fintype D] [DecidableEq D] (k : Type u) [CommRing k] [DecidableRel T.orient] (X : ↑T.zQuiver.nonprojective) : (LinearPaths.mapPaths T.forget ↑(T.zQuiver.tau X) ↑X) (meshRelation (T.zSigned k) X) = T.preprojRel k (T.toDbl (↑X).v)

Forgetting heights sends the signed mesh relation at (x, t) to ρ_x.

theorem MultiplicativeBasisDeformations.OrientedTree.ztau_ztauInv {D : Type v} (T : OrientedTree D) [Fintype D] [DecidableEq D] [DecidableRel T.orient] (Z : T.ZVert) : T.ztau (T.ztauInv Z) = Z

theorem MultiplicativeBasisDeformations.OrientedTree.forget_mem_preproj {D : Type v} (T : OrientedTree D) [Fintype D] [DecidableEq D] (k : Type u) [CommRing k] [DecidableRel T.orient] {X Y : T.ZVert} {f : LinearPaths.obj X ⟶ LinearPaths.obj Y} (hf : f ∈ (RelSystem.mesh (T.zSigned k)).ideal (LinearPaths.obj X) (LinearPaths.obj Y)) : (LinearPaths.mapPaths T.forget X Y) f ∈ (T.preproj k).ideal (LinearPaths.obj (T.forget.obj X)) (LinearPaths.obj (T.forget.obj Y))

Forgetting heights maps the signed mesh ideal of ℤΔ into the ideal of Π(Δ).

theorem MultiplicativeBasisDeformations.OrientedTree.mem_mesh_of_forget {D : Type v} (T : OrientedTree D) [Fintype D] [DecidableEq D] (k : Type u) [CommRing k] [DecidableRel T.orient] {X Y : T.ZVert} {f : LinearPaths.obj X ⟶ LinearPaths.obj Y} (hf : (LinearPaths.mapPaths T.forget X Y) f ∈ (T.preproj k).ideal (LinearPaths.obj (T.forget.obj X)) (LinearPaths.obj (T.forget.obj Y))) : f ∈ (RelSystem.mesh (T.zSigned k)).ideal (LinearPaths.obj X) (LinearPaths.obj Y)

Lifting Π(Δ) relations to ℤΔ: forgetting heights reflects the ideal.