Homogeneous module and arrow lifts (Proposition 7.6, weights)

weights-and-parameters.tex: "Lift a basis of the integer ray weights to mesh weights using Lemma 7.4. These give simultaneous gradings on the lifted modules. If μ has character χ, give ε weight −χ and choose the homogeneous solutions in the lemma. Then z_v has weight χ relative to its row."

The homogeneous solutions are obtained from arbitrary ones by taking weight parts: the lifted action equations and the arrow-lifting equations are linear, and all fixed maps in them shift weights, so the weight-χ parts of the corrections are again solutions (wLift, wLiftData). Their mesh errors shift by ν_x + χ (zE_wshift), hence lie in C(τx, x) of weight ν_x + χ (exists_liftData_wt).

def MultiplicativeBasisDeformations.MeshWalk.HasChar {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} {M : Type} [AddCommGroup M] (W : MeshWt Q M) (hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)) {L : CatAlg.LocalFamily (meshFam Q c)} (D : CatAlg.MeshData (meshFam Q c) L) (χ : M) (μ : (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ) : Prop

μ raises weights by χ.

Linear-map packaging

noncomputable def MultiplicativeBasisDeformations.MeshWalk.nuL {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} (hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)) {L : CatAlg.LocalFamily (meshFam Q c)} (D : CatAlg.MeshData (meshFam Q c) L) {q : ℕ} {μ : (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ} {X : V} (Lx : GExt.ActLift μ (↑q) (gmodEv D hfin X)) : (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] CatAlg.Rep D.F0 (meshFam Q c X) →ₗ[k] CatAlg.Rep D.F0 (meshFam Q c X)

The correction maps of a lifted action, linearly in the algebra element.

theorem MultiplicativeBasisDeformations.MeshWalk.nuL_apply {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} (hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)) {L : CatAlg.LocalFamily (meshFam Q c)} (D : CatAlg.MeshData (meshFam Q c) L) {q : ℕ} {μ : (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ} {X : V} (Lx : GExt.ActLift μ (↑q) (gmodEv D hfin X)) (a : (CatAlg.Alg D.F0)ᵐᵒᵖ) (m : CatAlg.Rep D.F0 (meshFam Q c X)) : ((nuL hfin D Lx) a) m = Lx.act m a

@[reducible, inline]

noncomputable abbrev MultiplicativeBasisDeformations.MeshWalk.actL {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} {L : CatAlg.LocalFamily (meshFam Q c)} (D : CatAlg.MeshData (meshFam Q c) L) (X : V) : (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] CatAlg.Rep D.F0 (meshFam Q c X) →ₗ[k] CatAlg.Rep D.F0 (meshFam Q c X)

The right action, linearly in the algebra element.

noncomputable def MultiplicativeBasisDeformations.MeshWalk.prL {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} {M : Type} [AddCommGroup M] (W : MeshWt Q M) (hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)) {L : CatAlg.LocalFamily (meshFam Q c)} (D : CatAlg.MeshData (meshFam Q c) L) (X : V) (γ : M) : (CatAlg.Rep D.F0 (meshFam Q c X) →ₗ[k] CatAlg.Rep D.F0 (meshFam Q c X)) →ₗ[k] CatAlg.Rep D.F0 (meshFam Q c X) →ₗ[k] CatAlg.Rep D.F0 (meshFam Q c X)

The weight part of an endomorphism of M_X, as a linear map.

