Integer mesh weights and their restriction to rays (Lemma 7.4)

weights-and-parameters.tex (def:integer-weights, lem:integer-weight-lifting). An integer mesh weight assigns w(a) to arrows and ν_v to mesh rows with w(σa) + w(a) = ν_v; it restricts to an integer ray weight, and "this restriction gives an exact sequence 0 → {ζ : ζ_P = 0} → H^mesh → H → 0".

The proof works on the lifted complex. "Pull a ray weight h back to L. By Proposition 7.2, write h(r : x → y) = b_y − b_x […] Choose one lift of each nonprojective label and assign it any integer. Extend by ζ_{gX} = ζ_X + γ(g). Differences along arrows and translation edges are deck invariant, hence descend to a mesh weight."

Formalization. The deck group of the formalization is the fundamental group of the coned complex, so we work in the component K₀ of a base vertex in the lifted Auslander–Reiten quiver (aconn), whose stabilizer plays the role of the paper's G = π₁(K). The connectivity of the lifted projective category used by the paper is replaced by the support lemma (supp_conn): the lifted projectives with nonzero maps to one lifted object are connected in L, by Lemma 4.8 and the locality of degree-one endomorphisms; hence the lifted projectives of K₀ lie in one component of L (conn_of_aconn).

theorem MultiplicativeBasisDeformations.MeshWalk.line_iff {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)] {z z' : LObj Q c v₀ D} : Thin.Line z z' ↔ ∃ f ∈ (deckGrading Q c v₀).part (z.2⁻¹ * z'.2) ↑z.1 ↑z'.1, f ≠ 0

def MultiplicativeBasisDeformations.MeshWalk.toL {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) (z : D.PV × Deck Q v₀) : LObj Q c v₀ D

A lifted projective vertex as an object of L.

def MultiplicativeBasisDeformations.MeshWalk.ofL {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 : LObj Q c v₀ D) : D.PV × Deck Q v₀

An object of L as a lifted projective vertex.

theorem MultiplicativeBasisDeformations.MeshWalk.supp_conn {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 : V × Deck Q v₀) {z₁ z₂ : D.PV × Deck Q v₀} {m₁ : meshFam Q c ↑z₁.1 ⟶ meshFam Q c X.1} (hm₁ : m₁ ∈ (deckGrading Q c v₀).part (z₁.2⁻¹ * X.2) (↑z₁.1) X.1) (h₁ : m₁ ≠ 0) {m₂ : meshFam Q c ↑z₂.1 ⟶ meshFam Q c X.1} (hm₂ : m₂ ∈ (deckGrading Q c v₀).part (z₂.2⁻¹ * X.2) (↑z₂.1) X.1) (h₂ : m₂ ≠ 0) : conn Q c v₀ D (toL Q c v₀ D z₁) (toL Q c v₀ D z₂)

The support lemma: two lifted projectives with nonzero maps to one lifted object are connected in L.

Supports along arrows

def MultiplicativeBasisDeformations.MeshWalk.aconn {V : Type} [Quiver V] (Q : TranslationQuiver V) (v₀ : V) (A B : V × Deck Q v₀) : Prop

Arrow-connectedness of lifted vertices.

def MultiplicativeBasisDeformations.MeshWalk.InSupp {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) (A : V × Deck Q v₀) (z : D.PV × Deck Q v₀) : Prop

z lies in the support of the lifted object A.

theorem MultiplicativeBasisDeformations.MeshWalk.exists_supp {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)] (A : V × Deck Q v₀) : ∃ (z : D.PV × Deck Q v₀), InSupp Q c v₀ D A z

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

theorem MultiplicativeBasisDeformations.MeshWalk.common_supp {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)] {Y X : V} (a : Y ⟶ X) (h : Deck Q v₀) : ∃ (z : D.PV × Deck Q v₀), InSupp Q c v₀ D (Y, h) z ∧ InSupp Q c v₀ D (X, h * dg Q v₀ a) z

