First-order mesh deformations (toward Proposition 12.5)

deformation-refinements.tex: "Given a correction tuple z_v ∈ C_{q+2}(τv, v), impose r_v − εz_v over k[ε]/(ε²). Corollary 12.4 makes this a free deformation of C."

Here C = kQ/(r) is the scalar mesh category, assumed to satisfy the hypothesis of Lemma 12.3 (its mesh presentations are resolutions). The deformation B = kQ[ε]/(𝔪^{N+1}, r − εz) is free over k[ε] with every path basis of C (Corollary 12.4, by base change from k[t]). Writing morphisms of B as ŝ(f) + ε ŝ(g) for a path section ŝ, the ε-part of ŝ(f) ŝ(g) is a Hochschild two-cocycle φ of C, whose mesh value Σ_a c_{x,a} φ(σa, a) is z_x (exists_cocycle).

The quotient map kQ → C

noncomputable def MultiplicativeBasisDeformations.MeshFirstOrder.qL {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [(x y : V) → Fintype (x ⟶ y)] {Q : TranslationQuiver V} (c : MeshCoefficients k Q) (x y : V) : FlatPert.Hm k x y →ₗ[k] ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y

The quotient map on Hom spaces.

theorem MultiplicativeBasisDeformations.MeshFirstOrder.qL_apply {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] [(x y : V) → Fintype (x ⟶ y)] [(x y : V) → DecidableEq (x ⟶ y)] {Q : TranslationQuiver V} (c : MeshCoefficients k Q) {x y : V} (g : FlatPert.Hm k x y) : (qL c x y) g = (RelationCategory.functor k (meshRelations c)).map g

theorem MultiplicativeBasisDeformations.MeshFirstOrder.qL_comp {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] [(x y : V) → Fintype (x ⟶ y)] [(x y : V) → DecidableEq (x ⟶ y)] {Q : TranslationQuiver V} (c : MeshCoefficients k Q) {x y z : V} (g : FlatPert.Hm k x y) (h : FlatPert.Hm k y z) : (qL c x z) (CategoryTheory.CategoryStruct.comp g h) = CategoryTheory.CategoryStruct.comp ((qL c x y) g) ((qL c y z) h)

theorem MultiplicativeBasisDeformations.MeshFirstOrder.qL_eq_zero_iff {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] [(x y : V) → Fintype (x ⟶ y)] [(x y : V) → DecidableEq (x ⟶ y)] {Q : TranslationQuiver V} (c : MeshCoefficients k Q) {x y : V} (g : FlatPert.Hm k x y) : (qL c x y) g = 0 ↔ g ∈ FlatPert.ctxSpan (FlatPert.meshPres c) (FlatPert.meshPres c).r x y

theorem MultiplicativeBasisDeformations.MeshFirstOrder.qL_surjective {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] [(x y : V) → Fintype (x ⟶ y)] [(x y : V) → DecidableEq (x ⟶ y)] {Q : TranslationQuiver V} (c : MeshCoefficients k Q) (x y : V) : Function.Surjective ⇑(qL c x y)

theorem MultiplicativeBasisDeformations.MeshFirstOrder.qL_arrow {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] [(x y : V) → Fintype (x ⟶ y)] [(x y : V) → DecidableEq (x ⟶ y)] {Q : TranslationQuiver V} (c : MeshCoefficients k Q) {x y : V} (α : x ⟶ y) : (qL c x y) (LinearPaths.arrow α) = ScalarMeshCategory.arrowMor c α

noncomputable def MultiplicativeBasisDeformations.MeshFirstOrder.eqv {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] [(x y : V) → Fintype (x ⟶ y)] [(x y : V) → DecidableEq (x ⟶ y)] {Q : TranslationQuiver V} (c : MeshCoefficients k Q) (x y : V) : FlatPert.Q (FlatPert.idealC (FlatPert.meshPres c)) x y ≃ₗ[k] ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y

C(x, y) = kQ(x, y)/I as a linear equivalence.

theorem MultiplicativeBasisDeformations.MeshFirstOrder.eqv_mk {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] [(x y : V) → Fintype (x ⟶ y)] [(x y : V) → DecidableEq (x ⟶ y)] {Q : TranslationQuiver V} (c : MeshCoefficients k Q) {x y : V} (g : FlatPert.Hm k x y) : (eqv c x y) (Submodule.Quotient.mk g) = (qL c x y) g

theorem MultiplicativeBasisDeformations.MeshFirstOrder.exists_hN {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] [(x y : V) → Fintype (x ⟶ y)] [(x y : V) → DecidableEq (x ⟶ y)] {Q : TranslationQuiver V} (c : MeshCoefficients k Q) [hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)] : ∃ (N : ℕ), ∀ (w y : V) (p : Quiver.Path w y), N ≤ p.length → LinearPaths.path p ∈ FlatPert.ctxSpan (FlatPert.meshPres c) (FlatPert.meshPres c).r w y

C_d = 0 for d ≥ N, as paths in the mesh ideal.

Exactness of the mesh presentations

theorem MultiplicativeBasisDeformations.MeshFirstOrder.eqv_compQ {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] [(x y : V) → Fintype (x ⟶ y)] [(x y : V) → DecidableEq (x ⟶ y)] {Q : TranslationQuiver V} (c : MeshCoefficients k Q) {w y z : V} (h : FlatPert.Hm k y z) (x : FlatPert.Q (FlatPert.idealC (FlatPert.meshPres c)) w y) : (eqv c w z) ((FlatPert.compQ (FlatPert.idealC (FlatPert.meshPres c)) h) x) = CategoryTheory.CategoryStruct.comp ((eqv c w y) x) ((qL c y z) h)

theorem MultiplicativeBasisDeformations.MeshFirstOrder.lastComp_mesh {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] [(x y : V) → Fintype (x ⟶ y)] [(x y : V) → DecidableEq (x ⟶ y)] {Q : TranslationQuiver V} (c : MeshCoefficients k Q) (x : V) (t : (FlatPert.meshPres c).T x) (a : (y : V) × (y ⟶ x)) : (FlatPert.lastComp a) ((FlatPert.meshPres c).r x t) = ↑(c ⟨x, ⋯⟩ a.fst a.snd) • LinearPaths.arrow ((Q.mate ⟨x, ⋯⟩ a.fst) a.snd)

theorem MultiplicativeBasisDeformations.MeshFirstOrder.lastComp_meshRelation {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] [(x y : V) → Fintype (x ⟶ y)] [(x y : V) → DecidableEq (x ⟶ y)] {Q : TranslationQuiver V} (c : MeshCoefficients k Q) (x : ↑Q.nonprojective) (a : (y : V) × (y ⟶ ↑x)) : (FlatPert.lastComp a) (meshRelation c x) = ↑(c x a.fst a.snd) • LinearPaths.arrow ((Q.mate x a.fst) a.snd)

theorem MultiplicativeBasisDeformations.MeshFirstOrder.hres_of_exact {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] [(x y : V) → Fintype (x ⟶ y)] [(x y : V) → DecidableEq (x ⟶ y)] {Q : TranslationQuiver V} (c : MeshCoefficients k Q) (hmono : ∀ (x : ↑Q.nonprojective) (w : V) (z : ScalarMeshCategory.obj c w ⟶ ScalarMeshCategory.obj c ↑(Q.tau x)), (∀ (a : (y : V) × (y ⟶ ↑x)), CategoryTheory.CategoryStruct.comp z (↑(c x a.fst a.snd) • ScalarMeshCategory.arrowMor c ((Q.mate x a.fst) a.snd)) = 0) → z = 0) (hexact : ∀ (x : ↑Q.nonprojective) (w : V) (g : (a : (y : V) × (y ⟶ ↑x)) → ScalarMeshCategory.obj c w ⟶ ScalarMeshCategory.obj c a.fst), ∑ a : (y : V) × (y ⟶ ↑x), CategoryTheory.CategoryStruct.comp (g a) (ScalarMeshCategory.arrowMor c a.snd) = 0 → ∃ (z : ScalarMeshCategory.obj c w ⟶ ScalarMeshCategory.obj c ↑(Q.tau x)), ∀ (a : (y : V) × (y ⟶ ↑x)), g a = CategoryTheory.CategoryStruct.comp z (↑(c x a.fst a.snd) • ScalarMeshCategory.arrowMor c ((Q.mate x a.fst) a.snd))) (hproj : ∀ x ∉ Q.nonprojective, ∀ (w : V) (g : (a : (y : V) × (y ⟶ x)) → ScalarMeshCategory.obj c w ⟶ ScalarMeshCategory.obj c a.fst), ∑ a : (y : V) × (y ⟶ x), CategoryTheory.CategoryStruct.comp (g a) (ScalarMeshCategory.arrowMor c a.snd) = 0 → ∀ (a : (y : V) × (y ⟶ x)), g a = 0) (w x : V) : Function.Injective ⇑(FlatPert.relMap (FlatPert.meshPres c) (FlatPert.idealC (FlatPert.meshPres c)) (FlatPert.meshPres c).r w x) ∧ (FlatPert.alpha (FlatPert.idealC (FlatPert.meshPres c)) w x).ker ≤ (FlatPert.relMap (FlatPert.meshPres c) (FlatPert.idealC (FlatPert.meshPres c)) (FlatPert.meshPres c).r w x).range

