Candidate rows killed by two (Lemma B.2 on a periodic star model)

characteristic-two-mesh-calculations.tex (proof of lem:integral-mesh-cokernels): "The proofs of Lemmas A.1 and A.2 apply over 𝒪 without change … Lemma A.2 gives a surjection from the twisted trace module over 𝒪 onto the integral derivative cokernel."

Over any commutative coefficient ring: on a periodic star model, if the twisted trace of a word W₀ is killed by two in every twisted trace module, then so is the class of its candidate row (star_two). The coefficients are first normalized (Lemma A.1, which divides only by units); the candidate row is then the trace of W₀.

def MultiplicativeBasisDeformations.ScalarMeshCategory.TwoRows {V : Type v'} [Quiver V] (Q : TranslationQuiver V) [(x : V) → Fintype ((y : V) × (y ⟶ x))] [DecidableEq V] (S : RowSet Q) : Prop

Rows killed by two over every coefficient ring (the form of Lemma B.2 used here): for all coefficients c over a commutative ring O, twice the class of each row is zero.

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.twoRows_empty {V : Type v'} [Quiver V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] [DecidableEq V] : TwoRows Q ∅

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.TwoRows.mono {V : Type v'} [Quiver V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] [DecidableEq V] {S S' : RowSet Q} (h : TwoRows Q S') (hS : S ⊆ S') : TwoRows Q S

theorem MultiplicativeBasisDeformations.StarTrace.rowClass_candRow {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] (c : MeshCoefficients k Q) (σ : StarV L ≃ StarV L) (hσ : ∀ (a b : StarV L), (starTree L).G.Adj (σ a) (σ b) ↔ (starTree L).G.Adj a b) (m : ℕ) (hσo : σ none = none) (W : List (Fin t)) (hW : 2 * W.length = m + 1) (e : π.obj ((starTree L).ztau X₀) = hQ.tauE (π.obj ((starTree L).liftEnd ((starTree L).ztau X₀) (StarCorner.wordP W)))) : ScalarMeshCategory.rowClass c m ⟨π.obj ((starTree L).liftEnd ((starTree L).ztau X₀) (StarCorner.wordP W)), ⋯⟩ (Quiver.Path.cast e ⋯ (π.mapPath (liftW W))) = wordTr hQ π c σ hσ m hσo W

theorem MultiplicativeBasisDeformations.StarTrace.star_two {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) (W₀ : List (Fin t)) (htwo : ∀ (M : Type (max u v' w)) [inst : AddCommGroup M] [Module k M] (D : TraceAlg.TraceData L M) (n : ℕ), D.θ = θ ^ n → 2 * W₀.length = 2 + n * c0 → D.tr W₀ + D.tr W₀ = 0) (c : MeshCoefficients k Q) (m : ℕ) (hm : 2 ≤ m) (R : (x : ↑Q.nonprojective) × Quiver.Path ↑(Q.tau x) ↑x) : R ∈ candRow hQ π W₀ → R.snd.length = m + 1 → 2 • ScalarMeshCategory.rowClass c m R.fst R.snd = 0

Candidate rows killed by two: if the twisted trace of W₀ is killed by two in every twisted trace module (for the twists θⁿ of its degrees), so is the class of its candidate row, over any commutative coefficient ring.

theorem MultiplicativeBasisDeformations.StarTrace.twoRows_candRow {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) [(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) (W₀ : List (Fin t)) (htwo : ∀ (M : Type (max u v' w)) [inst : AddCommGroup M] (D : TraceAlg.TraceData L M) (n : ℕ), D.θ = θ ^ n → 2 * W₀.length = 2 + n * c0 → D.tr W₀ + D.tr W₀ = 0) : ScalarMeshCategory.TwoRows Q (candRow hQ π W₀)

Candidate rows of words whose traces are killed by two.