noncomputable def MultiplicativeBasisDeformations.MeshWalk.wnu {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} {M : Type} [AddCommGroup M] (W : MeshWt Q M) (hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)) {L : CatAlg.LocalFamily (meshFam Q c)} (D : CatAlg.MeshData (meshFam Q c) L) {q : ℕ} {μ : (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ} (χ : M) {X : V} (Lx : GExt.ActLift μ (↑q) (gmodEv D hfin X)) : (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] CatAlg.Rep D.F0 (meshFam Q c X) →ₗ[k] CatAlg.Rep D.F0 (meshFam Q c X)

The weight-χ part of a lifted action.

theorem MultiplicativeBasisDeformations.MeshWalk.wnu_hom {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} {M : Type} [AddCommGroup M] (W : MeshWt Q M) (hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)) {L : CatAlg.LocalFamily (meshFam Q c)} (D : CatAlg.MeshData (meshFam Q c) L) {q : ℕ} {μ : (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ} (χ : M) {X : V} (Lx : GExt.ActLift μ (↑q) (gmodEv D hfin X)) {α : M} {a : (CatAlg.Alg D.F0)ᵐᵒᵖ} (ha : (grA0 W hfin D).IsHom α a) : (wnu W hfin D χ Lx) a = (grEv W hfin D X).pr (grEv W hfin D X) (α + χ) (Lx.ν (GExt.single a))

theorem MultiplicativeBasisDeformations.MeshWalk.wnu_equation_hom {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} {M : Type} [AddCommGroup M] {W : MeshWt Q M} {hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)} {L : CatAlg.LocalFamily (meshFam Q c)} {D : CatAlg.MeshData (meshFam Q c) L} {q : ℕ} {μ : (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ} {χ : M} (hμχ : HasChar W hfin D χ μ) {X : V} (Lx : GExt.ActLift μ (↑q) (gmodEv D hfin X)) {α β : M} {a b : (CatAlg.Alg D.F0)ᵐᵒᵖ} (ha : (grA0 W hfin D).IsHom α a) (hb : (grA0 W hfin D).IsHom β b) : (wnu W hfin D χ Lx) b ∘ₗ (actL D X) a - (wnu W hfin D χ Lx) (a * b) + (actL D X) b ∘ₗ (wnu W hfin D χ Lx) a = (actL D X) ((μ a) b)

noncomputable def MultiplicativeBasisDeformations.MeshWalk.eqDefect {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} {M : Type} [AddCommGroup M] {W : MeshWt Q M} {hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)} {L : CatAlg.LocalFamily (meshFam Q c)} {D : CatAlg.MeshData (meshFam Q c) L} {q : ℕ} {μ : (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ} {χ : M} {X : V} (Lx : GExt.ActLift μ (↑q) (gmodEv D hfin X)) : (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] CatAlg.Rep D.F0 (meshFam Q c X) →ₗ[k] CatAlg.Rep D.F0 (meshFam Q c X)

The defect of the lifted action equation, bilinearly.

theorem MultiplicativeBasisDeformations.MeshWalk.eqDefect_eq_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} {M : Type} [AddCommGroup M] {W : MeshWt Q M} {hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)} {L : CatAlg.LocalFamily (meshFam Q c)} {D : CatAlg.MeshData (meshFam Q c) L} {q : ℕ} {μ : (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ} {χ : M} (hμχ : HasChar W hfin D χ μ) {X : V} (Lx : GExt.ActLift μ (↑q) (gmodEv D hfin X)) : eqDefect Lx = 0

theorem MultiplicativeBasisDeformations.MeshWalk.wnu_equation {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} {M : Type} [AddCommGroup M] {W : MeshWt Q M} {hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)} {L : CatAlg.LocalFamily (meshFam Q c)} {D : CatAlg.MeshData (meshFam Q c) L} {q : ℕ} {μ : (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ} {χ : M} (hμχ : HasChar W hfin D χ μ) {X : V} (Lx : GExt.ActLift μ (↑q) (gmodEv D hfin X)) (a b : (CatAlg.Alg D.F0)ᵐᵒᵖ) : (wnu W hfin D χ Lx) b ∘ₗ (actL D X) a - (wnu W hfin D χ Lx) (a * b) + (actL D X) b ∘ₗ (wnu W hfin D χ Lx) a = (actL D X) ((μ a) b)

theorem MultiplicativeBasisDeformations.MeshWalk.wnu_zgr {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} {M : Type} [AddCommGroup M] {W : MeshWt Q M} {hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)} {L : CatAlg.LocalFamily (meshFam Q c)} {D : CatAlg.MeshData (meshFam Q c) L} {q : ℕ} {μ : (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ} {χ : M} {X : V} (Lx : GExt.ActLift μ (↑q) (gmodEv D hfin X)) {p d : ℤ} {a : (CatAlg.Alg D.F0)ᵐᵒᵖ} (ha : (galgA0 D hfin).gr.IsHom d a) {m : CatAlg.Rep D.F0 (meshFam Q c X)} (hm : (zgrEv D hfin X).IsHom p m) : (zgrEv D hfin X).IsHom (p + d + ↑q) (((wnu W hfin D χ Lx) a) m)

noncomputable def MultiplicativeBasisDeformations.MeshWalk.wLift {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} {M : Type} [AddCommGroup M] {W : MeshWt Q M} {hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)} {L : CatAlg.LocalFamily (meshFam Q c)} {D : CatAlg.MeshData (meshFam Q c) L} {q : ℕ} {μ : (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ} {χ : M} (hμχ : HasChar W hfin D χ μ) {X : V} (Lx : GExt.ActLift μ (↑q) (gmodEv D hfin X)) : GExt.ActLift μ (↑q) (gmodEv D hfin X)

The homogeneous lifted action.

theorem MultiplicativeBasisDeformations.MeshWalk.wLift_act {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} {M : Type} [AddCommGroup M] {W : MeshWt Q M} {hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)} {L : CatAlg.LocalFamily (meshFam Q c)} {D : CatAlg.MeshData (meshFam Q c) L} {q : ℕ} {μ : (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ} {χ : M} (hμχ : HasChar W hfin D χ μ) {X : V} (Lx : GExt.ActLift μ (↑q) (gmodEv D hfin X)) (m : CatAlg.Rep D.F0 (meshFam Q c X)) (a : (CatAlg.Alg D.F0)ᵐᵒᵖ) : (wLift hμχ Lx).act m a = ((wnu W hfin D χ Lx) a) m

Homogeneous arrow lifts

noncomputable def MultiplicativeBasisDeformations.MeshWalk.wg {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} {M : Type} [AddCommGroup M] (W : MeshWt Q M) {hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)} {L : CatAlg.LocalFamily (meshFam Q c)} {D : CatAlg.MeshData (meshFam Q c) L} {q : ℕ} {μ : (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ} (χ : M) (Ld : LiftData D hfin q μ) {y x : V} (a : y ⟶ x) : CatAlg.Rep D.F0 (meshFam Q c y) →ₗ[k] CatAlg.Rep D.F0 (meshFam Q c x)

The weight part of an arrow lift.

noncomputable def MultiplicativeBasisDeformations.MeshWalk.liftDefect {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} {M : Type} [AddCommGroup M] (W : MeshWt Q M) {hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)} {L : CatAlg.LocalFamily (meshFam Q c)} {D : CatAlg.MeshData (meshFam Q c) L} {q : ℕ} {μ : (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ} {χ : M} (Ld : LiftData D hfin q μ) {y x : V} (a : y ⟶ x) : (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] CatAlg.Rep D.F0 (meshFam Q c y) →ₗ[k] CatAlg.Rep D.F0 (meshFam Q c x)

The defect of the arrow-lifting equation, linearly in the algebra element.

theorem MultiplicativeBasisDeformations.MeshWalk.liftDefect_eq_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} {M : Type} [AddCommGroup M] {W : MeshWt Q M} {hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)} {L : CatAlg.LocalFamily (meshFam Q c)} {D : CatAlg.MeshData (meshFam Q c) L} {q : ℕ} {μ : (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ} {χ : M} (Ld : LiftData D hfin q μ) {y x : V} (a : y ⟶ x) : liftDefect W Ld a = 0

theorem MultiplicativeBasisDeformations.MeshWalk.wg_zgr {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} {M : Type} [AddCommGroup M] {W : MeshWt Q M} {hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)} {L : CatAlg.LocalFamily (meshFam Q c)} {D : CatAlg.MeshData (meshFam Q c) L} {q : ℕ} {μ : (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ} {χ : M} (Ld : LiftData D hfin q μ) {y x : V} (a : y ⟶ x) (p : ℤ) (m : CatAlg.Rep D.F0 (meshFam Q c y)) (hm : (zgrEv D hfin y).IsHom p m) : (zgrEv D hfin x).IsHom (p + (1 + ↑q)) ((wg W χ Ld a) m)

noncomputable def MultiplicativeBasisDeformations.MeshWalk.wLiftData {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} {M : Type} [AddCommGroup M] (W : MeshWt Q M) {hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)} {L : CatAlg.LocalFamily (meshFam Q c)} {D : CatAlg.MeshData (meshFam Q c) L} {q : ℕ} {μ : (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ} (χ : M) (hμχ : HasChar W hfin D χ μ) (Ld : LiftData D hfin q μ) : LiftData D hfin q μ

The homogeneous lift data.

theorem MultiplicativeBasisDeformations.MeshWalk.wLiftData_g {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} {M : Type} [AddCommGroup M] {W : MeshWt Q M} {hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)} {L : CatAlg.LocalFamily (meshFam Q c)} {D : CatAlg.MeshData (meshFam Q c) L} {q : ℕ} {μ : (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ} {χ : M} (hμχ : HasChar W hfin D χ μ) (Ld : LiftData D hfin q μ) {y x : V} (a : y ⟶ x) : (wLiftData W χ hμχ Ld).g a = wg W χ Ld a

theorem MultiplicativeBasisDeformations.MeshWalk.zE_wshift {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} {M : Type} [AddCommGroup M] {W : MeshWt Q M} {hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)} {L : CatAlg.LocalFamily (meshFam Q c)} {D : CatAlg.MeshData (meshFam Q c) L} {q : ℕ} {μ : (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ} {χ : M} (hμχ : HasChar W hfin D χ μ) (Ld : LiftData D hfin q μ) (x : ↑Q.nonprojective) : (grEv W hfin D ↑(Q.tau x)).Shift (grEv W hfin D ↑x) (W.ν x + χ) (zE (wLiftData W χ hμχ Ld) x)

The mesh errors of the homogeneous lift data shift by ν_x + χ.

theorem MultiplicativeBasisDeformations.MeshWalk.zhat_wLiftData {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} {M : Type} [AddCommGroup M] {W : MeshWt Q M} {hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)} {L : CatAlg.LocalFamily (meshFam Q c)} {D : CatAlg.MeshData (meshFam Q c) L} {q : ℕ} {μ : (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ} {χ : M} [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] (hμχ : HasChar W hfin D χ μ) (Ld : LiftData D hfin q μ) (x : ↑Q.nonprojective) : zhat (wLiftData W χ hμχ Ld) x ∈ wP c W (W.ν x + χ) ↑(Q.tau x) ↑x

Proposition 7.6, weights: a cocycle of character χ has lift data whose mesh errors have weight χ relative to their rows.