The mesh presentations are resolutions (the hypothesis of Lemma 12.3) when the mesh sequences of C are exact: the paragraph after Lemma 12.3.

Path bases

structure MultiplicativeBasisDeformations.MeshFirstOrder.PathBases {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] [(x y : V) → Fintype (x ⟶ y)] [(x y : V) → DecidableEq (x ⟶ y)] {Q : TranslationQuiver V} (c : MeshCoefficients k Q) : Type (u + 1)

Path bases of all Hom spaces of C.

• ι : V → V → Type u
• fin (w y : V) : Fintype (self.ι w y)
• p (w y : V) : self.ι w y → Quiver.Path w y
• li (w y : V) : LinearIndependent k fun (i : self.ι w y) => Submodule.Quotient.mk (LinearPaths.path (self.p w y i))
• sp (w y : V) : Submodule.span k (Set.range fun (i : self.ι w y) => Submodule.Quotient.mk (LinearPaths.path (self.p w y i))) = ⊤

theorem MultiplicativeBasisDeformations.MeshFirstOrder.nonempty_pathBases {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] [(x y : V) → Fintype (x ⟶ y)] [(x y : V) → DecidableEq (x ⟶ y)] {Q : TranslationQuiver V} (c : MeshCoefficients k Q) [hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)] : Nonempty (PathBases c)

noncomputable def MultiplicativeBasisDeformations.MeshFirstOrder.bC {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] [(x y : V) → Fintype (x ⟶ y)] [(x y : V) → DecidableEq (x ⟶ y)] {Q : TranslationQuiver V} {c : MeshCoefficients k Q} (B : PathBases c) (w y : V) : Module.Basis (B.ι w y) k (ScalarMeshCategory.obj c w ⟶ ScalarMeshCategory.obj c y)

The basis of C(w, y) given by the path classes.

theorem MultiplicativeBasisDeformations.MeshFirstOrder.bC_apply {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] [(x y : V) → Fintype (x ⟶ y)] [(x y : V) → DecidableEq (x ⟶ y)] {Q : TranslationQuiver V} {c : MeshCoefficients k Q} [hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)] (B : PathBases c) {w y : V} (i : B.ι w y) : (bC B w y) i = (qL c w y) (LinearPaths.path (B.p w y i))

theorem MultiplicativeBasisDeformations.MeshFirstOrder.exists_arrow_mem {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] [(x y : V) → Fintype (x ⟶ y)] [(x y : V) → DecidableEq (x ⟶ y)] {Q : TranslationQuiver V} {c : MeshCoefficients k Q} [hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)] (B : PathBases c) {w y : V} (α : w ⟶ y) : ∃ (i : B.ι w y), B.p w y i = α.toPath

Every path basis contains the arrows.

Changing coefficients twice

theorem MultiplicativeBasisDeformations.MeshFirstOrder.cmap_cmap {V : Type} [Quiver V] [Fintype V] [DecidableEq V] [(x y : V) → Fintype (x ⟶ y)] [(x y : V) → DecidableEq (x ⟶ y)] {A : Type u_1} {B : Type u_2} {C : Type u_3} [CommRing A] [CommRing B] [CommRing C] (φ : A →+* B) (ψ : B →+* C) {x y : V} (g : FlatPert.Hm A x y) : FlatPert.cmap ψ (FlatPert.cmap φ g) = FlatPert.cmap (ψ.comp φ) g

theorem MultiplicativeBasisDeformations.MeshFirstOrder.cmap_id {V : Type} [Quiver V] [Fintype V] [DecidableEq V] [(x y : V) → Fintype (x ⟶ y)] [(x y : V) → DecidableEq (x ⟶ y)] {A : Type u_1} [CommRing A] {x y : V} (g : FlatPert.Hm A x y) : FlatPert.cmap (RingHom.id A) g = g

The deformation over the dual numbers

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.MeshFirstOrder.Kp (k : Type u) [Field k] : Type u

The polynomial ring k[t].

def MultiplicativeBasisDeformations.MeshFirstOrder.φε {k : Type u} [Field k] : Kp k →+* DualNumber k

t ↦ ε.

def MultiplicativeBasisDeformations.MeshFirstOrder.ρ {k : Type u} [Field k] : DualNumber k →+* k

Reduction modulo ε.

theorem MultiplicativeBasisDeformations.MeshFirstOrder.ρ_comp {k : Type u} [Field k] : (ρ.comp φε).comp MvPolynomial.C = RingHom.id k

theorem MultiplicativeBasisDeformations.MeshFirstOrder.ρ_X {k : Type u} [Field k] : ρ (φε (MvPolynomial.X ())) = 0

theorem MultiplicativeBasisDeformations.MeshFirstOrder.φε_C {k : Type u} [Field k] (t : k) : φε (MvPolynomial.C t) = TrivSqZeroExt.inl t

theorem MultiplicativeBasisDeformations.MeshFirstOrder.φε_X {k : Type u} [Field k] : φε (MvPolynomial.X ()) = DualNumber.eps

noncomputable def MultiplicativeBasisDeformations.MeshFirstOrder.red {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [(x y : V) → Fintype (x ⟶ y)] {Q : TranslationQuiver V} (c : MeshCoefficients k Q) {w y : V} (g : FlatPert.Hm (DualNumber k) w y) : ScalarMeshCategory.obj c w ⟶ ScalarMeshCategory.obj c y

Reduction modulo ε B → C.

theorem MultiplicativeBasisDeformations.MeshFirstOrder.red_add {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] [(x y : V) → Fintype (x ⟶ y)] [(x y : V) → DecidableEq (x ⟶ y)] {Q : TranslationQuiver V} (c : MeshCoefficients k Q) [hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)] {w y : V} (g h : FlatPert.Hm (DualNumber k) w y) : red c (g + h) = red c g + red c h

theorem MultiplicativeBasisDeformations.MeshFirstOrder.red_smul {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] [(x y : V) → Fintype (x ⟶ y)] [(x y : V) → DecidableEq (x ⟶ y)] {Q : TranslationQuiver V} (c : MeshCoefficients k Q) [hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)] {w y : V} (a : DualNumber k) (g : FlatPert.Hm (DualNumber k) w y) : red c (a • g) = ρ a • red c g

theorem MultiplicativeBasisDeformations.MeshFirstOrder.red_comp {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] [(x y : V) → Fintype (x ⟶ y)] [(x y : V) → DecidableEq (x ⟶ y)] {Q : TranslationQuiver V} (c : MeshCoefficients k Q) [hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)] {w x y : V} (g : FlatPert.Hm (DualNumber k) w x) (h : FlatPert.Hm (DualNumber k) x y) : red c (CategoryTheory.CategoryStruct.comp g h) = CategoryTheory.CategoryStruct.comp (red c g) (red c h)

theorem MultiplicativeBasisDeformations.MeshFirstOrder.red_path {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] [(x y : V) → Fintype (x ⟶ y)] [(x y : V) → DecidableEq (x ⟶ y)] {Q : TranslationQuiver V} (c : MeshCoefficients k Q) [hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)] {w y : V} (p : Quiver.Path w y) : red c (LinearPaths.path p) = (qL c w y) (LinearPaths.path p)

theorem MultiplicativeBasisDeformations.MeshFirstOrder.red_sum {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] [(x y : V) → Fintype (x ⟶ y)] [(x y : V) → DecidableEq (x ⟶ y)] {Q : TranslationQuiver V} (c : MeshCoefficients k Q) [hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)] {w y : V} {ι : Type u_1} (s : Finset ι) (g : ι → FlatPert.Hm (DualNumber k) w y) : red c (∑ i ∈ s, g i) = ∑ i ∈ s, red c (g i)

