Injectivity of Ψ (Proposition 7.6)

weights-and-parameters.tex: "If Ψ[μ] = 0, change the arrows to remove the errors. They give a functor from C ⊗ k[ε]/(ε²) to the Hom category of the lifted modules reducing to the identity. […] On the actual projective corner it trivializes the algebra deformation with leading identity, so [μ] = 0."

A functor C ⊗ k[ε] → (lifted modules) reducing to the identity is recorded by its ε-part: a derivation δ of C into the k-linear maps between evaluated modules with (rs φ, δ φ) a lifted map for every φ. We build δ on paths (δp), extend it linearly to the path category (δL), show that it kills the mesh ideal once the mesh errors vanish (δL_ideal), and descend it to C (δC).

The derivation on paths

@[irreducible]

def MultiplicativeBasisDeformations.MeshWalk.δp {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 μ) {Y X : V} : Quiver.Path Y X → CatAlg.Rep D.F0 (meshFam Q c Y) →ₗ[k] CatAlg.Rep D.F0 (meshFam Q c X)

The ε-part of the lifted path: δ(p a) = a δ(p) + g_a p.

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

theorem MultiplicativeBasisDeformations.MeshWalk.rs_id {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 : V) : rs D (CategoryTheory.CategoryStruct.id (ScalarMeshCategory.obj c Y)) = LinearMap.id

theorem MultiplicativeBasisDeformations.MeshWalk.isLiftHom_id {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 μ) (Y : V) : GExt.IsLiftHom (Ld.L Y) (Ld.L Y) LinearMap.id 0

theorem MultiplicativeBasisDeformations.MeshWalk.rs_pathMor_cons {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 Z : V} (p : Quiver.Path Y X) (a : X ⟶ Z) : rs D (ScalarMeshCategory.pathMor c (p.cons a)) = fA D a ∘ₗ rs D (ScalarMeshCategory.pathMor c p)

theorem MultiplicativeBasisDeformations.MeshWalk.δp_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 μ) {Y X : V} (p : Quiver.Path Y X) : GExt.IsLiftHom (Ld.L Y) (Ld.L X) (rs D (ScalarMeshCategory.pathMor c p)) (δp Ld p)

theorem MultiplicativeBasisDeformations.MeshWalk.δp_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} {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 μ) {Y X : V} (p : Quiver.Path Y X) {Z : V} (p' : Quiver.Path X Z) : δp Ld (p.comp p') = rs D (ScalarMeshCategory.pathMor c p') ∘ₗ δp Ld p + δp Ld p' ∘ₗ rs D (ScalarMeshCategory.pathMor c p)

Linear extension to the path category

noncomputable def MultiplicativeBasisDeformations.MeshWalk.δ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)} {q : ℕ} {μ : (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ} (Ld : LiftData D hfin q μ) {Y X : V} : (LinearPaths.obj Y ⟶ LinearPaths.obj X) →ₗ[k] CatAlg.Rep D.F0 (meshFam Q c Y) →ₗ[k] CatAlg.Rep D.F0 (meshFam Q c X)

The linear extension of δp to the morphisms of kQ.

theorem MultiplicativeBasisDeformations.MeshWalk.δL_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} {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 μ) {Y X : V} (p : Quiver.Path Y X) : (δL Ld) (LinearPaths.path p) = δp Ld p

@[reducible, inline]

noncomputable abbrev MultiplicativeBasisDeformations.MeshWalk.img {k : Type u} [Field k] {V : Type} [Quiver V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients k Q} {Y X : V} (F : LinearPaths.obj Y ⟶ LinearPaths.obj X) : ScalarMeshCategory.obj c Y ⟶ ScalarMeshCategory.obj c X

The image of a morphism of kQ in C.

theorem MultiplicativeBasisDeformations.MeshWalk.img_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)] {Y X : V} : img 0 = 0

theorem MultiplicativeBasisDeformations.MeshWalk.img_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} [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] {Y X : V} (p : Quiver.Path Y X) : img (LinearPaths.path p) = ScalarMeshCategory.pathMor c p

theorem MultiplicativeBasisDeformations.MeshWalk.kQ_induction {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] [(x : V) → Fintype ((y : V) × (y ⟶ x))] {Y X : V} {P : (LinearPaths.obj Y ⟶ LinearPaths.obj X) → Prop} (h0 : P 0) (hadd : ∀ (F G : LinearPaths.obj Y ⟶ LinearPaths.obj X), P F → P G → P (F + G)) (hsmul : ∀ (t : k) (F : LinearPaths.obj Y ⟶ LinearPaths.obj X), P F → P (t • F)) (hpath : ∀ (p : Quiver.Path Y X), P (LinearPaths.path p)) (F : LinearPaths.obj Y ⟶ LinearPaths.obj X) : P F

