Weights on the universal cover are ratios of object values

Lemma 4.13 (scalar-normalization.tex): "Assign ν_X to t_X. These weights respect the triangles of K̃. Since this complex is simply connected, multiplying along walks gives object values ζ_X with w(a) = ζ_{target(a)} / ζ_{source(a)}."

A lifted vertex of K̃ is a walk class γ : v₀ → X of the coned complex (lift, sheet), and a weight assigns to each edge e and each lift γ of its source a value W e γ in a group. Weights respecting the triangles define a functor out of the fundamental groupoid into the semidirect groupoid SD (morphisms: a walk class together with values along it). Its first component is the identity (Ψ_fst, "simply connected"), and its values along walks from the basepoint are the object values: pot (γ ≫ e) = pot γ · W e γ (pot_comp).

def MultiplicativeBasisDeformations.MeshWalk.SD {V : Type} [Quiver V] (_Q : TranslationQuiver V) (_v₀ : V) (_K : Type w) : Type

The objects of the semidirect groupoid.

@[instance_reducible]

instance MultiplicativeBasisDeformations.MeshWalk.instGroupoidSD {V : Type} [Quiver V] (Q : TranslationQuiver V) (v₀ : V) (K : Type w) [CommGroup K] : CategoryTheory.Groupoid (SD Q v₀ K)

theorem MultiplicativeBasisDeformations.MeshWalk.SD_comp_fst {V : Type} [Quiver V] (Q : TranslationQuiver V) (v₀ : V) (K : Type w) [CommGroup K] {A B C : SD Q v₀ K} (f : A ⟶ B) (g : B ⟶ C) : (CategoryTheory.CategoryStruct.comp f g).1 = CategoryTheory.CategoryStruct.comp f.1 g.1

theorem MultiplicativeBasisDeformations.MeshWalk.SD_comp_snd {V : Type} [Quiver V] (Q : TranslationQuiver V) (v₀ : V) (K : Type w) [CommGroup K] {A B C : SD Q v₀ K} (f : A ⟶ B) (g : B ⟶ C) (γ : obC Q v₀ v₀ ⟶ obC Q v₀ A) : (CategoryTheory.CategoryStruct.comp f g).2 γ = f.2 γ * g.2 (CategoryTheory.CategoryStruct.comp γ f.1)

def MultiplicativeBasisDeformations.MeshWalk.toSD {V : Type} [Quiver V] (Q : TranslationQuiver V) (v₀ : V) (K : Type w) (X : V) : SD Q v₀ K

A vertex as an object of the semidirect groupoid.

def MultiplicativeBasisDeformations.MeshWalk.prj {V : Type} [Quiver V] (Q : TranslationQuiver V) (v₀ : V) (K : Type w) [CommGroup K] : CategoryTheory.Functor (SD Q v₀ K) (PiC Q v₀)

The projection to the fundamental groupoid.

def MultiplicativeBasisDeformations.MeshWalk.Ψ {V : Type} [Quiver V] {Q : TranslationQuiver V} {v₀ : V} {K : Type w} [CommGroup K] (W : (e : Ed Q ⊕ V) → (obC Q v₀ v₀ ⟶ obC Q v₀ (srcC Q v₀ e)) → K) (hW : ∀ (x : ↑Q.nonprojective) (a : (y : V) × (y ⟶ ↑x)) (γ : obC Q v₀ v₀ ⟶ obC Q v₀ ↑(Q.tau x)), W (Sum.inl (Sum.inl ⟨↑(Q.tau x), ⟨a.fst, (Q.mate x a.fst) a.snd⟩⟩)) γ * W (Sum.inl (Sum.inl ⟨a.fst, ⟨↑x, a.snd⟩⟩)) (CategoryTheory.CategoryStruct.comp γ (arrC Q v₀ ((Q.mate x a.fst) a.snd))) = W (Sum.inl (Sum.inr x)) γ) : CategoryTheory.Functor (PiC Q v₀) (SD Q v₀ K)

The transport functor of a weight respecting the triangles.

theorem MultiplicativeBasisDeformations.MeshWalk.Ψ_edge {V : Type} [Quiver V] {Q : TranslationQuiver V} {v₀ : V} {K : Type w} [CommGroup K] (W : (e : Ed Q ⊕ V) → (obC Q v₀ v₀ ⟶ obC Q v₀ (srcC Q v₀ e)) → K) (hW : ∀ (x : ↑Q.nonprojective) (a : (y : V) × (y ⟶ ↑x)) (γ : obC Q v₀ v₀ ⟶ obC Q v₀ ↑(Q.tau x)), W (Sum.inl (Sum.inl ⟨↑(Q.tau x), ⟨a.fst, (Q.mate x a.fst) a.snd⟩⟩)) γ * W (Sum.inl (Sum.inl ⟨a.fst, ⟨↑x, a.snd⟩⟩)) (CategoryTheory.CategoryStruct.comp γ (arrC Q v₀ ((Q.mate x a.fst) a.snd))) = W (Sum.inl (Sum.inr x)) γ) (e : Ed Q ⊕ V) : (Ψ W hW).map (edgeC Q v₀ e) = (edgeC Q v₀ e, W e)

