Lemma A.2 for an arbitrary tree

lem:twisted-trace-surjection (periodic-mesh-calculations.tex): "Let Q = Q(Δ, s, ρ) = ℤΔ/⟨τ^s ρ⟩ be a rooted periodic model with signed mesh coefficients, and put Π = Π(Δ). (1) The cokernel class of a correction in a row of degree d ≥ 3 is zero unless d is even and s ∣ (d/2 − 1). (2) In an allowed degree, put l = (1 − d/2)/s and θ = ρ^l. There is a surjection T_θ(Π)_d → coker D_{d−1}."

Here Δ is any finite tree (OrientedTree), and the covering π : ℤΔ → Q has fibres the orbits of the deck generator g (v, t) = (ρ v, t + c₀) in height coordinates (so c₀ = 2s). (1) is row_lift: a row of length m + 1 lifts to a path from τ X to g^n X with n c₀ = m − 1. (2) is twistedTraceSurjection: the twisted trace space T_σ(Π)_{m+1} is the quotient of ⊕_x kΔ̄(x, σ x) by the ideal of Π(Δ), the rotations uv − v σ(u) and the other degrees (TwTrace); lifting paths gives a linear map onto the degree-(m+1) cokernel of D_m (twMap). The star case is StarTrace.rowClass_mem_span with DegreeDeck.row_lift.

(1) The degree of a row