theorem MultiplicativeBasisDeformations.MeshWalk.rs_img_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)] {Y X : V} (F G : LinearPaths.obj Y ⟶ LinearPaths.obj X) : rs D (img (F + G)) = rs D (img F) + rs D (img G)

theorem MultiplicativeBasisDeformations.MeshWalk.rs_img_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)] {Y X : V} (t : k) (F : LinearPaths.obj Y ⟶ LinearPaths.obj X) : rs D (img (t • F)) = t • rs D (img F)

theorem MultiplicativeBasisDeformations.MeshWalk.δL_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 μ) {Y X : V} (F : LinearPaths.obj Y ⟶ LinearPaths.obj X) : GExt.IsLiftHom (Ld.L Y) (Ld.L X) (rs D (img F)) ((δL Ld) F)

theorem MultiplicativeBasisDeformations.MeshWalk.δL_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} {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 μ) {Y X Z : V} (F : LinearPaths.obj Y ⟶ LinearPaths.obj X) (G : LinearPaths.obj X ⟶ LinearPaths.obj Z) : (δL Ld) (CategoryTheory.CategoryStruct.comp F G) = rs D (img G) ∘ₗ (δL Ld) F + (δL Ld) G ∘ₗ rs D (img F)

The mesh ideal and descent to C

theorem MultiplicativeBasisDeformations.MeshWalk.δp_toPath {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 μ) {Y X : V} (a : Y ⟶ X) : δp Ld a.toPath = Ld.g a

theorem MultiplicativeBasisDeformations.MeshWalk.δL_meshRelation {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) : (δL Ld) (meshRelation c x) = zE Ld x

The ε-part of a mesh relation is the mesh error.

theorem MultiplicativeBasisDeformations.MeshWalk.img_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} [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] {Y X : V} (F G : LinearPaths.obj Y ⟶ LinearPaths.obj X) : img (F + G) = img F + img G

theorem MultiplicativeBasisDeformations.MeshWalk.img_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} [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] {Y X : V} (F G : LinearPaths.obj Y ⟶ LinearPaths.obj X) : img (F - G) = img F - img G

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

theorem MultiplicativeBasisDeformations.MeshWalk.img_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} [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] {Y X Z : V} (F : LinearPaths.obj Y ⟶ LinearPaths.obj X) (G : LinearPaths.obj X ⟶ LinearPaths.obj Z) : img (CategoryTheory.CategoryStruct.comp F G) = CategoryTheory.CategoryStruct.comp (img F) (img G)

theorem MultiplicativeBasisDeformations.MeshWalk.img_meshRelation {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) : img (meshRelation c x) = 0

theorem MultiplicativeBasisDeformations.MeshWalk.δL_sandwich {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 μ} (hz : ∀ (x : ↑Q.nonprojective), zE Ld x = 0) {Y X : V} (x : ↑Q.nonprojective) (a : LinearPaths.obj Y ⟶ LinearPaths.obj ↑(Q.tau x)) (b : LinearPaths.obj ↑x ⟶ LinearPaths.obj X) : (δL Ld) (CategoryTheory.CategoryStruct.comp a (CategoryTheory.CategoryStruct.comp (meshRelation c x) b)) = 0

theorem MultiplicativeBasisDeformations.MeshWalk.δL_ideal {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 μ} (hz : ∀ (x : ↑Q.nonprojective), zE Ld x = 0) {Y X : V} {F : LinearPaths.obj Y ⟶ LinearPaths.obj X} (hF : F ∈ (CategoricalIdeal.HomIdeal.linearSpan k (meshRelations c)).hom (LinearPaths.obj Y) (LinearPaths.obj X)) : (δL Ld) F = 0

When the mesh errors vanish, the derivation kills the mesh ideal.

theorem MultiplicativeBasisDeformations.MeshWalk.δL_eq_of_img {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 μ} (hz : ∀ (x : ↑Q.nonprojective), zE Ld x = 0) {Y X : V} {F G : LinearPaths.obj Y ⟶ LinearPaths.obj X} (h : img F = img G) : (δL Ld) F = (δL Ld) G

