Lemma 4.13: weights on L are ratios of object values

lem:scalar-object-values (scalar-normalization.tex). For the deck grading of a scalar mesh category with at most one arrow between two vertices, a weight d on L gives the automorphism Φ of the cover (ScalarAutomorphism.lean). "The endpoints of an arrow differ in height by one, so the entire morphism space between them is spanned by the arrow. Thus Φ(a) = w(a) a for some w(a) ∈ k*" (wArr). "Comparing coefficients gives w(σa) w(a) = ν_X" (mesh_compat). "Assign ν_X to t_X. These weights respect the triangles of K̃. Since this complex is simply connected, multiplying along walks gives object values ζ_X" (ζ, ζ_arrow). "Conjugation by these values fixes every arrow and hence every morphism, so Φ multiplies each morphism X̃ → Ỹ by ζ_Ỹ / ζ_X̃" (Φ_eq_ratio), and on L this gives d(x, y) = ζ_y / ζ_x (weight_eq_ratio).

Sheets of walks from the basepoint

def MultiplicativeBasisDeformations.MeshWalk.liftW {V : Type} [Quiver V] (Q : TranslationQuiver V) (v₀ : V) (h : Deck Q v₀) (X : V) : obC Q v₀ v₀ ⟶ obC Q v₀ X

The lift of X in sheet h, as a walk class from the basepoint.

def MultiplicativeBasisDeformations.MeshWalk.sheet {V : Type} [Quiver V] {Q : TranslationQuiver V} {v₀ X : V} (γ : obC Q v₀ v₀ ⟶ obC Q v₀ X) : Deck Q v₀

The sheet of a walk class from the basepoint.

