Hochschild classes and mesh corrections (Proposition 7.6, the map Ψ)

weights-and-parameters.tex (prop:hochschild-mesh-restriction): "Represent a homogeneous class by a normalized relative cocycle μ. Apply Lemma 6.6 with R = k, Λ = A₀ and the normalized modules, using Lemma 6.3. Choose the actual projectives at their labels, give ε degree −q, and lift the arrows homogeneously to the Hom category of the lifted modules. Each mesh error reduces to zero, so by the freeness in Lemma 6.6 it is ε times a map of the original category. Thus the mesh errors are εz_v with z_v ∈ C_{q+2}(τv, v). Changing the arrow lifts by εf_a changes their tuple by D_{q+1}f."

Here: the arrow maps fA on evaluated modules, the choice data LiftData (module lifts and arrow lifts), the mesh error zE, its representative zhat ∈ C_{q+2}(τx, x), and the class Ψ ∈ coker D_{q+1}.

theorem MultiplicativeBasisDeformations.MeshWalk.mesh_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} [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] (x : ↑Q.nonprojective) : ∑ a : (y : V) × (y ⟶ ↑x), ↑(c x a.fst a.snd) • CategoryTheory.CategoryStruct.comp (ScalarMeshCategory.arrowMor c ((Q.mate x a.fst) a.snd)) (ScalarMeshCategory.arrowMor c a.snd) = 0

The mesh relation holds in C.

Arrow maps and lift data

noncomputable def MultiplicativeBasisDeformations.MeshWalk.fA {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) {y x : V} (a : y ⟶ x) : CatAlg.Rep D.F0 (meshFam Q c y) →ₗ[k] CatAlg.Rep D.F0 (meshFam Q c x)

The arrow map M_y → M_x of evaluated modules.

theorem MultiplicativeBasisDeformations.MeshWalk.fA_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} {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) (m : CatAlg.Rep D.F0 (meshFam Q c y)) (b : (CatAlg.Alg D.F0)ᵐᵒᵖ) : (fA D a) (((evAct D y) m) b) = ((evAct D x) ((fA D a) m)) b

theorem MultiplicativeBasisDeformations.MeshWalk.arrowMor_mem_degreePart {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} [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] {y x : V} (a : y ⟶ x) : ScalarMeshCategory.arrowMor c a ∈ ScalarMeshCategory.degreePart c 1 y x

theorem MultiplicativeBasisDeformations.MeshWalk.fA_deg {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) (hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)) [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] {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) ((fA D a) m)

