Cokernels on a periodic star model spanned by one row (Appendix B)

characteristic-two-mesh-calculations.tex: "We will show that each periodic component contributes at most one correction line, represented by a single path." On a periodic star model, the twisted-trace surjection of Lemma A.2 (rowClass_mem_span) sends words at the centre onto the row classes. If every twisted trace of a word in an allowed degree is an integer multiple of the trace of one word W₀, then all cokernel classes are multiples of the class of the row given by W₀ at the centre (star_span_deg). This is the analogue of star_surjective_deg with a spanning word instead of vanishing traces.

def MultiplicativeBasisDeformations.StarTrace.X₀ {t : ℕ} {L : Fin t → ℕ} : (starTree L).ZVert

The centre of the star at height zero.

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.StarTrace.liftW {t : ℕ} {L : Fin t → ℕ} (W : List (Fin t)) : Quiver.Path ((starTree L).ztau X₀) ((starTree L).liftEnd ((starTree L).ztau X₀) (StarCorner.wordP W))

The lift of the word W at the centre, from τ X₀.

def MultiplicativeBasisDeformations.StarTrace.candRow {t : ℕ} {L : Fin t → ℕ} {V : Type v'} [Quiver V] {Q : TranslationQuiver V} (hQ : Q.IsStable) (π : (starTree L).ZVert ⥤q V) (W : List (Fin t)) : ScalarMeshCategory.RowSet Q

The candidate row of a word: the image of its lift, when it is a row.

theorem MultiplicativeBasisDeformations.StarTrace.candRow_subsingleton {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] (W : List (Fin t)) : Set.Subsingleton (candRow hQ π W)

theorem MultiplicativeBasisDeformations.StarTrace.candRow_length {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] (W : List (Fin t)) (R : (x : ↑Q.nonprojective) × Quiver.Path ↑(Q.tau x) ↑x) : R ∈ candRow hQ π W → R.snd.length = 2 * W.length

theorem MultiplicativeBasisDeformations.StarTrace.rowZ_liftW_mem {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) (m : ℕ) (W : List (Fin t)) (hW : 2 * W.length = m + 1) : (starTree L).rowZ hQ π c m (liftW W) ∈ ScalarMeshCategory.rowSpan c m (candRow hQ π W)

theorem MultiplicativeBasisDeformations.StarTrace.liftZ_cast_pathStar {t : ℕ} {L : Fin t → ℕ} (Y : (starTree L).ZVert) {b b' : (starTree L).Dbl} (p : Quiver.Path ((starTree L).toDbl Y.v) b) (e : b = b') : ⟨(starTree L).liftEnd Y (Quiver.Path.cast ⋯ e p), (starTree L).liftZ Y (Quiver.Path.cast ⋯ e p)⟩ = ⟨(starTree L).liftEnd Y p, (starTree L).liftZ Y p⟩

theorem MultiplicativeBasisDeformations.StarTrace.wordTr_mem {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)) : wordTr hQ π c σ hσ m hσo W ∈ ScalarMeshCategory.rowSpan c m (candRow hQ π W)

theorem MultiplicativeBasisDeformations.StarTrace.star_span_deg {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) (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)) (hspan : ∀ (M : Type (max u v' w)) [inst : AddCommGroup M] [Module k M] (D : TraceAlg.TraceData L M) (n : ℕ), D.θ = θ ^ n → ∀ (w : List (Fin t)), 2 ≤ w.length → 2 * w.length = 2 + n * c0 → ∃ (z : ℤ), D.tr w = z • D.tr W₀) : ScalarMeshCategory.CokerSpan c (candRow hQ π W₀)

On a periodic star model, the cokernels are spanned by the row of one word, when every twisted trace of a word in an allowed degree is a multiple of the trace of that word.