Mesh corrections on a periodic star model

Assembly of Appendix A for a periodic component covered by a star model whose deck group is generated by g (v, t) = (ρ v, t + c₀) with ρ fixing the centre (periodic-mesh-calculations.tex): normalize the coefficients (Lemma A.1(1)), lift the rows of degree m + 1 (they exist only when c₀ ∣ m - 1), express them as twisted traces of words at the centre (Lemmas A.2 and A.4), and conclude from the vanishing of the traces.

noncomputable def MultiplicativeBasisDeformations.StarTrace.traceData {t : ℕ} {L : Fin t → ℕ} {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} [CommRing k] [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] [DecidablePred fun (x : V) => x ∈ Q.nonprojective] (σ : StarV L ≃ StarV L) (hσ : ∀ (a b : StarV L), (starTree L).G.Adj (σ a) (σ b) ↔ (starTree L).G.Adj a b) (m : ℕ) (s : ℤ) (hσp : ∀ (v : StarV L), (starTree L).par (σ v) = (starTree L).par v + ↑s) (hπ : π.IsCovering) (hτ : ∀ (Y : (starTree L).ZVert), π.obj ((starTree L).ztau Y) = hQ.tauE (π.obj Y)) (hsig : (starTree L).pullCoeff hQ π c = (starTree L).zSigned k) (hc : ScalarMeshCategory.OppositeOnMates c hQ) (hdeck : ∀ (Z : (starTree L).ZVert), π.obj (((starTree L).zAct σ hσ s hσp).obj Z) = π.obj Z) (hs : ↑m + 1 = 2 + s) (hσo : σ none = none) (θ : Equiv.Perm (Fin t)) (hL : ∀ (i : Fin t), L (θ i) = L i) (hθ : ∀ (i : Fin t) (j : ℕ) (hj : j ≤ L i), σ (StarCorner.av L i j hj) = StarCorner.av L (θ i) j ⋯) : TraceAlg.TraceData L (ScalarMeshCategory.Coker c m)

The word traces form a twisted trace in the sense of TraceAlg.

theorem MultiplicativeBasisDeformations.StarTrace.rowClass_eq_zero {t : ℕ} {L : Fin t → ℕ} {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} [CommRing k] [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] [DecidablePred fun (x : V) => x ∈ Q.nonprojective] (σ : StarV L ≃ StarV L) (hσ : ∀ (a b : StarV L), (starTree L).G.Adj (σ a) (σ b) ↔ (starTree L).G.Adj a b) (m : ℕ) (s : ℤ) (hσp : ∀ (v : StarV L), (starTree L).par (σ v) = (starTree L).par v + ↑s) (hπ : π.IsCovering) (hτ : ∀ (Y : (starTree L).ZVert), π.obj ((starTree L).ztau Y) = hQ.tauE (π.obj Y)) (hsig : (starTree L).pullCoeff hQ π c = (starTree L).zSigned k) (hc : ScalarMeshCategory.OppositeOnMates c hQ) (hdeck : ∀ (Z : (starTree L).ZVert), π.obj (((starTree L).zAct σ hσ s hσp).obj Z) = π.obj Z) (hs : ↑m + 1 = 2 + s) (hσo : σ none = none) (θ : Equiv.Perm (Fin t)) (hL : ∀ (i : Fin t), L (θ i) = L i) (hθ : ∀ (i : Fin t) (j : ℕ) (hj : j ≤ L i), σ (StarCorner.av L i j hj) = StarCorner.av L (θ i) j ⋯) (hm : 2 ≤ m) (hsurj : ∀ (x : V), ∃ (X : (starTree L).ZVert), π.obj X = x) (hfib : ∀ (X E : (starTree L).ZVert), π.obj E = π.obj X → E.t = X.t + s → E = ((starTree L).zAct σ hσ s hσp).obj X) (hvan : ∀ (w : List (Fin t)), 2 ≤ w.length → 2 * w.length = m + 1 → (traceData hQ π c σ hσ m s hσp hπ hτ hsig hc hdeck hs hσo θ hL hθ).tr w = 0) (x : ↑Q.nonprojective) (p : Quiver.Path ↑(Q.tau x) ↑x) (hp : p.length = m + 1) : ScalarMeshCategory.rowClass c m x p = 0

