The odd quotients of even A in characteristic two (Appendix B)

characteristic-two-mesh-calculations.tex: "For the odd quotient of A_{2n} with period r, … If r ≤ 2n − 1, retain the first (r+1)/2 levels. The top paths of the resulting even-A tree have degree r, go to reflected vertices, and increase the repetition coordinate by r. They are nonzero radical endomorphisms at every quotient object. Thus r > 2n − 1. A path from τv to v starts and ends at the same level and has degree d ≡ 2 modulo r, whereas d ≤ 2n − 1 < r. Again no degree at least three is possible."

This file: the second part (a_even_long). A row of degree m + 1 ≥ 3 lifts to a path of length 2 + n r ≥ 2 + r > 2n, which vanishes in Π(A_{2n}) (ASort.long_mem); in characteristic two the all-one coefficients are the signed ones, so it gives the zero class (phiL_eq_zero_of_mem).

theorem MultiplicativeBasisDeformations.StarTrace.zSigned_char2 {k : Type u} [Field k] {D : Type u_1} (T : OrientedTree D) [DecidableRel T.orient] (hchar : 2 = 0) : T.zSigned k = fun (x : ↑T.zQuiver.nonprojective) (x_1 : T.ZVert) (x_2 : x_1 ⟶ ↑x) => 1

theorem MultiplicativeBasisDeformations.StarTrace.a_even_long {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) (hchar : 2 = 0) (h : ℕ) (hh : 1 ≤ h) (hL : L 0 = 2 * h - 2) (hrev : ∀ (x : StarV L), starDepth (ρ x) + starDepth x = L 0 + 1) (hr : 2 * h ≤ c0) (c : MeshCoefficients k Q) (m : ℕ) (hm : 2 ≤ m) : ScalarMeshCategory.MeshDerivativeSurjective c m

Odd quotients of A_{2n} with period at least 2n: in characteristic two the derivatives are surjective.

Short periods: deletion to a middle interval

theorem MultiplicativeBasisDeformations.StarTrace.not_brick_star_to' {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] {t : ℕ} {L' : Fin t → ℕ} (π' : (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) (c : MeshCoefficients k Q) (Del : Set (StarV L')) (v₀ : StarV L') (h0 : v₀ ∉ Del) (hDel : ∀ (v : StarV L'), ρ' v ∈ Del ↔ v ∈ Del) (n d : ℕ) (hnd : n * c0' = d) (hd : 0 < d) (hNV : ∀ v ∉ Del, ∃ (p : Quiver.Path v ((starTree L').toDbl ((ρ' ^ n) v))), p.length = d ∧ LinearPaths.path p ∉ (((starTree L').preproj k).del Del).ideal (LinearPaths.obj v) (LinearPaths.obj ((starTree L').toDbl ((ρ' ^ n) v)))) : ¬ScalarMeshCategory.BrickHypothesis c

not_brick_star_to with an arbitrary retained base vertex.

The shifted interval

def MultiplicativeBasisDeformations.StarTrace.intervalV {L Ls : Fin 1 → ℕ} (off : ℕ) (hoff : Ls 0 + off ≤ L 0) (y : StarV Ls) : StarV L

The embedding of a shorter line as an interval, shifting depths by off.

theorem MultiplicativeBasisDeformations.StarTrace.depth_intervalV {L Ls : Fin 1 → ℕ} (off : ℕ) (hoff : Ls 0 + off ≤ L 0) (y : StarV Ls) : starDepth (intervalV off hoff y) = starDepth y + off

theorem MultiplicativeBasisDeformations.StarTrace.intervalV_injective {L Ls : Fin 1 → ℕ} (off : ℕ) (hoff : Ls 0 + off ≤ L 0) : Function.Injective (intervalV off hoff)

theorem MultiplicativeBasisDeformations.StarTrace.intervalV_adj {L Ls : Fin 1 → ℕ} (off : ℕ) (hoff : Ls 0 + off ≤ L 0) (x y : StarV Ls) : (starTree L).G.Adj (intervalV off hoff x) (intervalV off hoff y) ↔ (starTree Ls).G.Adj x y

theorem MultiplicativeBasisDeformations.StarTrace.intervalV_orient {L Ls : Fin 1 → ℕ} (off : ℕ) (hoff : Ls 0 + off ≤ L 0) (x y : StarV Ls) : (starTree L).orient (intervalV off hoff x) (intervalV off hoff y) ↔ (starTree Ls).orient x y

theorem MultiplicativeBasisDeformations.StarTrace.mem_range_intervalV {L Ls : Fin 1 → ℕ} (off : ℕ) (hoff : Ls 0 + off ≤ L 0) (x : StarV L) : x ∈ Set.range (intervalV off hoff) ↔ off ≤ starDepth x ∧ starDepth x ≤ Ls 0 + 1 + off

theorem MultiplicativeBasisDeformations.StarTrace.a_even_short {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) (hodd : Odd c0) (hr : c0 ≤ 2 * h - 1) (c : MeshCoefficients k Q) : ¬ScalarMeshCategory.BrickHypothesis c

Odd quotients of A_{2n} with period at most 2n − 1 contradict the brick hypothesis (any characteristic).

theorem MultiplicativeBasisDeformations.StarTrace.a_even_surj {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) (hchar : 2 = 0) (c : MeshCoefficients k Q) (hbrick : ScalarMeshCategory.BrickHypothesis c) (h : ℕ) (hh : 1 ≤ h) (hL : L 0 = 2 * h - 2) (hrev : ∀ (x : StarV L), starDepth (ρ x) + starDepth x = L 0 + 1) (m : ℕ) (hm : 2 ≤ m) : ScalarMeshCategory.MeshDerivativeSurjective c m

Odd quotients of even A in characteristic two, under the brick hypothesis: the derivatives are surjective.