noncomputable def MultiplicativeBasisDeformations.MeshWalk.pre {k : Type u} [Field k] {V : Type} [Quiver V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients k Q} {Y X : V} (φ : ScalarMeshCategory.obj c Y ⟶ ScalarMeshCategory.obj c X) : LinearPaths.obj Y ⟶ LinearPaths.obj X

A preimage in kQ of a morphism of C.

theorem MultiplicativeBasisDeformations.MeshWalk.img_pre {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} (φ : ScalarMeshCategory.obj c Y ⟶ ScalarMeshCategory.obj c X) : img (pre φ) = φ

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 μ} (hz : ∀ (x : ↑Q.nonprojective), zE Ld x = 0) {Y X : V} : (ScalarMeshCategory.obj c Y ⟶ ScalarMeshCategory.obj c X) →ₗ[k] CatAlg.Rep D.F0 (meshFam Q c Y) →ₗ[k] CatAlg.Rep D.F0 (meshFam Q c X)

The derivation on C: the ε-part of the functor C ⊗ k[ε] → (lifted modules).

theorem MultiplicativeBasisDeformations.MeshWalk.δC_img {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 μ} (hz : ∀ (x : ↑Q.nonprojective), zE Ld x = 0) {Y X : V} (F : LinearPaths.obj Y ⟶ LinearPaths.obj X) : (δC hz) (img F) = (δL Ld) F

theorem MultiplicativeBasisDeformations.MeshWalk.δC_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 μ} (hz : ∀ (x : ↑Q.nonprojective), zE Ld x = 0) {Y X : V} (φ : ScalarMeshCategory.obj c Y ⟶ ScalarMeshCategory.obj c X) : GExt.IsLiftHom (Ld.L Y) (Ld.L X) (rs D φ) ((δC hz) φ)

theorem MultiplicativeBasisDeformations.MeshWalk.δC_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} {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 μ} (hz : ∀ (x : ↑Q.nonprojective), zE Ld x = 0) {Y X Z : V} (φ : ScalarMeshCategory.obj c Y ⟶ ScalarMeshCategory.obj c X) (ψ : ScalarMeshCategory.obj c X ⟶ ScalarMeshCategory.obj c Z) : (δC hz) (CategoryTheory.CategoryStruct.comp φ ψ) = rs D ψ ∘ₗ (δC hz) φ + (δC hz) ψ ∘ₗ rs D φ

theorem MultiplicativeBasisDeformations.MeshWalk.δC_pathMor {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 μ} (hz : ∀ (x : ↑Q.nonprojective), zE Ld x = 0) {Y X : V} (p : Quiver.Path Y X) : (δC hz) (ScalarMeshCategory.pathMor c p) = δp Ld p

theorem MultiplicativeBasisDeformations.MeshWalk.δC_id {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 μ} (hz : ∀ (x : ↑Q.nonprojective), zE Ld x = 0) (Y : V) : (δC hz) (CategoryTheory.CategoryStruct.id (ScalarMeshCategory.obj c Y)) = 0

The projective corner

Δ_X(m) = ∑_s δ(m_s)(e_s) on an evaluated module; every δφ is the commutator of Δ with φ. On the projective corner, Δ becomes a linear map of A₀ satisfying the hypothesis of GExt.eq_hcobdry_of_derivation.

noncomputable def MultiplicativeBasisDeformations.MeshWalk.Δm {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 μ} (hz : ∀ (x : ↑Q.nonprojective), zE Ld x = 0) (X : V) : CatAlg.Rep D.F0 (meshFam Q c X) →ₗ[k] CatAlg.Rep D.F0 (meshFam Q c X)

Δ_X(m) = ∑_s δ(m_s)(e_s).

theorem MultiplicativeBasisDeformations.MeshWalk.Δm_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} {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 μ} (hz : ∀ (x : ↑Q.nonprojective), zE Ld x = 0) (X : V) (m : CatAlg.Rep D.F0 (meshFam Q c X)) : (Δm hz X) m = ∑ s : D.PV, ((δC hz) (m s)) (CatAlg.unit s)

theorem MultiplicativeBasisDeformations.MeshWalk.rep_eq_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 : V} (n : CatAlg.Rep D.F0 (meshFam Q c X)) : ∑ s : D.PV, (rs D (n s)) (CatAlg.unit s) = n

