Proposition 7.2(1): W(P) ≅ ℤ^{n−1} ⊕ G_ab

weights-and-parameters.tex (prop:integral-ray-weights(1)): "There is an identification W(P) = (I_𝓛)_G […] the class θ_g of e_{gx} − e_x is independent of the object x, and g ↦ θ_g identifies G_ab with a direct summand of W(P) with complement ℤ^{n−1}: W(P) ≅ ℤ^{n−1} ⊕ G_ab."

With the deck group G of the base component (Hs, the stabilizer of the component 𝓛₀ of the base object in the deck group of the coned complex; see RayWeights.lean):

• W(P) = (I_𝓛₀)_G: [Σ v_o e_o] ↦ Σ v_o ζ(o) is an isomorphism (coinvEquiv), with inverse βW built from Ψ;
• the comparison Ψ of RayWeights.lean is an isomorphism onto the vectors with coordinate sum zero times G_ab (ΨW_ΦW, WPequiv), hence W(P) ≃ ℤ^{n−1} × G_ab (WPequivFree);
• θ_g = ζ(gx) − ζ(x) does not depend on x in 𝓛₀ and is the G_ab summand under WPequivFree (theta_summand). W(P) is free of finite rank (WP_free, WP_finite).

theorem MultiplicativeBasisDeformations.MeshWalk.grp_conj' {G : Type u_2} [Group G] (x y z w : G) : z * (x⁻¹ * (y * w⁻¹)) = (x * z⁻¹)⁻¹ * (y * w⁻¹)

theorem MultiplicativeBasisDeformations.MeshWalk.grp_mul_inv' {G : Type u_2} [Group G] (x : G) : x * x⁻¹ = 1

theorem MultiplicativeBasisDeformations.MeshWalk.grp_g1 {G : Type u_2} [Group G] (g a : G) : g * 1 * a⁻¹ = g * (1 * a⁻¹)

noncomputable def MultiplicativeBasisDeformations.MeshWalk.κ {k : Type u_1} [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₀) (o : LObj Q c v₀ D) (ho : conn Q c v₀ D (o₀ Q c v₀ D x₀) o) : Additive (Abelianization ↥(Hs Q c v₀ D x₀))

The class in H_ab of an object of the base component: κ(x, b) = b · a_x⁻¹.

