The deck group and the walk-class grading

Subsection 4.2 (subsec:universal-cover, scalar-normalization.tex): "Let K̃ be the universal cover of K, constructed from walks starting at a basepoint, modulo edge cancellation and the triangle relations. The fundamental group G acts on this cover by deck transformations." A lifted vertex is a vertex X with the class of a walk from the basepoint; a path of Γ lifts uniquely from a chosen lift of its source.

Formally we fix a basepoint v₀ and adjoin to K a cone of edges s_X : v₀ → X without triangles. This makes the complex connected without changing the argument (the source assumes A connected; with the cone, the cover is a disjoint union of universal covers of the components of K, and G is still free by the collapse of Lemma 4.2). The lift (X, h) of X in sheet h ∈ G is the walk class h · s_X; a path p : X → Y lifts from sheet h to sheet h · deg p, where deg p = s_X p s_Y⁻¹ (degW). Mesh relations are homogeneous for deg (their terms are homotopic to t_X), so deg grades C(Q, c) (WeightGrading.lean): this is the covering formula eq:walk-hom-sum. Edges have length one, translation edges length two and cone edges length zero; triangles preserve length, so length is a homomorphism ℓ : G → ℤ with ℓ (deg p) = |p| (len_degW); this is the height of the source.

def MultiplicativeBasisDeformations.Morse.Tris.ext {V Ed E : Type} {src tgt : Ed → V} (S : Tris src tgt) (srcE tgtE : E → V) : Tris (Sum.elim src srcE) (Sum.elim tgt tgtE)

The complex with additional edges and the same triangles.

theorem MultiplicativeBasisDeformations.Morse.Tris.ext_edge {V Ed E : Type} {src tgt : Ed → V} (S : Tris src tgt) (srcE tgtE : E → V) (t : S.T) (i : Fin 3) : (S.ext srcE tgtE).edge t i = Sum.inl (S.edge t i)

def MultiplicativeBasisDeformations.Morse.Matching.ext {V Ed E : Type} {src tgt : Ed → V} {S : Tris src tgt} (srcE tgtE : E → V) (M : Matching S) : Matching (S.ext srcE tgtE)

A matching extends to the complex with additional edges.

def MultiplicativeBasisDeformations.Morse.edgesP {V Ed : Type} {src tgt : Ed → V} {D : Type u_1} [CategoryTheory.Groupoid D] (obj : V → D) (val : (e : Ed) → obj (src e) ⟶ obj (tgt e)) : EQ src tgt ⥤q D

The prefunctor on edges given by values in a groupoid.

def MultiplicativeBasisDeformations.Morse.liftEdges {V Ed : Type} {src tgt : Ed → V} (S : Tris src tgt) {D : Type u_1} [CategoryTheory.Groupoid D] (obj : V → D) (val : (e : Ed) → obj (src e) ⟶ obj (tgt e)) (hrel : ∀ (t : S.T), CategoryTheory.CategoryStruct.comp (val (S.f t)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (val (S.g t))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (val (S.h t)) (CategoryTheory.eqToHom ⋯))) : CategoryTheory.Functor (Pi S) D

A functor out of the fundamental groupoid, from values on edges that respect the triangles.

theorem MultiplicativeBasisDeformations.Morse.liftEdges_obj {V Ed : Type} {src tgt : Ed → V} (S : Tris src tgt) {D : Type u_1} [CategoryTheory.Groupoid D] (obj : V → D) (val : (e : Ed) → obj (src e) ⟶ obj (tgt e)) (hrel : ∀ (t : S.T), CategoryTheory.CategoryStruct.comp (val (S.f t)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (val (S.g t))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (val (S.h t)) (CategoryTheory.eqToHom ⋯))) (X : V) : (liftEdges S obj val hrel).obj (Qf.obj (ob src tgt X)) = obj X