theorem MultiplicativeBasisDeformations.MeshFirstOrder.red_zero {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] [(x y : V) → Fintype (x ⟶ y)] [(x y : V) → DecidableEq (x ⟶ y)] {Q : TranslationQuiver V} (c : MeshCoefficients k Q) [hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)] {w y : V} : red c 0 = 0

The path section

noncomputable def MultiplicativeBasisDeformations.MeshFirstOrder.sh {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] [(x y : V) → Fintype (x ⟶ y)] [(x y : V) → DecidableEq (x ⟶ y)] {Q : TranslationQuiver V} {c : MeshCoefficients k Q} (B : PathBases c) {w y : V} (f : ScalarMeshCategory.obj c w ⟶ ScalarMeshCategory.obj c y) : FlatPert.Hm (DualNumber k) w y

The path section ŝ : C(w, y) → kQ[ε](w, y), ŝ(f) = Σ_i f_i p_i.

theorem MultiplicativeBasisDeformations.MeshFirstOrder.sh_add {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] [(x y : V) → Fintype (x ⟶ y)] [(x y : V) → DecidableEq (x ⟶ y)] {Q : TranslationQuiver V} {c : MeshCoefficients k Q} [hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)] (B : PathBases c) {w y : V} (f f' : ScalarMeshCategory.obj c w ⟶ ScalarMeshCategory.obj c y) : sh B (f + f') = sh B f + sh B f'

theorem MultiplicativeBasisDeformations.MeshFirstOrder.sh_smul {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] [(x y : V) → Fintype (x ⟶ y)] [(x y : V) → DecidableEq (x ⟶ y)] {Q : TranslationQuiver V} {c : MeshCoefficients k Q} [hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)] (B : PathBases c) {w y : V} (t : k) (f : ScalarMeshCategory.obj c w ⟶ ScalarMeshCategory.obj c y) : sh B (t • f) = TrivSqZeroExt.inl t • sh B f

theorem MultiplicativeBasisDeformations.MeshFirstOrder.sh_zero {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] [(x y : V) → Fintype (x ⟶ y)] [(x y : V) → DecidableEq (x ⟶ y)] {Q : TranslationQuiver V} {c : MeshCoefficients k Q} [hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)] (B : PathBases c) {w y : V} : sh B 0 = 0

theorem MultiplicativeBasisDeformations.MeshFirstOrder.sh_sub {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] [(x y : V) → Fintype (x ⟶ y)] [(x y : V) → DecidableEq (x ⟶ y)] {Q : TranslationQuiver V} {c : MeshCoefficients k Q} [hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)] (B : PathBases c) {w y : V} (f f' : ScalarMeshCategory.obj c w ⟶ ScalarMeshCategory.obj c y) : sh B (f - f') = sh B f - sh B f'

theorem MultiplicativeBasisDeformations.MeshFirstOrder.sh_sum {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] [(x y : V) → Fintype (x ⟶ y)] [(x y : V) → DecidableEq (x ⟶ y)] {Q : TranslationQuiver V} {c : MeshCoefficients k Q} [hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)] (B : PathBases c) {w y : V} {ι : Type u_1} (s : Finset ι) (f : ι → (ScalarMeshCategory.obj c w ⟶ ScalarMeshCategory.obj c y)) : sh B (∑ i ∈ s, f i) = ∑ i ∈ s, sh B (f i)

theorem MultiplicativeBasisDeformations.MeshFirstOrder.red_sh {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] [(x y : V) → Fintype (x ⟶ y)] [(x y : V) → DecidableEq (x ⟶ y)] {Q : TranslationQuiver V} {c : MeshCoefficients k Q} [hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)] (B : PathBases c) {w y : V} (f : ScalarMeshCategory.obj c w ⟶ ScalarMeshCategory.obj c y) : red c (sh B f) = f

theorem MultiplicativeBasisDeformations.MeshFirstOrder.sh_arrow {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] [(x y : V) → Fintype (x ⟶ y)] [(x y : V) → DecidableEq (x ⟶ y)] {Q : TranslationQuiver V} {c : MeshCoefficients k Q} [hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)] (B : PathBases c) {w y : V} (α : w ⟶ y) : sh B (ScalarMeshCategory.arrowMor c α) = LinearPaths.arrow α

@[reducible, inline]

noncomputable abbrev MultiplicativeBasisDeformations.MeshFirstOrder.PK {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [(x y : V) → Fintype (x ⟶ y)] {Q : TranslationQuiver V} (c : MeshCoefficients k Q) : FlatPert.Pres (Kp k) V

The presentation over k[t].

@[reducible, inline]

noncomputable abbrev MultiplicativeBasisDeformations.MeshFirstOrder.PR {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [(x y : V) → Fintype (x ⟶ y)] {Q : TranslationQuiver V} (c : MeshCoefficients k Q) : FlatPert.Pres (DualNumber k) V

The presentation over k[ε].

structure MultiplicativeBasisDeformations.MeshFirstOrder.Setup {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] [(x y : V) → Fintype (x ⟶ y)] [(x y : V) → DecidableEq (x ⟶ y)] {Q : TranslationQuiver V} (c : MeshCoefficients k Q) : Type u

The data of a first-order mesh deformation: a cutoff N, the resolution hypothesis of Lemma 12.3, and a correction tuple z_x ∈ C_{q+2}(τx, x) with q ≥ 1.

• N : ℕ
• hN (w y : V) (p : Quiver.Path w y) : self.N ≤ p.length → LinearPaths.path p ∈ FlatPert.ctxSpan (FlatPert.meshPres c) (FlatPert.meshPres c).r w y
• hres (w x : V) : Function.Injective ⇑(FlatPert.relMap (FlatPert.meshPres c) (FlatPert.idealC (FlatPert.meshPres c)) (FlatPert.meshPres c).r w x) ∧ (FlatPert.alpha (FlatPert.idealC (FlatPert.meshPres c)) w x).ker ≤ (FlatPert.relMap (FlatPert.meshPres c) (FlatPert.idealC (FlatPert.meshPres c)) (FlatPert.meshPres c).r w x).range
• q : ℕ
• hq : 1 ≤ self.q
• z : ScalarMeshCategory.MeshFamily c
• hz (x : ↑Q.nonprojective) : self.z x ∈ ScalarMeshCategory.degreePart c (self.q + 2) ↑(Q.tau x) ↑x

noncomputable def MultiplicativeBasisDeformations.MeshFirstOrder.Setup.zh {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] [(x y : V) → Fintype (x ⟶ y)] [(x y : V) → DecidableEq (x ⟶ y)] {Q : TranslationQuiver V} {c : MeshCoefficients k Q} (S : Setup c) (x : ↑Q.nonprojective) : FlatPert.Hm k ↑(Q.tau x) ↑x

Lifts of the corrections to kQ.

theorem MultiplicativeBasisDeformations.MeshFirstOrder.Setup.zh_mem {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] [(x y : V) → Fintype (x ⟶ y)] [(x y : V) → DecidableEq (x ⟶ y)] {Q : TranslationQuiver V} {c : MeshCoefficients k Q} [hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)] (S : Setup c) (x : ↑Q.nonprojective) : S.zh x ∈ LinearPaths.degreePart (S.q + 2) ↑(Q.tau x) ↑x

theorem MultiplicativeBasisDeformations.MeshFirstOrder.Setup.qL_zh {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] [(x y : V) → Fintype (x ⟶ y)] [(x y : V) → DecidableEq (x ⟶ y)] {Q : TranslationQuiver V} {c : MeshCoefficients k Q} [hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)] (S : Setup c) (x : ↑Q.nonprojective) : (qL c ↑(Q.tau x) ↑x) (S.zh x) = S.z x

noncomputable def MultiplicativeBasisDeformations.MeshFirstOrder.Setup.fK {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] [(x y : V) → Fintype (x ⟶ y)] [(x y : V) → DecidableEq (x ⟶ y)] {Q : TranslationQuiver V} {c : MeshCoefficients k Q} (S : Setup c) (x : V) (t : (PK c).T x) : FlatPert.Hm (Kp k) ((PK c).src x t) x

The perturbation t · z over k[t].