theorem MultiplicativeBasisDeformations.MeshWalk.κ_indep {k : Type u_1} [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₀) (o : LObj Q c v₀ D) (ho ho' : conn Q c v₀ D (o₀ Q c v₀ D x₀) o) : κ hconn o ho = κ hconn o ho'

theorem MultiplicativeBasisDeformations.MeshWalk.nz_of_line {k : Type u_1} [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} (h : Thin.Line o o') : NZ Q c v₀ D (o.1, o'.1, o.2⁻¹ * o'.2)

theorem MultiplicativeBasisDeformations.MeshWalk.ΨW_zeta_sub {k : Type u_1} [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) {o o' : LObj Q c v₀ D} (h : conn Q c v₀ D o o') (ho : conn Q c v₀ D (o₀ Q c v₀ D x₀) o) : (ΨW hconn) (ζ o' - ζ o) = (Pi.single o'.1 1 - Pi.single o.1 1, κ hconn o' ⋯ - κ hconn o ho)

Ψ on differences of object values in the base component.

theorem MultiplicativeBasisDeformations.MeshWalk.κ_aL {k : Type u_1} [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) : κ hconn (x, aL hconn x) ⋯ = 0

theorem MultiplicativeBasisDeformations.MeshWalk.conn_o₀_gL {k : Type u_1} [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} (g : ↥(Hs Q c v₀ D x₀)) : conn Q c v₀ D (o₀ Q c v₀ D x₀) (gL Q c v₀ D (↑g) (o₀ Q c v₀ D x₀))

theorem MultiplicativeBasisDeformations.MeshWalk.ΦW_inr {k : Type u_1} [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) (g : ↥(Hs Q c v₀ D x₀)) : (ΦW hconn hζ) (0, Additive.ofMul (Abelianization.of g)) = ζ (gL Q c v₀ D (↑g) (o₀ Q c v₀ D x₀)) - ζ (o₀ Q c v₀ D x₀)

theorem MultiplicativeBasisDeformations.MeshWalk.ΦW_inl {k : Type u_1} [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) (v : D.PV → ℤ) : (ΦW hconn hζ) (v, 0) = ∑ x : D.PV, v x • ζ (mkL Q c v₀ D x (aL hconn x))

theorem MultiplicativeBasisDeformations.MeshWalk.ΨW_ΦW {k : Type u_1} [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) (p : Tgt Q c v₀ D x₀) (hp : ∑ x : D.PV, p.1 x = 0) : (ΨW hconn) ((ΦW hconn hζ) p) = p

Ψ ∘ Φ = 1 on the vectors with coordinate sum zero.

def MultiplicativeBasisDeformations.MeshWalk.SumZero {k : Type u_1} [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} : AddSubgroup (Tgt Q c v₀ D x₀)

The vectors with coordinate sum zero, times H_ab.

theorem MultiplicativeBasisDeformations.MeshWalk.ΨW_mem {k : Type u_1} [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₀) (w : WP Q c v₀ D) : (ΨW hconn) w ∈ SumZero

noncomputable def MultiplicativeBasisDeformations.MeshWalk.WPequiv {k : Type u_1} [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) : WP Q c v₀ D ≃+ ↥SumZero

W(P) ≅ {v : Σ v = 0} × G_ab (Proposition 7.2(1)).

theorem MultiplicativeBasisDeformations.MeshWalk.sum_split {k : Type u_1} [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} [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} (f : D.PV → ℤ) : ∑ x : D.PV, f x = f x₀ + ∑ y : { x : D.PV // x ≠ x₀ }, f ↑y

def MultiplicativeBasisDeformations.MeshWalk.sumZeroEquiv {k : Type u_1} [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₀) : ↥SumZero ≃+ ({ x : D.PV // x ≠ x₀ } → ℤ) × Additive (Abelianization ↥(Hs Q c v₀ D x₀))

The vectors with coordinate sum zero are ℤ^{n−1}: forget the base coordinate.

noncomputable def MultiplicativeBasisDeformations.MeshWalk.WPequivFree {k : Type u_1} [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) : WP Q c v₀ D ≃+ ({ x : D.PV // x ≠ x₀ } → ℤ) × Additive (Abelianization ↥(Hs Q c v₀ D x₀))

Proposition 7.2(1): W(P) ≅ ℤ^{n−1} ⊕ G_ab, with G the (free) deck group of the base component and n the number of labels.

theorem MultiplicativeBasisDeformations.MeshWalk.theta_summand {k : Type u_1} [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) (g : ↥(Hs Q c v₀ D x₀)) (o : LObj Q c v₀ D) (ho : conn Q c v₀ D (o₀ Q c v₀ D x₀) o) : (WPequivFree hconn hζ) (ζ (gL Q c v₀ D (↑g) o) - ζ o) = (0, Additive.ofMul (Abelianization.of g))

θ_g = ζ(gx) − ζ(x) for every x of the base component, and under WPequivFree it is the G_ab summand: g ↦ θ_g identifies G_ab with a direct summand with complement ℤ^{n−1}.

The identification W(P) = (I_𝓛)_G

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.MeshWalk.L0 {k : Type u_1} [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) : Type

The base component 𝓛₀ of the lifted projective category.

def MultiplicativeBasisDeformations.MeshWalk.actL0 {k : Type u_1} [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} (g : ↥(Hs Q c v₀ D x₀)) (o : L0 Q c v₀ D x₀) : L0 Q c v₀ D x₀

The deck action of G = H on 𝓛₀.

noncomputable def MultiplicativeBasisDeformations.MeshWalk.coefSum {k : Type u_1} [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) : (L0 Q c v₀ D x₀ →₀ ℤ) →+ ℤ

The sum of coefficients.

@[reducible, inline]

noncomputable abbrev MultiplicativeBasisDeformations.MeshWalk.IL {k : Type u_1} [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) : AddSubgroup (L0 Q c v₀ D x₀ →₀ ℤ)

I_𝓛: finite sums with coefficient sum zero.

noncomputable def MultiplicativeBasisDeformations.MeshWalk.actF {k : Type u_1} [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} (g : ↥(Hs Q c v₀ D x₀)) : (L0 Q c v₀ D x₀ →₀ ℤ) →+ L0 Q c v₀ D x₀ →₀ ℤ

The deck action on finite sums.

theorem MultiplicativeBasisDeformations.MeshWalk.coefSum_actF {k : Type u_1} [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} (g : ↥(Hs Q c v₀ D x₀)) (v : L0 Q c v₀ D x₀ →₀ ℤ) : (coefSum Q c v₀ D x₀) ((actF g) v) = (coefSum Q c v₀ D x₀) v

noncomputable def MultiplicativeBasisDeformations.MeshWalk.relG {k : Type u_1} [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) : AddSubgroup ↥(IL Q c v₀ D x₀)

The relations g·v − v of the coinvariants.

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.MeshWalk.Coinv {k : Type u_1} [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 coinvariants (I_𝓛)_G.

noncomputable def MultiplicativeBasisDeformations.MeshWalk.αF {k : Type u_1} [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 → WP Q c v₀ D} : (L0 Q c v₀ D x₀ →₀ ℤ) →+ WP Q c v₀ D

The values of ζ on finite sums.

theorem MultiplicativeBasisDeformations.MeshWalk.zeta_act_sub {k : Type u_1} [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) (g : ↥(Hs Q c v₀ D x₀)) (o : L0 Q c v₀ D x₀) : ζ ↑(actL0 g o) - ζ ↑o = ζ (gL Q c v₀ D (↑g) (o₀ Q c v₀ D x₀)) - ζ (o₀ Q c v₀ D x₀)

ζ(g o) − ζ(o) does not depend on o in the base component.

theorem MultiplicativeBasisDeformations.MeshWalk.αF_actF {k : Type u_1} [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) (g : ↥(Hs Q c v₀ D x₀)) (v : L0 Q c v₀ D x₀ →₀ ℤ) : αF ((actF g) v) = αF v + (coefSum Q c v₀ D x₀) v • (ζ (gL Q c v₀ D (↑g) (o₀ Q c v₀ D x₀)) - ζ (o₀ Q c v₀ D x₀))

noncomputable def MultiplicativeBasisDeformations.MeshWalk.αbar {k : Type u_1} [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) : Coinv Q c v₀ D x₀ →+ WP Q c v₀ D

The comparison (I_𝓛)_G → W(P), [Σ v_o e_o] ↦ Σ v_o ζ(o).

theorem MultiplicativeBasisDeformations.MeshWalk.αbar_mk {k : Type u_1} [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) (v : ↥(IL Q c v₀ D x₀)) : (αbar hconn hζ) ↑v = αF ↑v

def MultiplicativeBasisDeformations.MeshWalk.b0 {k : Type u_1} [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} : L0 Q c v₀ D x₀

The base point of 𝓛₀.

noncomputable def MultiplicativeBasisDeformations.MeshWalk.bL {k : Type u_1} [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) : L0 Q c v₀ D x₀

The chosen lift of a label in 𝓛₀.

noncomputable def MultiplicativeBasisDeformations.MeshWalk.gen {k : Type u_1} [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} (o : L0 Q c v₀ D x₀) : ↥(IL Q c v₀ D x₀)

The generator e_o − e_{o₀} of I_𝓛.

noncomputable def MultiplicativeBasisDeformations.MeshWalk.τgen {k : Type u_1} [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} (g : ↥(Hs Q c v₀ D x₀)) : Coinv Q c v₀ D x₀

The class τ(g) = [e_{g o₀} − e_{o₀}].

theorem MultiplicativeBasisDeformations.MeshWalk.actL0_mul {k : Type u_1} [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} (g h : ↥(Hs Q c v₀ D x₀)) (o : L0 Q c v₀ D x₀) : actL0 (g * h) o = actL0 g (actL0 h o)

theorem MultiplicativeBasisDeformations.MeshWalk.mk_actF {k : Type u_1} [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} (g : ↥(Hs Q c v₀ D x₀)) (v : ↥(IL Q c v₀ D x₀)) (hv : (actF g) ↑v ∈ IL Q c v₀ D x₀) : ↑⟨(actF g) ↑v, hv⟩ = ↑v

theorem MultiplicativeBasisDeformations.MeshWalk.mk_gen_act {k : Type u_1} [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} (g : ↥(Hs Q c v₀ D x₀)) (o : L0 Q c v₀ D x₀) : ↑(gen (actL0 g o)) = ↑(gen o) + τgen g

[e_{g b} − e_{o₀}] = [e_b − e_{o₀}] + τ(g).

noncomputable def MultiplicativeBasisDeformations.MeshWalk.τhom {k : Type u_1} [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} : ↥(Hs Q c v₀ D x₀) →* Multiplicative (Coinv Q c v₀ D x₀)

τ is a homomorphism.

noncomputable def MultiplicativeBasisDeformations.MeshWalk.γW {k : Type u_1} [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₀) : Tgt Q c v₀ D x₀ →+ Coinv Q c v₀ D x₀

The map ℤ^{labels} × G_ab → (I_𝓛)_G.

noncomputable def MultiplicativeBasisDeformations.MeshWalk.βW {k : Type u_1} [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 →+ Coinv Q c v₀ D x₀

The inverse comparison W(P) → (I_𝓛)_G.

noncomputable def MultiplicativeBasisDeformations.MeshWalk.κ' {k : Type u_1} [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₀) (o : L0 Q c v₀ D x₀) : ↥(Hs Q c v₀ D x₀)

The class κ'(o) = o.2 · a_{o.1}⁻¹ ∈ G of an object of 𝓛₀.

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

theorem MultiplicativeBasisDeformations.MeshWalk.actL0_κ' {k : Type u_1} [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₀) (o : L0 Q c v₀ D x₀) : actL0 (κ' hconn o) (bL hconn (↑o).1) = o

theorem MultiplicativeBasisDeformations.MeshWalk.mk_gen_eq {k : Type u_1} [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₀) (o : L0 Q c v₀ D x₀) : ↑(gen o) = ↑(gen (bL hconn (↑o).1)) + τgen (κ' hconn o)

theorem MultiplicativeBasisDeformations.MeshWalk.gen_b0 {k : Type u_1} [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} : gen b0 = 0

theorem MultiplicativeBasisDeformations.MeshWalk.βW_gen {k : Type u_1} [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) (o : L0 Q c v₀ D x₀) : (βW hconn) ((αbar hconn hζ) ↑(gen o)) = ↑(gen o)

theorem MultiplicativeBasisDeformations.MeshWalk.mk_eq_sum {k : Type u_1} [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} (v : ↥(IL Q c v₀ D x₀)) : ↑v = ∑ o ∈ (↑v).support, ↑v o • ↑(gen o)

theorem MultiplicativeBasisDeformations.MeshWalk.βW_αbar {k : Type u_1} [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) (q : Coinv Q c v₀ D x₀) : (βW hconn) ((αbar hconn hζ) q) = q

theorem MultiplicativeBasisDeformations.MeshWalk.αbar_γW {k : Type u_1} [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) (p : Tgt Q c v₀ D x₀) (hp : ∑ x : D.PV, p.1 x = 0) : (αbar hconn hζ) ((γW hconn) p) = (ΦW hconn hζ) p

theorem MultiplicativeBasisDeformations.MeshWalk.αbar_βW {k : Type u_1} [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) : (αbar hconn hζ) ((βW hconn) w) = w

noncomputable def MultiplicativeBasisDeformations.MeshWalk.coinvEquiv {k : Type u_1} [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) : Coinv Q c v₀ D x₀ ≃+ WP Q c v₀ D

The identification W(P) = (I_𝓛)_G (Proposition 7.2(1)): [Σ v_o e_o] ↦ Σ v_o ζ(o), for the base component 𝓛₀ and its deck group G.

theorem MultiplicativeBasisDeformations.MeshWalk.coinvEquiv_line {k : Type u_1} [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) (o o' : L0 Q c v₀ D x₀) (h : Thin.Line ↑o ↑o') : (coinvEquiv hconn hζ) (↑(gen o') - ↑(gen o)) = wtL Q c v₀ D ↑o ↑o'

The identification on rays (Proposition 7.2(1)): the class of e_{o'} − e_o = (e_{o'} − e_{o₀}) − (e_o − e_{o₀}) for a lifted ray o → o' corresponds to the weight class of that ray.

theorem MultiplicativeBasisDeformations.MeshWalk.coinvEquiv_symm_line {k : Type u_1} [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) (o o' : L0 Q c v₀ D x₀) (h : Thin.Line ↑o ↑o') : (coinvEquiv hconn hζ).symm (wtL Q c v₀ D ↑o ↑o') = ↑(gen o') - ↑(gen o)

The inverse direction of coinvEquiv_line: a lifted ray r : o → o' goes to [e_{o'} − e_o].