theorem MultiplicativeBasisDeformations.Morse.liftEdges_edge {V Ed : Type} {src tgt : Ed → V} (S : Tris src tgt) {D : Type u_1} [CategoryTheory.Groupoid D] (obj : V → D) (val : (e : Ed) → obj (src e) ⟶ obj (tgt e)) (hrel : ∀ (t : S.T), CategoryTheory.CategoryStruct.comp (val (S.f t)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (val (S.g t))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (val (S.h t)) (CategoryTheory.eqToHom ⋯))) (e : Ed) : (liftEdges S obj val hrel).map (Qf.map (ofE src tgt e)) = val e

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.MeshWalk.srcC {V : Type} [Quiver V] (Q : TranslationQuiver V) (v₀ : V) : Ed Q ⊕ V → V

The source of an edge of the coned complex.

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.MeshWalk.tgtC {V : Type} [Quiver V] (Q : TranslationQuiver V) : Ed Q ⊕ V → V

The target of an edge of the coned complex.

def MultiplicativeBasisDeformations.MeshWalk.coneTris {V : Type} [Quiver V] (Q : TranslationQuiver V) (v₀ : V) : Morse.Tris (srcC Q v₀) (tgtC Q)

The complex K with a cone of edges s_X : v₀ → X.

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.MeshWalk.PiC {V : Type} [Quiver V] (Q : TranslationQuiver V) (v₀ : V) : Type

Its fundamental groupoid.

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.MeshWalk.obC {V : Type} [Quiver V] (Q : TranslationQuiver V) (v₀ X : V) : PiC Q v₀

A vertex as an object of PiC.

def MultiplicativeBasisDeformations.MeshWalk.edgeC {V : Type} [Quiver V] (Q : TranslationQuiver V) (v₀ : V) (e : Ed Q ⊕ V) : obC Q v₀ (srcC Q v₀ e) ⟶ obC Q v₀ (tgtC Q e)

The class of an edge.

def MultiplicativeBasisDeformations.MeshWalk.arrC {V : Type} [Quiver V] (Q : TranslationQuiver V) (v₀ : V) {y x : V} (a : y ⟶ x) : obC Q v₀ y ⟶ obC Q v₀ x

The class of an arrow.

def MultiplicativeBasisDeformations.MeshWalk.tC {V : Type} [Quiver V] (Q : TranslationQuiver V) (v₀ : V) (x : ↑Q.nonprojective) : obC Q v₀ ↑(Q.tau x) ⟶ obC Q v₀ ↑x

The class of a translation edge t_x : τ x → x.

def MultiplicativeBasisDeformations.MeshWalk.coneC {V : Type} [Quiver V] (Q : TranslationQuiver V) (v₀ X : V) : obC Q v₀ v₀ ⟶ obC Q v₀ X

The class of a cone edge s_X : v₀ → X.

@[irreducible]

def MultiplicativeBasisDeformations.MeshWalk.pathC {V : Type} [Quiver V] (Q : TranslationQuiver V) (v₀ : V) {x y : V} : Quiver.Path x y → (obC Q v₀ x ⟶ obC Q v₀ y)

The class of a path.

theorem MultiplicativeBasisDeformations.MeshWalk.pathC_comp {V : Type} [Quiver V] (Q : TranslationQuiver V) (v₀ : V) {x y z : V} (p : Quiver.Path x y) (q : Quiver.Path y z) : pathC Q v₀ (p.comp q) = CategoryTheory.CategoryStruct.comp (pathC Q v₀ p) (pathC Q v₀ q)

theorem MultiplicativeBasisDeformations.MeshWalk.pathC_toPath {V : Type} [Quiver V] (Q : TranslationQuiver V) (v₀ : V) {x y : V} (a : x ⟶ y) : pathC Q v₀ a.toPath = arrC Q v₀ a

theorem MultiplicativeBasisDeformations.MeshWalk.tri_rel {V : Type} [Quiver V] (Q : TranslationQuiver V) (v₀ : V) (x : ↑Q.nonprojective) (a : (y : V) × (y ⟶ ↑x)) : CategoryTheory.CategoryStruct.comp (arrC Q v₀ ((Q.mate x a.fst) a.snd)) (arrC Q v₀ a.snd) = tC Q v₀ x

The mesh triangles: (σ a) a = t_x in the fundamental groupoid.

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.MeshWalk.Deck {V : Type} [Quiver V] (Q : TranslationQuiver V) (v₀ : V) : Type

The deck group: loops at the basepoint, multiplied in walk order.

