The deck group of Proposition 7.2 is π₁(K)

prop:integral-ray-weights: "let G be the free deck group of Subsection 4.2", the fundamental group of the mesh complex K acting on the universal cover. The formalization's deck group is the fundamental group of K with a cone of edges s_X : v₀ → X adjoined (DeckGrading.lean), and Proposition 7.2 is proved for the stabilizer H of the component 𝓛₀ of a base object of the lifted projective category (RayWeightsIso.lean). For a connected quiver whose meshes have nonempty middle terms (the Auslander–Reiten quiver of a connected algebra), this file identifies H with π₁(K, b), b the base vertex, and 𝓛₀ with the lifted projectives of the universal cover of K:

• the inclusion K ⊂ K ∪ cone (incl) has a retraction (retr, sending s_X to a walk from v₀ to X), so w ↦ s_b w s_b⁻¹ is injective on π₁(K, b) (φ, φ_injective);
• the degree of a nonzero piece of A₀ is the class of a path (exists_path_of_nz), so the objects of 𝓛₀ are (x, s_b w s_x⁻¹) with w a walk class b → x (conn_δ), and H lies in the image of φ;
• conversely every walk class is realized by a zigzag of arrows in the lifted quiver (translation edges by the two arrows of a mesh, aconn_δ), whose lifted projectives lie in 𝓛₀ by the support lemma (conn_of_aconn); so the image of φ is H (range_φ, piOneEquiv). The connectedness of the quiver follows from that of A₀ (qConn_of_A0Conn: every vertex receives a nonzero map from a projective, and nonzero maps are combinations of paths); for Γ_A the meshes have nonempty middle terms (IndSkeleton.ar_hmid) and A₀ is connected for connected A (IndSkeleton.a0Conn_ar). Hence Proposition 7.2(1) holds with G = π₁(K, b): W(P) ≅ ℤ^{n−1} ⊕ π₁(K, b)_ab (WPequivFreePi1, theta_summand_pi1), and 𝓛₀ is the lifted projective category of the universal cover, equivariantly (liftEquiv, liftEquiv_act), so the coinvariants (I_𝓛₀)_H of coinvEquiv are (I_𝓛)_G.

theorem MultiplicativeBasisDeformations.Morse.Pi_ext {V Ed : Type} {src tgt : Ed → V} (S : Tris src tgt) {D : Type u_1} [CategoryTheory.Groupoid D] (F G : CategoryTheory.Functor (Pi S) D) (hobj : ∀ (X : V), F.obj (Qf.obj (ob src tgt X)) = G.obj (Qf.obj (ob src tgt X))) (hmap : ∀ (e : Ed), F.map (Qf.map (ofE src tgt e)) ≍ G.map (Qf.map (ofE src tgt e))) : F = G

Functors out of the fundamental groupoid agree if they agree on the edges (with equal objects).

def MultiplicativeBasisDeformations.MeshWalk.edgeK {V : Type} [Quiver V] (Q : TranslationQuiver V) (e : Ed Q) : obK Q (src Q e) ⟶ obK Q (tgt Q e)

The class of an edge of K.

def MultiplicativeBasisDeformations.MeshWalk.incl {V : Type} [Quiver V] (Q : TranslationQuiver V) (v₀ : V) : CategoryTheory.Functor (PiK Q) (PiC Q v₀)

The inclusion K ⊂ K ∪ cone on fundamental groupoids.

theorem MultiplicativeBasisDeformations.MeshWalk.incl_edge {V : Type} [Quiver V] [Fintype V] [DecidableEq V] (Q : TranslationQuiver V) [(x : V) → Fintype ((y : V) × (y ⟶ x))] [hone : ∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] (v₀ : V) (e : Ed Q) : (incl Q v₀).map (edgeK Q e) = edgeC Q v₀ (Sum.inl e)

def MultiplicativeBasisDeformations.MeshWalk.retr {V : Type} [Quiver V] (Q : TranslationQuiver V) (v₀ : V) (w : (X : V) → obK Q v₀ ⟶ obK Q X) : CategoryTheory.Functor (PiC Q v₀) (PiK Q)

The retraction, sending the cone edge s_X to a walk class v₀ → X of K.

