Mesh corrections on the odd quotients of even A #
Appendix A, "The odd quotients of even A" (periodic-mesh-calculations.tex): after normalizing all mesh coefficients to one (Lemma A.1(2)), rows are
reduced by the sum of their levels to words in the middle arrows, which vanish
when two is invertible.
theorem
MultiplicativeBasisDeformations.StarTrace.surjective_A_even
{L : Fin 1 → ℕ}
{V : Type v'}
[Quiver V]
[∀ (x y : V), Subsingleton (x ⟶ y)]
{Q : TranslationQuiver V}
(hQ : Q.IsStable)
(π : (starTree L).ZVert ⥤q V)
{k : Type u}
[Field k]
[(x : V) → Fintype ((y : V) × (y ⟶ x))]
[DecidableEq V]
[(x y : V) → DecidableEq (x ⟶ y)]
[DecidablePred fun (x : V) => x ∈ Q.nonprojective]
[Fintype ↑Q.nonprojective]
(hπ : π.IsCovering)
(hτ : ∀ (Y : (starTree L).ZVert), π.obj ((starTree L).ztau Y) = hQ.tauE (π.obj Y))
(hsurj : ∀ (x : V), ∃ (X : (starTree L).ZVert), π.obj X = x)
(ρ : StarV L ≃ StarV L)
(hρ : ∀ (a b : StarV L), (starTree L).G.Adj (ρ a) (ρ b) ↔ (starTree L).G.Adj a b)
(c0 : ℕ)
(hc0 : 0 < c0)
(hρp : ∀ (v : StarV L), (starTree L).par (ρ v) = (starTree L).par v + ↑↑c0)
(hdeck : ∀ (Z : (starTree L).ZVert), π.obj (((starTree L).zAct ρ hρ (↑c0) hρp).obj Z) = π.obj Z)
(hfib :
∀ (X Y : (starTree L).ZVert),
π.obj X = π.obj Y → ∃ (n : ℕ), Y = (StarGauge.gZ ρ hρ c0 hρp)^[n] X ∨ X = (StarGauge.gZ ρ hρ c0 hρp)^[n] Y)
(h : ℕ)
(hh : 1 ≤ h)
(hL : L 0 = 2 * h - 2)
(hrev : ∀ (x : StarV L), starDepth (ρ x) + starDepth x = L 0 + 1)
(h2 : 2 ≠ 0)
(c : MeshCoefficients k Q)
(m : ℕ)
(hm : 2 ≤ m)
:
Type A_{2h}, odd quotients: the deck generator reverses the path.