theorem MultiplicativeBasisDeformations.MeshWalk.rs_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)] {Y X : V} (f : ScalarMeshCategory.obj c Y ⟶ ScalarMeshCategory.obj c X) (m : CatAlg.Rep D.F0 (meshFam Q c Y)) (b : (CatAlg.Alg D.F0)ᵐᵒᵖ) : (rs D f) (((gmodEv D hfin Y).act m) b) = ((gmodEv D hfin X).act ((rs D f) m)) b

theorem MultiplicativeBasisDeformations.MeshWalk.δC_comm {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 μ} (hz : ∀ (x : ↑Q.nonprojective), zE Ld x = 0) {Y X : V} (φ : ScalarMeshCategory.obj c Y ⟶ ScalarMeshCategory.obj c X) (n : CatAlg.Rep D.F0 (meshFam Q c Y)) : ((δC hz) φ) n = (Δm hz X) ((rs D φ) n) - (rs D φ) ((Δm hz Y) n)

δφ is the commutator of Δ with φ.

Transport to A₀

@[reducible, inline]

noncomputable abbrev MultiplicativeBasisDeformations.MeshWalk.ψP {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)) (p : D.PV) : CatAlg.Rep D.F0 (meshFam Q c ↑p) →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ

The coordinate ψ_p : M_p → A₀ of an evaluated projective.

@[reducible, inline]

noncomputable abbrev MultiplicativeBasisDeformations.MeshWalk.eP {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) (p : D.PV) : (CatAlg.Alg D.F0)ᵐᵒᵖ

The idempotent e_p of A₀.

@[reducible, inline]

noncomputable abbrev MultiplicativeBasisDeformations.MeshWalk.gA {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)) (p : D.PV) : (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] CatAlg.Rep D.F0 (meshFam Q c ↑p)

b ↦ e_p·b ∈ M_p.

theorem MultiplicativeBasisDeformations.MeshWalk.ψP_unit {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)] (p : D.PV) : (ψP D hfin p) (CatAlg.unit p) = eP D p

theorem MultiplicativeBasisDeformations.MeshWalk.ψP_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)] (p : D.PV) (m : CatAlg.Rep D.F0 (meshFam Q c ↑p)) (b : (CatAlg.Alg D.F0)ᵐᵒᵖ) : (ψP D hfin p) (((gmodEv D hfin ↑p).act m) b) = (ψP D hfin p) m * b

theorem MultiplicativeBasisDeformations.MeshWalk.act_ψP {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)] (p : D.PV) (m : CatAlg.Rep D.F0 (meshFam Q c ↑p)) : (gA D hfin p) ((ψP D hfin p) m) = m

theorem MultiplicativeBasisDeformations.MeshWalk.ψP_gA {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)] (p : D.PV) (b : (CatAlg.Alg D.F0)ᵐᵒᵖ) : (ψP D hfin p) ((gA D hfin p) b) = eP D p * b

theorem MultiplicativeBasisDeformations.MeshWalk.eP_mul_ψP {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)] (p : D.PV) (m : CatAlg.Rep D.F0 (meshFam Q c ↑p)) : eP D p * (ψP D hfin p) m = (ψP D hfin p) m

theorem MultiplicativeBasisDeformations.MeshWalk.eP_idem {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)] (p : D.PV) : eP D p * eP D p = eP D p

theorem MultiplicativeBasisDeformations.MeshWalk.sum_eP {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)] : ∑ p : D.PV, eP D p = 1

theorem MultiplicativeBasisDeformations.MeshWalk.gA_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)] (p : D.PV) : (gA D hfin p) 1 = CatAlg.unit p

theorem MultiplicativeBasisDeformations.MeshWalk.ψP_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} {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)] {r p : D.PV} (f : ScalarMeshCategory.obj c ↑r ⟶ ScalarMeshCategory.obj c ↑p) (n : CatAlg.Rep D.F0 (meshFam Q c ↑r)) : (ψP D hfin p) ((rs D f) n) = (ψP D hfin p) ((rs D f) (CatAlg.unit r)) * (ψP D hfin r) n

theorem MultiplicativeBasisDeformations.MeshWalk.gA_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} {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)] (p : D.PV) (x : (CatAlg.Alg D.F0)ᵐᵒᵖ) (r : D.PV) : (gA D hfin p) x r = MulOpposite.unop x r p

theorem MultiplicativeBasisDeformations.MeshWalk.sum_ψP_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} {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 : (CatAlg.Alg D.F0)ᵐᵒᵖ) (r : D.PV) : ∑ p : D.PV, (ψP D hfin p) ((rs D ((gA D hfin p) x r)) (CatAlg.unit r)) = x * eP D r