structure MultiplicativeBasisDeformations.MeshWalk.LiftData {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) (hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)) (q : ℕ) (μ : (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ) : Type u

Choices for Ψ: lifted actions on all evaluated modules and lifts of the arrow maps, homogeneous of degree 1 + q.

• L (X : V) : GExt.ActLift μ (↑q) (gmodEv D hfin X)
• g {y x : V} : (y ⟶ x) → CatAlg.Rep D.F0 (meshFam Q c y) →ₗ[k] CatAlg.Rep D.F0 (meshFam Q c x)
• lift {y x : V} (a : y ⟶ x) : GExt.IsLiftHom (self.L y) (self.L x) (fA D a) (self.g a)
• deg {y x : V} (a : y ⟶ x) (p : ℤ) (m : CatAlg.Rep D.F0 (meshFam Q c y)) : (zgrEv D hfin y).IsHom p m → (zgrEv D hfin x).IsHom (p + (1 + ↑q)) ((self.g a) m)

theorem MultiplicativeBasisDeformations.MeshWalk.isLiftHom_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} {L : CatAlg.LocalFamily (meshFam Q c)} {D : CatAlg.MeshData (meshFam Q c) L} {hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)} [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] {q : ℕ} {μ : (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ} {M : Type u_1} {N : Type u_2} [AddCommGroup M] [Module k M] [AddCommGroup N] [Module k N] {MM : GExt.GMod (galgA0 D hfin) M} {NN : GExt.GMod (galgA0 D hfin) N} {L₁ : GExt.ActLift μ (↑q) MM} {L₂ : GExt.ActLift μ (↑q) NN} : GExt.IsLiftHom L₁ L₂ 0 0

theorem MultiplicativeBasisDeformations.MeshWalk.IsLiftHom.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} {L : CatAlg.LocalFamily (meshFam Q c)} {D : CatAlg.MeshData (meshFam Q c) L} {hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)} [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] {q : ℕ} {μ : (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ} {M : Type u_1} {N : Type u_2} [AddCommGroup M] [Module k M] [AddCommGroup N] [Module k N] {MM : GExt.GMod (galgA0 D hfin) M} {NN : GExt.GMod (galgA0 D hfin) N} {L₁ : GExt.ActLift μ (↑q) MM} {L₂ : GExt.ActLift μ (↑q) NN} {ι : Type u_3} (s : Finset ι) {f g : ι → M →ₗ[k] N} (h : ∀ i ∈ s, GExt.IsLiftHom L₁ L₂ (f i) (g i)) : GExt.IsLiftHom L₁ L₂ (∑ i ∈ s, f i) (∑ i ∈ s, g i)

noncomputable def MultiplicativeBasisDeformations.MeshWalk.zE {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} {hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)} {q : ℕ} {μ : (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ} (Ld : LiftData D hfin q μ) (x : ↑Q.nonprojective) : CatAlg.Rep D.F0 (meshFam Q c ↑(Q.tau x)) →ₗ[k] CatAlg.Rep D.F0 (meshFam Q c ↑x)

The mesh error Σ_a c_{x,a} (f_a g_{σa} + g_a f_{σa}) at a row.

theorem MultiplicativeBasisDeformations.MeshWalk.mesh_fA {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} [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] (x : ↑Q.nonprojective) : ∑ a : (y : V) × (y ⟶ ↑x), ↑(c x a.fst a.snd) • fA D a.snd ∘ₗ fA D ((Q.mate x a.fst) a.snd) = 0

theorem MultiplicativeBasisDeformations.MeshWalk.zE_lift {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} {hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)} [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] {q : ℕ} {μ : (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ} (Ld : LiftData D hfin q μ) (x : ↑Q.nonprojective) : GExt.IsLiftHom (Ld.L ↑(Q.tau x)) (Ld.L ↑x) 0 (zE Ld x)

theorem MultiplicativeBasisDeformations.MeshWalk.zE_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} {L : CatAlg.LocalFamily (meshFam Q c)} {D : CatAlg.MeshData (meshFam Q c) L} {hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)} [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] {q : ℕ} {μ : (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ} (Ld : LiftData D hfin q μ) (x : ↑Q.nonprojective) (m : CatAlg.Rep D.F0 (meshFam Q c ↑(Q.tau x))) (b : (CatAlg.Alg D.F0)ᵐᵒᵖ) : (zE Ld x) (((evAct D ↑(Q.tau x)) m) b) = ((evAct D ↑x) ((zE Ld x) m)) b

The representative zhat and the class Ψ

theorem MultiplicativeBasisDeformations.MeshWalk.mem_degreePart_of_repMap {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) (hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)) [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] {X Y : V} {f : ScalarMeshCategory.obj c X ⟶ ScalarMeshCategory.obj c Y} {r : ℕ} (h : ∀ (p : ℤ) (m : CatAlg.Rep D.F0 (meshFam Q c X)), (zgrEv D hfin X).IsHom p m → (zgrEv D hfin Y).IsHom (p + ↑r) ((↑k (CatAlg.repMap f)) m)) : f ∈ ScalarMeshCategory.degreePart c r X Y

A homogeneous A₀-map between evaluated modules comes from C in that degree.

