Mesh corrections for periodic models of type A #
Appendix A, "Types A and D" (periodic-mesh-calculations.tex):
"When the twist is trivial … we may root the path at an endpoint and regard it
as a star with one arm … For the reflection of A_{2n-1}, rooted at its middle
vertex, the two closed paths at the centre are x and -x, and reflection sends
x to -x."
theorem
MultiplicativeBasisDeformations.StarTrace.surjective_A_id
{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)
(hρ' : ∀ (a b : StarV L), starAdj a b ↔ starAdj (ρ 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)
(hid : ∀ (x : StarV L), starDepth (ρ x) = starDepth x)
(c : MeshCoefficients k Q)
(m : ℕ)
(hm : 2 ≤ m)
:
Type A, trivial twist: the deck generator preserves depths.
theorem
MultiplicativeBasisDeformations.StarTrace.surjective_A_odd_reflection
{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 - 1)
(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+1}, reflection: re-root at the middle vertex; the two closed
paths at the centre are x and -x.