theorem MultiplicativeBasisDeformations.MeshFirstOrder.Setup.hfK {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] [(x y : V) → Fintype (x ⟶ y)] [(x y : V) → DecidableEq (x ⟶ y)] {Q : TranslationQuiver V} {c : MeshCoefficients k Q} [hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)] (S : Setup c) (x : V) (t : (PK c).T x) : S.fK x t ∈ FlatPert.geSpan (Kp k) ((PK c).deg x t + 1) ((PK c).src x t) x

@[reducible, inline]

noncomputable abbrev MultiplicativeBasisDeformations.MeshFirstOrder.Setup.IB {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] [(x y : V) → Fintype (x ⟶ y)] [(x y : V) → DecidableEq (x ⟶ y)] {Q : TranslationQuiver V} {c : MeshCoefficients k Q} [hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)] (S : Setup c) : FlatPert.IdealFam (DualNumber k) V

The ideal of the deformation B = kQ[ε]/(𝔪^{N+1}, r − εz).

theorem MultiplicativeBasisDeformations.MeshFirstOrder.Setup.basisR {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] [(x y : V) → Fintype (x ⟶ y)] [(x y : V) → DecidableEq (x ⟶ y)] {Q : TranslationQuiver V} {c : MeshCoefficients k Q} [hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)] (B : PathBases c) (S : Setup c) (w y : V) : (LinearIndependent (DualNumber k) fun (i : B.ι w y) => Submodule.Quotient.mk (LinearPaths.path (B.p w y i))) ∧ Submodule.span (DualNumber k) (Set.range fun (i : B.ι w y) => Submodule.Quotient.mk (LinearPaths.path (B.p w y i))) = ⊤

noncomputable def MultiplicativeBasisDeformations.MeshFirstOrder.Setup.bR {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] [(x y : V) → Fintype (x ⟶ y)] [(x y : V) → DecidableEq (x ⟶ y)] {Q : TranslationQuiver V} {c : MeshCoefficients k Q} [hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)] (B : PathBases c) (S : Setup c) (w y : V) : Module.Basis (B.ι w y) (DualNumber k) (FlatPert.Q S.IB w y)

The basis of B(w, y) over k[ε] given by the path basis of C.

theorem MultiplicativeBasisDeformations.MeshFirstOrder.Setup.bR_apply {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] [(x y : V) → Fintype (x ⟶ y)] [(x y : V) → DecidableEq (x ⟶ y)] {Q : TranslationQuiver V} {c : MeshCoefficients k Q} [hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)] (B : PathBases c) (S : Setup c) {w y : V} (i : B.ι w y) : (bR B S w y) i = Submodule.Quotient.mk (LinearPaths.path (B.p w y i))

@[reducible, inline]

noncomputable abbrev MultiplicativeBasisDeformations.MeshFirstOrder.Setup.mkB {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] [(x y : V) → Fintype (x ⟶ y)] [(x y : V) → DecidableEq (x ⟶ y)] {Q : TranslationQuiver V} {c : MeshCoefficients k Q} [hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)] (S : Setup c) {w y : V} (g : FlatPert.Hm (DualNumber k) w y) : FlatPert.Q S.IB w y

The quotient map onto B.

theorem MultiplicativeBasisDeformations.MeshFirstOrder.Setup.mk_comp_congr {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] [(x y : V) → Fintype (x ⟶ y)] [(x y : V) → DecidableEq (x ⟶ y)] {Q : TranslationQuiver V} {c : MeshCoefficients k Q} [hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)] (S : Setup c) {w x y : V} {g g' : FlatPert.Hm (DualNumber k) w x} {h h' : FlatPert.Hm (DualNumber k) x y} (hg : S.mkB g = S.mkB g') (hh : S.mkB h = S.mkB h') : S.mkB (CategoryTheory.CategoryStruct.comp g h) = S.mkB (CategoryTheory.CategoryStruct.comp g' h')

theorem MultiplicativeBasisDeformations.MeshFirstOrder.Setup.cmap_rR {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] [(x y : V) → Fintype (x ⟶ y)] [(x y : V) → DecidableEq (x ⟶ y)] {Q : TranslationQuiver V} {c : MeshCoefficients k Q} [hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)] (x : V) (t : (PR c).T x) : FlatPert.cmap ρ ((PR c).r x t) = (FlatPert.meshPres c).r x t

The relations of B reduce to those of C.

theorem MultiplicativeBasisDeformations.MeshFirstOrder.Setup.cmap_fR {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] [(x y : V) → Fintype (x ⟶ y)] [(x y : V) → DecidableEq (x ⟶ y)] {Q : TranslationQuiver V} {c : MeshCoefficients k Q} [hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)] (S : Setup c) (x : V) (t : (PR c).T x) : FlatPert.cmap ρ (FlatPert.fmap φε (PK c) S.fK x t) = 0

theorem MultiplicativeBasisDeformations.MeshFirstOrder.Setup.red_eq_zero {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] [(x y : V) → Fintype (x ⟶ y)] [(x y : V) → DecidableEq (x ⟶ y)] {Q : TranslationQuiver V} {c : MeshCoefficients k Q} [hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)] (S : Setup c) {w y : V} {g : FlatPert.Hm (DualNumber k) w y} (hg : g ∈ S.IB.I w y) : red c g = 0

Reduction kills the ideal of B.

Coordinates in B

theorem MultiplicativeBasisDeformations.MeshFirstOrder.Setup.repr_mkB_sh {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] [(x y : V) → Fintype (x ⟶ y)] [(x y : V) → DecidableEq (x ⟶ y)] {Q : TranslationQuiver V} {c : MeshCoefficients k Q} [hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)] (B : PathBases c) (S : Setup c) {w y : V} (f : ScalarMeshCategory.obj c w ⟶ ScalarMeshCategory.obj c y) (i : B.ι w y) : ((bR B S w y).repr (S.mkB (sh B f))) i = TrivSqZeroExt.inl (((bC B w y).repr f) i)

noncomputable def MultiplicativeBasisDeformations.MeshFirstOrder.Setup.redQ {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] [(x y : V) → Fintype (x ⟶ y)] [(x y : V) → DecidableEq (x ⟶ y)] {Q : TranslationQuiver V} {c : MeshCoefficients k Q} [hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)] (B : PathBases c) (S : Setup c) {w y : V} (x : FlatPert.Q S.IB w y) : ScalarMeshCategory.obj c w ⟶ ScalarMeshCategory.obj c y

The reduction of a morphism of B, by coordinates.

noncomputable def MultiplicativeBasisDeformations.MeshFirstOrder.Setup.π1 {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] [(x y : V) → Fintype (x ⟶ y)] [(x y : V) → DecidableEq (x ⟶ y)] {Q : TranslationQuiver V} {c : MeshCoefficients k Q} [hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)] (B : PathBases c) (S : Setup c) {w y : V} (x : FlatPert.Q S.IB w y) : ScalarMeshCategory.obj c w ⟶ ScalarMeshCategory.obj c y

The ε-part of a morphism of B.

theorem MultiplicativeBasisDeformations.MeshFirstOrder.Setup.red_eq_redQ {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] [(x y : V) → Fintype (x ⟶ y)] [(x y : V) → DecidableEq (x ⟶ y)] {Q : TranslationQuiver V} {c : MeshCoefficients k Q} [hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)] (B : PathBases c) (S : Setup c) {w y : V} (g : FlatPert.Hm (DualNumber k) w y) : red c g = redQ B S (S.mkB g)

theorem MultiplicativeBasisDeformations.MeshFirstOrder.Setup.π1_add {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] [(x y : V) → Fintype (x ⟶ y)] [(x y : V) → DecidableEq (x ⟶ y)] {Q : TranslationQuiver V} {c : MeshCoefficients k Q} [hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)] (B : PathBases c) (S : Setup c) {w y : V} (x x' : FlatPert.Q S.IB w y) : π1 B S (x + x') = π1 B S x + π1 B S x'

theorem MultiplicativeBasisDeformations.MeshFirstOrder.Setup.π1_mkB_sh {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] [(x y : V) → Fintype (x ⟶ y)] [(x y : V) → DecidableEq (x ⟶ y)] {Q : TranslationQuiver V} {c : MeshCoefficients k Q} [hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)] (B : PathBases c) (S : Setup c) {w y : V} (f : ScalarMeshCategory.obj c w ⟶ ScalarMeshCategory.obj c y) : π1 B S (S.mkB (sh B f)) = 0

theorem MultiplicativeBasisDeformations.MeshFirstOrder.Setup.snd_eps_inl {k : Type u} [Field k] (r : k) : TrivSqZeroExt.snd (DualNumber.eps * TrivSqZeroExt.inl r) = r