theorem MultiplicativeBasisDeformations.MeshWalk.supp_aconn {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)] {A B : V × Deck Q v₀} (hAB : aconn Q v₀ A B) {z z' : D.PV × Deck Q v₀} : InSupp Q c v₀ D A z → InSupp Q c v₀ D B z' → conn Q c v₀ D (toL Q c v₀ D z) (toL Q c v₀ D z')

theorem MultiplicativeBasisDeformations.MeshWalk.self_supp {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)] (p : D.PV) (g : Deck Q v₀) : InSupp Q c v₀ D (↑p, g) (p, g)

theorem MultiplicativeBasisDeformations.MeshWalk.conn_of_aconn {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)] {p q : D.PV} {a b : Deck Q v₀} (h : aconn Q v₀ (↑p, a) (↑q, b)) : conn Q c v₀ D (toL Q c v₀ D (p, a)) (toL Q c v₀ D (q, b))

Lifted projectives in one arrow-component lie in one component of L.

theorem MultiplicativeBasisDeformations.MeshWalk.exists_path_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)) : ∃ (p : Quiver.Path ↑x ↑y), (degW Q v₀).deg p = g

A nonzero piece contains the image of a path of its degree.

Integer mesh weights

structure MultiplicativeBasisDeformations.MeshWalk.MeshWt {V : Type} [Quiver V] (Q : TranslationQuiver V) (M : Type u_1) [AddCommGroup M] : Type u_1

An integer mesh weight (Definition 7.3(2)), with values in an abelian group: w(σa) + w(a) = ν_v.

• w {y x : V} : (y ⟶ x) → M
• ν : ↑Q.nonprojective → M
• mesh (x : ↑Q.nonprojective) (a : (y : V) × (y ⟶ ↑x)) : self.w ((Q.mate x a.fst) a.snd) + self.w a.snd = self.ν x

@[irreducible]

def MultiplicativeBasisDeformations.MeshWalk.MeshWt.pw {V : Type} [Quiver V] {Q : TranslationQuiver V} {M : Type z} [AddCommGroup M] (W : MeshWt Q M) {y x : V} : Quiver.Path y x → M

The weight of a path: the sum of its arrow weights.

def MultiplicativeBasisDeformations.MeshWalk.MeshWt.WE {V : Type} [Quiver V] {Q : TranslationQuiver V} {v₀ : V} {M : Type z} [AddCommGroup M] (W : MeshWt Q M) (e : Ed Q ⊕ V) : (obC Q v₀ v₀ ⟶ obC Q v₀ (srcC Q v₀ e)) → Multiplicative M

The edge weights on the coned complex: arrows, rows, and zero on cone edges.

theorem MultiplicativeBasisDeformations.MeshWalk.MeshWt.WE_tri {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)] {M : Type z} [AddCommGroup M] (W : MeshWt Q M) (x : ↑Q.nonprojective) (a : (y : V) × (y ⟶ ↑x)) (γ : obC Q v₀ v₀ ⟶ obC Q v₀ ↑(Q.tau x)) : W.WE (Sum.inl (Sum.inl ⟨↑(Q.tau x), ⟨a.fst, (Q.mate x a.fst) a.snd⟩⟩)) γ * W.WE (Sum.inl (Sum.inl ⟨a.fst, ⟨↑x, a.snd⟩⟩)) (CategoryTheory.CategoryStruct.comp γ (arrC Q v₀ ((Q.mate x a.fst) a.snd))) = W.WE (Sum.inl (Sum.inr x)) γ

def MultiplicativeBasisDeformations.MeshWalk.MeshWt.pot {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)] {M : Type z} [AddCommGroup M] (W : MeshWt Q M) (A : V × Deck Q v₀) : M

The object values of a mesh weight on the lifted vertices.

theorem MultiplicativeBasisDeformations.MeshWalk.MeshWt.pot_arrow {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)] {M : Type z} [AddCommGroup M] (W : MeshWt Q M) (h : Deck Q v₀) {y x : V} (a : y ⟶ x) : pot v₀ W (x, h * dg Q v₀ a) = pot v₀ W (y, h) + W.w a

theorem MultiplicativeBasisDeformations.MeshWalk.liftW_t {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)] (h : Deck Q v₀) (x : ↑Q.nonprojective) : CategoryTheory.CategoryStruct.comp (liftW Q v₀ h ↑(Q.tau x)) (tC Q v₀ x) = liftW Q v₀ (h * tdeg x) ↑x

theorem MultiplicativeBasisDeformations.MeshWalk.MeshWt.pot_t {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)] {M : Type z} [AddCommGroup M] (W : MeshWt Q M) (h : Deck Q v₀) (x : ↑Q.nonprojective) : pot v₀ W (↑x, h * tdeg x) = pot v₀ W (↑(Q.tau x), h) + W.ν x