theorem MultiplicativeBasisDeformations.MeshWalk.retr_edge {V : Type} [Quiver V] [Fintype V] [DecidableEq V] (Q : TranslationQuiver V) [(x : V) → Fintype ((y : V) × (y ⟶ x))] [hone : ∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] (v₀ : V) (w : (X : V) → obK Q v₀ ⟶ obK Q X) (e : Ed Q) : (retr Q v₀ w).map (edgeC Q v₀ (Sum.inl e)) = edgeK Q e

theorem MultiplicativeBasisDeformations.MeshWalk.incl_retr {V : Type} [Quiver V] [Fintype V] [DecidableEq V] (Q : TranslationQuiver V) [(x : V) → Fintype ((y : V) × (y ⟶ x))] [hone : ∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] (v₀ : V) (w : (X : V) → obK Q v₀ ⟶ obK Q X) : (incl Q v₀).comp (retr Q v₀ w) = CategoryTheory.Functor.id (PiK Q)

theorem MultiplicativeBasisDeformations.MeshWalk.incl_map_injective {V : Type} [Quiver V] [Fintype V] [DecidableEq V] (Q : TranslationQuiver V) [(x : V) → Fintype ((y : V) × (y ⟶ x))] [hone : ∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] (v₀ : V) (w : (X : V) → obK Q v₀ ⟶ obK Q X) {X Y : V} {f f' : obK Q X ⟶ obK Q Y} (h : (incl Q v₀).map f = (incl Q v₀).map f') : f = f'

The conjugated walk class δ(w) = s_X w s_Y⁻¹

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

The inclusion on morphisms, with the objects of PiC.

