The scalar-weight group W(P) of A₀ (Definition 7.1, Proposition 7.2)

weights-and-parameters.tex. For a finite ray category Q, W(Q) = ℤ⟨[r] : r ≠ 0, 1⟩ / ⟨[rs] − [r] − [s] : rs ≠ 0⟩ (def:scalar-weight-group). For P = ray A₀ we use the deck-homogeneous pieces of A₀ as the nonzero rays (Proposition 4.14: each homogeneous ray line lies in one deck degree and the products of the normed basis are the ray products): generators [x, y, g] for the nonzero pieces A₀(x, y)_g, relations [x, z, gh] = [x, y, g] + [y, z, h] when a product of the two pieces is nonzero (WP).

"Every additive weight on L, with values in any abelian group, is a difference of object values" (Proposition 7.2(2), L_addWeight_eq_diff), from the generic cov_addWeight_eq_diff and Lemma 4.13 (ratio_hyp). For Proposition 7.2(1) see Ψ, Φ below.

Deviation in Proposition 7.2(1): the deck group of the formalization is the fundamental group of the coned complex (DeckGrading.lean), so the lifted projective category need not be connected. We use the stabilizer H of the component of a base object in place of G = π₁(K); for connected A the paper's argument then gives W(P) ≅ ℤ^{n−1} ⊕ H_ab (Φ ∘ Ψ = 1). Its freeness, needed later, follows: W(P) is finitely generated and embeds in a torsion-free group.

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.MeshWalk.LObj {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] (Q : TranslationQuiver V) [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) (v₀ : V) {L : CatAlg.LocalFamily (meshFam Q c)} (D : CatAlg.MeshData (meshFam Q c) L) : Type

The lifted projective category L.