theorem MultiplicativeBasisDeformations.MeshWalk.sheet_liftW {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {v₀ : V} (h : Deck Q v₀) (X : V) : sheet (liftW Q v₀ h X) = h

theorem MultiplicativeBasisDeformations.MeshWalk.liftW_arr {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {v₀ : V} (h : Deck Q v₀) {y x : V} (a : y ⟶ x) : CategoryTheory.CategoryStruct.comp (liftW Q v₀ h y) (arrC Q v₀ a) = liftW Q v₀ (h * (degW Q v₀).deg a.toPath) x

theorem MultiplicativeBasisDeformations.MeshWalk.sheet_comp_arr {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {v₀ y x : V} (γ : obC Q v₀ v₀ ⟶ obC Q v₀ y) (a : y ⟶ x) : sheet (CategoryTheory.CategoryStruct.comp γ (arrC Q v₀ a)) = sheet γ * (degW Q v₀).deg a.toPath

theorem MultiplicativeBasisDeformations.MeshWalk.path_length_one {V : Type} [Quiver V] {y x : V} (p : Quiver.Path y x) (hp : p.length = 1) : ∃ (b : y ⟶ x), p = b.toPath

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.MeshWalk.dg {V : Type} [Quiver V] (Q : TranslationQuiver V) (v₀ : V) {y x : V} (a : y ⟶ x) : Deck Q v₀

The deck degree of an arrow.

theorem MultiplicativeBasisDeformations.MeshWalk.arrowMor_ne_zero {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} {y x : V} (a : y ⟶ x) : ScalarMeshCategory.arrowMor c a ≠ 0

theorem MultiplicativeBasisDeformations.MeshWalk.arrow_mem {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} (h : Deck Q v₀) {y x : V} (a : y ⟶ x) : ScalarMeshCategory.arrowMor c a ∈ (deckGrading Q c v₀).part (h⁻¹ * (h * dg Q v₀ a)) y x

theorem MultiplicativeBasisDeformations.MeshWalk.part_arrow {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)] {y x : V} (a : y ⟶ x) {g : ScalarMeshCategory.obj c y ⟶ ScalarMeshCategory.obj c x} (hg : g ∈ (deckGrading Q c v₀).part (dg Q v₀ a) y x) : ∃ (t : k), g = t • ScalarMeshCategory.arrowMor c a

Arrow lines: the morphisms of the degree of an arrow are its multiples.

The automorphism Φ on arrows and meshes

noncomputable def MultiplicativeBasisDeformations.MeshWalk.wArr {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} [IsAlgClosed k] [Infinite k] [hone : ∀ (x y : V), Subsingleton (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)ᵐᵒᵖ) {d : D.PV × Deck Q v₀ → D.PV × Deck Q v₀ → k} (hd : Thin.IsWeight Set.univ d) (h : Deck Q v₀) {y x : V} (a : y ⟶ x) : k

Φ(a) = w(a) a: the scalar of Φ on the lift of an arrow in sheet h.

theorem MultiplicativeBasisDeformations.MeshWalk.wArr_spec {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} [IsAlgClosed k] [Infinite k] [hone : ∀ (x y : V), Subsingleton (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)ᵐᵒᵖ) {d : D.PV × Deck Q v₀ → D.PV × Deck Q v₀ → k} (hd : Thin.IsWeight Set.univ d) (h : Deck Q v₀) {y x : V} (a : y ⟶ x) : CatAlg.MeshData.Φ hd (deckHeight Q c v₀) hF (ScalarMeshCategory.arrowMor c a) ⋯ = wArr hF hd h a • ScalarMeshCategory.arrowMor c a

theorem MultiplicativeBasisDeformations.MeshWalk.wArr_ne {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} [IsAlgClosed k] [Infinite k] [hone : ∀ (x y : V), Subsingleton (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)ᵐᵒᵖ) {d : D.PV × Deck Q v₀ → D.PV × Deck Q v₀ → k} (hd : Thin.IsWeight Set.univ d) (h : Deck Q v₀) {y x : V} (a : y ⟶ x) : wArr hF hd h a ≠ 0

theorem MultiplicativeBasisDeformations.MeshWalk.Φ_cast {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} [IsAlgClosed k] [Infinite k] [hone : ∀ (x y : V), Subsingleton (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)ᵐᵒᵖ) {d : D.PV × Deck Q v₀ → D.PV × Deck Q v₀ → k} (hd : Thin.IsWeight Set.univ d) {X : V × Deck Q v₀} {y : V} {g g' : Deck Q v₀} (hg : g = g') {f f' : ScalarMeshCategory.obj c X.1 ⟶ ScalarMeshCategory.obj c y} (hf : f = f') (h1 : f ∈ (deckGrading Q c v₀).part (X.2⁻¹ * g) X.1 y) (h2 : f' ∈ (deckGrading Q c v₀).part (X.2⁻¹ * g') X.1 y) : CatAlg.MeshData.Φ hd (deckHeight Q c v₀) hF f h1 = CatAlg.MeshData.Φ hd (deckHeight Q c v₀) hF f' h2

theorem MultiplicativeBasisDeformations.MeshWalk.Φ_zero {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} [IsAlgClosed k] [Infinite k] [hone : ∀ (x y : V), Subsingleton (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)ᵐᵒᵖ) {d : D.PV × Deck Q v₀ → D.PV × Deck Q v₀ → k} (hd : Thin.IsWeight Set.univ d) {X Y : V × Deck Q v₀} (h0 : 0 ∈ (deckGrading Q c v₀).part (X.2⁻¹ * Y.2) X.1 Y.1) : CatAlg.MeshData.Φ hd (deckHeight Q c v₀) hF 0 h0 = 0

theorem MultiplicativeBasisDeformations.MeshWalk.Φ_sum {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} [IsAlgClosed k] [Infinite k] [hone : ∀ (x y : V), Subsingleton (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)ᵐᵒᵖ) {d : D.PV × Deck Q v₀ → D.PV × Deck Q v₀ → k} (hd : Thin.IsWeight Set.univ d) {X Y : V × Deck Q v₀} {ι : Type} (s : Finset ι) (f : ι → (ScalarMeshCategory.obj c X.1 ⟶ ScalarMeshCategory.obj c Y.1)) (hf : ∀ (i : ι), f i ∈ (deckGrading Q c v₀).part (X.2⁻¹ * Y.2) X.1 Y.1) : CatAlg.MeshData.Φ hd (deckHeight Q c v₀) hF (∑ i ∈ s, f i) ⋯ = ∑ i ∈ s, CatAlg.MeshData.Φ hd (deckHeight Q c v₀) hF (f i) ⋯

def MultiplicativeBasisDeformations.MeshWalk.tdeg {V : Type} [Quiver V] {Q : TranslationQuiver V} {v₀ : V} (x : ↑Q.nonprojective) : Deck Q v₀

The deck degree of the translation edge t_x.

theorem MultiplicativeBasisDeformations.MeshWalk.dg_mesh {V : Type} [Quiver V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {v₀ : V} [hone : ∀ (x y : V), Subsingleton (x ⟶ y)] (x : ↑Q.nonprojective) (a : (y : V) × (y ⟶ ↑x)) : dg Q v₀ ((Q.mate x a.fst) a.snd) * dg Q v₀ a.snd = tdeg x

theorem MultiplicativeBasisDeformations.MeshWalk.mesh_compat {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} [IsAlgClosed k] [Infinite k] [hone : ∀ (x y : V), Subsingleton (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)ᵐᵒᵖ) {d : D.PV × Deck Q v₀ → D.PV × Deck Q v₀ → k} (hd : Thin.IsWeight Set.univ d) (x : ↑Q.nonprojective) (h : Deck Q v₀) : ∃ (ν : k), ∀ (a : (y : V) × (y ⟶ ↑x)), wArr hF hd h ((Q.mate x a.fst) a.snd) * wArr hF hd (h * dg Q v₀ ((Q.mate x a.fst) a.snd)) a.snd = ν

Compatibility at a mesh: w(σa) w(a) = ν_X for every mate pair.

Object values by simple connectivity

noncomputable def MultiplicativeBasisDeformations.MeshWalk.νv {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} [IsAlgClosed k] [Infinite k] [hone : ∀ (x y : V), Subsingleton (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)ᵐᵒᵖ) {d : D.PV × Deck Q v₀ → D.PV × Deck Q v₀ → k} (hd : Thin.IsWeight Set.univ d) (h : Deck Q v₀) (x : ↑Q.nonprojective) : k

The value ν_X assigned to the translation edge t_X in a sheet.

theorem MultiplicativeBasisDeformations.MeshWalk.νv_eq {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} [IsAlgClosed k] [Infinite k] [hone : ∀ (x y : V), Subsingleton (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)ᵐᵒᵖ) {d : D.PV × Deck Q v₀ → D.PV × Deck Q v₀ → k} (hd : Thin.IsWeight Set.univ d) (h : Deck Q v₀) (x : ↑Q.nonprojective) (a : (y : V) × (y ⟶ ↑x)) : wArr hF hd h ((Q.mate x a.fst) a.snd) * wArr hF hd (h * dg Q v₀ ((Q.mate x a.fst) a.snd)) a.snd = νv hF hd h x

theorem MultiplicativeBasisDeformations.MeshWalk.νv_ne {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} [IsAlgClosed k] [Infinite k] [hone : ∀ (x y : V), Subsingleton (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)ᵐᵒᵖ) {d : D.PV × Deck Q v₀ → D.PV × Deck Q v₀ → k} (hd : Thin.IsWeight Set.univ d) (h : Deck Q v₀) (x : ↑Q.nonprojective) : νv hF hd h x ≠ 0

noncomputable def MultiplicativeBasisDeformations.MeshWalk.Wt {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} [IsAlgClosed k] [Infinite k] [hone : ∀ (x y : V), Subsingleton (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)ᵐᵒᵖ) {d : D.PV × Deck Q v₀ → D.PV × Deck Q v₀ → k} (hd : Thin.IsWeight Set.univ d) (e : Ed Q ⊕ V) : (obC Q v₀ v₀ ⟶ obC Q v₀ (srcC Q v₀ e)) → kˣ

The weights on the edges of the lifted complex: w(a) on arrows, ν_X on translation edges, one on cone edges.

theorem MultiplicativeBasisDeformations.MeshWalk.Wt_tri {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} [IsAlgClosed k] [Infinite k] [hone : ∀ (x y : V), Subsingleton (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)ᵐᵒᵖ) {d : D.PV × Deck Q v₀ → D.PV × Deck Q v₀ → k} (hd : Thin.IsWeight Set.univ d) (x : ↑Q.nonprojective) (a : (y : V) × (y ⟶ ↑x)) (γ : obC Q v₀ v₀ ⟶ obC Q v₀ ↑(Q.tau x)) : Wt hF hd (Sum.inl (Sum.inl ⟨↑(Q.tau x), ⟨a.fst, (Q.mate x a.fst) a.snd⟩⟩)) γ * Wt hF hd (Sum.inl (Sum.inl ⟨a.fst, ⟨↑x, a.snd⟩⟩)) (CategoryTheory.CategoryStruct.comp γ (arrC Q v₀ ((Q.mate x a.fst) a.snd))) = Wt hF hd (Sum.inl (Sum.inr x)) γ

The weights respect the triangles.

noncomputable def MultiplicativeBasisDeformations.MeshWalk.ζ {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} [IsAlgClosed k] [Infinite k] [hone : ∀ (x y : V), Subsingleton (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)ᵐᵒᵖ) {d : D.PV × Deck Q v₀ → D.PV × Deck Q v₀ → k} (hd : Thin.IsWeight Set.univ d) (X : V × Deck Q v₀) : kˣ

The object values ζ on the lifted vertices.

theorem MultiplicativeBasisDeformations.MeshWalk.ζ_arrow {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} [IsAlgClosed k] [Infinite k] [hone : ∀ (x y : V), Subsingleton (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)ᵐᵒᵖ) {d : D.PV × Deck Q v₀ → D.PV × Deck Q v₀ → k} (hd : Thin.IsWeight Set.univ d) (h : Deck Q v₀) {y x : V} (a : y ⟶ x) : ↑(ζ hF hd (x, h * dg Q v₀ a)) = ↑(ζ hF hd (y, h)) * wArr hF hd h a

w(a) = ζ_{target(a)} / ζ_{source(a)}.

Conjugation by the object values

theorem MultiplicativeBasisDeformations.MeshWalk.pathMor_mem {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} [IsAlgClosed k] [Infinite k] [hone : ∀ (x y : V), Subsingleton (x ⟶ y)] [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] (X : V × Deck Q v₀) {y : V} (p : Quiver.Path X.1 y) : ScalarMeshCategory.pathMor c p ∈ (deckGrading Q c v₀).part (X.2⁻¹ * (X.2 * (degW Q v₀).deg p)) X.1 y

theorem MultiplicativeBasisDeformations.MeshWalk.Φ_path {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} [IsAlgClosed k] [Infinite k] [hone : ∀ (x y : V), Subsingleton (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)ᵐᵒᵖ) {d : D.PV × Deck Q v₀ → D.PV × Deck Q v₀ → k} (hd : Thin.IsWeight Set.univ d) (X : V × Deck Q v₀) {y : V} (p : Quiver.Path X.1 y) : CatAlg.MeshData.Φ hd (deckHeight Q c v₀) hF (ScalarMeshCategory.pathMor c p) ⋯ = (↑(ζ hF hd (y, X.2 * (degW Q v₀).deg p)) / ↑(ζ hF hd X)) • ScalarMeshCategory.pathMor c p

Φ on paths: the lift of a path is multiplied by ζ_Ỹ / ζ_X̃.

theorem MultiplicativeBasisDeformations.MeshWalk.Φ_eq_ratio {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} [IsAlgClosed k] [Infinite k] [hone : ∀ (x y : V), Subsingleton (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)ᵐᵒᵖ) {d : D.PV × Deck Q v₀ → D.PV × Deck Q v₀ → k} (hd : Thin.IsWeight Set.univ d) (X Y : V × Deck Q v₀) (f : ScalarMeshCategory.obj c X.1 ⟶ ScalarMeshCategory.obj c Y.1) (hf : f ∈ (deckGrading Q c v₀).part (X.2⁻¹ * Y.2) X.1 Y.1) : CatAlg.MeshData.Φ hd (deckHeight Q c v₀) hF f hf = (↑(ζ hF hd Y) / ↑(ζ hF hd X)) • f

Conjugation: Φ multiplies each morphism X̃ → Ỹ by ζ_Ỹ / ζ_X̃.

theorem MultiplicativeBasisDeformations.MeshWalk.weight_eq_ratio {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} [IsAlgClosed k] [Infinite k] [hone : ∀ (x y : V), Subsingleton (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)ᵐᵒᵖ) {d : D.PV × Deck Q v₀ → D.PV × Deck Q v₀ → k} (hd : Thin.IsWeight Set.univ d) : ∃ (ζ' : D.PV × Deck Q v₀ → k), (∀ (z : D.PV × Deck Q v₀), ζ' z ≠ 0) ∧ ∀ (z₁ z₂ : D.PV × Deck Q v₀), ∀ f ∈ (deckGrading Q c v₀).part (z₁.2⁻¹ * z₂.2) ↑z₁.1 ↑z₂.1, f ≠ 0 → d z₁ z₂ = ζ' z₂ / ζ' z₁

Lemma 4.13: every multiplicative scalar weight on L is a ratio of object values, d(x, y) = ζ_y / ζ_x on every nonzero morphism line.