def MultiplicativeBasisDeformations.MeshWalk.degW {V : Type} [Quiver V] (Q : TranslationQuiver V) (v₀ : V) : PathWeight V (Deck Q v₀)

The walk-class weight deg p = s_X p s_Y⁻¹.

theorem MultiplicativeBasisDeformations.MeshWalk.degW_deg {V : Type} [Quiver V] (Q : TranslationQuiver V) (v₀ : V) {x y : V} (p : Quiver.Path x y) : (degW Q v₀).deg p = MulOpposite.op (CategoryTheory.CategoryStruct.comp (coneC Q v₀ x) (CategoryTheory.CategoryStruct.comp (pathC Q v₀ p) (CategoryTheory.Groupoid.inv (coneC Q v₀ y))))

theorem MultiplicativeBasisDeformations.MeshWalk.meshHomogeneous {V : Type} [Quiver V] (Q : TranslationQuiver V) (v₀ : V) : ScalarMeshCategory.MeshHomogeneous (degW Q v₀)

The mesh relations are homogeneous for the walk-class weight.

Freeness of the deck group

theorem MultiplicativeBasisDeformations.MeshWalk.isFreeGroup_deck {V : Type} [Quiver V] (Q : TranslationQuiver V) (v₀ : 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)) : IsFreeGroup (Deck Q v₀)

The deck group is free (Lemma 4.2, for the coned complex).

Length

def MultiplicativeBasisDeformations.MeshWalk.lenE {V : Type} [Quiver V] (Q : TranslationQuiver V) : Ed Q ⊕ V → ℤ

Lengths of edges: one for arrows, two for translation edges, zero for cone edges.

def MultiplicativeBasisDeformations.MeshWalk.lenF {V : Type} [Quiver V] (Q : TranslationQuiver V) (v₀ : V) : CategoryTheory.Functor (PiC Q v₀) (CategoryTheory.SingleObj (Multiplicative ℤ))

The length functor on the fundamental groupoid.

theorem MultiplicativeBasisDeformations.MeshWalk.lenF_edge {V : Type} [Quiver V] (Q : TranslationQuiver V) (v₀ : V) (e : Ed Q ⊕ V) : (lenF Q v₀).map (edgeC Q v₀ e) = Multiplicative.ofAdd (lenE Q e)

theorem MultiplicativeBasisDeformations.MeshWalk.lenF_arrC {V : Type} [Quiver V] (Q : TranslationQuiver V) (v₀ : V) {x y : V} (a : x ⟶ y) : (lenF Q v₀).map (arrC Q v₀ a) = Multiplicative.ofAdd 1

theorem MultiplicativeBasisDeformations.MeshWalk.lenF_coneC {V : Type} [Quiver V] (Q : TranslationQuiver V) (v₀ X : V) : (lenF Q v₀).map (coneC Q v₀ X) = Multiplicative.ofAdd 0

theorem MultiplicativeBasisDeformations.MeshWalk.lenF_pathC {V : Type} [Quiver V] (Q : TranslationQuiver V) (v₀ : V) {x y : V} (p : Quiver.Path x y) : (lenF Q v₀).map (pathC Q v₀ p) = Multiplicative.ofAdd ↑p.length

def MultiplicativeBasisDeformations.MeshWalk.hgt {V : Type} [Quiver V] (Q : TranslationQuiver V) (v₀ : V) (g : Deck Q v₀) : ℤ

The length homomorphism ℓ : G → ℤ.

theorem MultiplicativeBasisDeformations.MeshWalk.hgt_mul {V : Type} [Quiver V] (Q : TranslationQuiver V) (v₀ : V) (g h : Deck Q v₀) : hgt Q v₀ (g * h) = hgt Q v₀ g + hgt Q v₀ h

theorem MultiplicativeBasisDeformations.MeshWalk.hgt_one {V : Type} [Quiver V] (Q : TranslationQuiver V) (v₀ : V) : hgt Q v₀ 1 = 0

theorem MultiplicativeBasisDeformations.MeshWalk.hgt_degW {V : Type} [Quiver V] (Q : TranslationQuiver V) (v₀ : V) {x y : V} (p : Quiver.Path x y) : hgt Q v₀ ((degW Q v₀).deg p) = ↑p.length

Height: the length of a path is the length of its walk class.