theorem MultiplicativeBasisDeformations.MeshWalk.sum_sum_ψP_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} {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 : (CatAlg.Alg D.F0)ᵐᵒᵖ) (n : (r : D.PV) → CatAlg.Rep D.F0 (meshFam Q c ↑r)) : ∑ p : D.PV, ∑ r : D.PV, (ψP D hfin p) ((rs D ((gA D hfin p) x r)) (n r)) = x * ∑ r : D.PV, (ψP D hfin r) (n r)

theorem MultiplicativeBasisDeformations.MeshWalk.sum_rs_gA {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)] (p : D.PV) (x b : (CatAlg.Alg D.F0)ᵐᵒᵖ) : ∑ r : D.PV, (rs D ((gA D hfin p) x r)) ((gA D hfin r) b) = (gA D hfin p) (x * b)

noncomputable def MultiplicativeBasisDeformations.MeshWalk.Dfull {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 μ} (hz : ∀ (x : ↑Q.nonprojective), zE Ld x = 0) : (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ

The derivation on A₀: Δ̂(b) = ∑_p ψ_p(Δ_p(e_p b)).

theorem MultiplicativeBasisDeformations.MeshWalk.Dfull_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} {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 μ} (hz : ∀ (x : ↑Q.nonprojective), zE Ld x = 0) (b : (CatAlg.Alg D.F0)ᵐᵒᵖ) : (Dfull D hfin hz) b = ∑ p : D.PV, (ψP D hfin p) ((Δm hz ↑p) ((gA D hfin p) b))

theorem MultiplicativeBasisDeformations.MeshWalk.Dfull_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} {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 μ} (hz : ∀ (x : ↑Q.nonprojective), zE Ld x = 0) (hreg : ∀ (p : D.PV) (m : CatAlg.Rep D.F0 (meshFam Q c ↑p)) (b : (CatAlg.Alg D.F0)ᵐᵒᵖ), (Ld.L ↑p).act m b = (gA D hfin p) ((μ ((ψP D hfin p) m)) b)) (x b : (CatAlg.Alg D.F0)ᵐᵒᵖ) : (Dfull D hfin hz) (x * b) - x * (Dfull D hfin hz) b - ((Dfull D hfin hz) x - x * (Dfull D hfin hz) 1) * b = ∑ p : D.PV, eP D p * (μ (eP D p * x)) b - x * ∑ p : D.PV, eP D p * (μ (eP D p)) b

The derivation identity on A₀.

Removing the mesh errors

"If Ψ[μ] = 0, change the arrows to remove the errors."

theorem MultiplicativeBasisDeformations.MeshWalk.rs_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)] {X Y : V} {s : ℕ} {f : ScalarMeshCategory.obj c X ⟶ ScalarMeshCategory.obj c Y} (hf : f ∈ ScalarMeshCategory.degreePart c s X Y) {p : ℤ} {m : CatAlg.Rep D.F0 (meshFam Q c X)} (hm : (zgrEv D hfin X).IsHom p m) : (zgrEv D hfin Y).IsHom (p + ↑s) ((rs D f) m)

theorem MultiplicativeBasisDeformations.MeshWalk.isLiftHom_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} {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)ᵐᵒᵖ} {Y X : V} (L₁ : GExt.ActLift μ (↑q) (gmodEv D hfin Y)) (L₂ : GExt.ActLift μ (↑q) (gmodEv D hfin X)) (f : ScalarMeshCategory.obj c Y ⟶ ScalarMeshCategory.obj c X) : GExt.IsLiftHom L₁ L₂ 0 (rs D f)

noncomputable def MultiplicativeBasisDeformations.MeshWalk.LiftData.shift {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 μ) (f : ScalarMeshCategory.ArrowFamily c) (hf : f ∈ ScalarMeshCategory.familiesDeg c (q + 1)) : LiftData D hfin q μ

Changing the arrows by a family f of degree q + 1.

theorem MultiplicativeBasisDeformations.MeshWalk.zE_shift {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 μ) (f : ScalarMeshCategory.ArrowFamily c) (hf : f ∈ ScalarMeshCategory.familiesDeg c (q + 1)) (x : ↑Q.nonprojective) : zE (Ld.shift f hf) x = zE Ld x - rs D (ScalarMeshCategory.meshDerivative c f x)

