Gauge transformations preserve derivative surjectivity

Appendix A (periodic-mesh-calculations.tex): "rescaling arrows and entire relations changes the mesh derivative by invertible diagonal maps, so it changes neither its cokernel nor the brick property." For c'_{x,a} = η_x c_{x,a} μ_{σ a} μ_a, the gauge functor kQ → kQ descends to a functor Φ : C(Q, c) → C(Q, c') with Φ(a) = μ_a a; and for f'_a = μ_a⁻¹ Φ(f_a), D'(f') = η Φ(D f). Hence each row of C(Q, c') lies in the image of D'_m when the corresponding row of C(Q, c) lies in that of D_m.

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

The gauge functor on the linear path category.

noncomputable def MultiplicativeBasisDeformations.ScalarMeshCategory.gaugeQ {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) : CategoryTheory.Functor (ScalarMeshCategory k Q c) (ScalarMeshCategory k Q c')

The induced functor C(Q, c) → C(Q, c').

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.gaugeQ_map {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) : (gaugeQ (fun {x y : V} => μ) η c c' h).map ((RelationCategory.functor k (meshRelations c)).map f) = (RelationCategory.functor k (meshRelations c')).map ((gaugeMap (fun {x y : V} => μ) x y) f)

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.gaugeQ_obj {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 : V) : (gaugeQ (fun {x y : V} => μ) η c c' h).obj (obj c x) = obj c' x

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.gaugeQ_pathMor {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) : (gaugeQ (fun {x y : V} => μ) η c c' h).map (pathMor c p) = ↑(pathWt (fun {x y : V} => μ) p) • pathMor c' p

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.gaugeQ_arrowMor {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} (a : x ⟶ y) : (gaugeQ (fun {x y : V} => μ) η c c' h).map (arrowMor c a) = ↑(μ a) • arrowMor c' a

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.gaugeQ_map_add {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 g : obj c x ⟶ obj c y) : (gaugeQ (fun {x y : V} => μ) η c c' h).map (f + g) = (gaugeQ (fun {x y : V} => μ) η c c' h).map f + (gaugeQ (fun {x y : V} => μ) η c c' h).map g

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.gaugeQ_map_smul {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} (t : k) (f : obj c x ⟶ obj c y) : (gaugeQ (fun {x y : V} => μ) η c c' h).map (t • f) = t • (gaugeQ (fun {x y : V} => μ) η c c' h).map f

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.gaugeQ_map_zero {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} : (gaugeQ (fun {x y : V} => μ) η c c' h).map 0 = 0

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.gaugeQ_mem_degreePart {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} {n : ℕ} {f : obj c x ⟶ obj c y} (hf : f ∈ degreePart c n x y) : (gaugeQ (fun {x y : V} => μ) η c c' h).map f ∈ degreePart c' n x y

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.gaugeQ_map_sum {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} {ι : Type u_1} (S : Finset ι) (f : ι → (obj c x ⟶ obj c y)) : (gaugeQ (fun {x y : V} => μ) η c c' h).map (∑ i ∈ S, f i) = ∑ i ∈ S, (gaugeQ (fun {x y : V} => μ) η c c' h).map (f i)

noncomputable def MultiplicativeBasisDeformations.ScalarMeshCategory.gaugeFamily {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) (f : ArrowFamily c) : ArrowFamily c'

The transported family f'_a = μ_a⁻¹ Φ(f_a).

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.meshDerivative_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) (f : ArrowFamily c) (x : ↑Q.nonprojective) : meshDerivative c' (gaugeFamily (fun {x y : V} => μ) η c c' h f) x = ↑(η x) • (gaugeQ (fun {x y : V} => μ) η c c' h).map (meshDerivative c f x)

The derivative is changed by an invertible diagonal map: D'(f') = η Φ(D f).

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.gaugeFamily_mem {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) {m : ℕ} {f : ArrowFamily c} (hf : f ∈ familiesDeg c m) : gaugeFamily (fun {x y : V} => μ) η c c' h f ∈ familiesDeg c' m

The degree of the transported family.

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.row_mem_imageD_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) [DecidableEq V] {m : ℕ} (x : ↑Q.nonprojective) (w : Quiver.Path ↑(Q.tau x) ↑x) (hw : row c x w ∈ imageD c m) : row c' x w ∈ imageD c' m

Rows transfer along a gauge transformation.

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.surjective_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) [DecidableEq V] [Fintype ↑Q.nonprojective] [(x y : V) → DecidableEq (x ⟶ y)] [DecidablePred fun (x : V) => x ∈ Q.nonprojective] {m : ℕ} (hS : MeshDerivativeSurjective c m) : MeshDerivativeSurjective c' m

Surjectivity of D_m is gauge invariant.

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.gauge_symm {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) [DecidableEq V] (x : ↑Q.nonprojective) (y : V) (a : y ⟶ ↑x) : c x y a = (η x)⁻¹ * c' x y a * (μ ((Q.mate x y) a))⁻¹ * (μ a)⁻¹