theorem MultiplicativeBasisDeformations.MeshWalk.Ψ_prj {V : Type} [Quiver V] {Q : TranslationQuiver V} {v₀ : V} {K : Type w} [CommGroup K] (W : (e : Ed Q ⊕ V) → (obC Q v₀ v₀ ⟶ obC Q v₀ (srcC Q v₀ e)) → K) (hW : ∀ (x : ↑Q.nonprojective) (a : (y : V) × (y ⟶ ↑x)) (γ : obC Q v₀ v₀ ⟶ obC Q v₀ ↑(Q.tau x)), W (Sum.inl (Sum.inl ⟨↑(Q.tau x), ⟨a.fst, (Q.mate x a.fst) a.snd⟩⟩)) γ * W (Sum.inl (Sum.inl ⟨a.fst, ⟨↑x, a.snd⟩⟩)) (CategoryTheory.CategoryStruct.comp γ (arrC Q v₀ ((Q.mate x a.fst) a.snd))) = W (Sum.inl (Sum.inr x)) γ) : (Ψ W hW).comp (prj Q v₀ K) = CategoryTheory.Functor.id (PiC Q v₀)

Simple connectivity: the walk component of the transport is the walk.

theorem MultiplicativeBasisDeformations.MeshWalk.Ψ_fst {V : Type} [Quiver V] {Q : TranslationQuiver V} {v₀ : V} {K : Type w} [CommGroup K] (W : (e : Ed Q ⊕ V) → (obC Q v₀ v₀ ⟶ obC Q v₀ (srcC Q v₀ e)) → K) (hW : ∀ (x : ↑Q.nonprojective) (a : (y : V) × (y ⟶ ↑x)) (γ : obC Q v₀ v₀ ⟶ obC Q v₀ ↑(Q.tau x)), W (Sum.inl (Sum.inl ⟨↑(Q.tau x), ⟨a.fst, (Q.mate x a.fst) a.snd⟩⟩)) γ * W (Sum.inl (Sum.inl ⟨a.fst, ⟨↑x, a.snd⟩⟩)) (CategoryTheory.CategoryStruct.comp γ (arrC Q v₀ ((Q.mate x a.fst) a.snd))) = W (Sum.inl (Sum.inr x)) γ) {A B : V} (π : obC Q v₀ A ⟶ obC Q v₀ B) : ((Ψ W hW).map π).1 = π

def MultiplicativeBasisDeformations.MeshWalk.potW {V : Type} [Quiver V] {Q : TranslationQuiver V} {v₀ : V} {K : Type w} [CommGroup K] (W : (e : Ed Q ⊕ V) → (obC Q v₀ v₀ ⟶ obC Q v₀ (srcC Q v₀ e)) → K) (hW : ∀ (x : ↑Q.nonprojective) (a : (y : V) × (y ⟶ ↑x)) (γ : obC Q v₀ v₀ ⟶ obC Q v₀ ↑(Q.tau x)), W (Sum.inl (Sum.inl ⟨↑(Q.tau x), ⟨a.fst, (Q.mate x a.fst) a.snd⟩⟩)) γ * W (Sum.inl (Sum.inl ⟨a.fst, ⟨↑x, a.snd⟩⟩)) (CategoryTheory.CategoryStruct.comp γ (arrC Q v₀ ((Q.mate x a.fst) a.snd))) = W (Sum.inl (Sum.inr x)) γ) {X : V} (γ : obC Q v₀ v₀ ⟶ obC Q v₀ X) : K

The object values: the transport along a walk from the basepoint.

theorem MultiplicativeBasisDeformations.MeshWalk.potW_comp {V : Type} [Quiver V] {Q : TranslationQuiver V} {v₀ : V} {K : Type w} [CommGroup K] (W : (e : Ed Q ⊕ V) → (obC Q v₀ v₀ ⟶ obC Q v₀ (srcC Q v₀ e)) → K) (hW : ∀ (x : ↑Q.nonprojective) (a : (y : V) × (y ⟶ ↑x)) (γ : obC Q v₀ v₀ ⟶ obC Q v₀ ↑(Q.tau x)), W (Sum.inl (Sum.inl ⟨↑(Q.tau x), ⟨a.fst, (Q.mate x a.fst) a.snd⟩⟩)) γ * W (Sum.inl (Sum.inl ⟨a.fst, ⟨↑x, a.snd⟩⟩)) (CategoryTheory.CategoryStruct.comp γ (arrC Q v₀ ((Q.mate x a.fst) a.snd))) = W (Sum.inl (Sum.inr x)) γ) (e : Ed Q ⊕ V) (γ : obC Q v₀ v₀ ⟶ obC Q v₀ (srcC Q v₀ e)) : potW W hW (CategoryTheory.CategoryStruct.comp γ (edgeC Q v₀ e)) = potW W hW γ * W e γ