Unit mesh coefficients

Lemma 4.4 (lem:unit-mesh-coefficients, scalar-normalization.tex): "Regard its coefficients as a multiplicative cellular two-cochain on K, assigning c_{X,a} to the triangle with boundary (σa) a t_X⁻¹. […] Rescale the path arrow a by φ(a) and divide the whole mesh relation at X by φ(t_X). These operations change its coefficient to c_{X,a}(dφ)(X,a) […] There are no 3-cells, and Lemma 4.2 makes K homotopy equivalent to a graph. Thus its cellular H²(K;k^*) is zero, so every two-cochain is a coboundary."

Here H²(K; G) = 0 for an abelian group G is proved from the acyclic matching of Lemma 4.2 (Morse.exists_cochain): the matched edge of each triangle is solved for, in increasing order of the potential. For the mesh complex this gives the rescaling (exists_unit_rescaling).

def MultiplicativeBasisDeformations.Morse.CochainEq {V Ed : Type} {src tgt : Ed → V} {S : Tris src tgt} {G : Type u_1} [CommGroup G] (c : S.T → G) (φ : Ed → G) (t : S.T) : Prop

The cocycle equation c_t φ(f) φ(g) = φ(h) of a triangle.

def MultiplicativeBasisDeformations.Morse.solve {V Ed : Type} {src tgt : Ed → V} {S : Tris src tgt} {G : Type u_1} [CommGroup G] (M : Matching S) (c : S.T → G) (φ : Ed → G) (t : S.T) : G

The value forced on the matched edge of t by its equation.

theorem MultiplicativeBasisDeformations.Morse.exists_cochain {V Ed : Type} {src tgt : Ed → V} {S : Tris src tgt} {G : Type u_1} [CommGroup G] (M : Matching S) (hN : ∃ (N : ℕ), ∀ (t : S.T), M.pot t < N) (c : S.T → G) : ∃ (φ : Ed → G), ∀ (t : S.T), CochainEq c φ t

H² of a complex with a complete acyclic matching vanishes: every two-cochain is a coboundary.

theorem MultiplicativeBasisDeformations.MeshWalk.exists_unit_rescaling {V : Type} [Quiver V] {Q : TranslationQuiver V} [Fintype V] [DecidableEq V] [∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] [(x : V) → Fintype ((y : V) × (y ⟶ x))] {k : Type u_1} [Field k] (c : MeshCoefficients k Q) (hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)) (c' : MeshCoefficients k Q) : ∃ (φ : Arr V → kˣ) (ψ : ↑Q.nonprojective → kˣ), ∀ (x : ↑Q.nonprojective) (y : V) (a : y ⟶ ↑x), c' x y a * φ ⟨↑(Q.tau x), ⟨y, (Q.mate x y) a⟩⟩ * φ ⟨y, ⟨↑x, a⟩⟩ = ψ x

Lemma 4.4: every coefficient system c' on Q becomes 1 after rescaling each arrow a by φ(a) and each whole mesh relation at x by ψ(x)⁻¹: c'_{x,a} φ(σa) φ(a) = ψ(x). (The acyclic matching of K comes from a reference system c with finite-dimensional mesh category, e.g. that of Γ_A.)