theorem MultiplicativeBasisDeformations.MeshWalk.zE_deg {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} {hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)} [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] {q : ℕ} {μ : (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ} (Ld : LiftData D hfin q μ) (x : ↑Q.nonprojective) (p : ℤ) (m : CatAlg.Rep D.F0 (meshFam Q c ↑(Q.tau x))) (hm : (zgrEv D hfin ↑(Q.tau x)).IsHom p m) : (zgrEv D hfin ↑x).IsHom (p + ↑(q + 2)) ((zE Ld x) m)

noncomputable def MultiplicativeBasisDeformations.MeshWalk.zhat {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} {hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)} [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] {q : ℕ} {μ : (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ} (Ld : LiftData D hfin q μ) (x : ↑Q.nonprojective) : ScalarMeshCategory.obj c ↑(Q.tau x) ⟶ ScalarMeshCategory.obj c ↑x

The mesh error as a morphism of C: z_x ∈ C_{q+2}(τx, x).

theorem MultiplicativeBasisDeformations.MeshWalk.zhat_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} {L : CatAlg.LocalFamily (meshFam Q c)} {D : CatAlg.MeshData (meshFam Q c) L} {hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)} [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] {q : ℕ} {μ : (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ} (Ld : LiftData D hfin q μ) (x : ↑Q.nonprojective) : zE Ld x = ↑k (CatAlg.repMap (zhat Ld x))

theorem MultiplicativeBasisDeformations.MeshWalk.zhat_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} {L : CatAlg.LocalFamily (meshFam Q c)} {D : CatAlg.MeshData (meshFam Q c) L} {hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)} [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] {q : ℕ} {μ : (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ} (Ld : LiftData D hfin q μ) (x : ↑Q.nonprojective) : zhat Ld x ∈ ScalarMeshCategory.degreePart c (q + 2) ↑(Q.tau x) ↑x

noncomputable def MultiplicativeBasisDeformations.MeshWalk.Ψc {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} {hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)} [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] {q : ℕ} {μ : (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ} (Ld : LiftData D hfin q μ) : ScalarMeshCategory.Coker c (q + 1)

The class Ψ of the mesh errors in coker D_{q+1}.

Independence of the arrow lifts

@[reducible, inline]

noncomputable abbrev MultiplicativeBasisDeformations.MeshWalk.rs {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 Y : V} (f : ScalarMeshCategory.obj c X ⟶ ScalarMeshCategory.obj c Y) : CatAlg.Rep D.F0 (meshFam Q c X) →ₗ[k] CatAlg.Rep D.F0 (meshFam Q c Y)

An evaluated morphism as a k-linear map.

theorem MultiplicativeBasisDeformations.MeshWalk.rs_comp {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} [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] {X Y Z : V} (f : ScalarMeshCategory.obj c X ⟶ ScalarMeshCategory.obj c Y) (g : ScalarMeshCategory.obj c Y ⟶ ScalarMeshCategory.obj c Z) : rs D g ∘ₗ rs D f = rs D (CategoryTheory.CategoryStruct.comp f g)

theorem MultiplicativeBasisDeformations.MeshWalk.rs_add {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} [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] {X Y : V} (f f' : ScalarMeshCategory.obj c X ⟶ ScalarMeshCategory.obj c Y) : rs D (f + f') = rs D f + rs D f'

theorem MultiplicativeBasisDeformations.MeshWalk.rs_sub {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} [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] {X Y : V} (f f' : ScalarMeshCategory.obj c X ⟶ ScalarMeshCategory.obj c Y) : rs D (f - f') = rs D f - rs D f'

theorem MultiplicativeBasisDeformations.MeshWalk.rs_smul {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} [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] {X Y : V} (t : k) (f : ScalarMeshCategory.obj c X ⟶ ScalarMeshCategory.obj c Y) : rs D (t • f) = t • rs D f

theorem MultiplicativeBasisDeformations.MeshWalk.rs_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} {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 : V} {ι : Type u_1} (s : Finset ι) (f : ι → (ScalarMeshCategory.obj c X ⟶ ScalarMeshCategory.obj c Y)) : rs D (∑ i ∈ s, f i) = ∑ i ∈ s, rs D (f i)

theorem MultiplicativeBasisDeformations.MeshWalk.rs_inj {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} [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] {X Y : V} {f f' : ScalarMeshCategory.obj c X ⟶ ScalarMeshCategory.obj c Y} (h : rs D f = rs D f') : f = f'

theorem MultiplicativeBasisDeformations.MeshWalk.zhat_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} {L : CatAlg.LocalFamily (meshFam Q c)} {D : CatAlg.MeshData (meshFam Q c) L} {hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)} [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] {q : ℕ} {μ : (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ} (Ld : LiftData D hfin q μ) (x : ↑Q.nonprojective) : zE Ld x = rs D (zhat Ld x)

theorem MultiplicativeBasisDeformations.MeshWalk.isLiftHom_sub {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} {hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)} [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] {q : ℕ} {μ : (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ} {M : Type u_1} {N : Type u_2} [AddCommGroup M] [Module k M] [AddCommGroup N] [Module k N] {MM : GExt.GMod (galgA0 D hfin) M} {NN : GExt.GMod (galgA0 D hfin) N} {L₁ : GExt.ActLift μ (↑q) MM} {L₂ : GExt.ActLift μ (↑q) NN} {f g g' : M →ₗ[k] N} (h : GExt.IsLiftHom L₁ L₂ f g) (h' : GExt.IsLiftHom L₁ L₂ f g') : GExt.IsLiftHom L₁ L₂ 0 (g' - g)

theorem MultiplicativeBasisDeformations.MeshWalk.Ψc_eq_of_L {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} {hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)} [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] {q : ℕ} {μ : (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ} (Ld Ld' : LiftData D hfin q μ) (hL : Ld'.L = Ld.L) : Ψc Ld' = Ψc Ld

Existence of choices and independence of the module lifts

theorem MultiplicativeBasisDeformations.MeshWalk.extVanish_one {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} {hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)} [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] {q : ℕ} (J : D.InjData) (h1 : DegOne D) (X : V) : GExt.ExtVanish (gmodEv D hfin X) (gmodEv D hfin X) 1 ↑q