Vanishing traces kill the cokernel. If all word traces of length at least two vanish, every row of degree m + 1 = 2 + s lies in the image of D_m.

theorem MultiplicativeBasisDeformations.OrientedTree.oppositeOnMates_of_signed {D : Type u_1} (T : OrientedTree D) [Fintype D] [DecidableEq D] [DecidableRel T.orient] {V : Type v'} [Quiver V] [∀ (x y : V), Subsingleton (x ⟶ y)] {Q : TranslationQuiver V} (hQ : Q.IsStable) (π : T.ZVert ⥤q V) {k : Type u} [CommRing k] [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) (hπ : π.IsCovering) (hτ : ∀ (Y : T.ZVert), π.obj (T.ztau Y) = hQ.tauE (π.obj Y)) (hsurj : ∀ (x : V), ∃ (X : T.ZVert), π.obj X = x) (hsig : T.pullCoeff hQ π c = T.zSigned k) : ScalarMeshCategory.OppositeOnMates c hQ

Signed coefficients are opposite on mates ("the two mesh coefficients of the corresponding tree edge … are opposite", proof of Lemma A.2).

theorem MultiplicativeBasisDeformations.StarTrace.adj_pow {t : ℕ} {L : Fin t → ℕ} (ρ : StarV L ≃ StarV L) (hρ : ∀ (a b : StarV L), (starTree L).G.Adj (ρ a) (ρ b) ↔ (starTree L).G.Adj a b) (n : ℕ) (a b : StarV L) : (starTree L).G.Adj ((ρ ^ n) a) ((ρ ^ n) b) ↔ (starTree L).G.Adj a b

Powers of a graph automorphism.

theorem MultiplicativeBasisDeformations.StarTrace.depth_pow {t : ℕ} {L : Fin t → ℕ} (ρ : StarV L ≃ StarV L) (hd : ∀ (v : StarV L), starDepth (ρ v) = starDepth v) (n : ℕ) (v : StarV L) : starDepth ((ρ ^ n) v) = starDepth v

theorem MultiplicativeBasisDeformations.StarTrace.depth_ρ {t : ℕ} {L : Fin t → ℕ} (ρ : StarV L ≃ StarV L) (hρ : ∀ (a b : StarV L), (starTree L).G.Adj (ρ a) (ρ b) ↔ (starTree L).G.Adj a b) (h0 : ρ none = none) (θ : Equiv.Perm (Fin t)) (hL : ∀ (i : Fin t), L (θ i) = L i) (hθ : ∀ (i : Fin t) (j : ℕ) (hj : j ≤ L i), ρ (StarGauge.ch i j hj) = StarGauge.ch (θ i) j ⋯) (v : StarV L) : starDepth (ρ v) = starDepth v

theorem MultiplicativeBasisDeformations.StarTrace.pow_ch' {t : ℕ} {L : Fin t → ℕ} (ρ : StarV L ≃ StarV L) (θ : Equiv.Perm (Fin t)) (hL : ∀ (i : Fin t), L (θ i) = L i) (hθ : ∀ (i : Fin t) (j : ℕ) (hj : j ≤ L i), ρ (StarGauge.ch i j hj) = StarGauge.ch (θ i) j ⋯) (n : ℕ) (i : Fin t) (j : ℕ) (hj : j ≤ L i) : (ρ ^ n) (StarCorner.av L i j hj) = StarCorner.av L ((θ ^ n) i) j ⋯

theorem MultiplicativeBasisDeformations.StarTrace.star_surjective_deg {t : ℕ} {L : Fin t → ℕ} {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} [CommRing 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) (h0 : ρ none = none) (θ : Equiv.Perm (Fin t)) (hL : ∀ (i : Fin t), L (θ i) = L i) (hθ : ∀ (i : Fin t) (j : ℕ) (hj : j ≤ L i), ρ (StarGauge.ch i j hj) = StarGauge.ch (θ i) j ⋯) (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) (hc0 : 0 < c0) (hvan : ∀ (M : Type (max u v' w)) [inst : AddCommGroup M] [Module k M] (D : TraceAlg.TraceData L M) (n : ℕ), D.θ = θ ^ n → ∀ (w : List (Fin t)), 2 ≤ w.length → 2 * w.length = 2 + n * c0 → D.tr w = 0) (c : MeshCoefficients k Q) (m : ℕ) (hm : 2 ≤ m) : ScalarMeshCategory.MeshDerivativeSurjective c m

Mesh corrections vanish on a periodic star model when the word traces vanish in the degrees where rows occur: a word of length l with twist θ^n matters only when 2 l = 2 + n c₀ (Lemma A.2(1)).

theorem MultiplicativeBasisDeformations.StarTrace.star_surjective {t : ℕ} {L : Fin t → ℕ} {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} [CommRing 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) (h0 : ρ none = none) (θ : Equiv.Perm (Fin t)) (hL : ∀ (i : Fin t), L (θ i) = L i) (hθ : ∀ (i : Fin t) (j : ℕ) (hj : j ≤ L i), ρ (StarGauge.ch i j hj) = StarGauge.ch (θ i) j ⋯) (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) (hc0 : 0 < c0) (hvan : ∀ (M : Type (max u v' w)) [inst : AddCommGroup M] [Module k M] (D : TraceAlg.TraceData L M), (∃ (l : ℕ), D.θ = θ ^ l) → ∀ (w : List (Fin t)), 2 ≤ w.length → D.tr w = 0) (c : MeshCoefficients k Q) (m : ℕ) (hm : 2 ≤ m) : ScalarMeshCategory.MeshDerivativeSurjective c m

Mesh corrections vanish on a periodic star model when all word traces of length at least two vanish, for every twist θ^l.

theorem MultiplicativeBasisDeformations.StarTrace.surjective_of_fixed_centre {t : ℕ} {L : Fin t → ℕ} {V : Type v'} [Quiver V] {Q : TranslationQuiver V} (hQ : Q.IsStable) (π : (starTree L).ZVert ⥤q V) {k : Type u} [CommRing 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) [∀ (x y : V), Subsingleton (x ⟶ y)] (ρ : 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)) (h0 : ρ none = none) (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) (hvan : ∀ (θ : Equiv.Perm (Fin t)), (∀ (i : Fin t), L (θ i) = L i) → ∀ (M : Type (max u v' w)) [inst : AddCommGroup M] [Module k M] (D : TraceAlg.TraceData L M), (∃ (l : ℕ), D.θ = θ ^ l) → ∀ (w : List (Fin t)), 2 ≤ w.length → D.tr w = 0) (c : MeshCoefficients k Q) (m : ℕ) (hm : 2 ≤ m) : ScalarMeshCategory.MeshDerivativeSurjective c m

Mesh corrections vanish on a periodic star model whose deck generator fixes the centre, given the vanishing of the twisted traces for the induced arm permutation.

theorem MultiplicativeBasisDeformations.TraceAlg.two_cancel {k : Type u_1} [Field k] (h2 : 2 ≠ 0) {M : Type u_2} [AddCommGroup M] [Module k M] (x : M) (hx : x + x = 0) : x = 0

theorem MultiplicativeBasisDeformations.TraceAlg.trace_D_any {M : Type u_1} [AddCommGroup M] {L : Fin 3 → ℕ} (D : TraceData L M) (h2 : ∀ (m : M), m + m = 0 → m = 0) {a b c : Fin 3} (hab : a ≠ b) (hac : a ≠ c) (hbc : b ≠ c) (hLa : L a = 0) (hLb : L b = 0) {w : List (Fin 3)} (hw : 2 ≤ w.length) : D.tr w = 0

Type D with any twist preserving the arm lengths: all traces of length at least two vanish (twists of a D_n with n ≥ 5 fix the long arm; for D_4 a twist fixing an arm is handled as a short-arm interchange, and a fixed-point free twist is a three-cycle).