theorem MultiplicativeBasisDeformations.MeshWalk.inclMap_comp {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] [hone : ∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] {v₀ X Y Z : V} (w : obK Q X ⟶ obK Q Y) (w' : obK Q Y ⟶ obK Q Z) : inclMap (CategoryTheory.CategoryStruct.comp w w') = CategoryTheory.CategoryStruct.comp (inclMap w) (inclMap w')

theorem MultiplicativeBasisDeformations.MeshWalk.inclMap_id {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] [hone : ∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] {v₀ : V} (X : V) : inclMap (CategoryTheory.CategoryStruct.id (obK Q X)) = CategoryTheory.CategoryStruct.id (obC Q v₀ X)

def MultiplicativeBasisDeformations.MeshWalk.δ {V : Type} [Quiver V] {Q : TranslationQuiver V} {v₀ X Y : V} (w : obK Q X ⟶ obK Q Y) : Deck Q v₀

δ(w) = s_X w s_Y⁻¹ in the deck group.

theorem MultiplicativeBasisDeformations.MeshWalk.δ_comp {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] [hone : ∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] {v₀ X Y Z : V} (w : obK Q X ⟶ obK Q Y) (w' : obK Q Y ⟶ obK Q Z) : δ (CategoryTheory.CategoryStruct.comp w w') = δ w * δ w'

theorem MultiplicativeBasisDeformations.MeshWalk.δ_id {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] [hone : ∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] {v₀ : V} (X : V) : δ (CategoryTheory.CategoryStruct.id (obK Q X)) = 1

theorem MultiplicativeBasisDeformations.MeshWalk.δ_inv {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] [hone : ∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] {v₀ X Y : V} (w : obK Q X ⟶ obK Q Y) : δ (CategoryTheory.Groupoid.inv w) = (δ w)⁻¹

theorem MultiplicativeBasisDeformations.MeshWalk.δ_injective {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] [hone : ∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] {v₀ : V} (w : (X : V) → obK Q v₀ ⟶ obK Q X) {X Y : V} {f f' : obK Q X ⟶ obK Q Y} (h : δ f = δ f') : f = f'

def MultiplicativeBasisDeformations.MeshWalk.arrK {V : Type} [Quiver V] (Q : TranslationQuiver V) {y x : V} (a : y ⟶ x) : obK Q y ⟶ obK Q x

The class of an arrow in π₁(K).

theorem MultiplicativeBasisDeformations.MeshWalk.inclMap_arrK {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] [hone : ∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] {v₀ y x : V} (a : y ⟶ x) : inclMap (arrK Q a) = arrC Q v₀ a

@[irreducible]

def MultiplicativeBasisDeformations.MeshWalk.pathK {V : Type} [Quiver V] (Q : TranslationQuiver V) {x y : V} : Quiver.Path x y → (obK Q x ⟶ obK Q y)

The class of a path in π₁(K).

theorem MultiplicativeBasisDeformations.MeshWalk.inclMap_pathK {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] [hone : ∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] {v₀ x y : V} (p : Quiver.Path x y) : inclMap (pathK Q p) = pathC Q v₀ p

theorem MultiplicativeBasisDeformations.MeshWalk.δ_pathK {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] [hone : ∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] {v₀ x y : V} (p : Quiver.Path x y) : δ (pathK Q p) = (degW Q v₀).deg p

theorem MultiplicativeBasisDeformations.MeshWalk.δ_arrK {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] [hone : ∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] {v₀ y x : V} (a : y ⟶ x) : δ (arrK Q a) = dg Q v₀ a

def MultiplicativeBasisDeformations.MeshWalk.tK {V : Type} [Quiver V] {Q : TranslationQuiver V} (x : ↑Q.nonprojective) : obK Q ↑(Q.tau x) ⟶ obK Q ↑x

The class of a translation edge in π₁(K).

theorem MultiplicativeBasisDeformations.MeshWalk.triK {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] [hone : ∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] (x : ↑Q.nonprojective) {y : V} (b : y ⟶ ↑x) : CategoryTheory.CategoryStruct.comp (arrK Q ((Q.mate x y) b)) (arrK Q b) = tK x

Zigzags of arrows realize walk classes

structure MultiplicativeBasisDeformations.MeshWalk.Tg {V : Type} [Quiver V] (_Q : TranslationQuiver V) (_v₀ : V) : Type

Vertices of K, with morphisms the deck elements realized by arrow zigzags.

• v : V

structure MultiplicativeBasisDeformations.MeshWalk.TgHom {V : Type} [Quiver V] (Q : TranslationQuiver V) (v₀ X Y : V) : Type

A deck element realized by arrow zigzags from every sheet.

• d : Deck Q v₀
• h (g : Deck Q v₀) : aconn Q v₀ (X, g) (Y, g * self.d)

theorem MultiplicativeBasisDeformations.MeshWalk.TgHom.ext {V : Type} {inst✝ : Quiver V} {Q : TranslationQuiver V} {v₀ X Y : V} {x y : TgHom Q v₀ X Y} (d : x.d = y.d) : x = y

theorem MultiplicativeBasisDeformations.MeshWalk.TgHom.ext_iff {V : Type} {inst✝ : Quiver V} {Q : TranslationQuiver V} {v₀ X Y : V} {x y : TgHom Q v₀ X Y} : x = y ↔ x.d = y.d

@[instance_reducible]

instance MultiplicativeBasisDeformations.MeshWalk.instGroupoidTg {V : Type} [Quiver V] {Q : TranslationQuiver V} {v₀ : V} : CategoryTheory.Groupoid (Tg Q v₀)

def MultiplicativeBasisDeformations.MeshWalk.tgd {V : Type} [Quiver V] {Q : TranslationQuiver V} {v₀ : V} {X Y : Tg Q v₀} (f : X ⟶ Y) : Deck Q v₀

The deck element of a morphism of Tg.

theorem MultiplicativeBasisDeformations.MeshWalk.tgd_h {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] [hone : ∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] {v₀ : V} {X Y : Tg Q v₀} (f : X ⟶ Y) (g : Deck Q v₀) : aconn Q v₀ (X.v, g) (Y.v, g * tgd f)

theorem MultiplicativeBasisDeformations.MeshWalk.tgd_ext {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] [hone : ∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] {v₀ : V} {X Y : Tg Q v₀} {f g : X ⟶ Y} (h : tgd f = tgd g) : f = g

theorem MultiplicativeBasisDeformations.MeshWalk.Tg_comp_d {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] [hone : ∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] {v₀ : V} {X Y Z : Tg Q v₀} (f : X ⟶ Y) (g : Y ⟶ Z) : tgd (CategoryTheory.CategoryStruct.comp f g) = tgd f * tgd g

theorem MultiplicativeBasisDeformations.MeshWalk.Tg_eqToHom_d {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] [hone : ∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] {v₀ : V} {X Y : Tg Q v₀} (p : X = Y) : tgd (CategoryTheory.eqToHom p) = 1

theorem MultiplicativeBasisDeformations.MeshWalk.edge_aconn {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] [hone : ∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] {v₀ : V} (hmid : ∀ (x : ↑Q.nonprojective), Nonempty ((y : V) × (y ⟶ ↑x))) (e : Ed Q) (h : Deck Q v₀) : aconn Q v₀ (src Q e, h) (tgt Q e, h * δ (edgeK Q e))

def MultiplicativeBasisDeformations.MeshWalk.Fa {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] [hone : ∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] {v₀ : V} (hmid : ∀ (x : ↑Q.nonprojective), Nonempty ((y : V) × (y ⟶ ↑x))) : CategoryTheory.Functor (PiK Q) (Tg Q v₀)

The walk classes as arrow zigzags.

def MultiplicativeBasisDeformations.MeshWalk.Eu {V : Type} [Quiver V] {Q : TranslationQuiver V} {v₀ : V} : CategoryTheory.Functor (Tg Q v₀) (PiC Q v₀)

Undo the conjugation by the cone edges.

theorem MultiplicativeBasisDeformations.MeshWalk.Fa_Eu {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] [hone : ∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] {v₀ : V} (hmid : ∀ (x : ↑Q.nonprojective), Nonempty ((y : V) × (y ⟶ ↑x))) : (Fa hmid).comp Eu = incl Q v₀

theorem MultiplicativeBasisDeformations.MeshWalk.Fa_d {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] [hone : ∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] {v₀ : V} (hmid : ∀ (x : ↑Q.nonprojective), Nonempty ((y : V) × (y ⟶ ↑x))) {X Y : V} (w : obK Q X ⟶ obK Q Y) : tgd ((Fa hmid).map w) = δ w

theorem MultiplicativeBasisDeformations.MeshWalk.aconn_δ {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] [hone : ∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] {v₀ : V} (hmid : ∀ (x : ↑Q.nonprojective), Nonempty ((y : V) × (y ⟶ ↑x))) {X Y : V} (w : obK Q X ⟶ obK Q Y) (h : Deck Q v₀) : aconn Q v₀ (X, h) (Y, h * δ w)

Every walk class is realized by a zigzag of arrows in the lifted quiver.

H ≅ π₁(K, b)

theorem MultiplicativeBasisDeformations.MeshWalk.conn_δ {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] [hone : ∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] {v₀ : V} {k : Type u_1} [Field k] [IsAlgClosed k] [Infinite k] {c : MeshCoefficients k Q} {L : CatAlg.LocalFamily (meshFam Q c)} {D : CatAlg.MeshData (meshFam Q c) L} [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] {o o' : LObj Q c v₀ D} (h : conn Q c v₀ D o o') : ∃ (w : obK Q ↑o.1 ⟶ obK Q ↑o'.1), o'.2 = o.2 * δ w

The lifted projectives connected in L differ by conjugated walk classes.

theorem MultiplicativeBasisDeformations.MeshWalk.exists_walk {V : Type} [Quiver V] {Q : TranslationQuiver V} (hQ : QConn V) (X Y : V) : Nonempty (obK Q X ⟶ obK Q Y)

theorem MultiplicativeBasisDeformations.MeshWalk.exists_path_of_part {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] [hone : ∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] {v₀ : V} {k : Type u_1} [Field k] [IsAlgClosed k] [Infinite k] {c : MeshCoefficients k Q} [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] {x y : V} {g : Deck Q v₀} {m : meshFam Q c x ⟶ meshFam Q c y} (hm : m ∈ (deckGrading Q c v₀).part g x y) (hm0 : m ≠ 0) : Nonempty (Quiver.Path x y)

A nonzero homogeneous morphism of the mesh category is a combination of paths of its degree; in particular there is a path.

theorem MultiplicativeBasisDeformations.MeshWalk.eqvGen_of_path {V : Type} [Quiver V] {x y : V} (p : Quiver.Path x y) : Relation.EqvGen (fun (X Y : V) => Nonempty (X ⟶ Y)) x y

theorem MultiplicativeBasisDeformations.MeshWalk.qConn_of_A0Conn {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] [hone : ∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] {v₀ : V} {k : Type u_1} [Field k] [IsAlgClosed k] [Infinite k] {c : MeshCoefficients k Q} {L : CatAlg.LocalFamily (meshFam Q c)} {D : CatAlg.MeshData (meshFam Q c) L} [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] {x₀ : D.PV} (hconn : A0Conn Q c v₀ D x₀) : QConn V

The quiver is connected when A₀ is: every vertex receives a nonzero map from a projective (the support lemma), and nonzero maps are combinations of paths.

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.MeshWalk.PiOne {V : Type} [Quiver V] (Q : TranslationQuiver V) (b : V) : Type

π₁(K, b), with the multiplication convention of the deck group.

def MultiplicativeBasisDeformations.MeshWalk.φ {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] [hone : ∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] (v₀ b : V) : PiOne Q b →* Deck Q v₀

g ↦ s_b g s_b⁻¹.

theorem MultiplicativeBasisDeformations.MeshWalk.φ_injective {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] [hone : ∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] {v₀ : V} (hQ : QConn V) (b : V) : Function.Injective ⇑(φ v₀ b)

theorem MultiplicativeBasisDeformations.MeshWalk.conn_of_walk {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] [hone : ∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] {v₀ : V} {k : Type u_1} [Field k] [IsAlgClosed k] [Infinite k] {c : MeshCoefficients k Q} {L : CatAlg.LocalFamily (meshFam Q c)} {D : CatAlg.MeshData (meshFam Q c) L} [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] (hmid : ∀ (x : ↑Q.nonprojective), Nonempty ((y : V) × (y ⟶ ↑x))) (x₀ x : D.PV) (w : obK Q ↑x₀ ⟶ obK Q ↑x) : conn Q c v₀ D (o₀ Q c v₀ D x₀) (x, δ w)

theorem MultiplicativeBasisDeformations.MeshWalk.range_φ {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] [hone : ∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] {v₀ : V} {k : Type u_1} [Field k] [IsAlgClosed k] [Infinite k] {c : MeshCoefficients k Q} {L : CatAlg.LocalFamily (meshFam Q c)} {D : CatAlg.MeshData (meshFam Q c) L} [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] (hmid : ∀ (x : ↑Q.nonprojective), Nonempty ((y : V) × (y ⟶ ↑x))) (hQ : QConn V) (x₀ : D.PV) : (φ v₀ ↑x₀).range = Hs Q c v₀ D x₀

The image of π₁(K, b) is the stabilizer H of the base component.

noncomputable def MultiplicativeBasisDeformations.MeshWalk.piOneEquiv {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] [hone : ∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] {v₀ : V} {k : Type u_1} [Field k] [IsAlgClosed k] [Infinite k] {c : MeshCoefficients k Q} {L : CatAlg.LocalFamily (meshFam Q c)} {D : CatAlg.MeshData (meshFam Q c) L} [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] (hmid : ∀ (x : ↑Q.nonprojective), Nonempty ((y : V) × (y ⟶ ↑x))) (hQ : QConn V) (x₀ : D.PV) : PiOne Q ↑x₀ ≃* ↥(Hs Q c v₀ D x₀)

H ≅ π₁(K, b): the deck group of the base component is the fundamental group of K.

theorem MultiplicativeBasisDeformations.MeshWalk.piOneEquiv_apply {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] [hone : ∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] {v₀ : V} {k : Type u_1} [Field k] [IsAlgClosed k] [Infinite k] {c : MeshCoefficients k Q} {L : CatAlg.LocalFamily (meshFam Q c)} {D : CatAlg.MeshData (meshFam Q c) L} [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] (hmid : ∀ (x : ↑Q.nonprojective), Nonempty ((y : V) × (y ⟶ ↑x))) (hQ : QConn V) (x₀ : D.PV) (g : PiOne Q ↑x₀) : ↑((piOneEquiv hmid hQ x₀) g) = (φ v₀ ↑x₀) g

noncomputable def MultiplicativeBasisDeformations.MeshWalk.liftEquiv {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] [hone : ∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] {v₀ : V} {k : Type u_1} [Field k] [IsAlgClosed k] [Infinite k] {c : MeshCoefficients k Q} {L : CatAlg.LocalFamily (meshFam Q c)} {D : CatAlg.MeshData (meshFam Q c) L} [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] (hmid : ∀ (x : ↑Q.nonprojective), Nonempty ((y : V) × (y ⟶ ↑x))) (hQ : QConn V) (x₀ : D.PV) : (x : D.PV) × (obK Q ↑x₀ ⟶ obK Q ↑x) ≃ { o : LObj Q c v₀ D // conn Q c v₀ D (o₀ Q c v₀ D x₀) o }

The lifted projectives of the universal cover of K, (x, w) with w a walk class b → x, are the objects of the base component 𝓛₀.

theorem MultiplicativeBasisDeformations.MeshWalk.liftEquiv_act {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] [hone : ∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] {v₀ : V} {k : Type u_1} [Field k] [IsAlgClosed k] [Infinite k] {c : MeshCoefficients k Q} {L : CatAlg.LocalFamily (meshFam Q c)} {D : CatAlg.MeshData (meshFam Q c) L} [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] (hmid : ∀ (x : ↑Q.nonprojective), Nonempty ((y : V) × (y ⟶ ↑x))) (hQ : QConn V) (x₀ : D.PV) (g : PiOne Q ↑x₀) (xw : (x : D.PV) × (obK Q ↑x₀ ⟶ obK Q ↑x)) : ↑((liftEquiv hmid hQ x₀) ⟨xw.fst, CategoryTheory.CategoryStruct.comp (MulOpposite.unop g) xw.snd⟩) = gL Q c v₀ D ((φ v₀ ↑x₀) g) ↑((liftEquiv hmid hQ x₀) xw)

The deck action corresponds to the action of π₁(K, b) on walk classes.

noncomputable def MultiplicativeBasisDeformations.MeshWalk.WPequivFreePi1 {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] [hone : ∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] {v₀ : V} {k : Type u_1} [Field k] [IsAlgClosed k] [Infinite k] {c : MeshCoefficients k Q} {L : CatAlg.LocalFamily (meshFam Q c)} {D : CatAlg.MeshData (meshFam Q c) L} [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] (hmid : ∀ (x : ↑Q.nonprojective), Nonempty ((y : V) × (y ⟶ ↑x))) {x₀ : D.PV} (hconn : A0Conn Q c v₀ D x₀) {ζ : LObj Q c v₀ D → WP Q c v₀ D} (hζ : ∀ (o o' : LObj Q c v₀ D), Thin.Line o o' → wtL Q c v₀ D o o' = ζ o' - ζ o) : WP Q c v₀ D ≃+ ({ x : D.PV // x ≠ x₀ } → ℤ) × Additive (Abelianization (PiOne Q ↑x₀))

Proposition 7.2(1) with G = π₁(K, b): W(P) ≅ ℤ^{n−1} ⊕ π₁(K, b)_ab.

theorem MultiplicativeBasisDeformations.MeshWalk.theta_summand_pi1 {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] [hone : ∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] {v₀ : V} {k : Type u_1} [Field k] [IsAlgClosed k] [Infinite k] {c : MeshCoefficients k Q} {L : CatAlg.LocalFamily (meshFam Q c)} {D : CatAlg.MeshData (meshFam Q c) L} [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] (hmid : ∀ (x : ↑Q.nonprojective), Nonempty ((y : V) × (y ⟶ ↑x))) {x₀ : D.PV} (hconn : A0Conn Q c v₀ D x₀) {ζ : LObj Q c v₀ D → WP Q c v₀ D} (hζ : ∀ (o o' : LObj Q c v₀ D), Thin.Line o o' → wtL Q c v₀ D o o' = ζ o' - ζ o) (g : PiOne Q ↑x₀) (o : LObj Q c v₀ D) (ho : conn Q c v₀ D (o₀ Q c v₀ D x₀) o) : (WPequivFreePi1 hmid hconn hζ) (ζ (gL Q c v₀ D ((φ v₀ ↑x₀) g) o) - ζ o) = (0, Additive.ofMul (Abelianization.of g))

θ_g is the π₁(K, b)_ab summand under WPequivFreePi1, for g ∈ π₁(K, b) acting by s_b g s_b⁻¹.