The mesh complex K and its collapse

Subsection 4.1 (subsec:mesh-walk-cover, scalar-normalization.tex): "For every nonprojective vertex X, adjoin an edge t_X : τX → X to the underlying graph of Γ. For each arrow a : Y → X with X nonprojective, attach a triangle with boundary (σa) a t_X⁻¹." Its fundamental groupoid is Morse.Pi (meshTris Q).

The proof of Lemma 4.2 (lem:mesh-walk-free, lines 96–113) eliminates edges and triangles. Here the eliminations are an acyclic matching (meshMatching):

• an arrow whose mate orbit is a finite chain is eliminated with its own triangle, from the end of the chain ("Along a chain, the triangles successively express all but one quiver edge in terms of that edge and the edges t_X. Eliminate these edges and triangles from one end of the chain"); the potential is the remaining length of the chain;
• on the arrows with cyclic mate orbits (the periodic components) the matching is read off from a depth function e on vertices that is invariant under τ and such that each vertex has at most one cyclic incoming arrow from a vertex of depth at most its own: the triangle of the arrow from the parent eliminates t_X, the other triangles eliminate their arrow. This is the combinatorial form of "a periodic component containing arrows gives a mapping torus, which retracts onto its core circle"; the depth function is constructed from the tree model in PeriodicDepth.lean.

Once every triangle is eliminated, the remaining complex is a graph and the vertex groups are free (Morse.isFreeGroup_end).

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.MeshWalk.Arr (V : Type) [Quiver V] : Type

Arrows of the quiver.

def MultiplicativeBasisDeformations.MeshWalk.MateChain {V : Type} [Quiver V] (Q : TranslationQuiver V) : Arr V → ℕ → Prop

σ^j a is defined for all j < n.

def MultiplicativeBasisDeformations.MeshWalk.Cyclic {V : Type} [Quiver V] (Q : TranslationQuiver V) (A : Arr V) : Prop

An arrow whose mate orbit is a cycle: all powers of σ are defined.

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.MeshWalk.Ed {V : Type} [Quiver V] (Q : TranslationQuiver V) : Type

The edges of K: the arrows and the translation edges t_X.

def MultiplicativeBasisDeformations.MeshWalk.src {V : Type} [Quiver V] (Q : TranslationQuiver V) : Ed Q → V

Source of an edge.

def MultiplicativeBasisDeformations.MeshWalk.tgt {V : Type} [Quiver V] (Q : TranslationQuiver V) : Ed Q → V

Target of an edge.

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.MeshWalk.Tri {V : Type} [Quiver V] (Q : TranslationQuiver V) : Type

The triangles of K: one for each arrow a : y → x with x nonprojective.

def MultiplicativeBasisDeformations.MeshWalk.Tri.arr {V : Type} [Quiver V] {Q : TranslationQuiver V} (t : Tri Q) : Arr V

The arrow of a triangle.

def MultiplicativeBasisDeformations.MeshWalk.Tri.mateArr {V : Type} [Quiver V] {Q : TranslationQuiver V} (t : Tri Q) : Arr V

The mate arrow σ a : τ x → y of a triangle.

def MultiplicativeBasisDeformations.MeshWalk.meshTris {V : Type} [Quiver V] (Q : TranslationQuiver V) : Morse.Tris (src Q) (tgt Q)

The mesh complex: triangles (σa) a = t_X.

theorem MultiplicativeBasisDeformations.MeshWalk.cyclic_mate {V : Type} [Quiver V] {Q : TranslationQuiver V} (t : Tri Q) (h : Cyclic Q t.arr) : Cyclic Q t.mateArr

theorem MultiplicativeBasisDeformations.MeshWalk.cyclic_of_mate {V : Type} [Quiver V] {Q : TranslationQuiver V} (t : Tri Q) (h : Cyclic Q t.mateArr) : Cyclic Q t.arr

noncomputable def MultiplicativeBasisDeformations.MeshWalk.len {V : Type} [Quiver V] {Q : TranslationQuiver V} (A : Arr V) : ℕ

The remaining length of a finite mate chain.

theorem MultiplicativeBasisDeformations.MeshWalk.len_mate {V : Type} [Quiver V] {Q : TranslationQuiver V} (t : Tri Q) (h : ¬Cyclic Q t.arr) : len t.mateArr + 1 = len t.arr

theorem MultiplicativeBasisDeformations.MeshWalk.arr_injective {V : Type} [Quiver V] {Q : TranslationQuiver V} {t t' : Tri Q} (h : t'.arr = t.arr) : t' = t

theorem MultiplicativeBasisDeformations.MeshWalk.arr_fst {V : Type} [Quiver V] {Q : TranslationQuiver V} {t : Tri Q} {A : Arr V} (h : t.arr = A) : t.snd.fst = A.fst

theorem MultiplicativeBasisDeformations.MeshWalk.arr_snd {V : Type} [Quiver V] {Q : TranslationQuiver V} {t : Tri Q} {A : Arr V} (h : t.arr = A) : ↑t.fst = A.snd.fst

structure MultiplicativeBasisDeformations.MeshWalk.Depth {V : Type} [Quiver V] (Q : TranslationQuiver V) : Type