theorem MultiplicativeBasisDeformations.MeshFirstOrder.Setup.fst_eps_inl {k : Type u} [Field k] (r : k) : TrivSqZeroExt.fst (DualNumber.eps * TrivSqZeroExt.inl r) = 0

theorem MultiplicativeBasisDeformations.MeshFirstOrder.Setup.π1_eps {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] [(x y : V) → Fintype (x ⟶ y)] [(x y : V) → DecidableEq (x ⟶ y)] {Q : TranslationQuiver V} {c : MeshCoefficients k Q} [hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)] (B : PathBases c) (S : Setup c) {w y : V} (f : ScalarMeshCategory.obj c w ⟶ ScalarMeshCategory.obj c y) : π1 B S (DualNumber.eps • S.mkB (sh B f)) = f

theorem MultiplicativeBasisDeformations.MeshFirstOrder.Setup.redQ_mkB_sh {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] [(x y : V) → Fintype (x ⟶ y)] [(x y : V) → DecidableEq (x ⟶ y)] {Q : TranslationQuiver V} {c : MeshCoefficients k Q} [hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)] (B : PathBases c) (S : Setup c) {w y : V} (f : ScalarMeshCategory.obj c w ⟶ ScalarMeshCategory.obj c y) : redQ B S (S.mkB (sh B f)) = f

theorem MultiplicativeBasisDeformations.MeshFirstOrder.Setup.decomp {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] [(x y : V) → Fintype (x ⟶ y)] [(x y : V) → DecidableEq (x ⟶ y)] {Q : TranslationQuiver V} {c : MeshCoefficients k Q} [hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)] (B : PathBases c) (S : Setup c) {w y : V} (x : FlatPert.Q S.IB w y) : x = S.mkB (sh B (redQ B S x)) + DualNumber.eps • S.mkB (sh B (π1 B S x))

Decomposition x = ŝ(x̄) + ε ŝ(π₁ x).

theorem MultiplicativeBasisDeformations.MeshFirstOrder.Setup.eps_eps {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] [(x y : V) → Fintype (x ⟶ y)] [(x y : V) → DecidableEq (x ⟶ y)] {Q : TranslationQuiver V} {c : MeshCoefficients k Q} [hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)] (S : Setup c) {w y : V} (x : FlatPert.Q S.IB w y) : DualNumber.eps • DualNumber.eps • x = 0

theorem MultiplicativeBasisDeformations.MeshFirstOrder.Setup.π1_pair {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] [(x y : V) → Fintype (x ⟶ y)] [(x y : V) → DecidableEq (x ⟶ y)] {Q : TranslationQuiver V} {c : MeshCoefficients k Q} [hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)] (B : PathBases c) (S : Setup c) {w y : V} (f g : ScalarMeshCategory.obj c w ⟶ ScalarMeshCategory.obj c y) : π1 B S (S.mkB (sh B f) + DualNumber.eps • S.mkB (sh B g)) = g

theorem MultiplicativeBasisDeformations.MeshFirstOrder.Setup.π1_inl_smul {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] [(x y : V) → Fintype (x ⟶ y)] [(x y : V) → DecidableEq (x ⟶ y)] {Q : TranslationQuiver V} {c : MeshCoefficients k Q} [hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)] (B : PathBases c) (S : Setup c) {w y : V} (t : k) (x : FlatPert.Q S.IB w y) : π1 B S (TrivSqZeroExt.inl t • x) = t • π1 B S x

theorem MultiplicativeBasisDeformations.MeshFirstOrder.Setup.mkB_add {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] [(x y : V) → Fintype (x ⟶ y)] [(x y : V) → DecidableEq (x ⟶ y)] {Q : TranslationQuiver V} {c : MeshCoefficients k Q} [hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)] (S : Setup c) {w y : V} (g h : FlatPert.Hm (DualNumber k) w y) : S.mkB (g + h) = S.mkB g + S.mkB h

theorem MultiplicativeBasisDeformations.MeshFirstOrder.Setup.mkB_smul {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] [(x y : V) → Fintype (x ⟶ y)] [(x y : V) → DecidableEq (x ⟶ y)] {Q : TranslationQuiver V} {c : MeshCoefficients k Q} [hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)] (S : Setup c) {w y : V} (a : DualNumber k) (g : FlatPert.Hm (DualNumber k) w y) : S.mkB (a • g) = a • S.mkB g

The cocycle

noncomputable def MultiplicativeBasisDeformations.MeshFirstOrder.Setup.phi {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] [(x y : V) → Fintype (x ⟶ y)] [(x y : V) → DecidableEq (x ⟶ y)] {Q : TranslationQuiver V} {c : MeshCoefficients k Q} [hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)] (B : PathBases c) (S : Setup c) {X Y Z : V} (f : ScalarMeshCategory.obj c X ⟶ ScalarMeshCategory.obj c Y) (g : ScalarMeshCategory.obj c Y ⟶ ScalarMeshCategory.obj c Z) : ScalarMeshCategory.obj c X ⟶ ScalarMeshCategory.obj c Z

The ε-part of a product of sections φ(f, g) = π₁(ŝ f · ŝ g).

theorem MultiplicativeBasisDeformations.MeshFirstOrder.Setup.mkB_comp {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] [(x y : V) → Fintype (x ⟶ y)] [(x y : V) → DecidableEq (x ⟶ y)] {Q : TranslationQuiver V} {c : MeshCoefficients k Q} [hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)] (B : PathBases c) (S : Setup c) {X Y Z : V} (f : ScalarMeshCategory.obj c X ⟶ ScalarMeshCategory.obj c Y) (g : ScalarMeshCategory.obj c Y ⟶ ScalarMeshCategory.obj c Z) : S.mkB (CategoryTheory.CategoryStruct.comp (sh B f) (sh B g)) = S.mkB (sh B (CategoryTheory.CategoryStruct.comp f g)) + DualNumber.eps • S.mkB (sh B (phi B S f g))

ŝ f · ŝ g = ŝ(f g) + ε ŝ(φ(f, g)) in B.

theorem MultiplicativeBasisDeformations.MeshFirstOrder.Setup.eps_mkB_comp {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] [(x y : V) → Fintype (x ⟶ y)] [(x y : V) → DecidableEq (x ⟶ y)] {Q : TranslationQuiver V} {c : MeshCoefficients k Q} [hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)] (B : PathBases c) (S : Setup c) {X Y Z : V} (f : ScalarMeshCategory.obj c X ⟶ ScalarMeshCategory.obj c Y) (g : ScalarMeshCategory.obj c Y ⟶ ScalarMeshCategory.obj c Z) : DualNumber.eps • S.mkB (CategoryTheory.CategoryStruct.comp (sh B f) (sh B g)) = DualNumber.eps • S.mkB (sh B (CategoryTheory.CategoryStruct.comp f g))

theorem MultiplicativeBasisDeformations.MeshFirstOrder.Setup.phi_add_left {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] [(x y : V) → Fintype (x ⟶ y)] [(x y : V) → DecidableEq (x ⟶ y)] {Q : TranslationQuiver V} {c : MeshCoefficients k Q} [hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)] (B : PathBases c) (S : Setup c) {X Y Z : V} (f f' : ScalarMeshCategory.obj c X ⟶ ScalarMeshCategory.obj c Y) (g : ScalarMeshCategory.obj c Y ⟶ ScalarMeshCategory.obj c Z) : phi B S (f + f') g = phi B S f g + phi B S f' g

theorem MultiplicativeBasisDeformations.MeshFirstOrder.Setup.phi_add_right {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] [(x y : V) → Fintype (x ⟶ y)] [(x y : V) → DecidableEq (x ⟶ y)] {Q : TranslationQuiver V} {c : MeshCoefficients k Q} [hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)] (B : PathBases c) (S : Setup c) {X Y Z : V} (f : ScalarMeshCategory.obj c X ⟶ ScalarMeshCategory.obj c Y) (g g' : ScalarMeshCategory.obj c Y ⟶ ScalarMeshCategory.obj c Z) : phi B S f (g + g') = phi B S f g + phi B S f g'