theorem MultiplicativeBasisDeformations.MeshWalk.ratio_add {k : Type u} [Field k] [IsAlgClosed k] [Infinite k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients k Q} {v₀ : V} [hone : ∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] {L : CatAlg.LocalFamily (meshFam Q c)} {D : CatAlg.MeshData (meshFam Q c) L} [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] (hF : IsRepresentationFinite k (CatAlg.Alg D.F0)ᵐᵒᵖ) (w' : LObj Q c v₀ D → LObj Q c v₀ D → Additive kˣ) (hw : Thin.IsAddWeight Set.univ w') : ∃ (ζ : LObj Q c v₀ D → Additive kˣ), ∀ (o o' : LObj Q c v₀ D), Thin.Line o o' → w' o o' = ζ o' - ζ o

Lemma 4.13, additively: an Additive kˣ-valued weight on L is a difference of object values.

theorem MultiplicativeBasisDeformations.MeshWalk.L_addWeight_eq_diff {k : Type u} [Field k] [IsAlgClosed k] [Infinite k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients k Q} {v₀ : V} [hone : ∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] {L : CatAlg.LocalFamily (meshFam Q c)} {D : CatAlg.MeshData (meshFam Q c) L} [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] (hF : IsRepresentationFinite k (CatAlg.Alg D.F0)ᵐᵒᵖ) {M : Type z} [AddCommGroup M] (w' : LObj Q c v₀ D → LObj Q c v₀ D → M) (hw : Thin.IsAddWeight Set.univ w') : ∃ (ζ : LObj Q c v₀ D → M), ∀ (o o' : LObj Q c v₀ D), Thin.Line o o' → w' o o' = ζ o' - ζ o

Proposition 7.2(2) (prop:integral-ray-weights) for A₀: every additive weight on L, with values in any abelian group, is a difference of object values.

The group W(P)

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.MeshWalk.Piece {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] (Q : TranslationQuiver V) [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) (v₀ : V) {L : CatAlg.LocalFamily (meshFam Q c)} (D : CatAlg.MeshData (meshFam Q c) L) : Type

A deck piece A₀(x, y)_g.

def MultiplicativeBasisDeformations.MeshWalk.NZ {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] (Q : TranslationQuiver V) [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) (v₀ : V) {L : CatAlg.LocalFamily (meshFam Q c)} (D : CatAlg.MeshData (meshFam Q c) L) (t : Piece Q c v₀ D) : Prop

A nonzero piece, that is, a nonzero ray of P.

noncomputable def MultiplicativeBasisDeformations.MeshWalk.relW {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] (Q : TranslationQuiver V) [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) (v₀ : V) {L : CatAlg.LocalFamily (meshFam Q c)} (D : CatAlg.MeshData (meshFam Q c) L) : AddSubgroup (Piece Q c v₀ D →₀ ℤ)

The relations of W(P).

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.MeshWalk.WP {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] (Q : TranslationQuiver V) [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) (v₀ : V) {L : CatAlg.LocalFamily (meshFam Q c)} (D : CatAlg.MeshData (meshFam Q c) L) : Type

The scalar-weight group W(P) (Definition 7.1).

noncomputable def MultiplicativeBasisDeformations.MeshWalk.cls {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] (Q : TranslationQuiver V) [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) (v₀ : V) {L : CatAlg.LocalFamily (meshFam Q c)} (D : CatAlg.MeshData (meshFam Q c) L) (t : Piece Q c v₀ D) : WP Q c v₀ D

The class [r] of a ray.

theorem MultiplicativeBasisDeformations.MeshWalk.grp_cancel {G : Type u_1} [Group G] (a b d : G) : a⁻¹ * b * (b⁻¹ * d) = a⁻¹ * d

theorem MultiplicativeBasisDeformations.MeshWalk.grp_shift {G : Type u_1} [Group G] (g a b : G) : (g * a)⁻¹ * (g * b) = a⁻¹ * b

theorem MultiplicativeBasisDeformations.MeshWalk.deck_cancel {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {v₀ : V} [hone : ∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] (a b d : Deck Q v₀) : a⁻¹ * b * (b⁻¹ * d) = a⁻¹ * d

theorem MultiplicativeBasisDeformations.MeshWalk.deck_shift {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {v₀ : V} [hone : ∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] (g a b : Deck Q v₀) : (g * a)⁻¹ * (g * b) = a⁻¹ * b

theorem MultiplicativeBasisDeformations.MeshWalk.cls_mul {k : Type u} [Field k] [IsAlgClosed k] [Infinite k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients k Q} {v₀ : V} [hone : ∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] {L : CatAlg.LocalFamily (meshFam Q c)} {D : CatAlg.MeshData (meshFam Q c) L} [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] {x y z : D.PV} {g h : Deck Q v₀} {f : D.F0 x ⟶ D.F0 y} {f' : D.F0 y ⟶ D.F0 z} (hf : f ∈ (D0 Q c v₀ D).part g x y) (hf' : f' ∈ (D0 Q c v₀ D).part h y z) (hff : CategoryTheory.CategoryStruct.comp f f' ≠ 0) : cls Q c v₀ D (x, z, g * h) = cls Q c v₀ D (x, y, g) + cls Q c v₀ D (y, z, h)

theorem MultiplicativeBasisDeformations.MeshWalk.cls_of_not_nz {k : Type u} [Field k] [IsAlgClosed k] [Infinite k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients k Q} {v₀ : V} [hone : ∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] {L : CatAlg.LocalFamily (meshFam Q c)} {D : CatAlg.MeshData (meshFam Q c) L} [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] {t : Piece Q c v₀ D} (ht : ¬NZ Q c v₀ D t) : cls Q c v₀ D t = 0

The tautological weight on L and its object values

noncomputable def MultiplicativeBasisDeformations.MeshWalk.wtL {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] (Q : TranslationQuiver V) [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) (v₀ : V) {L : CatAlg.LocalFamily (meshFam Q c)} (D : CatAlg.MeshData (meshFam Q c) L) (o o' : LObj Q c v₀ D) : WP Q c v₀ D

The weight of a line of L: the class of its ray.

theorem MultiplicativeBasisDeformations.MeshWalk.wtL_isAddWeight {k : Type u} [Field k] [IsAlgClosed k] [Infinite k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients k Q} {v₀ : V} [hone : ∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] {L : CatAlg.LocalFamily (meshFam Q c)} {D : CatAlg.MeshData (meshFam Q c) L} [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] : Thin.IsAddWeight Set.univ (wtL Q c v₀ D)

theorem MultiplicativeBasisDeformations.MeshWalk.exists_zetaW {k : Type u} [Field k] [IsAlgClosed k] [Infinite k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients k Q} {v₀ : V} [hone : ∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] {L : CatAlg.LocalFamily (meshFam Q c)} {D : CatAlg.MeshData (meshFam Q c) L} [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] (hF : IsRepresentationFinite k (CatAlg.Alg D.F0)ᵐᵒᵖ) : ∃ (ζ : LObj Q c v₀ D → WP Q c v₀ D), ∀ (o o' : LObj Q c v₀ D), Thin.Line o o' → wtL Q c v₀ D o o' = ζ o' - ζ o

def MultiplicativeBasisDeformations.MeshWalk.gL {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] (Q : TranslationQuiver V) [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) (v₀ : V) {L : CatAlg.LocalFamily (meshFam Q c)} (D : CatAlg.MeshData (meshFam Q c) L) (g : Deck Q v₀) (o : LObj Q c v₀ D) : LObj Q c v₀ D

The deck action on L.

theorem MultiplicativeBasisDeformations.MeshWalk.gL_mul {k : Type u} [Field k] [IsAlgClosed k] [Infinite k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients k Q} {v₀ : V} [hone : ∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] {L : CatAlg.LocalFamily (meshFam Q c)} {D : CatAlg.MeshData (meshFam Q c) L} [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] (g h : Deck Q v₀) (o : LObj Q c v₀ D) : gL Q c v₀ D (g * h) o = gL Q c v₀ D g (gL Q c v₀ D h o)

theorem MultiplicativeBasisDeformations.MeshWalk.line_gL {k : Type u} [Field k] [IsAlgClosed k] [Infinite k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients k Q} {v₀ : V} [hone : ∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] {L : CatAlg.LocalFamily (meshFam Q c)} {D : CatAlg.MeshData (meshFam Q c) L} [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] {o o' : LObj Q c v₀ D} (g : Deck Q v₀) (h : Thin.Line o o') : Thin.Line (gL Q c v₀ D g o) (gL Q c v₀ D g o')

theorem MultiplicativeBasisDeformations.MeshWalk.wtL_gL {k : Type u} [Field k] [IsAlgClosed k] [Infinite k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients k Q} {v₀ : V} [hone : ∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] {L : CatAlg.LocalFamily (meshFam Q c)} {D : CatAlg.MeshData (meshFam Q c) L} [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] (g : Deck Q v₀) (o o' : LObj Q c v₀ D) : wtL Q c v₀ D (gL Q c v₀ D g o) (gL Q c v₀ D g o') = wtL Q c v₀ D o o'

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.MeshWalk.mkL {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] (Q : TranslationQuiver V) [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) (v₀ : V) {L : CatAlg.LocalFamily (meshFam Q c)} (D : CatAlg.MeshData (meshFam Q c) L) (x : D.PV) (a : Deck Q v₀) : LObj Q c v₀ D

An object of L.

def MultiplicativeBasisDeformations.MeshWalk.conn {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] (Q : TranslationQuiver V) [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) (v₀ : V) {L : CatAlg.LocalFamily (meshFam Q c)} (D : CatAlg.MeshData (meshFam Q c) L) (o o' : LObj Q c v₀ D) : Prop

Connectedness in L.

theorem MultiplicativeBasisDeformations.MeshWalk.conn_gL {k : Type u} [Field k] [IsAlgClosed k] [Infinite k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients k Q} {v₀ : V} [hone : ∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] {L : CatAlg.LocalFamily (meshFam Q c)} {D : CatAlg.MeshData (meshFam Q c) L} [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] {o o' : LObj Q c v₀ D} (g : Deck Q v₀) (h : conn Q c v₀ D o o') : conn Q c v₀ D (gL Q c v₀ D g o) (gL Q c v₀ D g o')

theorem MultiplicativeBasisDeformations.MeshWalk.zeta_shift {k : Type u} [Field k] [IsAlgClosed k] [Infinite k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients k Q} {v₀ : V} [hone : ∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] {L : CatAlg.LocalFamily (meshFam Q c)} {D : CatAlg.MeshData (meshFam Q c) L} [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] {ζ : LObj Q c v₀ D → WP Q c v₀ D} (hζ : ∀ (o o' : LObj Q c v₀ D), Thin.Line o o' → wtL Q c v₀ D o o' = ζ o' - ζ o) (g : Deck Q v₀) {o o' : LObj Q c v₀ D} (h : conn Q c v₀ D o o') : ζ (gL Q c v₀ D g o') - ζ (gL Q c v₀ D g o) = ζ o' - ζ o

The stabilizer of the base component

def MultiplicativeBasisDeformations.MeshWalk.o₀ {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] (Q : TranslationQuiver V) [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) (v₀ : V) {L : CatAlg.LocalFamily (meshFam Q c)} (D : CatAlg.MeshData (meshFam Q c) L) (x₀ : D.PV) : LObj Q c v₀ D

The base object (x₀, 1).

def MultiplicativeBasisDeformations.MeshWalk.Hs {k : Type u} [Field k] [IsAlgClosed k] [Infinite k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] (Q : TranslationQuiver V) [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) (v₀ : V) [hone : ∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] {L : CatAlg.LocalFamily (meshFam Q c)} (D : CatAlg.MeshData (meshFam Q c) L) [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] (x₀ : D.PV) : Subgroup (Deck Q v₀)

The stabilizer H of the component of the base object.

def MultiplicativeBasisDeformations.MeshWalk.A0Conn {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] (Q : TranslationQuiver V) [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) (v₀ : V) {L : CatAlg.LocalFamily (meshFam Q c)} (D : CatAlg.MeshData (meshFam Q c) L) (x₀ : D.PV) : Prop

The connectedness of A₀: a zigzag of nonzero pieces from x₀ to every label.

theorem MultiplicativeBasisDeformations.MeshWalk.line_of_nz {k : Type u} [Field k] [IsAlgClosed k] [Infinite k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients k Q} {v₀ : V} [hone : ∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] {L : CatAlg.LocalFamily (meshFam Q c)} {D : CatAlg.MeshData (meshFam Q c) L} [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] {x y : D.PV} {g : Deck Q v₀} (h : NZ Q c v₀ D (x, y, g)) (a : Deck Q v₀) : Thin.Line (have this := (x, a); this) (y, a * g)

theorem MultiplicativeBasisDeformations.MeshWalk.exists_lift {k : Type u} [Field k] [IsAlgClosed k] [Infinite k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients k Q} {v₀ : V} [hone : ∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] {L : CatAlg.LocalFamily (meshFam Q c)} {D : CatAlg.MeshData (meshFam Q c) L} [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] {x y : D.PV} (h : Relation.EqvGen (fun (x y : D.PV) => ∃ (g : Deck Q v₀), NZ Q c v₀ D (x, y, g)) x y) (a : Deck Q v₀) : ∃ (b : Deck Q v₀), conn Q c v₀ D (x, a) (y, b)

noncomputable def MultiplicativeBasisDeformations.MeshWalk.aL {k : Type u} [Field k] [IsAlgClosed k] [Infinite k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients k Q} {v₀ : V} [hone : ∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] {L : CatAlg.LocalFamily (meshFam Q c)} {D : CatAlg.MeshData (meshFam Q c) L} [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] {x₀ : D.PV} (hconn : A0Conn Q c v₀ D x₀) (x : D.PV) : Deck Q v₀

A lift of each label in the base component.

theorem MultiplicativeBasisDeformations.MeshWalk.aL_spec {k : Type u} [Field k] [IsAlgClosed k] [Infinite k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients k Q} {v₀ : V} [hone : ∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] {L : CatAlg.LocalFamily (meshFam Q c)} {D : CatAlg.MeshData (meshFam Q c) L} [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] {x₀ : D.PV} (hconn : A0Conn Q c v₀ D x₀) (x : D.PV) : conn Q c v₀ D (o₀ Q c v₀ D x₀) (x, aL hconn x)

theorem MultiplicativeBasisDeformations.MeshWalk.mem_Hs {k : Type u} [Field k] [IsAlgClosed k] [Infinite k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients k Q} {v₀ : V} [hone : ∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] {L : CatAlg.LocalFamily (meshFam Q c)} {D : CatAlg.MeshData (meshFam Q c) L} [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] {x₀ : D.PV} (hconn : A0Conn Q c v₀ D x₀) {x : D.PV} {b : Deck Q v₀} (h : conn Q c v₀ D (o₀ Q c v₀ D x₀) (x, b)) : b * (aL hconn x)⁻¹ ∈ Hs Q c v₀ D x₀

theorem MultiplicativeBasisDeformations.MeshWalk.conn_nz {k : Type u} [Field k] [IsAlgClosed k] [Infinite k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients k Q} {v₀ : V} [hone : ∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] {L : CatAlg.LocalFamily (meshFam Q c)} {D : CatAlg.MeshData (meshFam Q c) L} [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] {x₀ : D.PV} (hconn : A0Conn Q c v₀ D x₀) {x y : D.PV} {g : Deck Q v₀} (h : NZ Q c v₀ D (x, y, g)) : conn Q c v₀ D (o₀ Q c v₀ D x₀) (y, aL hconn x * g)

The comparison W(P) → ℤ^{labels} × H_ab and its left inverse

theorem MultiplicativeBasisDeformations.MeshWalk.grp_mid {G : Type u_1} [Group G] (a g b h d : G) : a * g * b⁻¹ * (b * h * d⁻¹) = a * (g * h) * d⁻¹

theorem MultiplicativeBasisDeformations.MeshWalk.grp_back {G : Type u_1} [Group G] (a g b : G) : a * g * b⁻¹ * b = a * g

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.MeshWalk.Tgt {k : Type u} [Field k] [IsAlgClosed k] [Infinite k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] (Q : TranslationQuiver V) [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) (v₀ : V) [hone : ∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] {L : CatAlg.LocalFamily (meshFam Q c)} (D : CatAlg.MeshData (meshFam Q c) L) [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] (x₀ : D.PV) : Type

The target ℤ^{labels} × H_ab.

noncomputable def MultiplicativeBasisDeformations.MeshWalk.ψgen {k : Type u} [Field k] [IsAlgClosed k] [Infinite k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients k Q} {v₀ : V} [hone : ∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] {L : CatAlg.LocalFamily (meshFam Q c)} {D : CatAlg.MeshData (meshFam Q c) L} [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] {x₀ : D.PV} (hconn : A0Conn Q c v₀ D x₀) (t : Piece Q c v₀ D) : Tgt Q c v₀ D x₀

The value of the comparison on a generator.

theorem MultiplicativeBasisDeformations.MeshWalk.nz_of_comp {k : Type u} [Field k] [IsAlgClosed k] [Infinite k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients k Q} {v₀ : V} [hone : ∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] {L : CatAlg.LocalFamily (meshFam Q c)} {D : CatAlg.MeshData (meshFam Q c) L} [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] {x y z : D.PV} {g h : Deck Q v₀} {f : D.F0 x ⟶ D.F0 y} {f' : D.F0 y ⟶ D.F0 z} (hf : f ∈ (D0 Q c v₀ D).part g x y) (hf' : f' ∈ (D0 Q c v₀ D).part h y z) (hff : CategoryTheory.CategoryStruct.comp f f' ≠ 0) : NZ Q c v₀ D (x, y, g) ∧ NZ Q c v₀ D (y, z, h) ∧ NZ Q c v₀ D (x, z, g * h)

noncomputable def MultiplicativeBasisDeformations.MeshWalk.ΨW {k : Type u} [Field k] [IsAlgClosed k] [Infinite k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients k Q} {v₀ : V} [hone : ∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] {L : CatAlg.LocalFamily (meshFam Q c)} {D : CatAlg.MeshData (meshFam Q c) L} [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] {x₀ : D.PV} (hconn : A0Conn Q c v₀ D x₀) : WP Q c v₀ D →+ Tgt Q c v₀ D x₀

The comparison Ψ : W(P) → ℤ^{labels} × H_ab.

theorem MultiplicativeBasisDeformations.MeshWalk.ΨW_cls {k : Type u} [Field k] [IsAlgClosed k] [Infinite k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients k Q} {v₀ : V} [hone : ∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] {L : CatAlg.LocalFamily (meshFam Q c)} {D : CatAlg.MeshData (meshFam Q c) L} [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] {x₀ : D.PV} (hconn : A0Conn Q c v₀ D x₀) (t : Piece Q c v₀ D) : (ΨW hconn) (cls Q c v₀ D t) = ψgen hconn t

noncomputable def MultiplicativeBasisDeformations.MeshWalk.γH {k : Type u} [Field k] [IsAlgClosed k] [Infinite k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients k Q} {v₀ : V} [hone : ∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] {L : CatAlg.LocalFamily (meshFam Q c)} {D : CatAlg.MeshData (meshFam Q c) L} [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] {x₀ : D.PV} {ζ : LObj Q c v₀ D → WP Q c v₀ D} (hζ : ∀ (o o' : LObj Q c v₀ D), Thin.Line o o' → wtL Q c v₀ D o o' = ζ o' - ζ o) : ↥(Hs Q c v₀ D x₀) →* Multiplicative (WP Q c v₀ D)

The deck classes θ_h = [e_{h x} − e_x], h ∈ H.

noncomputable def MultiplicativeBasisDeformations.MeshWalk.ΦW {k : Type u} [Field k] [IsAlgClosed k] [Infinite k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients k Q} {v₀ : V} [hone : ∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] {L : CatAlg.LocalFamily (meshFam Q c)} {D : CatAlg.MeshData (meshFam Q c) L} [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] {x₀ : D.PV} (hconn : A0Conn Q c v₀ D x₀) {ζ : LObj Q c v₀ D → WP Q c v₀ D} (hζ : ∀ (o o' : LObj Q c v₀ D), Thin.Line o o' → wtL Q c v₀ D o o' = ζ o' - ζ o) : Tgt Q c v₀ D x₀ →+ WP Q c v₀ D

The inverse comparison Φ : ℤ^{labels} × H_ab → W(P).

theorem MultiplicativeBasisDeformations.MeshWalk.ΦW_ΨW {k : Type u} [Field k] [IsAlgClosed k] [Infinite k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients k Q} {v₀ : V} [hone : ∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] {L : CatAlg.LocalFamily (meshFam Q c)} {D : CatAlg.MeshData (meshFam Q c) L} [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] {x₀ : D.PV} (hconn : A0Conn Q c v₀ D x₀) {ζ : LObj Q c v₀ D → WP Q c v₀ D} (hζ : ∀ (o o' : LObj Q c v₀ D), Thin.Line o o' → wtL Q c v₀ D o o' = ζ o' - ζ o) (w : WP Q c v₀ D) : (ΦW hconn hζ) ((ΨW hconn) w) = w

Φ ∘ Ψ = 1 (Proposition 7.2(1), injectivity of the comparison).

Freeness of W(P)

theorem MultiplicativeBasisDeformations.MeshWalk.finite_nz {k : Type u} [Field k] [IsAlgClosed k] [Infinite k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients k Q} {v₀ : V} [hone : ∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] {L : CatAlg.LocalFamily (meshFam Q c)} {D : CatAlg.MeshData (meshFam Q c) L} [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] : {t : Piece Q c v₀ D | NZ Q c v₀ D t}.Finite

theorem MultiplicativeBasisDeformations.MeshWalk.WP_finite {k : Type u} [Field k] [IsAlgClosed k] [Infinite k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients k Q} {v₀ : V} [hone : ∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] {L : CatAlg.LocalFamily (meshFam Q c)} {D : CatAlg.MeshData (meshFam Q c) L} [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] : Module.Finite ℤ (WP Q c v₀ D)

W(P) is finitely generated.

theorem MultiplicativeBasisDeformations.MeshWalk.abelianization_torsionFree {Hg : Type u_1} [Group Hg] [IsFreeGroup Hg] : Module.IsTorsionFree ℤ (Additive (Abelianization Hg))

theorem MultiplicativeBasisDeformations.MeshWalk.WP_free {k : Type u} [Field k] [IsAlgClosed k] [Infinite k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients k Q} {v₀ : V} [hone : ∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] {L : CatAlg.LocalFamily (meshFam Q c)} {D : CatAlg.MeshData (meshFam Q c) L} [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] (hF : IsRepresentationFinite k (CatAlg.Alg D.F0)ᵐᵒᵖ) {x₀ : D.PV} (hconn : A0Conn Q c v₀ D x₀) : Module.Free ℤ (WP Q c v₀ D)

W(P) is a free abelian group of finite rank (Proposition 7.2(1)).