A depth function on the vertices, adapted to the cyclic arrows.

• e : V → ℕ

  the depth

• tau_eq (t : Tri Q) : Cyclic Q t.arr → self.e ↑(Q.tau t.fst) = self.e ↑t.fst

  invariance under τ along cyclic arrows

• uniq (t t' : Tri Q) : t.fst = t'.fst → Cyclic Q t.arr → Cyclic Q t'.arr → self.e t.snd.fst ≤ self.e ↑t.fst → self.e t'.snd.fst ≤ self.e ↑t'.fst → t = t'

  at most one cyclic arrow into a vertex comes from depth at most its own

def MultiplicativeBasisDeformations.MeshWalk.Up {V : Type} [Quiver V] {Q : TranslationQuiver V} (D : Depth Q) (t : Tri Q) : Prop

The condition for a triangle to eliminate its translation edge.

theorem MultiplicativeBasisDeformations.MeshWalk.edge_zero {V : Type} [Quiver V] {Q : TranslationQuiver V} (t : Tri Q) : (meshTris Q).edge t 0 = Sum.inl t.mateArr

theorem MultiplicativeBasisDeformations.MeshWalk.edge_one {V : Type} [Quiver V] {Q : TranslationQuiver V} (t : Tri Q) : (meshTris Q).edge t 1 = Sum.inl t.arr

theorem MultiplicativeBasisDeformations.MeshWalk.edge_two {V : Type} [Quiver V] {Q : TranslationQuiver V} (t : Tri Q) : (meshTris Q).edge t 2 = Sum.inr t.fst

theorem MultiplicativeBasisDeformations.MeshWalk.matched_inr {V : Type} [Quiver V] {Q : TranslationQuiver V} (D : Depth Q) {t : Tri Q} {x : ↑Q.nonprojective} (h : (meshTris Q).edge t (if Up D t then 2 else 1) = Sum.inr x) : t.fst = x ∧ Up D t

theorem MultiplicativeBasisDeformations.MeshWalk.matched_inl {V : Type} [Quiver V] {Q : TranslationQuiver V} (D : Depth Q) {t : Tri Q} {A : Arr V} (h : (meshTris Q).edge t (if Up D t then 2 else 1) = Sum.inl A) : t.arr = A ∧ ¬Up D t

def MultiplicativeBasisDeformations.MeshWalk.B {V : Type} [Quiver V] {Q : TranslationQuiver V} (D : Depth Q) [Fintype V] : ℕ

A bound above all the periodic potentials.

theorem MultiplicativeBasisDeformations.MeshWalk.lt_B {V : Type} [Quiver V] {Q : TranslationQuiver V} (D : Depth Q) [Fintype V] (v : V) : 2 * D.e v + 1 < B D

noncomputable def MultiplicativeBasisDeformations.MeshWalk.pot {V : Type} [Quiver V] {Q : TranslationQuiver V} (D : Depth Q) [Fintype V] (t : Tri Q) : ℕ

The potential of a triangle.

theorem MultiplicativeBasisDeformations.MeshWalk.pot_up {V : Type} [Quiver V] {Q : TranslationQuiver V} (D : Depth Q) [Fintype V] {t : Tri Q} (hu : Up D t) : pot D t = 2 * D.e ↑t.fst

theorem MultiplicativeBasisDeformations.MeshWalk.pot_down {V : Type} [Quiver V] {Q : TranslationQuiver V} (D : Depth Q) [Fintype V] {t : Tri Q} (hc : Cyclic Q t.arr) (hd : D.e ↑t.fst < D.e t.snd.fst) : pot D t = 2 * D.e ↑t.fst + 1

theorem MultiplicativeBasisDeformations.MeshWalk.pot_chain {V : Type} [Quiver V] {Q : TranslationQuiver V} (D : Depth Q) [Fintype V] {t : Tri Q} (hc : ¬Cyclic Q t.arr) : pot D t = B D + len t.arr

theorem MultiplicativeBasisDeformations.MeshWalk.pot_ge {V : Type} [Quiver V] {Q : TranslationQuiver V} (D : Depth Q) [Fintype V] {t : Tri Q} : 2 * D.e ↑t.fst ≤ pot D t

noncomputable def MultiplicativeBasisDeformations.MeshWalk.meshMatching {V : Type} [Quiver V] {Q : TranslationQuiver V} (D : Depth Q) [Fintype V] : Morse.Matching (meshTris Q)

The matching of the mesh complex.

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.MeshWalk.PiK {V : Type} [Quiver V] (Q : TranslationQuiver V) : Type

The fundamental groupoid Π(K) of the mesh complex: walks modulo cancellation and the triangle relations.

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.MeshWalk.obK {V : Type} [Quiver V] (Q : TranslationQuiver V) (X : V) : PiK Q

A vertex of Γ as an object of Π(K).

theorem MultiplicativeBasisDeformations.MeshWalk.isFreeGroup_end_of_depth {V : Type} [Quiver V] {Q : TranslationQuiver V} (D : Depth Q) [Fintype V] (X : V) : IsFreeGroup (CategoryTheory.End (obK Q X))

The vertex groups of K are free, given a depth function on the periodic part.