Stable translation quivers

For a stable translation quiver (every vertex nonprojective and noninjective, TranslationQuiver.IsStable) the translation is a permutation τ of the vertices. The mate bijections give y → x iff τ x → y, and τ preserves arrows. These facts are used throughout the proof of Proposition 4.1 (periodic-mesh-calculations.tex).

theorem MultiplicativeBasisDeformations.TranslationQuiver.IsStable.mem_nonprojective {V : Type v} [Quiver V] {Q : TranslationQuiver V} (hQ : Q.IsStable) (v : V) : v ∈ Q.nonprojective

theorem MultiplicativeBasisDeformations.TranslationQuiver.IsStable.mem_noninjective {V : Type v} [Quiver V] {Q : TranslationQuiver V} (hQ : Q.IsStable) (v : V) : v ∈ Q.noninjective

def MultiplicativeBasisDeformations.TranslationQuiver.IsStable.tauE {V : Type v} [Quiver V] {Q : TranslationQuiver V} (hQ : Q.IsStable) : Equiv.Perm V

The translation of a stable translation quiver, as a permutation.

theorem MultiplicativeBasisDeformations.TranslationQuiver.IsStable.tauE_apply {V : Type v} [Quiver V] {Q : TranslationQuiver V} (hQ : Q.IsStable) (v : V) : hQ.tauE v = ↑(Q.tau ⟨v, ⋯⟩)

theorem MultiplicativeBasisDeformations.TranslationQuiver.IsStable.nonempty_hom_iff {V : Type v} [Quiver V] {Q : TranslationQuiver V} (hQ : Q.IsStable) (x y : V) : Nonempty (y ⟶ x) ↔ Nonempty (hQ.tauE x ⟶ y)

Arrows into x correspond to arrows out of τ x.

theorem MultiplicativeBasisDeformations.TranslationQuiver.IsStable.nonempty_hom_tau_iff {V : Type v} [Quiver V] {Q : TranslationQuiver V} (hQ : Q.IsStable) (u v : V) : Nonempty (hQ.tauE u ⟶ hQ.tauE v) ↔ Nonempty (u ⟶ v)

τ preserves arrows.

theorem MultiplicativeBasisDeformations.TranslationQuiver.IsStable.nonempty_hom_zpow_iff {V : Type v} [Quiver V] {Q : TranslationQuiver V} (hQ : Q.IsStable) (n : ℤ) (u v : V) : Nonempty ((hQ.tauE ^ n) u ⟶ (hQ.tauE ^ n) v) ↔ Nonempty (u ⟶ v)