theorem MultiplicativeBasisDeformations.MeshWalk.exists_zE_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)ᵐᵒᵖ} (Ld : LiftData D hfin q μ) (h : Ψc Ld = 0) : ∃ (Ld' : LiftData D hfin q μ), Ld'.L = Ld.L ∧ ∀ (x : ↑Q.nonprojective), zE Ld' x = 0

If Ψ[μ] = 0, the arrows can be changed to remove the mesh errors.

Degrees

theorem MultiplicativeBasisDeformations.MeshWalk.δp_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 μ} {Y X : V} (p : Quiver.Path Y X) {e : ℤ} {m : CatAlg.Rep D.F0 (meshFam Q c Y)} (hm : (zgrEv D hfin Y).IsHom e m) : (zgrEv D hfin X).IsHom (e + (↑p.length + ↑q)) ((δp Ld p) m)

theorem MultiplicativeBasisDeformations.MeshWalk.δL_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 μ} {Y X : V} {d : ℕ} {F : LinearPaths.obj Y ⟶ LinearPaths.obj X} (hF : F ∈ LinearPaths.degreePart d Y X) {e : ℤ} {m : CatAlg.Rep D.F0 (meshFam Q c Y)} (hm : (zgrEv D hfin Y).IsHom e m) : (zgrEv D hfin X).IsHom (e + (↑d + ↑q)) (((δL Ld) F) m)

theorem MultiplicativeBasisDeformations.MeshWalk.δC_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 μ} (hz : ∀ (x : ↑Q.nonprojective), zE Ld x = 0) {Y X : V} {d : ℕ} {φ : ScalarMeshCategory.obj c Y ⟶ ScalarMeshCategory.obj c X} (hφ : φ ∈ ScalarMeshCategory.degreePart c d Y X) {e : ℤ} {m : CatAlg.Rep D.F0 (meshFam Q c Y)} (hm : (zgrEv D hfin Y).IsHom e m) : (zgrEv D hfin X).IsHom (e + (↑d + ↑q)) (((δC hz) φ) m)

theorem MultiplicativeBasisDeformations.MeshWalk.unit_isHom {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)] (s : D.PV) : (zgrEv D hfin ↑s).IsHom 0 (CatAlg.unit s)

theorem MultiplicativeBasisDeformations.MeshWalk.Δm_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 μ} (hz : ∀ (x : ↑Q.nonprojective), zE Ld x = 0) (X : V) {d : ℤ} {m : CatAlg.Rep D.F0 (meshFam Q c X)} (hm : (zgrEv D hfin X).IsHom d m) : (zgrEv D hfin X).IsHom (d + ↑q) ((Δm hz X) m)

theorem MultiplicativeBasisDeformations.MeshWalk.eP_isHom {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)] (p : D.PV) : (galgA0 D hfin).gr.IsHom 0 (eP D p)

theorem MultiplicativeBasisDeformations.MeshWalk.Dfull_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 μ} (hz : ∀ (x : ↑Q.nonprojective), zE Ld x = 0) {d : ℤ} {b : (CatAlg.Alg D.F0)ᵐᵒᵖ} (hb : (galgA0 D hfin).gr.IsHom d b) : (galgA0 D hfin).gr.IsHom (d + ↑q) ((Dfull D hfin hz) b)

Injectivity of Ψ

theorem MultiplicativeBasisDeformations.MeshWalk.stdL_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)ᵐᵒᵖ} (J : D.InjData) (h1 : DegOne D) (hμ : GExt.IsHCocycle μ) (hμdeg : GExt.HDeg (galgA0 D hfin) μ ↑q) (p : D.PV) (m : CatAlg.Rep D.F0 (meshFam Q c ↑p)) (b : (CatAlg.Alg D.F0)ᵐᵒᵖ) : (stdL J h1 hμ hμdeg ↑p).act m b = (gA D hfin p) ((μ ((ψP D hfin p) m)) b)

theorem MultiplicativeBasisDeformations.MeshWalk.eq_hcobdry_of_Ψc_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} {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 μ) (h : Ψc Ld = 0) : ∃ (H : (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ), (∀ (p : ℤ) (a : (CatAlg.Alg D.F0)ᵐᵒᵖ), (galgA0 D hfin).gr.IsHom p a → (galgA0 D hfin).gr.IsHom (p + ↑q) (H a)) ∧ μ = GExt.hcobdry H

Proposition 7.6, injectivity (weights-and-parameters.tex): if Ψ[μ] = 0, then μ is the coboundary of a map of degree q.