theorem MultiplicativeBasisDeformations.MeshFirstOrder.Setup.phi_smul_left {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] [(x y : V) → Fintype (x ⟶ y)] [(x y : V) → DecidableEq (x ⟶ y)] {Q : TranslationQuiver V} {c : MeshCoefficients k Q} [hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)] (B : PathBases c) (S : Setup c) {X Y Z : V} (t : k) (f : ScalarMeshCategory.obj c X ⟶ ScalarMeshCategory.obj c Y) (g : ScalarMeshCategory.obj c Y ⟶ ScalarMeshCategory.obj c Z) : phi B S (t • f) g = t • phi B S f g

theorem MultiplicativeBasisDeformations.MeshFirstOrder.Setup.phi_smul_right {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] [(x y : V) → Fintype (x ⟶ y)] [(x y : V) → DecidableEq (x ⟶ y)] {Q : TranslationQuiver V} {c : MeshCoefficients k Q} [hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)] (B : PathBases c) (S : Setup c) {X Y Z : V} (t : k) (f : ScalarMeshCategory.obj c X ⟶ ScalarMeshCategory.obj c Y) (g : ScalarMeshCategory.obj c Y ⟶ ScalarMeshCategory.obj c Z) : phi B S f (t • g) = t • phi B S f g

theorem MultiplicativeBasisDeformations.MeshFirstOrder.Setup.π1_assoc_left {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] [(x y : V) → Fintype (x ⟶ y)] [(x y : V) → DecidableEq (x ⟶ y)] {Q : TranslationQuiver V} {c : MeshCoefficients k Q} [hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)] (B : PathBases c) (S : Setup c) {W X Y Z : V} (f : ScalarMeshCategory.obj c W ⟶ ScalarMeshCategory.obj c X) (g : ScalarMeshCategory.obj c X ⟶ ScalarMeshCategory.obj c Y) (h : ScalarMeshCategory.obj c Y ⟶ ScalarMeshCategory.obj c Z) : π1 B S (S.mkB (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (sh B f) (sh B g)) (sh B h))) = phi B S (CategoryTheory.CategoryStruct.comp f g) h + CategoryTheory.CategoryStruct.comp (phi B S f g) h

theorem MultiplicativeBasisDeformations.MeshFirstOrder.Setup.π1_assoc_right {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] [(x y : V) → Fintype (x ⟶ y)] [(x y : V) → DecidableEq (x ⟶ y)] {Q : TranslationQuiver V} {c : MeshCoefficients k Q} [hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)] (B : PathBases c) (S : Setup c) {W X Y Z : V} (f : ScalarMeshCategory.obj c W ⟶ ScalarMeshCategory.obj c X) (g : ScalarMeshCategory.obj c X ⟶ ScalarMeshCategory.obj c Y) (h : ScalarMeshCategory.obj c Y ⟶ ScalarMeshCategory.obj c Z) : π1 B S (S.mkB (CategoryTheory.CategoryStruct.comp (sh B f) (CategoryTheory.CategoryStruct.comp (sh B g) (sh B h)))) = phi B S f (CategoryTheory.CategoryStruct.comp g h) + CategoryTheory.CategoryStruct.comp f (phi B S g h)

theorem MultiplicativeBasisDeformations.MeshFirstOrder.Setup.phi_cocycle {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] [(x y : V) → Fintype (x ⟶ y)] [(x y : V) → DecidableEq (x ⟶ y)] {Q : TranslationQuiver V} {c : MeshCoefficients k Q} [hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)] (B : PathBases c) (S : Setup c) {W X Y Z : V} (f : ScalarMeshCategory.obj c W ⟶ ScalarMeshCategory.obj c X) (g : ScalarMeshCategory.obj c X ⟶ ScalarMeshCategory.obj c Y) (h : ScalarMeshCategory.obj c Y ⟶ ScalarMeshCategory.obj c Z) : CategoryTheory.CategoryStruct.comp f (phi B S g h) - phi B S (CategoryTheory.CategoryStruct.comp f g) h + phi B S f (CategoryTheory.CategoryStruct.comp g h) - CategoryTheory.CategoryStruct.comp (phi B S f g) h = 0

The cocycle identity.

The mesh value

theorem MultiplicativeBasisDeformations.MeshFirstOrder.Setup.eps_mkB_red {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] [(x y : V) → Fintype (x ⟶ y)] [(x y : V) → DecidableEq (x ⟶ y)] {Q : TranslationQuiver V} {c : MeshCoefficients k Q} [hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)] (B : PathBases c) (S : Setup c) {w y : V} (u : FlatPert.Hm (DualNumber k) w y) : DualNumber.eps • S.mkB u = DualNumber.eps • S.mkB (sh B (red c u))

theorem MultiplicativeBasisDeformations.MeshFirstOrder.Setup.rR_eq {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] [(x y : V) → Fintype (x ⟶ y)] [(x y : V) → DecidableEq (x ⟶ y)] {Q : TranslationQuiver V} {c : MeshCoefficients k Q} [hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)] (x : ↑Q.nonprojective) (t : (PR c).T ↑x) : (PR c).r (↑x) t = ∑ a : (y : V) × (y ⟶ ↑x), TrivSqZeroExt.inl ↑(c x a.fst a.snd) • CategoryTheory.CategoryStruct.comp (LinearPaths.arrow ((Q.mate x a.fst) a.snd)) (LinearPaths.arrow a.snd)

theorem MultiplicativeBasisDeformations.MeshFirstOrder.Setup.fR_eq {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] [(x y : V) → Fintype (x ⟶ y)] [(x y : V) → DecidableEq (x ⟶ y)] {Q : TranslationQuiver V} {c : MeshCoefficients k Q} [hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)] (S : Setup c) (x : V) (t : (PR c).T x) : FlatPert.fmap φε (PK c) S.fK x t = DualNumber.eps • FlatPert.cmap (φε.comp MvPolynomial.C) (S.zh ⟨x, ⋯⟩)

theorem MultiplicativeBasisDeformations.MeshFirstOrder.Setup.red_fR_part {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] [(x y : V) → Fintype (x ⟶ y)] [(x y : V) → DecidableEq (x ⟶ y)] {Q : TranslationQuiver V} {c : MeshCoefficients k Q} [hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)] (S : Setup c) (x : V) (t : (PR c).T x) : red c (FlatPert.cmap (φε.comp MvPolynomial.C) (S.zh ⟨x, ⋯⟩)) = S.z ⟨x, ⋯⟩

theorem MultiplicativeBasisDeformations.MeshFirstOrder.Setup.mkB_rR {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] [(x y : V) → Fintype (x ⟶ y)] [(x y : V) → DecidableEq (x ⟶ y)] {Q : TranslationQuiver V} {c : MeshCoefficients k Q} [hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)] (S : Setup c) (x : V) (t : (PR c).T x) : S.mkB ((PR c).r x t) = S.mkB (FlatPert.fmap φε (PK c) S.fK x t)

theorem MultiplicativeBasisDeformations.MeshFirstOrder.Setup.mkB_sum {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] [(x y : V) → Fintype (x ⟶ y)] [(x y : V) → DecidableEq (x ⟶ y)] {Q : TranslationQuiver V} {c : MeshCoefficients k Q} [hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)] (S : Setup c) {w y : V} {ι : Type u_1} (s : Finset ι) (g : ι → FlatPert.Hm (DualNumber k) w y) : S.mkB (∑ i ∈ s, g i) = ∑ i ∈ s, S.mkB (g i)

theorem MultiplicativeBasisDeformations.MeshFirstOrder.Setup.mkB_zero {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] [(x y : V) → Fintype (x ⟶ y)] [(x y : V) → DecidableEq (x ⟶ y)] {Q : TranslationQuiver V} {c : MeshCoefficients k Q} [hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)] (S : Setup c) {w y : V} : S.mkB 0 = 0

theorem MultiplicativeBasisDeformations.MeshFirstOrder.Setup.meshVal_phi {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] [(x y : V) → Fintype (x ⟶ y)] [(x y : V) → DecidableEq (x ⟶ y)] {Q : TranslationQuiver V} {c : MeshCoefficients k Q} [hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)] (B : PathBases c) (S : Setup c) (x : ↑Q.nonprojective) : ∑ a : (y : V) × (y ⟶ ↑x), ↑(c x a.fst a.snd) • phi B S (ScalarMeshCategory.arrowMor c ((Q.mate x a.fst) a.snd)) (ScalarMeshCategory.arrowMor c a.snd) = S.z x

The mesh value of φ is the correction tuple z.

Homogeneous components of a cocycle

