Mesh relations along a covering ℤΔ → Q

The general form of SectionalMesh: for any covering π : ℤΔ → Q commuting with translation, pulling the coefficients of Q back along π makes π map the mesh relation at X to the mesh relation at π X, so π preserves the mesh ideal (periodic-mesh-calculations.tex). This is how the twisted trace calculation (Lemma A.2) passes relations downstairs.

def MultiplicativeBasisDeformations.OrientedTree.piNP {D : Type v} (T : OrientedTree D) {V : Type v'} [Quiver V] {Q : TranslationQuiver V} (hQ : Q.IsStable) (π : T.ZVert ⥤q V) (X : T.ZVert) : ↑Q.nonprojective

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

def MultiplicativeBasisDeformations.OrientedTree.pullCoeff {D : Type v} (T : OrientedTree D) {V : Type v'} [Quiver V] {Q : TranslationQuiver V} (hQ : Q.IsStable) (π : T.ZVert ⥤q V) {k : Type u} [CommRing k] (c : MeshCoefficients k Q) : MeshCoefficients k T.zQuiver

The coefficients of Q, pulled back along π.

theorem MultiplicativeBasisDeformations.OrientedTree.path_two_eq {V : Type v'} [Quiver V] [∀ (x y : V), Subsingleton (x ⟶ y)] {k : Type u} [CommRing k] [(x : V) → Fintype ((y : V) × (y ⟶ x))] {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.OrientedTree.mapPaths_meshRelation {D : Type v} (T : OrientedTree D) {V : Type v'} [Quiver V] [∀ (x y : V), Subsingleton (x ⟶ y)] {Q : TranslationQuiver V} (hQ : Q.IsStable) (π : T.ZVert ⥤q V) {k : Type u} [CommRing k] [Fintype D] [DecidableEq D] [(x : V) → Fintype ((y : V) × (y ⟶ x))] (hπ : π.IsCovering) (hτ : ∀ (Y : T.ZVert), π.obj (T.ztau Y) = hQ.tauE (π.obj Y)) (c : MeshCoefficients k Q) (X : ↑T.zQuiver.nonprojective) : (LinearPaths.mapPaths π ↑(T.zQuiver.tau X) ↑X) (meshRelation (T.pullCoeff hQ π c) X) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (meshRelation c (T.piNP hQ π ↑X))

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

theorem MultiplicativeBasisDeformations.OrientedTree.mapPaths_mem_mesh {D : Type v} (T : OrientedTree D) {V : Type v'} [Quiver V] [∀ (x y : V), Subsingleton (x ⟶ y)] {Q : TranslationQuiver V} (hQ : Q.IsStable) (π : T.ZVert ⥤q V) {k : Type u} [CommRing k] [Fintype D] [DecidableEq D] [(x : V) → Fintype ((y : V) × (y ⟶ x))] (hπ : π.IsCovering) (hτ : ∀ (Y : T.ZVert), π.obj (T.ztau Y) = hQ.tauE (π.obj Y)) (c : MeshCoefficients k Q) {X Y : T.ZVert} {f : LinearPaths.obj X ⟶ LinearPaths.obj Y} (hf : f ∈ (RelSystem.mesh (T.pullCoeff hQ π c)).ideal (LinearPaths.obj X) (LinearPaths.obj Y)) : (LinearPaths.mapPaths π X Y) f ∈ (RelSystem.mesh c).ideal (LinearPaths.obj (π.obj X)) (LinearPaths.obj (π.obj Y))

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