The types E: traces and the brick hypothesis

Appendix A, periodic-mesh-calculations.tex: the possible correction classes of E₆, E₇, E₈ live in path degrees six, ten and eighteen; their periods are excluded by deletion to D₄ (Lemma A.5) or to E₇ (Lemma A.7) and the brick hypothesis.

First the exclusion on a periodic star model: if the deck generator g fixes the retained vertices after n steps and n c₀ = d, closed paths of degree d of Π of the retained part lift to closed paths of Q, and the brick hypothesis fails (not_brick_star).

theorem MultiplicativeBasisDeformations.StarTrace.not_brick_star {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} [Field k] [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) (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) (Del : Set (StarV L)) (h0 : none ∉ Del) (hDel : ∀ (v : StarV L), ρ v ∈ Del ↔ v ∈ Del) (n d : ℕ) (hnd : n * c0 = d) (hd : 0 < d) (hfix : ∀ v ∉ Del, (ρ ^ n) v = v) (hNV : ∀ v ∉ Del, ∃ (p : Quiver.Path v v), p.length = d ∧ LinearPaths.path p ∉ (((starTree L).preproj k).del Del).ideal (LinearPaths.obj v) (LinearPaths.obj v)) : ¬ScalarMeshCategory.BrickHypothesis c

Exclusion of a period by deletion. Let Del be a ρ-stable set of vertices of the star not containing the centre, let n c₀ = d > 0, and let ρ^n fix every retained vertex. If each retained vertex carries a closed path of degree d that is nonzero in Π modulo Del, the brick hypothesis fails.

theorem MultiplicativeBasisDeformations.StarTrace.not_brick_D4 {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))] (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 ⋯) (n : ℕ) (hn : n * c0 = 4) (hθn : ∀ (i : Fin 3), (θ ^ n) i = i) : ¬ScalarMeshCategory.BrickHypothesis c

Periods dividing two: deletion to D₄ (Lemma A.5 and periodic-mesh-calculations.tex).

theorem MultiplicativeBasisDeformations.StarTrace.not_brick_E7 {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))] (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) {a b c' : Fin 3} (hab : a ≠ b) (hac : a ≠ c') (hbc : b ≠ c') (hLa : L a = 0) (hLb : L b = 1) (hLc : L c' = 3) (hρid : ∀ (v : StarV L), ρ v = v) (n : ℕ) (hn : n * c0 = 16) : ¬ScalarMeshCategory.BrickHypothesis c

Periods four and eight of E₈: deletion to E₇ (Lemma A.7 and periodic-mesh-calculations.tex).

theorem MultiplicativeBasisDeformations.StarTrace.period_cases (c0 n N : ℕ) (h : n * c0 = N) (hN : N = 4 ∨ N = 8 ∨ N = 16) (he : Even c0) (hpos : 0 < c0) : (∃ (n' : ℕ), n' * c0 = 4) ∨ N ≠ 4 ∧ ∃ (n' : ℕ), n' * c0 = 16

The periods allowed by the degrees six, ten and eighteen.

theorem MultiplicativeBasisDeformations.StarTrace.perm_sq_one {a b c' : Fin 3} (hab : a ≠ b) (hac : a ≠ c') (hbc : b ≠ c') (θ : Equiv.Perm (Fin 3)) (ha : θ a = a) (hb : θ b = c') (hc : θ c' = b) (n : ℕ) : (Even n → ∀ (i : Fin 3), (θ ^ n) i = i) ∧ (Odd n → θ ^ n = θ)

theorem MultiplicativeBasisDeformations.StarTrace.e_surjective {V : Type v'} [Quiver V] [Fintype V] [DecidableEq V] [∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] [(x : V) → Fintype ((y : V) × (y ⟶ x))] [(x y : V) → DecidableEq (x ⟶ y)] {Q : TranslationQuiver V} (hQ : Q.IsStable) [DecidablePred fun (x : V) => x ∈ Q.nonprojective] [Fintype ↑Q.nonprojective] {k : Type u} [Field k] (c : MeshCoefficients k Q) (hbrick : ScalarMeshCategory.BrickHypothesis c) (h2 : 2 ≠ 0) (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) (hEL : ∃ (a : Fin 3) (b : Fin 3) (c : Fin 3), a ≠ b ∧ a ≠ c ∧ b ≠ c ∧ L a = 0 ∧ L b = 1 ∧ 1 ≤ L c ∧ L c ≤ 3) (m : ℕ) (hm : 2 ≤ m) : ScalarMeshCategory.MeshDerivativeSurjective c m

Mesh corrections vanish for the types E under the brick hypothesis, when two is invertible (periodic-mesh-calculations.tex).