Type D in characteristic two (Appendix B)

characteristic-two-mesh-calculations.tex. On a periodic star model of type D_n (N = n − 2) with period c₀ = 2s, a row of path degree 2j exists only for j = 1 + n s with twist θ^n (Lemma A.2(1)), and its class is an integer multiple of the alternating word w_j (trace_D_span), which vanishes for j > N. "The brick hypothesis forces N < 2s. Otherwise delete the terminal part of the long arm, retaining D_{2s+2}. Its top paths have degree 4s, fix the tree vertices, and increase the repetition coordinate by 2s. They become radical endomorphisms at every object, for either trivial action or an interchange." Hence only j = s + 1 remains: all cokernel classes are multiples of the class of the row of w_{s+1} at the centre.

For the three-cycle of the arms of D_4, all classes vanish.

def MultiplicativeBasisDeformations.TraceAlg.altL (a b : Fin 3) : ℕ → List (Fin 3)

The alternating word of length n in the arms a, b, starting with a.

theorem MultiplicativeBasisDeformations.TraceAlg.length_altL (a b : Fin 3) (n : ℕ) : (altL a b n).length = n

theorem MultiplicativeBasisDeformations.TraceAlg.altE_succ_left {S : Type u_1} [Ring S] (p q : S) (n : ℕ) : p * altE q p n = altE p q (n + 1)

theorem MultiplicativeBasisDeformations.TraceAlg.prod_altL {L : Fin 3 → ℕ} (n : ℕ) (a b : Fin 3) : (List.map (x L) (altL a b n)).prod = altE (x L a) (x L b) n

theorem MultiplicativeBasisDeformations.TraceAlg.perm_three_fpf (θ : Equiv.Perm (Fin 3)) (hθ : ∀ (i : Fin 3), θ i ≠ i) (n : ℕ) : θ ^ n = 1 ∧ 3 ∣ n ∨ ∀ (i : Fin 3), (θ ^ n) i ≠ i

theorem MultiplicativeBasisDeformations.TraceAlg.trace_D_hspan {M : Type u_1} [AddCommGroup M] {L : Fin 3 → ℕ} {a b c : Fin 3} (hab : a ≠ b) (hac : a ≠ c) (hbc : b ≠ c) (hLa : L a = 0) (hLb : L b = 0) (θ : Equiv.Perm (Fin 3)) (hθL : ∀ (i : Fin 3), L (θ i) = L i) (s : ℕ) (hcase : θ c = c ∧ L c + 2 < 2 * s ∨ ∀ (i : Fin 3), θ i ≠ i) (D : TraceData L M) (n : ℕ) (hn : D.θ = θ ^ n) (w : List (Fin 3)) (hw : 2 ≤ w.length) (hd : 2 * w.length = 2 + n * (2 * s)) : ∃ (z : ℤ), D.tr w = z • D.tr (altL a b (s + 1))

The spanning hypothesis for type D: every trace of a word of length j = 1 + n s with twist θ^n is a multiple of the trace of w_{s+1}, when either θ fixes the long arm and N < 2s, or θ is a three-cycle.

theorem MultiplicativeBasisDeformations.Substar.mem_Out_iff {t : ℕ} {L L' : Fin t → ℕ} (hle : ∀ (i : Fin t), L' i ≤ L i) (x : StarV L) : x ∈ Out hle ↔ ∃ (i : Fin t) (j : Fin (L i + 1)), x = some ⟨i, j⟩ ∧ L' i < ↑j

theorem MultiplicativeBasisDeformations.StarTrace.not_brick_D_long {V : Type v'} [Quiver V] [∀ (x y : V), Subsingleton (x ⟶ y)] {Q : TranslationQuiver V} (hQ : Q.IsStable) {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] (c : MeshCoefficients k Q) {L : Fin 3 → ℕ} {π : (starTree L).ZVert ⥤q V} (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 : ℕ) (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) (h0 : ρ none = none) (θ : Equiv.Perm (Fin 3)) (hL : ∀ (i : Fin 3), L (θ i) = L i) (hθ : ∀ (i : Fin 3) (j : ℕ) (hj : j ≤ L i), ρ (StarGauge.ch i j hj) = StarGauge.ch (θ i) j ⋯) {a b c' : Fin 3} (hab : a ≠ b) (hac : a ≠ c') (hbc : b ≠ c') (hLa : L a = 0) (hLb : L b = 0) (hθc : θ c' = c') (hc0e : Even c0) (hc0 : 0 < c0) (hN : c0 ≤ L c' + 2) : ¬ScalarMeshCategory.BrickHypothesis c

The brick hypothesis bounds the long arm of type D: if θ fixes the long arm c and c₀ ≤ N = L c + 2, the brick hypothesis fails (deletion to D_{c₀ + 2} and Lemma B.1).

theorem MultiplicativeBasisDeformations.StarTrace.d_cokerSpan {V : Type v'} [Quiver V] {Q : TranslationQuiver V} (hQ : Q.IsStable) {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] (c : MeshCoefficients k Q) {L : Fin 3 → ℕ} {π : (starTree L).ZVert ⥤q V} (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 : ℕ) (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) [∀ (x y : V), Subsingleton (x ⟶ y)] (hbrick : ScalarMeshCategory.BrickHypothesis c) (hρ' : ∀ (a b : StarV L), starAdj a b ↔ starAdj (ρ a) (ρ b)) (h0 : ρ none = none) (hc0 : 0 < c0) {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)), W₀.length = c0 / 2 + 1 ∧ ScalarMeshCategory.CokerSpan c (candRow hQ π W₀) ∧ ScalarMeshCategory.TwoRows Q (candRow hQ π W₀)

Type D in characteristic two: on a periodic star model of type D whose deck generator fixes the centre, the cokernels are spanned by the row of one word of length c₀/2 + 1 at the centre, under the brick hypothesis.