Integer cocycles from an acyclic matching

For Proposition 7.6. An integer one-cocycle on a 2-complex (f_t + g_t = h_t on every triangle) is determined by arbitrary values on the unmatched edges of an acyclic matching: each matched edge is solved from its triangle, by recursion on the potential (zval, zval_tri). This is the abelian form of the collapse of Lemma 4.2 ("each matched edge is expressed through the remaining ones").

zval_agree: on a set of edges closed under the matching triangles, a cocycle agreeing with the prescribed values on the unmatched edges of the set agrees with zval.

def MultiplicativeBasisDeformations.Morse.triZ {G : Type u_1} [AddCommGroup G] (v : Fin 3 → G) : Fin 3 → G

The value of edge i of a triangle solved from the values v of the other two.

noncomputable def MultiplicativeBasisDeformations.Morse.zval {V Ed : Type} {src tgt : Ed → V} {S : Tris src tgt} (M : Matching S) {G : Type u_1} [AddCommGroup G] (f : Ed → G) : Ed → G

The cocycle with prescribed values f on the unmatched edges.

theorem MultiplicativeBasisDeformations.Morse.zval_eq {V Ed : Type} {src tgt : Ed → V} {S : Tris src tgt} (M : Matching S) {G : Type u_1} [AddCommGroup G] (f : Ed → G) (e : Ed) : zval M f e = if h : Matched M e then triZ (fun (j : Fin 3) => if j = M.m (Classical.choose h) then 0 else zval M f (S.edge (Classical.choose h) j)) (M.m (Classical.choose h)) else f e

theorem MultiplicativeBasisDeformations.Morse.zval_unmatched {V Ed : Type} {src tgt : Ed → V} {S : Tris src tgt} (M : Matching S) {G : Type u_1} [AddCommGroup G] (f : Ed → G) {e : Ed} (h : ¬Matched M e) : zval M f e = f e

theorem MultiplicativeBasisDeformations.Morse.zval_matched {V Ed : Type} {src tgt : Ed → V} {S : Tris src tgt} (M : Matching S) {G : Type u_1} [AddCommGroup G] (f : Ed → G) (t : S.T) : zval M f (S.edge t (M.m t)) = triZ (fun (j : Fin 3) => if j = M.m t then 0 else zval M f (S.edge t j)) (M.m t)

theorem MultiplicativeBasisDeformations.Morse.triZ_rel {G : Type u_1} [AddCommGroup G] (v : Fin 3 → G) (i : Fin 3) (w : Fin 3 → G) (hw : w = fun (j : Fin 3) => if j = i then triZ (fun (j : Fin 3) => if j = i then 0 else v j) i else v j) : w 0 + w 1 = w 2

theorem MultiplicativeBasisDeformations.Morse.zval_tri {V Ed : Type} {src tgt : Ed → V} {S : Tris src tgt} (M : Matching S) {G : Type u_1} [AddCommGroup G] (f : Ed → G) (t : S.T) : zval M f (S.f t) + zval M f (S.g t) = zval M f (S.h t)

The triangle relations hold.

theorem MultiplicativeBasisDeformations.Morse.zval_agree {V Ed : Type} {src tgt : Ed → V} {S : Tris src tgt} (M : Matching S) {G : Type u_1} [AddCommGroup G] (f : Ed → G) (E : Set Ed) (g : Ed → G) (hE : ∀ (t : S.T), S.edge t (M.m t) ∈ E → ∀ (j : Fin 3), S.edge t j ∈ E) (hg : ∀ (t : S.T), (∀ (j : Fin 3), S.edge t j ∈ E) → g (S.f t) + g (S.g t) = g (S.h t)) (hf : ∀ e ∈ E, ¬Matched M e → f e = g e) (e : Ed) : e ∈ E → zval M f e = g e

Agreement on a closed set of edges.