Mesh relations along the covering ℤΔ → Q

Proof of Proposition 4.1, Step 1 (periodic-mesh-calculations.tex). Pull the coefficients of Q back along π. The mesh relation of ℤΔ at X maps to the mesh relation of Q at π X, so π preserves the mesh ideal; and every mesh relation of Q starting at π Z lifts to one starting at Z, so π reflects it (RelSystem.mem_ideal_of_mapPaths_mem). In particular, if paths of length at least N vanish in C(Q, c), they vanish upstairs.

def MultiplicativeBasisDeformations.TranslationQuiver.SecPath.piNP {V : Type v} [Quiver V] {Q : TranslationQuiver V} (hQ : Q.IsStable) {x₀ : V} (X : tree.ZVert) : ↑Q.nonprojective

The vertex π X, as a nonprojective vertex of Q.

noncomputable def MultiplicativeBasisDeformations.TranslationQuiver.SecPath.pullCoeff {V : Type v} [Quiver V] [∀ (x y : V), Subsingleton (x ⟶ y)] {Q : TranslationQuiver V} (hQ : Q.IsStable) {x₀ : V} {k : Type u} [Field k] (c : MeshCoefficients k Q) : MeshCoefficients k tree.zQuiver

The coefficients of Q, pulled back to ℤΔ.

theorem MultiplicativeBasisDeformations.TranslationQuiver.SecPath.toPath_eq_cast {V : Type v} [Quiver V] [∀ (x y : V), Subsingleton (x ⟶ y)] {u u' y : V} (e : u = u') (f : u ⟶ y) (g : u' ⟶ y) : f.toPath = Quiver.Path.cast ⋯ ⋯ g.toPath

theorem MultiplicativeBasisDeformations.TranslationQuiver.SecPath.path_two_eq {V : Type v} [Quiver V] [∀ (x y : V), Subsingleton (x ⟶ y)] {k : Type u} [Field k] {u u' y z : V} (e : u = u') (f : u ⟶ y) (g : u' ⟶ y) (h : y ⟶ z) : LinearPaths.path (f.toPath.comp h.toPath) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (LinearPaths.path (g.toPath.comp h.toPath))

theorem MultiplicativeBasisDeformations.TranslationQuiver.SecPath.mapPaths_meshRelation {V : Type v} [Quiver V] [∀ (x y : V), Subsingleton (x ⟶ y)] {Q : TranslationQuiver V} (hQ : Q.IsStable) {x₀ : V} {k : Type u} [Field k] [Fintype (Q.SecPath x₀)] [DecidableEq (Q.SecPath x₀)] [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) (X : ↑tree.zQuiver.nonprojective) : (LinearPaths.mapPaths (piQ hQ) ↑(tree.zQuiver.tau X) ↑X) (meshRelation (pullCoeff hQ c) X) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (meshRelation c (piNP hQ ↑X))

The mesh relation of ℤΔ at X maps to the mesh relation of Q at π X.

theorem MultiplicativeBasisDeformations.TranslationQuiver.SecPath.mapPaths_mem_mesh {V : Type v} [Quiver V] [∀ (x y : V), Subsingleton (x ⟶ y)] {Q : TranslationQuiver V} (hQ : Q.IsStable) {x₀ : V} {k : Type u} [Field k] [Fintype (Q.SecPath x₀)] [DecidableEq (Q.SecPath x₀)] [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) {X Y : tree.ZVert} {f : LinearPaths.obj X ⟶ LinearPaths.obj Y} (hf : f ∈ (RelSystem.mesh (pullCoeff hQ c)).ideal (LinearPaths.obj X) (LinearPaths.obj Y)) : (LinearPaths.mapPaths (piQ hQ) X Y) f ∈ (RelSystem.mesh c).ideal (LinearPaths.obj ((piQ hQ).obj X)) (LinearPaths.obj ((piQ hQ).obj Y))

π maps the mesh ideal of ℤΔ into that of Q.

theorem MultiplicativeBasisDeformations.TranslationQuiver.SecPath.mem_mesh_of_mapPaths {V : Type v} [Quiver V] [∀ (x y : V), Subsingleton (x ⟶ y)] {Q : TranslationQuiver V} (hQ : Q.IsStable) {x₀ : V} {k : Type u} [Field k] [Fintype (Q.SecPath x₀)] [DecidableEq (Q.SecPath x₀)] [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) {X Y : tree.ZVert} {f : LinearPaths.obj X ⟶ LinearPaths.obj Y} (hf : (LinearPaths.mapPaths (piQ hQ) X Y) f ∈ (RelSystem.mesh c).ideal (LinearPaths.obj ((piQ hQ).obj X)) (LinearPaths.obj ((piQ hQ).obj Y))) : f ∈ (RelSystem.mesh (pullCoeff hQ c)).ideal (LinearPaths.obj X) (LinearPaths.obj Y)

π reflects the mesh ideal.