Periodic components are connected stable translation quivers

Proof of Proposition 5.3, reduction to components (periodic-mesh-calculations.tex): on a finite translation quiver, a periodic component K is closed under τ^{±1} and every vertex of K is the translate of a vertex of K, so the full translation subquiver on K is stable; it is connected by arrows and translation edges.

theorem MultiplicativeBasisDeformations.TranslationQuiver.periodic_nonproj {V : Type v} [Quiver V] {Q : TranslationQuiver V} {v : V} (hv : v ∈ Q.periodic) : v ∈ Q.nonprojective

theorem MultiplicativeBasisDeformations.TranslationQuiver.periodic_tau {V : Type v} [Quiver V] {Q : TranslationQuiver V} {v : V} (hv : v ∈ Q.periodic) : ↑(Q.tau ⟨v, ⋯⟩) ∈ Q.periodic

theorem MultiplicativeBasisDeformations.TranslationQuiver.periodic_mem_noninjective {V : Type v} [Quiver V] {Q : TranslationQuiver V} [Finite V] {v : V} (hv : v ∈ Q.periodic) : v ∈ Q.noninjective

On a finite quiver periodic vertices are translates, hence noninjective.

theorem MultiplicativeBasisDeformations.TranslationQuiver.restrict_isStable {V : Type v} [Quiver V] {Q : TranslationQuiver V} (x : V) [Finite V] : (restrict ⋯).IsStable

The full subquiver on a periodic component is stable.

theorem MultiplicativeBasisDeformations.TranslationQuiver.restrict_conn {V : Type v} [Quiver V] {Q : TranslationQuiver V} (x : V) [Finite V] (hx : x ∈ Q.periodic) (a : FullSub (Q.component x)) : Relation.EqvGen (SecPath.ConnAdj ⋯) (FullSub.mk x ⋯) a

A periodic component is connected by arrows and translation edges.