structure MultiplicativeBasisDeformations.MeshFirstOrder.RawCocycle {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [(x y : V) → Fintype (x ⟶ y)] {Q : TranslationQuiver V} (c : MeshCoefficients k Q) : Type u

A bilinear Hochschild two-cocycle of C, not necessarily homogeneous.

• φ {X Y Z : V} : (ScalarMeshCategory.obj c X ⟶ ScalarMeshCategory.obj c Y) → (ScalarMeshCategory.obj c Y ⟶ ScalarMeshCategory.obj c Z) → (ScalarMeshCategory.obj c X ⟶ ScalarMeshCategory.obj c Z)
• add_left {X Y Z : V} (f f' : ScalarMeshCategory.obj c X ⟶ ScalarMeshCategory.obj c Y) (g : ScalarMeshCategory.obj c Y ⟶ ScalarMeshCategory.obj c Z) : self.φ (f + f') g = self.φ f g + self.φ f' g
• add_right {X Y Z : V} (f : ScalarMeshCategory.obj c X ⟶ ScalarMeshCategory.obj c Y) (g g' : ScalarMeshCategory.obj c Y ⟶ ScalarMeshCategory.obj c Z) : self.φ f (g + g') = self.φ f g + self.φ f g'
• smul_left {X Y Z : V} (t : k) (f : ScalarMeshCategory.obj c X ⟶ ScalarMeshCategory.obj c Y) (g : ScalarMeshCategory.obj c Y ⟶ ScalarMeshCategory.obj c Z) : self.φ (t • f) g = t • self.φ f g
• smul_right {X Y Z : V} (t : k) (f : ScalarMeshCategory.obj c X ⟶ ScalarMeshCategory.obj c Y) (g : ScalarMeshCategory.obj c Y ⟶ ScalarMeshCategory.obj c Z) : self.φ f (t • g) = t • self.φ f g
• cocycle {W X Y Z : V} (f : ScalarMeshCategory.obj c W ⟶ ScalarMeshCategory.obj c X) (g : ScalarMeshCategory.obj c X ⟶ ScalarMeshCategory.obj c Y) (h : ScalarMeshCategory.obj c Y ⟶ ScalarMeshCategory.obj c Z) : CategoryTheory.CategoryStruct.comp f (self.φ g h) - self.φ (CategoryTheory.CategoryStruct.comp f g) h + self.φ f (CategoryTheory.CategoryStruct.comp g h) - CategoryTheory.CategoryStruct.comp (self.φ f g) h = 0

theorem MultiplicativeBasisDeformations.MeshFirstOrder.RawCocycle.zero_left {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] [(x y : V) → Fintype (x ⟶ y)] [(x y : V) → DecidableEq (x ⟶ y)] {Q : TranslationQuiver V} {c : MeshCoefficients k Q} [hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)] (Φ : RawCocycle c) {X Y Z : V} (g : ScalarMeshCategory.obj c Y ⟶ ScalarMeshCategory.obj c Z) : Φ.φ 0 g = 0

theorem MultiplicativeBasisDeformations.MeshFirstOrder.RawCocycle.zero_right {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] [(x y : V) → Fintype (x ⟶ y)] [(x y : V) → DecidableEq (x ⟶ y)] {Q : TranslationQuiver V} {c : MeshCoefficients k Q} [hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)] (Φ : RawCocycle c) {X Y Z : V} (f : ScalarMeshCategory.obj c X ⟶ ScalarMeshCategory.obj c Y) : Φ.φ f 0 = 0

theorem MultiplicativeBasisDeformations.MeshFirstOrder.RawCocycle.degProj_comp_right {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] [(x y : V) → Fintype (x ⟶ y)] [(x y : V) → DecidableEq (x ⟶ y)] {Q : TranslationQuiver V} {c : MeshCoefficients k Q} [hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)] {p r : ℕ} {x y z : V} (f : ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y) {h : ScalarMeshCategory.obj c y ⟶ ScalarMeshCategory.obj c z} (hh : h ∈ ScalarMeshCategory.degreePart c p y z) : (ScalarMeshCategory.degProj c (r + p) x z) (CategoryTheory.CategoryStruct.comp f h) = CategoryTheory.CategoryStruct.comp ((ScalarMeshCategory.degProj c r x y) f) h

noncomputable def MultiplicativeBasisDeformations.MeshFirstOrder.RawCocycle.φq {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [(x y : V) → Fintype (x ⟶ y)] {Q : TranslationQuiver V} {c : MeshCoefficients k Q} [hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)] (Φ : RawCocycle c) (q : ℕ) {X Y Z : V} (f : ScalarMeshCategory.obj c X ⟶ ScalarMeshCategory.obj c Y) (g : ScalarMeshCategory.obj c Y ⟶ ScalarMeshCategory.obj c Z) : ScalarMeshCategory.obj c X ⟶ ScalarMeshCategory.obj c Z

The degree-q component of a cocycle.

theorem MultiplicativeBasisDeformations.MeshFirstOrder.RawCocycle.φq_hom {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] [(x y : V) → Fintype (x ⟶ y)] [(x y : V) → DecidableEq (x ⟶ y)] {Q : TranslationQuiver V} {c : MeshCoefficients k Q} [hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)] (Φ : RawCocycle c) (q : ℕ) {X Y Z : V} {a b : ℕ} {f : ScalarMeshCategory.obj c X ⟶ ScalarMeshCategory.obj c Y} {g : ScalarMeshCategory.obj c Y ⟶ ScalarMeshCategory.obj c Z} (hf : f ∈ ScalarMeshCategory.degreePart c a X Y) (hg : g ∈ ScalarMeshCategory.degreePart c b Y Z) : Φ.φq q f g = (ScalarMeshCategory.degProj c (a + b + q) X Z) (Φ.φ f g)

theorem MultiplicativeBasisDeformations.MeshFirstOrder.RawCocycle.φq_add_left {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] [(x y : V) → Fintype (x ⟶ y)] [(x y : V) → DecidableEq (x ⟶ y)] {Q : TranslationQuiver V} {c : MeshCoefficients k Q} [hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)] (Φ : RawCocycle c) (q : ℕ) {X Y Z : V} (f f' : ScalarMeshCategory.obj c X ⟶ ScalarMeshCategory.obj c Y) (g : ScalarMeshCategory.obj c Y ⟶ ScalarMeshCategory.obj c Z) : Φ.φq q (f + f') g = Φ.φq q f g + Φ.φq q f' g

theorem MultiplicativeBasisDeformations.MeshFirstOrder.RawCocycle.φq_add_right {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] [(x y : V) → Fintype (x ⟶ y)] [(x y : V) → DecidableEq (x ⟶ y)] {Q : TranslationQuiver V} {c : MeshCoefficients k Q} [hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)] (Φ : RawCocycle c) (q : ℕ) {X Y Z : V} (f : ScalarMeshCategory.obj c X ⟶ ScalarMeshCategory.obj c Y) (g g' : ScalarMeshCategory.obj c Y ⟶ ScalarMeshCategory.obj c Z) : Φ.φq q f (g + g') = Φ.φq q f g + Φ.φq q f g'

theorem MultiplicativeBasisDeformations.MeshFirstOrder.RawCocycle.φq_smul_left {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] [(x y : V) → Fintype (x ⟶ y)] [(x y : V) → DecidableEq (x ⟶ y)] {Q : TranslationQuiver V} {c : MeshCoefficients k Q} [hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)] (Φ : RawCocycle c) (q : ℕ) {X Y Z : V} (t : k) (f : ScalarMeshCategory.obj c X ⟶ ScalarMeshCategory.obj c Y) (g : ScalarMeshCategory.obj c Y ⟶ ScalarMeshCategory.obj c Z) : Φ.φq q (t • f) g = t • Φ.φq q f g

theorem MultiplicativeBasisDeformations.MeshFirstOrder.RawCocycle.φq_smul_right {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] [(x y : V) → Fintype (x ⟶ y)] [(x y : V) → DecidableEq (x ⟶ y)] {Q : TranslationQuiver V} {c : MeshCoefficients k Q} [hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)] (Φ : RawCocycle c) (q : ℕ) {X Y Z : V} (t : k) (f : ScalarMeshCategory.obj c X ⟶ ScalarMeshCategory.obj c Y) (g : ScalarMeshCategory.obj c Y ⟶ ScalarMeshCategory.obj c Z) : Φ.φq q f (t • g) = t • Φ.φq q f g

