Rescaling arrows and mesh relations

graded-category.tex and Appendix A (periodic-mesh-calculations.tex): "rescaling arrows and entire mesh relations changes the mesh derivative by invertible diagonal maps". Given arrow scalars μ and relation scalars η with c'_{x,a} = η_x c_{x,a} μ_{σ a} μ_a, the linear functor kQ → kQ multiplying each path by the product of the scalars of its arrows (gaugeMap) sends the mesh relation r_x(c) to η_x⁻¹ r_x(c'), hence the mesh ideal of c into that of c' (gaugeMap_mem_ideal). A single path therefore lies in one ideal iff it lies in the other.

def MultiplicativeBasisDeformations.pathWt {k : Type u} [CommRing k] {V : Type v} [Quiver V] (μ : {x y : V} → (x ⟶ y) → kˣ) {x y : V} : Quiver.Path x y → kˣ

The weight of a path: the product of the scalars of its arrows.

theorem MultiplicativeBasisDeformations.pathWt_comp {k : Type u} [CommRing k] {V : Type v} [Quiver V] (μ : {x y : V} → (x ⟶ y) → kˣ) {x y z : V} (p : Quiver.Path x y) (q : Quiver.Path y z) : pathWt (fun {x y : V} => μ) (p.comp q) = pathWt (fun {x y : V} => μ) p * pathWt (fun {x y : V} => μ) q

theorem MultiplicativeBasisDeformations.pathWt_toPath {k : Type u} [CommRing k] {V : Type v} [Quiver V] (μ : {x y : V} → (x ⟶ y) → kˣ) {x y : V} (a : x ⟶ y) : pathWt (fun {x y : V} => μ) a.toPath = μ a

noncomputable def MultiplicativeBasisDeformations.gaugeMap {k : Type u} [CommRing k] {V : Type v} [Quiver V] (μ : {x y : V} → (x ⟶ y) → kˣ) (x y : V) : (LinearPaths.obj x ⟶ LinearPaths.obj y) →ₗ[k] LinearPaths.obj x ⟶ LinearPaths.obj y

Multiplying each path by its weight.

theorem MultiplicativeBasisDeformations.gaugeMap_path {k : Type u} [CommRing k] {V : Type v} [Quiver V] (μ : {x y : V} → (x ⟶ y) → kˣ) {x y : V} (p : Quiver.Path x y) : (gaugeMap (fun {x y : V} => μ) x y) (LinearPaths.path p) = ↑(pathWt (fun {x y : V} => μ) p) • LinearPaths.path p

theorem MultiplicativeBasisDeformations.gaugeMap_comp {k : Type u} [CommRing k] {V : Type v} [Quiver V] (μ : {x y : V} → (x ⟶ y) → kˣ) {x y z : V} (f : LinearPaths.obj x ⟶ LinearPaths.obj y) (g : LinearPaths.obj y ⟶ LinearPaths.obj z) : (gaugeMap (fun {x y : V} => μ) x z) (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp ((gaugeMap (fun {x y : V} => μ) x y) f) ((gaugeMap (fun {x y : V} => μ) y z) g)

theorem MultiplicativeBasisDeformations.gaugeMap_meshRelation {k : Type u} [CommRing k] {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] (μ : {x y : V} → (x ⟶ y) → kˣ) (η : ↑Q.nonprojective → kˣ) (c c' : MeshCoefficients k Q) (h : ∀ (x : ↑Q.nonprojective) (y : V) (a : y ⟶ ↑x), c' x y a = η x * c x y a * μ ((Q.mate x y) a) * μ a) (x : ↑Q.nonprojective) : (gaugeMap (fun {x y : V} => μ) ↑(Q.tau x) ↑x) (meshRelation c x) = (η x)⁻¹ • meshRelation c' x

Gauge transformations of mesh relations.

theorem MultiplicativeBasisDeformations.gaugeMap_mem_ideal {k : Type u} [CommRing k] {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] (μ : {x y : V} → (x ⟶ y) → kˣ) (η : ↑Q.nonprojective → kˣ) (c c' : MeshCoefficients k Q) (h : ∀ (x : ↑Q.nonprojective) (y : V) (a : y ⟶ ↑x), c' x y a = η x * c x y a * μ ((Q.mate x y) a) * μ a) {X Y : V} {f : LinearPaths.obj X ⟶ LinearPaths.obj Y} (hf : f ∈ (RelSystem.mesh c).ideal (LinearPaths.obj X) (LinearPaths.obj Y)) : (gaugeMap (fun {x y : V} => μ) X Y) f ∈ (RelSystem.mesh c').ideal (LinearPaths.obj X) (LinearPaths.obj Y)

A gauge transformation maps the mesh ideal of c into that of c'.

theorem MultiplicativeBasisDeformations.path_mem_of_gauge {k : Type u} [CommRing k] {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] (μ : {x y : V} → (x ⟶ y) → kˣ) (η : ↑Q.nonprojective → kˣ) (c c' : MeshCoefficients k Q) (h : ∀ (x : ↑Q.nonprojective) (y : V) (a : y ⟶ ↑x), c' x y a = η x * c x y a * μ ((Q.mate x y) a) * μ a) {X Y : V} (P : Quiver.Path X Y) (hP : LinearPaths.path P ∈ (RelSystem.mesh c).ideal (LinearPaths.obj X) (LinearPaths.obj Y)) : LinearPaths.path P ∈ (RelSystem.mesh c').ideal (LinearPaths.obj X) (LinearPaths.obj Y)

A single path lies in the mesh ideal of c' if it lies in that of c.