theorem MultiplicativeBasisDeformations.OrientedTree.length_cast' {W : Type u_2} [Quiver W] {a b a' b' : W} (p : Quiver.Path a b) (ha : a = a') (hb : b = b') : (Quiver.Path.cast ha hb p).length = p.length

theorem MultiplicativeBasisDeformations.OrientedTree.adj_pow {D : Type u_1} (T : OrientedTree D) (ρ : D ≃ D) (hρ : ∀ (a b : D), T.G.Adj (ρ a) (ρ b) ↔ T.G.Adj a b) (n : ℕ) (a b : D) : T.G.Adj ((ρ ^ n) a) ((ρ ^ n) b) ↔ T.G.Adj a b

theorem MultiplicativeBasisDeformations.OrientedTree.par_pow {D : Type u_1} (T : OrientedTree D) (ρ : D ≃ D) (c0 : ℕ) (hρp : ∀ (v : D), T.par (ρ v) = T.par v + ↑↑c0) (n : ℕ) (v : D) : T.par ((ρ ^ n) v) = T.par v + ↑↑(n * c0)

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.OrientedTree.gV {D : Type u_1} (T : OrientedTree D) (ρ : D ≃ D) (hρ : ∀ (a b : D), T.G.Adj (ρ a) (ρ b) ↔ T.G.Adj a b) (c0 : ℕ) (hρp : ∀ (v : D), T.par (ρ v) = T.par v + ↑↑c0) : T.ZVert → T.ZVert

The deck generator on vertices.

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.OrientedTree.gPow {D : Type u_1} (T : OrientedTree D) (ρ : D ≃ D) (hρ : ∀ (a b : D), T.G.Adj (ρ a) (ρ b) ↔ T.G.Adj a b) (c0 : ℕ) (hρp : ∀ (v : D), T.par (ρ v) = T.par v + ↑↑c0) (n : ℕ) : T.ZVert ⥤q T.ZVert

The deck transformation g^n in height form.

theorem MultiplicativeBasisDeformations.OrientedTree.gV_iter {D : Type u_1} (T : OrientedTree D) (ρ : D ≃ D) (hρ : ∀ (a b : D), T.G.Adj (ρ a) (ρ b) ↔ T.G.Adj a b) (c0 : ℕ) (hρp : ∀ (v : D), T.par (ρ v) = T.par v + ↑↑c0) (n : ℕ) (X : T.ZVert) : ((T.gV ρ hρ c0 hρp)^[n] X).v = (ρ ^ n) X.v ∧ ((T.gV ρ hρ c0 hρp)^[n] X).t = X.t + ↑n * ↑c0

theorem MultiplicativeBasisDeformations.OrientedTree.gPow_obj {D : Type u_1} (T : OrientedTree D) (ρ : D ≃ D) (hρ : ∀ (a b : D), T.G.Adj (ρ a) (ρ b) ↔ T.G.Adj a b) (c0 : ℕ) (hρp : ∀ (v : D), T.par (ρ v) = T.par v + ↑↑c0) (n : ℕ) (Z : T.ZVert) : (T.gPow ρ hρ c0 hρp n).obj Z = (T.gV ρ hρ c0 hρp)^[n] Z

theorem MultiplicativeBasisDeformations.OrientedTree.gPow_deck {D : Type u_1} (T : OrientedTree D) {V : Type v'} [Quiver V] [∀ (x y : V), Subsingleton (x ⟶ y)] (π : T.ZVert ⥤q V) [(x : V) → Fintype ((y : V) × (y ⟶ x))] [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] (ρ : D ≃ D) (hρ : ∀ (a b : D), T.G.Adj (ρ a) (ρ b) ↔ T.G.Adj a b) (c0 : ℕ) (hρp : ∀ (v : D), T.par (ρ v) = T.par v + ↑↑c0) (hdeck : ∀ (Z : T.ZVert), π.obj ((T.zAct ρ hρ (↑c0) hρp).obj Z) = π.obj Z) (n : ℕ) (Z : T.ZVert) : π.obj ((T.gPow ρ hρ c0 hρp n).obj Z) = π.obj Z

theorem MultiplicativeBasisDeformations.OrientedTree.gPow_fib {D : Type u_1} (T : OrientedTree D) {V : Type v'} [Quiver V] [∀ (x y : V), Subsingleton (x ⟶ y)] (π : T.ZVert ⥤q V) [(x : V) → Fintype ((y : V) × (y ⟶ x))] [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] (ρ : D ≃ D) (hρ : ∀ (a b : D), T.G.Adj (ρ a) (ρ b) ↔ T.G.Adj a b) (c0 : ℕ) (hρp : ∀ (v : D), T.par (ρ v) = T.par v + ↑↑c0) (hfib : ∀ (X Y : T.ZVert), π.obj X = π.obj Y → ∃ (n : ℕ), Y = (T.gV ρ hρ c0 hρp)^[n] X ∨ X = (T.gV ρ hρ c0 hρp)^[n] Y) (hc0 : 0 < c0) (n : ℕ) (X E : T.ZVert) (h1 : π.obj E = π.obj X) (h2 : E.t = X.t + ↑(n * c0)) : E = (T.gPow ρ hρ c0 hρp n).obj X

theorem MultiplicativeBasisDeformations.OrientedTree.row_lift {D : Type u_1} (T : OrientedTree D) {V : Type v'} [Quiver V] [∀ (x y : V), Subsingleton (x ⟶ y)] {Q : TranslationQuiver V} (hQ : Q.IsStable) (π : T.ZVert ⥤q V) {k : Type u} [Field 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] (ρ : D ≃ D) (hρ : ∀ (a b : D), T.G.Adj (ρ a) (ρ b) ↔ T.G.Adj a b) (c0 : ℕ) (hρp : ∀ (v : D), T.par (ρ v) = T.par v + ↑↑c0) (hfib : ∀ (X Y : T.ZVert), π.obj X = π.obj Y → ∃ (n : ℕ), Y = (T.gV ρ hρ c0 hρp)^[n] X ∨ X = (T.gV ρ hρ c0 hρp)^[n] Y) [Fintype D] [DecidableEq D] (hπ : π.IsCovering) (hτ : ∀ (Y : T.ZVert), π.obj (T.ztau Y) = hQ.tauE (π.obj Y)) (hsurj : ∀ (x : V), ∃ (X : T.ZVert), π.obj X = x) (hc0 : 0 < c0) {m : ℕ} (hm : 1 ≤ m) (x : ↑Q.nonprojective) (p : Quiver.Path ↑(Q.tau x) ↑x) (hp : p.length = m + 1) : ∃ (n : ℕ) (X : T.ZVert) (P : Quiver.Path (T.ztau X) ((T.gPow ρ hρ c0 hρp n).obj X)), ↑(n * c0) = ↑m - 1 ∧ P.length = m + 1 ∧ ScalarMeshCategory.rowClass c m x p = T.rowZ hQ π c m P

Lemma A.2(1): a row of length m + 1 ≥ 2 lifts to a path from τ X to g^n X with n c₀ = m − 1; in particular rows, hence nonzero cokernel classes, occur only in these degrees.

(2) The twisted trace surjection

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.OrientedTree.TwPaths {D : Type u_1} (T : OrientedTree D) {k : Type u} [Field k] (σ : D ≃ D) (hσ : ∀ (a b : D), T.G.Adj (σ a) (σ b) ↔ T.G.Adj a b) : Type (max u_1 u u_1)

⊕_x kΔ̄(x, σ x).

noncomputable def MultiplicativeBasisDeformations.OrientedTree.tsingle {D : Type u_1} (T : OrientedTree D) {k : Type u} [Field k] [DecidableEq D] (σ : D ≃ D) (hσ : ∀ (a b : D), T.G.Adj (σ a) (σ b) ↔ T.G.Adj a b) (x : D) (g : LinearPaths.obj (T.toDbl x) ⟶ LinearPaths.obj ((T.dAct σ hσ).obj (T.toDbl x))) : T.TwPaths σ hσ

The component at x.

theorem MultiplicativeBasisDeformations.OrientedTree.tsingle_apply_same {D : Type u_1} (T : OrientedTree D) {k : Type u} [Field k] [Fintype D] [DecidableEq D] [DecidableRel T.orient] (σ : D ≃ D) (hσ : ∀ (a b : D), T.G.Adj (σ a) (σ b) ↔ T.G.Adj a b) (x : D) (g : LinearPaths.obj (T.toDbl x) ⟶ LinearPaths.obj ((T.dAct σ hσ).obj (T.toDbl x))) : T.tsingle σ hσ x g x = g

theorem MultiplicativeBasisDeformations.OrientedTree.tsingle_apply_ne {D : Type u_1} (T : OrientedTree D) {k : Type u} [Field k] [Fintype D] [DecidableEq D] [DecidableRel T.orient] (σ : D ≃ D) (hσ : ∀ (a b : D), T.G.Adj (σ a) (σ b) ↔ T.G.Adj a b) {x x' : D} (h : x' ≠ x) (g : LinearPaths.obj (T.toDbl x) ⟶ LinearPaths.obj ((T.dAct σ hσ).obj (T.toDbl x))) : T.tsingle σ hσ x g x' = 0

noncomputable def MultiplicativeBasisDeformations.OrientedTree.twRel {D : Type u_1} (T : OrientedTree D) {k : Type u} [Field k] [Fintype D] [DecidableEq D] [DecidableRel T.orient] (σ : D ≃ D) (hσ : ∀ (a b : D), T.G.Adj (σ a) (σ b) ↔ T.G.Adj a b) (d : ℕ) : Submodule k (T.TwPaths σ hσ)

The relations of the twisted trace space in degree d: the ideal of Π(Δ), the twisted rotations uv − v σ(u), and the other degrees.

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.OrientedTree.TwTrace {D : Type u_1} (T : OrientedTree D) {k : Type u} [Field k] [Fintype D] [DecidableEq D] [DecidableRel T.orient] (σ : D ≃ D) (hσ : ∀ (a b : D), T.G.Adj (σ a) (σ b) ↔ T.G.Adj a b) (d : ℕ) : Type (max (max u_1 u) u u_1)

The twisted trace space T_σ(Π)_d of eq:twisted-trace-space.

def MultiplicativeBasisDeformations.OrientedTree.X0 {D : Type u_1} (T : OrientedTree D) (x : D) : T.ZVert

A base point of height of the parity of x.

noncomputable def MultiplicativeBasisDeformations.OrientedTree.twMapF {D : Type u_1} (T : OrientedTree D) {V : Type v'} [Quiver V] {Q : TranslationQuiver V} (hQ : Q.IsStable) (π : T.ZVert ⥤q V) {k : Type u} [Field k] [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) [DecidableEq V] [Fintype D] (σ : D ≃ D) (hσ : ∀ (a b : D), T.G.Adj (σ a) (σ b) ↔ T.G.Adj a b) (m : ℕ) : T.TwPaths σ hσ →ₗ[k] ScalarMeshCategory.Coker c m

Lifting the degree-(m+1) components from the base points.

theorem MultiplicativeBasisDeformations.OrientedTree.twMapF_single {D : Type u_1} (T : OrientedTree D) {V : Type v'} [Quiver V] [∀ (x y : V), Subsingleton (x ⟶ y)] {Q : TranslationQuiver V} (hQ : Q.IsStable) (π : T.ZVert ⥤q V) {k : Type u} [Field 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] [Fintype D] [DecidableEq D] [DecidableRel T.orient] (σ : D ≃ D) (hσ : ∀ (a b : D), T.G.Adj (σ a) (σ b) ↔ T.G.Adj a b) (m : ℕ) (x : D) (g : LinearPaths.obj (T.toDbl x) ⟶ LinearPaths.obj ((T.dAct σ hσ).obj (T.toDbl x))) : (T.twMapF hQ π c σ hσ m) (T.tsingle σ hσ x g) = (T.phiL hQ π c m (T.X0 x) ((T.dAct σ hσ).obj (T.toDbl x))) ((LinearPaths.proj (m + 1) (T.toDbl (T.X0 x).v) ((T.dAct σ hσ).obj (T.toDbl x))) g)

theorem MultiplicativeBasisDeformations.OrientedTree.proj_mem_ideal {D : Type u_1} (T : OrientedTree D) {k : Type u} [Field k] [Fintype D] [DecidableEq D] [DecidableRel T.orient] (e : ℕ) {a b : T.Dbl} {g : LinearPaths.obj a ⟶ LinearPaths.obj b} (hg : g ∈ (T.preproj k).ideal (LinearPaths.obj a) (LinearPaths.obj b)) : (LinearPaths.proj e a b) g ∈ (T.preproj k).ideal (LinearPaths.obj a) (LinearPaths.obj b)

@[reducible, inline]

noncomputable abbrev MultiplicativeBasisDeformations.OrientedTree.cokerDeg' {V : Type v'} [Quiver V] {Q : TranslationQuiver V} {k : Type u} [Field k] [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) (m : ℕ) : Submodule k (ScalarMeshCategory.Coker c m)

The degree-(m+1) cokernel of D_m, inside Coker c m.

theorem MultiplicativeBasisDeformations.OrientedTree.rowQ_mem {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) [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] [DecidablePred fun (x : V) => x ∈ Q.nonprojective] [Fintype V] [DecidablePred fun (x : V) => x ∈ Q.periodic] [Fintype ↑Q.nonprojective] (m : ℕ) {u y : V} (w : Quiver.Path u y) (hw : w.length = m + 1) : ScalarMeshCategory.rowQ c hQ m w ∈ cokerDeg' c m

theorem MultiplicativeBasisDeformations.OrientedTree.phiL_mem {D : Type u_1} (T : OrientedTree D) {V : Type v'} [Quiver V] [∀ (x y : V), Subsingleton (x ⟶ y)] {Q : TranslationQuiver V} (hQ : Q.IsStable) (π : T.ZVert ⥤q V) {k : Type u} [Field 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] [Fintype D] [DecidableEq D] [DecidableRel T.orient] [Fintype V] [DecidablePred fun (x : V) => x ∈ Q.periodic] [Fintype ↑Q.nonprojective] (m : ℕ) (X : T.ZVert) (b : T.Dbl) {g : LinearPaths.obj (T.toDbl X.v) ⟶ LinearPaths.obj b} (hg : g ∈ LinearPaths.degreePart (m + 1) (T.toDbl X.v) b) : (T.phiL hQ π c m X b) g ∈ cokerDeg' c m

theorem MultiplicativeBasisDeformations.OrientedTree.twRel_le_ker {D : Type u_1} (T : OrientedTree D) {V : Type v'} [Quiver V] [∀ (x y : V), Subsingleton (x ⟶ y)] {Q : TranslationQuiver V} (hQ : Q.IsStable) (π : T.ZVert ⥤q V) {k : Type u} [Field 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] [Fintype D] [DecidableEq D] [DecidableRel T.orient] (σ : D ≃ D) (hσ : ∀ (a b : D), T.G.Adj (σ a) (σ b) ↔ T.G.Adj a b) [Fintype V] [DecidablePred fun (x : V) => x ∈ Q.periodic] [Fintype ↑Q.nonprojective] (hπ : π.IsCovering) (hτ : ∀ (Y : T.ZVert), π.obj (T.ztau Y) = hQ.tauE (π.obj Y)) (hsig : T.pullCoeff hQ π c = T.zSigned k) (hc : ScalarMeshCategory.OppositeOnMates c hQ) (s : ℤ) (hσp : ∀ (v : D), T.par (σ v) = T.par v + ↑s) (hdeck : ∀ (Z : T.ZVert), π.obj ((T.zAct σ hσ s hσp).obj Z) = π.obj Z) {m : ℕ} (hs : ↑m + 1 = 2 + s) : T.twRel σ hσ (m + 1) ≤ (T.twMapF hQ π c σ hσ m).ker

The relations of T_σ(Π)_{m+1} have zero row classes: the ideal of Π(Δ) lifts term by term, twisted rotation is phiD_rotate_path, and the height does not matter (phiD_height).

noncomputable def MultiplicativeBasisDeformations.OrientedTree.twMap {D : Type u_1} (T : OrientedTree D) {V : Type v'} [Quiver V] [∀ (x y : V), Subsingleton (x ⟶ y)] {Q : TranslationQuiver V} (hQ : Q.IsStable) (π : T.ZVert ⥤q V) {k : Type u} [Field 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] [Fintype D] [DecidableEq D] [DecidableRel T.orient] (σ : D ≃ D) (hσ : ∀ (a b : D), T.G.Adj (σ a) (σ b) ↔ T.G.Adj a b) [Fintype V] [DecidablePred fun (x : V) => x ∈ Q.periodic] [Fintype ↑Q.nonprojective] (hπ : π.IsCovering) (hτ : ∀ (Y : T.ZVert), π.obj (T.ztau Y) = hQ.tauE (π.obj Y)) (hsig : T.pullCoeff hQ π c = T.zSigned k) (hc : ScalarMeshCategory.OppositeOnMates c hQ) (s : ℤ) (hσp : ∀ (v : D), T.par (σ v) = T.par v + ↑s) (hdeck : ∀ (Z : T.ZVert), π.obj ((T.zAct σ hσ s hσp).obj Z) = π.obj Z) {m : ℕ} (hs : ↑m + 1 = 2 + s) : T.TwTrace σ hσ (m + 1) →ₗ[k] ScalarMeshCategory.Coker c m

The twisted trace map T_σ(Π)_{m+1} → coker D_m.

theorem MultiplicativeBasisDeformations.OrientedTree.twistedTraceSurjection {D : Type u_1} (T : OrientedTree D) {V : Type v'} [Quiver V] [∀ (x y : V), Subsingleton (x ⟶ y)] {Q : TranslationQuiver V} (hQ : Q.IsStable) (π : T.ZVert ⥤q V) {k : Type u} [Field 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] [Fintype D] [DecidableEq D] [DecidableRel T.orient] (σ : D ≃ D) (hσ : ∀ (a b : D), T.G.Adj (σ a) (σ b) ↔ T.G.Adj a b) [Fintype V] [DecidablePred fun (x : V) => x ∈ Q.periodic] [Fintype ↑Q.nonprojective] (hπ : π.IsCovering) (hτ : ∀ (Y : T.ZVert), π.obj (T.ztau Y) = hQ.tauE (π.obj Y)) (hsig : T.pullCoeff hQ π c = T.zSigned k) (hc : ScalarMeshCategory.OppositeOnMates c hQ) (s : ℤ) (hσp : ∀ (v : D), T.par (σ v) = T.par v + ↑s) (hdeck : ∀ (Z : T.ZVert), π.obj ((T.zAct σ hσ s hσp).obj Z) = π.obj Z) (hsurj : ∀ (x : V), ∃ (X : T.ZVert), π.obj X = x) (hfib : ∀ (X E : T.ZVert), π.obj E = π.obj X → E.t = X.t + s → E = (T.zAct σ hσ s hσp).obj X) {m : ℕ} (hs : ↑m + 1 = 2 + s) : (T.twMap hQ π c σ hσ hπ hτ hsig hc s hσp hdeck hs).range = cokerDeg' c m

Lemma A.2(2) (lem:twisted-trace-surjection), for an arbitrary finite tree Δ: for the twist σ with height shift s (m + 1 = 2 + s, so the degree is d = m + 1), when the lifts of rows from τ X end at σ-translates (hfib), the twisted trace map is a surjection T_σ(Π)_d → coker D_{d−1}: its range is the degree-d cokernel.

The allowed degrees

theorem MultiplicativeBasisDeformations.OrientedTree.twistedTraceSurjection_deck {D : Type u_1} (T : OrientedTree D) {V : Type v'} [Quiver V] [∀ (x y : V), Subsingleton (x ⟶ y)] {Q : TranslationQuiver V} (hQ : Q.IsStable) (π : T.ZVert ⥤q V) {k : Type u} [Field 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] [Fintype D] [DecidableEq D] [DecidableRel T.orient] [Fintype V] [DecidablePred fun (x : V) => x ∈ Q.periodic] [Fintype ↑Q.nonprojective] (ρ : D ≃ D) (hρ : ∀ (a b : D), T.G.Adj (ρ a) (ρ b) ↔ T.G.Adj a b) (c0 : ℕ) (hc0 : 0 < c0) (hρp : ∀ (v : D), T.par (ρ v) = T.par v + ↑↑c0) (hdeck : ∀ (Z : T.ZVert), π.obj ((T.zAct ρ hρ (↑c0) hρp).obj Z) = π.obj Z) (hfib : ∀ (X Y : T.ZVert), π.obj X = π.obj Y → ∃ (n : ℕ), Y = (T.gV ρ hρ c0 hρp)^[n] X ∨ X = (T.gV ρ hρ c0 hρp)^[n] Y) (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) (hc : ScalarMeshCategory.OppositeOnMates c hQ) {m n : ℕ} (hn : ↑(n * c0) = ↑m - 1) : (T.twMap hQ π c (ρ ^ n) ⋯ hπ hτ hsig hc ↑(n * c0) ⋯ ⋯ ⋯).range = cokerDeg' c m

Lemma A.2(2) in an allowed degree: if n c₀ = m − 1, the twisted trace map for the twist θ = ρ^n is onto the degree-(m+1) cokernel.