theorem MultiplicativeBasisDeformations.MeshWalk.grp_mul_one {G : Type u_1} [Group G] (h : G) : h * 1 = h

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

theorem MultiplicativeBasisDeformations.MeshWalk.deg_cons {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)] {y x z : V} (p : Quiver.Path y x) (a : x ⟶ z) : (degW Q v₀).deg (p.cons a) = (degW Q v₀).deg p * dg Q v₀ a

theorem MultiplicativeBasisDeformations.MeshWalk.MeshWt.pot_path {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)] {M : Type z} [AddCommGroup M] (W : MeshWt Q M) (h : Deck Q v₀) {y x : V} (p : Quiver.Path y x) : pot v₀ W (x, h * (degW Q v₀).deg p) = pot v₀ W (y, h) + W.pw p

Potentials along paths: ζ(x, h·deg p) = ζ(y, h) + w(p).

Restriction to rays

noncomputable def MultiplicativeBasisDeformations.MeshWalk.MeshWt.rv {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} [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} {M : Type z} [AddCommGroup M] (W : MeshWt Q M) (t : Piece Q c v₀ D) : M

The restriction on a generator: the weight of the paths of the ray.

theorem MultiplicativeBasisDeformations.MeshWalk.grp_one_mul {G : Type u_1} [Group G] (h : G) : 1 * h = h

theorem MultiplicativeBasisDeformations.MeshWalk.MeshWt.rv_path {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)] {M : Type z} [AddCommGroup M] (W : MeshWt Q M) {x y : D.PV} {g : Deck Q v₀} (h : NZ Q c v₀ D (x, y, g)) {p : Quiver.Path ↑x ↑y} (hp : (degW Q v₀).deg p = g) : W.rv (x, y, g) = W.pw p

noncomputable def MultiplicativeBasisDeformations.MeshWalk.MeshWt.res {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)] {M : Type z} [AddCommGroup M] (W : MeshWt Q M) : WP Q c v₀ D →+ M

The restriction of a mesh weight to an integer ray weight (Lemma 7.4).

theorem MultiplicativeBasisDeformations.MeshWalk.MeshWt.res_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)] {M : Type z} [AddCommGroup M] (W : MeshWt Q M) (t : Piece Q c v₀ D) : (res c D W) (cls Q c v₀ D t) = W.rv t

Lemma 7.4: lifting ray weights to mesh weights

theorem MultiplicativeBasisDeformations.MeshWalk.grp_shift1 {G : Type u_1} [Group G] (u : G) : u * 1 = u

theorem MultiplicativeBasisDeformations.MeshWalk.grp_cancel_r {G : Type u_1} [Group G] (g k' : G) : g * k'⁻¹ * k' = g

theorem MultiplicativeBasisDeformations.MeshWalk.grp_split {G : Type u_1} [Group G] (v gY d gX : G) : v * d * gX⁻¹ = v * gY⁻¹ * (gY * d * gX⁻¹)

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

def MultiplicativeBasisDeformations.MeshWalk.shV {V : Type} [Quiver V] (Q : TranslationQuiver V) (v₀ : V) (u : Deck Q v₀) (A : V × Deck Q v₀) : V × Deck Q v₀

Translating a lifted vertex by a deck element.

theorem MultiplicativeBasisDeformations.MeshWalk.aconn_shV {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 : V × Deck Q v₀} (u : Deck Q v₀) (h : aconn Q v₀ A B) : aconn Q v₀ (shV Q v₀ u A) (shV Q v₀ u B)

theorem MultiplicativeBasisDeformations.MeshWalk.aconn_arrow {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 : V × Deck Q v₀) {X : V} (a : A.1 ⟶ X) : aconn Q v₀ A (X, A.2 * dg Q v₀ a)

theorem MultiplicativeBasisDeformations.MeshWalk.aconn_path {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)] {Y X : V} (p : Quiver.Path Y X) (v : Deck Q v₀) : aconn Q v₀ (Y, v) (X, v * (degW Q v₀).deg p)

noncomputable def MultiplicativeBasisDeformations.MeshWalk.gK {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) (hK : ∀ (X : V), ∃ (g : Deck Q v₀), aconn Q v₀ (↑x₀, 1) (X, g)) (X : V) : Deck Q v₀

