Lemma 4.2 for the Auslander--Reiten quiver

lem:mesh-walk-free (scalar-normalization.tex): the complex K of Γ_A has free vertex groups. The hypotheses of MeshWalk.isFreeGroup_end are Lemma 2.2 (at most one arrow, hasAtMostOneArrow) and the finite-dimensionality of k(Γ_A) (finiteDimensional_meshHom), which is what Proposition 4.1 needs. The source assumes A connected; the vertex group at every vertex is free without this assumption.

theorem MultiplicativeBasisDeformations.IndSkeleton.meshWalk_isFreeGroup {k A : Type w} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : IndSkeleton k A) (X : S.ARVertex) : IsFreeGroup (CategoryTheory.End (MeshWalk.obK S.arTranslationQuiver X))

Lemma 4.2 (lem:mesh-walk-free): the fundamental group of the mesh complex K of Γ_A at every vertex is free.