theorem MultiplicativeBasisDeformations.MeshWalk.extVanish_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} {L : CatAlg.LocalFamily (meshFam Q c)} {D : CatAlg.MeshData (meshFam Q c) L} {hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)} [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] (J : D.InjData) (h1 : DegOne D) (X Y : V) (t : ℤ) (ht : -2 < t) : GExt.ExtVanish (gmodEv D hfin X) (gmodEv D hfin Y) 0 t

noncomputable def MultiplicativeBasisDeformations.MeshWalk.stdL {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} {hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)} [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] {q : ℕ} {μ : (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ} (J : D.InjData) (h1 : DegOne D) (hμ : GExt.IsHCocycle μ) (hμdeg : GExt.HDeg (galgA0 D hfin) μ ↑q) (X : V) : GExt.ActLift μ (↑q) (gmodEv D hfin X)

The lifted actions: the regular lifts at projective labels.

theorem MultiplicativeBasisDeformations.MeshWalk.exists_liftData {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} {hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)} [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] {q : ℕ} {μ : (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ} (J : D.InjData) (h1 : DegOne D) (hμ : GExt.IsHCocycle μ) (hμdeg : GExt.HDeg (galgA0 D hfin) μ ↑q) : ∃ (Ld : LiftData D hfin q μ), ∀ (X : V), Ld.L X = stdL J h1 hμ hμdeg X

Choices for Ψ exist (Lemma 6.6 with Lemma 6.3).

theorem MultiplicativeBasisDeformations.MeshWalk.Ψc_indep {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} {hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)} [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] {q : ℕ} {μ : (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ} (J : D.InjData) (h1 : DegOne D) (Ld Ld' : LiftData D hfin q μ) : Ψc Ld' = Ψc Ld

Ψ does not depend on the choices.

Linearity of Ψ and invariance under coboundaries

noncomputable def MultiplicativeBasisDeformations.MeshWalk.LiftData.add {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} {hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)} [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] {q : ℕ} {μ μ' : (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ} (Ld : LiftData D hfin q μ) (Ld' : LiftData D hfin q μ') : LiftData D hfin q (μ + μ')

The sum of choices for μ and μ'.

noncomputable def MultiplicativeBasisDeformations.MeshWalk.LiftData.smul {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} {hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)} [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] {q : ℕ} {μ : (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ} (Ld : LiftData D hfin q μ) (t : k) : LiftData D hfin q (t • μ)

A scalar multiple of choices.

theorem MultiplicativeBasisDeformations.MeshWalk.Ψc_add {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} {hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)} [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] {q : ℕ} {μ μ' : (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ} (Ld : LiftData D hfin q μ) (Ld' : LiftData D hfin q μ') : Ψc (Ld.add Ld') = Ψc Ld + Ψc Ld'

theorem MultiplicativeBasisDeformations.MeshWalk.Ψc_smul {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} {hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)} [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] {q : ℕ} {μ : (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ} (Ld : LiftData D hfin q μ) (t : k) : Ψc (Ld.smul t) = t • Ψc Ld

noncomputable def MultiplicativeBasisDeformations.MeshWalk.LiftData.cobdry {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} {hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)} [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] {q : ℕ} {μ : (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ} (h : (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ) (hdeg : ∀ (p : ℤ) (a : (CatAlg.Alg D.F0)ᵐᵒᵖ), (galgA0 D hfin).gr.IsHom p a → (galgA0 D hfin).gr.IsHom (p + ↑q) (h a)) (Ld : LiftData D hfin q μ) : LiftData D hfin q (μ + GExt.hcobdry h)

The transport of choices along a coboundary.

theorem MultiplicativeBasisDeformations.MeshWalk.Ψc_cobdry {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} {hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)} [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] {q : ℕ} {μ : (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ} (h : (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ) (hdeg : ∀ (p : ℤ) (a : (CatAlg.Alg D.F0)ᵐᵒᵖ), (galgA0 D hfin).gr.IsHom p a → (galgA0 D hfin).gr.IsHom (p + ↑q) (h a)) (Ld : LiftData D hfin q μ) : Ψc (LiftData.cobdry h hdeg Ld) = Ψc Ld