The base lift of each label.

theorem MultiplicativeBasisDeformations.MeshWalk.gK_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) (hK : ∀ (X : V), ∃ (g : Deck Q v₀), aconn Q v₀ (↑x₀, 1) (X, g)) (X : V) : aconn Q v₀ (↑x₀, 1) (X, gK x₀ hK X)

theorem MultiplicativeBasisDeformations.MeshWalk.inK_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)] (x₀ : D.PV) {X : V} {g g' : Deck Q v₀} (h : aconn Q v₀ (↑x₀, 1) (X, g)) (h' : aconn Q v₀ (↑x₀, 1) (X, g')) : aconn Q v₀ (↑x₀, 1) (↑x₀, g' * g⁻¹)

theorem MultiplicativeBasisDeformations.MeshWalk.hwt_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)] {M : Type z} [AddCommGroup M] (h : WP Q c v₀ D →+ M) : Thin.IsAddWeight Set.univ fun (o o' : LObj Q c v₀ D) => h (wtL Q c v₀ D o o')

theorem MultiplicativeBasisDeformations.MeshWalk.b_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)] {M : Type z} [AddCommGroup M] (h : WP Q c v₀ D →+ M) {b : LObj Q c v₀ D → M} (hb : ∀ (o o' : LObj Q c v₀ D), Thin.Line o o' → h (wtL Q c v₀ D o o') = b o' - b o) (u : Deck Q v₀) {o o' : LObj Q c v₀ D} (hc : conn Q c v₀ D o o') : b (gL Q c v₀ D u o') - b (gL Q c v₀ D u o) = b o' - b o

theorem MultiplicativeBasisDeformations.MeshWalk.exists_meshWt_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)] {M : Type z} [AddCommGroup M] {hF : IsRepresentationFinite k (CatAlg.Alg D.F0)ᵐᵒᵖ} {x₀ : D.PV} {hK : ∀ (X : V), ∃ (g : Deck Q v₀), aconn Q v₀ (↑x₀, 1) (X, g)} (h : WP Q c v₀ D →+ M) : ∃ (W : MeshWt Q M), MeshWt.res c D W = h

Lemma 7.4, surjectivity: every ray weight is the restriction of a mesh weight.

theorem MultiplicativeBasisDeformations.MeshWalk.MeshWt.pw_of_diff {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] [hone : ∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] {M : Type z} [AddCommGroup M] (W : MeshWt Q M) {ζ : V → M} (hζ : ∀ {y x : V} (a : y ⟶ x), W.w a = ζ x - ζ y) {Y X : V} (p : Quiver.Path Y X) : W.pw p = ζ X - ζ Y

theorem MultiplicativeBasisDeformations.MeshWalk.res_eq_zero_iff {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)] {M : Type z} [AddCommGroup M] {x₀ : D.PV} {hK : ∀ (X : V), ∃ (g : Deck Q v₀), aconn Q v₀ (↑x₀, 1) (X, g)} (hmid : ∀ (x : ↑Q.nonprojective), Nonempty ((y : V) × (y ⟶ ↑x))) (W : MeshWt Q M) : MeshWt.res c D W = 0 ↔ ∃ (ζ : V → M), (∀ (p : D.PV), ζ ↑p = 0) ∧ (∀ {y x : V} (a : y ⟶ x), W.w a = ζ x - ζ y) ∧ ∀ (x : ↑Q.nonprojective), W.ν x = ζ ↑x - ζ ↑(Q.tau x)

Lemma 7.4, exactness in the middle: a mesh weight restricts to zero exactly when it is the difference of object values vanishing at the projectives. Every mesh row is assumed to have an arrow (hmid), as in an Auslander–Reiten quiver.

theorem MultiplicativeBasisDeformations.MeshWalk.eq_zero_of_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)] {M : Type z} [AddCommGroup M] {x₀ : D.PV} {hK : ∀ (X : V), ∃ (g : Deck Q v₀), aconn Q v₀ (↑x₀, 1) (X, g)} (ζ : V → M) (h0 : ∀ (p : D.PV), ζ ↑p = 0) (harr : ∀ {y x : V} (x_1 : y ⟶ x), ζ x = ζ y) : ζ = 0

Lemma 7.4, injectivity on the left: object values vanishing at the projectives are determined by their differences along arrows.