The deck group is countable

The exhaustion of Lemma 4.12 enumerates the objects of L; for this the deck group must be countable. Its elements are classes of walks in a finite complex: paths in the symmetrized edge quiver are determined by their lists of edges (arrowList_injective), and the fundamental groupoid is a quotient of the path category.

theorem Quiver.Path.arrowList_inj {V : Type v} [Quiver V] {x y : V} (p q : Path x y) : p.arrowList = q.arrowList → p = q

instance Quiver.Path.instCountable {V : Type v} [Quiver V] [Countable ((u : V) × (v : V) × (u ⟶ v))] {x y : V} : Countable (Path x y)

instance MultiplicativeBasisDeformations.MeshWalk.instCountableArr {V : Type} [Quiver V] [Fintype V] [(x : V) → Fintype ((y : V) × (y ⟶ x))] : Countable (Arr V)

instance MultiplicativeBasisDeformations.MeshWalk.instCountableSumEd {V : Type} [Quiver V] [Fintype V] (Q : TranslationQuiver V) [(x : V) → Fintype ((y : V) × (y ⟶ x))] : Countable (Ed Q ⊕ V)

instance MultiplicativeBasisDeformations.MeshWalk.countable_deck {V : Type} [Quiver V] [Fintype V] (Q : TranslationQuiver V) [(x : V) → Fintype ((y : V) × (y ⟶ x))] (v₀ : V) : Countable (Deck Q v₀)

The deck group is countable.