Proposition 7.5: the residual characters are part of an integer basis

weights-and-parameters.tex (prop:primitive-parameter-characters): "In the weight lattice L = W(P), the residual characters χ_i form part of an integer basis."

Here χ_i = w(p_i) − ν_{v_i} for a mesh weight W_u with values in W(P) restricting to the identity (Lemma 7.4 with h = id). Given integer mesh weights W_j with W_j(p_i) − ν_{v_i} = δ_ij (residual_dual), the integer ray weights h_j = res W_j satisfy h_j(χ_i) = δ_ij: the mesh weights h_j ∘ W_u and W_j have the same restriction, so by Lemma 7.4 they differ by object values vanishing at the projectives, which do not change the weight of a row relative to its mesh (rowWt_eq_of_res). As W(P) is free of finite rank, the χ_i are part of a basis (exists_basis_of_dual).

Deviation: the source identifies χ_i with the deck class ±θ_{g_i} and uses a lemma on the periodic core; we use the dual mesh weights instead.

def MultiplicativeBasisDeformations.MeshWalk.MeshWt.map {V : Type} [Quiver V] {Q : TranslationQuiver V} {M N : Type} [AddCommGroup M] [AddCommGroup N] (h : M →+ N) (W : MeshWt Q M) : MeshWt Q N

The image of a mesh weight under a homomorphism.

def MultiplicativeBasisDeformations.MeshWalk.MeshWt.sub {V : Type} [Quiver V] {Q : TranslationQuiver V} {M : Type} [AddCommGroup M] (W W' : MeshWt Q M) : MeshWt Q M

The difference of two mesh weights.

theorem MultiplicativeBasisDeformations.MeshWalk.MeshWt.pw_map {V : Type} [Quiver V] {Q : TranslationQuiver V} {M N : Type} [AddCommGroup M] [AddCommGroup N] (h : M →+ N) (W : MeshWt Q M) {y x : V} (p : Quiver.Path y x) : (map h W).pw p = h (W.pw p)

theorem MultiplicativeBasisDeformations.MeshWalk.MeshWt.pw_sub {V : Type} [Quiver V] {Q : TranslationQuiver V} {M : Type} [AddCommGroup M] (W W' : MeshWt Q M) {y x : V} (p : Quiver.Path y x) : (W.sub W').pw p = W.pw p - W'.pw p

theorem MultiplicativeBasisDeformations.MeshWalk.MeshWt.rv_map {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 N : Type} [AddCommGroup M] [AddCommGroup N] (h : M →+ N) (W : MeshWt Q M) (t : Piece Q c v₀ D) : (map h W).rv t = h (W.rv t)

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

theorem MultiplicativeBasisDeformations.MeshWalk.WP_hom_ext {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} [AddCommGroup M] {f g : WP Q c v₀ D →+ M} (h : ∀ (t : Piece Q c v₀ D), f (cls Q c v₀ D t) = g (cls Q c v₀ D t)) : f = g

theorem MultiplicativeBasisDeformations.MeshWalk.MeshWt.res_map {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 N : Type} [AddCommGroup M] [AddCommGroup N] (h : M →+ N) (W : MeshWt Q M) : res c D (map h W) = h.comp (res c D W)

theorem MultiplicativeBasisDeformations.MeshWalk.MeshWt.res_sub {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} [AddCommGroup M] (W W' : MeshWt Q M) : res c D (W.sub W') = res c D W - res c D W'

theorem MultiplicativeBasisDeformations.MeshWalk.rowWt_eq_of_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)] (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))) {M : Type} [AddCommGroup M] (W W' : MeshWt Q M) (hres : MeshWt.res c D W = MeshWt.res c D W') (R : (x : ↑Q.nonprojective) × Quiver.Path ↑(Q.tau x) ↑x) : rowWt W R = rowWt W' R

Mesh weights with the same restriction give the same row weights.

theorem MultiplicativeBasisDeformations.MeshWalk.rowWt_map {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 N : Type} [AddCommGroup M] [AddCommGroup N] (h : M →+ N) (W : MeshWt Q M) (R : (x : ↑Q.nonprojective) × Quiver.Path ↑(Q.tau x) ↑x) : rowWt (MeshWt.map h W) R = h (rowWt W R)

theorem MultiplicativeBasisDeformations.MeshWalk.chars_part_of_basis {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)) (hmid : ∀ (x : ↑Q.nonprojective), Nonempty ((y : V) × (y ⟶ ↑x))) [Module.Free ℤ (WP Q c v₀ D)] [Module.Finite ℤ (WP Q c v₀ D)] (Wu : MeshWt Q (WP Q c v₀ D)) (hWu : MeshWt.res c D Wu = AddMonoidHom.id (WP Q c v₀ D)) {n : ℕ} (R : Fin n → (x : ↑Q.nonprojective) × Quiver.Path ↑(Q.tau x) ↑x) (hdual : ∀ (i : Fin n), ∃ (W : MeshWt Q ℤ), ∀ (j : Fin n), rowWt W (R j) = if j = i then 1 else 0) : ∃ (ι : Type) (b : Module.Basis ι ℤ (WP Q c v₀ D)) (j : Fin n → ι), Function.Injective j ∧ ∀ (i : Fin n), b (j i) = rowWt Wu (R i)

Proposition 7.5 (prop:primitive-parameter-characters): the residual characters are part of an integer basis of W(P).