theorem MultiplicativeBasisDeformations.MeshFirstOrder.RawCocycle.eq_zero_of_hom {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] [(x y : V) → Fintype (x ⟶ y)] [(x y : V) → DecidableEq (x ⟶ y)] {Q : TranslationQuiver V} {c : MeshCoefficients k Q} [hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)] {X Y : V} {M : Type u_1} [AddCommGroup M] (F : (ScalarMeshCategory.obj c X ⟶ ScalarMeshCategory.obj c Y) →+ M) (h : ∀ (d : ℕ), ∀ f ∈ ScalarMeshCategory.degreePart c d X Y, F f = 0) (f : ScalarMeshCategory.obj c X ⟶ ScalarMeshCategory.obj c Y) : F f = 0

An additive function vanishing on homogeneous morphisms vanishes.

noncomputable def MultiplicativeBasisDeformations.MeshFirstOrder.RawCocycle.cocExpr {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [(x y : V) → Fintype (x ⟶ y)] {Q : TranslationQuiver V} {c : MeshCoefficients k Q} [hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)] (Φ : RawCocycle c) (q : ℕ) {W X Y Z : V} (f : ScalarMeshCategory.obj c W ⟶ ScalarMeshCategory.obj c X) (g : ScalarMeshCategory.obj c X ⟶ ScalarMeshCategory.obj c Y) (h : ScalarMeshCategory.obj c Y ⟶ ScalarMeshCategory.obj c Z) : ScalarMeshCategory.obj c W ⟶ ScalarMeshCategory.obj c Z

The cocycle expression of φ_q.

theorem MultiplicativeBasisDeformations.MeshFirstOrder.RawCocycle.cocExpr_hom {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] [(x y : V) → Fintype (x ⟶ y)] [(x y : V) → DecidableEq (x ⟶ y)] {Q : TranslationQuiver V} {c : MeshCoefficients k Q} [hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)] (Φ : RawCocycle c) (q : ℕ) {W X Y Z : V} {a b d : ℕ} {f : ScalarMeshCategory.obj c W ⟶ ScalarMeshCategory.obj c X} {g : ScalarMeshCategory.obj c X ⟶ ScalarMeshCategory.obj c Y} {h : ScalarMeshCategory.obj c Y ⟶ ScalarMeshCategory.obj c Z} (hf : f ∈ ScalarMeshCategory.degreePart c a W X) (hg : g ∈ ScalarMeshCategory.degreePart c b X Y) (hh : h ∈ ScalarMeshCategory.degreePart c d Y Z) : Φ.cocExpr q f g h = 0

theorem MultiplicativeBasisDeformations.MeshFirstOrder.RawCocycle.cocExpr_eq_zero {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] [(x y : V) → Fintype (x ⟶ y)] [(x y : V) → DecidableEq (x ⟶ y)] {Q : TranslationQuiver V} {c : MeshCoefficients k Q} [hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)] (Φ : RawCocycle c) (q : ℕ) {W X Y Z : V} (f : ScalarMeshCategory.obj c W ⟶ ScalarMeshCategory.obj c X) (g : ScalarMeshCategory.obj c X ⟶ ScalarMeshCategory.obj c Y) (h : ScalarMeshCategory.obj c Y ⟶ ScalarMeshCategory.obj c Z) : Φ.cocExpr q f g h = 0

noncomputable def MultiplicativeBasisDeformations.MeshFirstOrder.RawCocycle.toCat {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] [(x y : V) → Fintype (x ⟶ y)] [(x y : V) → DecidableEq (x ⟶ y)] {Q : TranslationQuiver V} {c : MeshCoefficients k Q} [hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)] (Φ : RawCocycle c) (q : ℕ) : MeshWalk.CatCocycle c q

The homogeneous cocycle of internal degree q.

noncomputable def MultiplicativeBasisDeformations.MeshFirstOrder.Setup.raw {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] [(x y : V) → Fintype (x ⟶ y)] [(x y : V) → DecidableEq (x ⟶ y)] {Q : TranslationQuiver V} {c : MeshCoefficients k Q} [hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)] (B : PathBases c) (S : Setup c) : RawCocycle c

The cocycle of the deformation.

theorem MultiplicativeBasisDeformations.MeshFirstOrder.Setup.meshVal_toCat {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] [(x y : V) → Fintype (x ⟶ y)] [(x y : V) → DecidableEq (x ⟶ y)] {Q : TranslationQuiver V} {c : MeshCoefficients k Q} [hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)] (B : PathBases c) (S : Setup c) : ((raw B S).toCat S.q).meshVal = S.z

The deformation gives a homogeneous cocycle with mesh value z.

theorem MultiplicativeBasisDeformations.MeshFirstOrder.exists_catCocycle {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] [(x y : V) → Fintype (x ⟶ y)] [(x y : V) → DecidableEq (x ⟶ y)] {Q : TranslationQuiver V} {c : MeshCoefficients k Q} [hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)] (S : Setup c) : ∃ (Φ : MeshWalk.CatCocycle c S.q), Φ.meshVal = S.z

Every correction tuple is the mesh value of a homogeneous cocycle (the first-order deformation r − εz of C, Corollary 12.4).

Proposition 12.5: the full Hochschild comparison

theorem MultiplicativeBasisDeformations.MeshWalk.Ψc_surjective {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] [(x y : V) → Fintype (x ⟶ y)] [(x y : V) → DecidableEq (x ⟶ y)] {Q : TranslationQuiver V} {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)] (hres : ∀ (w x : V), Function.Injective ⇑(FlatPert.relMap (FlatPert.meshPres c) (FlatPert.idealC (FlatPert.meshPres c)) (FlatPert.meshPres c).r w x) ∧ (FlatPert.alpha (FlatPert.idealC (FlatPert.meshPres c)) w x).ker ≤ (FlatPert.relMap (FlatPert.meshPres c) (FlatPert.idealC (FlatPert.meshPres c)) (FlatPert.meshPres c).r w x).range) {q : ℕ} (hq : 1 ≤ q) (z : ScalarMeshCategory.MeshFamily c) (hz : ∀ (x : ↑Q.nonprojective), z x ∈ ScalarMeshCategory.degreePart c (q + 2) ↑(Q.tau x) ↑x) : ∃ (μ : (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ) (_ : GExt.IsHCocycle μ) (_ : GExt.HDeg (galgA0 D hfin) μ ↑q) (Ld : LiftData D hfin q μ), Ψc Ld = Submodule.Quotient.mk z

Proposition 12.5, surjectivity (prop:full-hochschild-comparison): if the mesh presentations of C are resolutions (the hypothesis of Lemma 12.3), every class of coker D_{q+1} in degree q + 2 ≥ 3 is Ψ[μ] for a Hochschild two-cocycle μ of A₀ of internal degree q: the corner of the first-order deformation r − εz of C.

theorem MultiplicativeBasisDeformations.MeshWalk.fullHochschildComparison {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] [(x y : V) → Fintype (x ⟶ y)] [(x y : V) → DecidableEq (x ⟶ y)] {Q : TranslationQuiver V} {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) (hres : ∀ (w x : V), Function.Injective ⇑(FlatPert.relMap (FlatPert.meshPres c) (FlatPert.idealC (FlatPert.meshPres c)) (FlatPert.meshPres c).r w x) ∧ (FlatPert.alpha (FlatPert.idealC (FlatPert.meshPres c)) w x).ker ≤ (FlatPert.relMap (FlatPert.meshPres c) (FlatPert.idealC (FlatPert.meshPres c)) (FlatPert.meshPres c).r w x).range) {q : ℕ} (hq : 1 ≤ q) : (∀ (z : ScalarMeshCategory.MeshFamily c), (∀ (x : ↑Q.nonprojective), z x ∈ ScalarMeshCategory.degreePart c (q + 2) ↑(Q.tau x) ↑x) → ∃ (μ : (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ) (_ : GExt.IsHCocycle μ) (_ : GExt.HDeg (galgA0 D hfin) μ ↑q) (Ld : LiftData D hfin q μ), Ψc Ld = Submodule.Quotient.mk z) ∧ ∀ (μ : (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ), GExt.IsHCocycle μ → GExt.HDeg (galgA0 D hfin) μ ↑q → ∀ (Ld : LiftData D hfin q μ), Ψ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 12.5 (prop:full-hochschild-comparison): in every internal degree q ≥ 1, Ψ : HH²(A₀)_q → coker D_{q+1} is an isomorphism — onto the degree-(q+2) mesh families, and injective by Proposition 7.7.