Rotation of rows with signed coefficients

Proof of Lemma A.2 (lem:twisted-trace-surjection, periodic-mesh-calculations.tex): "In the signed meshes an arrow correction identifies a row path wa with (τa)w, with coefficient one. Indeed, the correction column gives c[wa] + c'[(τa)w] = 0, where c, c' are the two mesh coefficients of the corresponding tree edge, and these are opposite."

Here the cokernel of D_m is the quotient MeshFamily c ⧸ imageD c m, and the coefficients are opposite on mates: c_{y, σ a} = - c_{x, a} for a : y → x.

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.ScalarMeshCategory.Coker {k : Type u} [CommRing k] {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) (m : ℕ) : Type (max (max (max w v) u) (max u v) w)

The cokernel of D_m.

noncomputable def MultiplicativeBasisDeformations.ScalarMeshCategory.rowClass {k : Type u} [CommRing k] {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) [DecidableEq V] (m : ℕ) (x : ↑Q.nonprojective) (w : Quiver.Path ↑(Q.tau x) ↑x) : Coker c m

The class of a row in the cokernel.

def MultiplicativeBasisDeformations.ScalarMeshCategory.OppositeOnMates {k : Type u} [CommRing k] {V : Type v} [Quiver V] {Q : TranslationQuiver V} (c : MeshCoefficients k Q) (hQ : Q.IsStable) : Prop

Coefficients opposite on mates.

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.rowClass_rotate {k : Type u} [CommRing k] {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(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] (hQ : Q.IsStable) (hc : OppositeOnMates c hQ) {m : ℕ} (x : ↑Q.nonprojective) {y : V} (a : y ⟶ ↑x) (q : Quiver.Path (↑(Q.tau x)) y) (hq : q.length = m) : rowClass c m x (q.cons a) = rowClass c m ⟨y, ⋯⟩ (((Q.mate ⟨y, ⋯⟩ ↑(Q.tau x)) ((Q.mate x y) a)).toPath.comp q)

Rotation: with coefficients opposite on mates, a row (x, q a) has the class of its rotation (y, (σσ a) q).

noncomputable def MultiplicativeBasisDeformations.ScalarMeshCategory.rowQ {k : Type u} [CommRing k] {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) [DecidableEq V] (hQ : Q.IsStable) (m : ℕ) {u y : V} (w : Quiver.Path u y) : Coker c m

The class of an arbitrary path in the cokernel: the row class of w if it runs from τ y to y, and zero otherwise. Its endpoints are free, so it is insensitive to casts.

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.rowQ_cast {k : Type u} [CommRing k] {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(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] (hQ : Q.IsStable) (m : ℕ) {u y u' y' : V} (hu : u = u') (hy : y = y') (w : Quiver.Path u y) : rowQ c hQ m (Quiver.Path.cast hu hy w) = rowQ c hQ m w

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.rowQ_eq {k : Type u} [CommRing k] {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(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] (hQ : Q.IsStable) (m : ℕ) {y : V} (w : Quiver.Path (hQ.tauE y) y) : rowQ c hQ m w = rowClass c m ⟨y, ⋯⟩ w

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.rowQ_rotate {k : Type u} [CommRing k] {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(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] (hQ : Q.IsStable) [∀ (x y : V), Subsingleton (x ⟶ y)] (hc : OppositeOnMates c hQ) {m : ℕ} {x y : V} (a : y ⟶ x) (b : hQ.tauE y ⟶ hQ.tauE x) (q : Quiver.Path (hQ.tauE x) y) (hq : q.length = m) : rowQ c hQ m (b.toPath.comp q) = rowQ c hQ m (q.cons a)

Rotation of rows, with free endpoints: for a : y → x and b : τ y → τ x, the row b q at y and the row q a at x have the same class (coefficients opposite on mates).

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.rowQ_eq_mk {k : Type u} [CommRing k] {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(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] (hQ : Q.IsStable) (m : ℕ) {y : V} (w : Quiver.Path (hQ.tauE y) y) : rowQ c hQ m w = Submodule.Quotient.mk (Pi.single ⟨y, ⋯⟩ (pathMor c w))

The row class of a path as a linear function of its image in C(Q, c).