Proposition 5.1: the periodic localization of the derivative cokernels

mesh-deformations.tex (prop:periodic-localization): "Let T be the set of vertices periodic under τ, and let C_T be the quotient by the identities outside T. For the derivative D_m, the quotient induces isomorphisms coker D_m(C) ≅ coker D_m(C_T) (m ≥ 2)."

C_T is the scalar mesh category of the full translation subquiver Q_T with the restricted coefficients (eq:mesh-object-quotient, restrictQuotEquiv). The quotient acts on Hom spaces between vertices of T by restricting path combinations (resE); a composite through a vertex outside T goes to zero, so the restriction commutes with the mesh derivative (resF_D). On the degree-(m+1) cokernels (CokerDeg) the induced map (cokerRes) is bijective (cokerRes_bijective): surjective since every family on Q_T is the restriction of its inclusion; injective since a family of Q differs from the inclusion of its restriction by rows leaving T, which lie in the image of D_m (row_mem_imageD_of_not_periodic), while the inclusion of a derivative of Q_T is a derivative of Q up to such rows (inclRow_mem_imageD).

Restriction on Hom spaces

noncomputable def MultiplicativeBasisDeformations.ScalarMeshCategory.resE {k : Type u} [Field k] {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {S : Set V} (hS : Q.IsTauClosed S) (c : MeshCoefficients k Q) {a b : FullSub S} (φ : obj c a.val ⟶ obj c b.val) : obj (MeshCoefficients.restrict hS c) a ⟶ obj (MeshCoefficients.restrict hS c) b

The quotient C → C_S on Hom spaces between vertices of S.

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.resE_map {k : Type u} [Field k] {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {S : Set V} (hS : Q.IsTauClosed S) (c : MeshCoefficients k Q) {a b : FullSub S} (Φ : LinearPaths.obj a.val ⟶ LinearPaths.obj b.val) : resE hS c ((RelationCategory.functor k (meshRelations c)).map Φ) = (RelationCategory.functor k (meshRelations (MeshCoefficients.restrict hS c))).map ((FullSub.restrict k a b) Φ)

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.resE_add {k : Type u} [Field k] {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {S : Set V} (hS : Q.IsTauClosed S) (c : MeshCoefficients k Q) {a b : FullSub S} (φ ψ : obj c a.val ⟶ obj c b.val) : resE hS c (φ + ψ) = resE hS c φ + resE hS c ψ

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.resE_smul {k : Type u} [Field k] {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {S : Set V} (hS : Q.IsTauClosed S) (c : MeshCoefficients k Q) {a b : FullSub S} (t : k) (φ : obj c a.val ⟶ obj c b.val) : resE hS c (t • φ) = t • resE hS c φ

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.resE_zero {k : Type u} [Field k] {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {S : Set V} (hS : Q.IsTauClosed S) (c : MeshCoefficients k Q) {a b : FullSub S} : resE hS c 0 = 0

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.resE_sum {k : Type u} [Field k] {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {S : Set V} (hS : Q.IsTauClosed S) (c : MeshCoefficients k Q) {a b : FullSub S} {ι : Type u_1} (s : Finset ι) (φ : ι → (obj c a.val ⟶ obj c b.val)) : resE hS c (∑ i ∈ s, φ i) = ∑ i ∈ s, resE hS c (φ i)

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.resE_comp {k : Type u} [Field k] {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {S : Set V} (hS : Q.IsTauClosed S) (c : MeshCoefficients k Q) {a b d : FullSub S} (φ : obj c a.val ⟶ obj c b.val) (ψ : obj c b.val ⟶ obj c d.val) : resE hS c (CategoryTheory.CategoryStruct.comp φ ψ) = CategoryTheory.CategoryStruct.comp (resE hS c φ) (resE hS c ψ)

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.resE_comp_out {k : Type u} [Field k] {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {S : Set V} (hS : Q.IsTauClosed S) (c : MeshCoefficients k Q) {a d : FullSub S} {y : V} (hy : y ∉ S) (φ : obj c a.val ⟶ obj c y) (ψ : obj c y ⟶ obj c d.val) : resE hS c (CategoryTheory.CategoryStruct.comp φ ψ) = 0

A composite through a vertex outside S vanishes in C_S.

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.resE_arrowMor {k : Type u} [Field k] {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {S : Set V} (hS : Q.IsTauClosed S) (c : MeshCoefficients k Q) {a b : FullSub S} (e : a ⟶ b) : resE hS c (arrowMor c (have this := e; this)) = arrowMor (MeshCoefficients.restrict hS c) e

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.restrict_mem_degreePart {k : Type u} [Field k] {V : Type v} [Quiver V] [(x : V) → Fintype ((y : V) × (y ⟶ x))] {S : Set V} {a b : FullSub S} {n : ℕ} {Φ : LinearPaths.obj a.val ⟶ LinearPaths.obj b.val} (hΦ : Φ ∈ LinearPaths.degreePart n a.val b.val) : (FullSub.restrict k a b) Φ ∈ LinearPaths.degreePart n a b

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.resE_degreePart {k : Type u} [Field k] {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {S : Set V} (hS : Q.IsTauClosed S) (c : MeshCoefficients k Q) {a b : FullSub S} {n : ℕ} {φ : obj c a.val ⟶ obj c b.val} (hφ : φ ∈ degreePart c n a.val b.val) : resE hS c φ ∈ degreePart (MeshCoefficients.restrict hS c) n a b

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.resE_comp_arrow {k : Type u} [Field k] {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {S : Set V} (hS : Q.IsTauClosed S) (c : MeshCoefficients k Q) {a b d : FullSub S} (φ : obj c a.val ⟶ obj c b.val) (e : b ⟶ d) : resE hS c (CategoryTheory.CategoryStruct.comp φ (arrowMor c (have this := e; this))) = CategoryTheory.CategoryStruct.comp (resE hS c φ) (arrowMor (MeshCoefficients.restrict hS c) e)

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.resE_arrow_comp {k : Type u} [Field k] {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {S : Set V} (hS : Q.IsTauClosed S) (c : MeshCoefficients k Q) {a b d : FullSub S} (e : a ⟶ b) (φ : obj c b.val ⟶ obj c d.val) : resE hS c (CategoryTheory.CategoryStruct.comp (arrowMor c (have this := e; this)) φ) = CategoryTheory.CategoryStruct.comp (arrowMor (MeshCoefficients.restrict hS c) e) (resE hS c φ)

Restriction of families

noncomputable def MultiplicativeBasisDeformations.ScalarMeshCategory.resF {k : Type u} [Field k] {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {S : Set V} (hS : Q.IsTauClosed S) (c : MeshCoefficients k Q) (g : MeshFamily c) : MeshFamily (MeshCoefficients.restrict hS c)

The restriction of a mesh family to Q_S.

noncomputable def MultiplicativeBasisDeformations.ScalarMeshCategory.resA {k : Type u} [Field k] {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {S : Set V} (hS : Q.IsTauClosed S) (c : MeshCoefficients k Q) (f : ArrowFamily c) : ArrowFamily (MeshCoefficients.restrict hS c)

The restriction of an arrow family to Q_S.

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.resF_D {k : Type u} [Field k] {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {S : Set V} (hS : Q.IsTauClosed S) (c : MeshCoefficients k Q) (f : ArrowFamily c) : resF hS c (meshDerivative c f) = meshDerivative (MeshCoefficients.restrict hS c) (resA hS c f)

Restriction commutes with the mesh derivative.

The degree-(m+1) cokernels

def MultiplicativeBasisDeformations.ScalarMeshCategory.famDeg {k : Type u} [Field k] {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) (n : ℕ) : Submodule k (MeshFamily c)

The mesh families of degree n.

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.imageD_le_famDeg {k : Type u} [Field k] {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) (m : ℕ) : imageD c m ≤ famDeg c (m + 1)

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.ScalarMeshCategory.CokerDeg {k : Type u} [Field k] {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) (m : ℕ) : Type (max (max u v) w)

The cokernel of D_m on the degree-(m+1) mesh families.

noncomputable def MultiplicativeBasisDeformations.ScalarMeshCategory.resFL {k : Type u} [Field k] {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {S : Set V} (hS : Q.IsTauClosed S) (c : MeshCoefficients k Q) : MeshFamily c →ₗ[k] MeshFamily (MeshCoefficients.restrict hS c)

The restriction of families as a linear map.

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.resF_famDeg {k : Type u} [Field k] {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {S : Set V} (hS : Q.IsTauClosed S) (c : MeshCoefficients k Q) {n : ℕ} {g : MeshFamily c} (hg : g ∈ famDeg c n) : resF hS c g ∈ famDeg (MeshCoefficients.restrict hS c) n

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.resF_imageD {k : Type u} [Field k] {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {S : Set V} (hS : Q.IsTauClosed S) (c : MeshCoefficients k Q) {m : ℕ} {g : MeshFamily c} (hg : g ∈ imageD c m) : resF hS c g ∈ imageD (MeshCoefficients.restrict hS c) m

noncomputable def MultiplicativeBasisDeformations.ScalarMeshCategory.cokerRes {k : Type u} [Field k] {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {S : Set V} (hS : Q.IsTauClosed S) (c : MeshCoefficients k Q) (m : ℕ) : CokerDeg c m →ₗ[k] CokerDeg (MeshCoefficients.restrict hS c) m

The map coker D_m(C) → coker D_m(C_S) induced by the quotient.

Bijectivity

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.end_mem_vertices {V : Type v} [Quiver V] [(x : V) → Fintype ((y : V) × (y ⟶ x))] [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] {a b : V} (p : Quiver.Path a b) : b ∈ p.vertices

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.inclRow_of_mem {k : Type u} [Field k] {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {S : Set V} (hS : Q.IsTauClosed S) (c : MeshCoefficients k Q) [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] [DecidablePred fun (x : V) => x ∈ S] [DecidablePred fun (x : V) => x ∈ Q.nonprojective] (G : RowFam hS) (x : ↑Q.nonprojective) (hx : ↑x ∈ S) : inclRow hS c G x = (RelationCategory.functor k (meshRelations c)).map ((FullSub.inclL k (↑((TranslationQuiver.restrict hS).tau ⟨FullSub.mk (↑x) hx, ⋯⟩)) (FullSub.mk (↑x) hx)) (G ⟨FullSub.mk (↑x) hx, ⋯⟩))

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.inclRow_of_not_mem {k : Type u} [Field k] {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {S : Set V} (hS : Q.IsTauClosed S) (c : MeshCoefficients k Q) [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] [DecidablePred fun (x : V) => x ∈ S] [DecidablePred fun (x : V) => x ∈ Q.nonprojective] (G : RowFam hS) (x : ↑Q.nonprojective) (hx : ↑x ∉ S) : inclRow hS c G x = 0

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.resF_inclRow {k : Type u} [Field k] {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {S : Set V} (hS : Q.IsTauClosed S) (c : MeshCoefficients k Q) [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] [DecidablePred fun (x : V) => x ∈ S] [DecidablePred fun (x : V) => x ∈ Q.nonprojective] (G : RowFam hS) (xS : ↑(TranslationQuiver.restrict hS).nonprojective) : resF hS c (inclRow hS c G) xS = (RelationCategory.functor k (meshRelations (MeshCoefficients.restrict hS c))).map (G xS)

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.cokerRes_surjective {k : Type u} [Field k] {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {S : Set V} (hS : Q.IsTauClosed S) (c : MeshCoefficients k Q) [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] [DecidablePred fun (x : V) => x ∈ S] [DecidablePred fun (x : V) => x ∈ Q.nonprojective] (m : ℕ) : Function.Surjective ⇑(cokerRes hS c m)

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.cokerRes_injective {k : Type u} [Field k] {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {S : Set V} (hS : Q.IsTauClosed S) (c : MeshCoefficients k Q) [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] [DecidablePred fun (x : V) => x ∈ S] [DecidablePred fun (x : V) => x ∈ Q.nonprojective] {m : ℕ} (hout : ∀ (x : ↑Q.nonprojective) (w : Quiver.Path ↑(Q.tau x) ↑x), w.length = m + 1 → (∃ v ∈ w.vertices, v ∉ S) → row c x w ∈ imageD c m) [Fintype V] [Fintype ↑Q.nonprojective] : Function.Injective ⇑(cokerRes hS c m)

The periodic vertices

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.isTauClosed_periodic {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] : Q.IsTauClosed Q.periodic

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.periodicLocalization {k : Type u} [Field k] {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) [Fintype V] [Fintype ↑Q.nonprojective] [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] [DecidablePred fun (x : V) => x ∈ Q.periodic] [DecidablePred fun (x : V) => x ∈ Q.nonprojective] (m : ℕ) : Function.Bijective ⇑(cokerRes ⋯ c m)

Proposition 5.1 (prop:periodic-localization): the quotient C → C_T by the identities outside the periodic vertices T induces isomorphisms coker D_m(C) ≅ coker D_m(C_T) (for every m; the source states m ≥ 2). Here C_T is the scalar mesh category of Q_T (eq:mesh-object-quotient).