Periodic localization for spanning rows

prop:periodic-localization (scalar-normalization.tex), as used in Appendix B: "The quotient maps in Proposition 5.1 specify the direct-sum identification." We extend the transfer row_mem_imageD_of_restrict from one row to any family of path combinations on a τ-closed subquiver Q_S (inclRow_mem_imageD): if its classes lie in the image of D_m(C(Q_S)), its inclusion lies in the image of D_m(C(Q)), provided the rows through vertices outside S do. Consequently spanning rows transfer (rowClass_mem_rowSpan_of_restrict).

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.RowFam {k : Type u} [CommRing k] {V : Type v} [Quiver V] {Q : TranslationQuiver V} {S : Set V} (hS : Q.IsTauClosed S) : Type (max v (max u v) w)

A family of morphisms of kQ_S at the rows of Q_S.

noncomputable def MultiplicativeBasisDeformations.inclRow {k : Type u} [CommRing 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) [DecidablePred fun (x : V) => x ∈ S] (G : RowFam hS) : ScalarMeshCategory.MeshFamily c

The inclusion of a family on Q_S into the mesh families of Q.

theorem MultiplicativeBasisDeformations.inclRow_add {k : Type u} [CommRing 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) [DecidablePred fun (x : V) => x ∈ S] [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] [DecidablePred fun (x : V) => x ∈ Q.nonprojective] (G G' : RowFam hS) : inclRow hS c (G + G') = inclRow hS c G + inclRow hS c G'

theorem MultiplicativeBasisDeformations.inclRow_smul {k : Type u} [CommRing 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) [DecidablePred fun (x : V) => x ∈ S] [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] [DecidablePred fun (x : V) => x ∈ Q.nonprojective] (a : k) (G : RowFam hS) : inclRow hS c (a • G) = a • inclRow hS c G

theorem MultiplicativeBasisDeformations.inclRow_zero {k : Type u} [CommRing 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) [DecidablePred fun (x : V) => x ∈ S] [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] [DecidablePred fun (x : V) => x ∈ Q.nonprojective] : inclRow hS c 0 = 0

theorem MultiplicativeBasisDeformations.inclRow_sum {k : Type u} [CommRing 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) [DecidablePred fun (x : V) => x ∈ S] [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] [DecidablePred fun (x : V) => x ∈ Q.nonprojective] {ι : Type u_1} (s : Finset ι) (G : ι → RowFam hS) : inclRow hS c (∑ i ∈ s, G i) = ∑ i ∈ s, inclRow hS c (G i)

theorem MultiplicativeBasisDeformations.inclRow_sub {k : Type u} [CommRing 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) [DecidablePred fun (x : V) => x ∈ S] [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] [DecidablePred fun (x : V) => x ∈ Q.nonprojective] (G G' : RowFam hS) : inclRow hS c (G - G') = inclRow hS c G - inclRow hS c G'

theorem MultiplicativeBasisDeformations.inclRow_mem_imageD {k : Type u} [CommRing 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) [DecidablePred fun (x : V) => x ∈ S] [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] [DecidablePred fun (x : V) => x ∈ Q.nonprojective] [Fintype V] {m : ℕ} (hout : ∀ (x : ↑Q.nonprojective) (w : Quiver.Path ↑(Q.tau x) ↑x), w.length = m + 1 → ↑x ∈ S → (∃ v ∈ w.vertices, v ∉ S) → ScalarMeshCategory.row c x w ∈ ScalarMeshCategory.imageD c m) (G : RowFam hS) (hGd : ∀ (xS : ↑(TranslationQuiver.restrict hS).nonprojective), G xS ∈ LinearPaths.degreePart (m + 1) ↑((TranslationQuiver.restrict hS).tau xS) ↑xS) (hG : (fun (xS : ↑(TranslationQuiver.restrict hS).nonprojective) => (RelationCategory.functor k (meshRelations (MeshCoefficients.restrict hS c))).map (G xS)) ∈ ScalarMeshCategory.imageD (MeshCoefficients.restrict hS c) m) : inclRow hS c G ∈ ScalarMeshCategory.imageD c m

Proposition 5.1, transfer of families to a τ-closed subquiver.

Spanning rows

noncomputable def MultiplicativeBasisDeformations.rowP {k : Type u} [CommRing k] {V : Type v} [Quiver V] {Q : TranslationQuiver V} {S : Set V} (hS : Q.IsTauClosed S) [DecidableEq V] (xS : ↑(TranslationQuiver.restrict hS).nonprojective) (p : Quiver.Path ↑((TranslationQuiver.restrict hS).tau xS) ↑xS) : RowFam hS

The family of one row of Q_S.

theorem MultiplicativeBasisDeformations.map_rowP {k : Type u} [CommRing 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) [DecidablePred fun (x : V) => x ∈ S] [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] [DecidablePred fun (x : V) => x ∈ Q.nonprojective] [Fintype V] (xS : ↑(TranslationQuiver.restrict hS).nonprojective) (p : Quiver.Path ↑((TranslationQuiver.restrict hS).tau xS) ↑xS) : (fun (yS : ↑(TranslationQuiver.restrict hS).nonprojective) => (RelationCategory.functor k (meshRelations (MeshCoefficients.restrict hS c))).map (rowP hS xS p yS)) = ScalarMeshCategory.row (MeshCoefficients.restrict hS c) xS p

theorem MultiplicativeBasisDeformations.map_rowP_apply {k : Type u} [CommRing 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) [DecidablePred fun (x : V) => x ∈ S] [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] [DecidablePred fun (x : V) => x ∈ Q.nonprojective] [Fintype V] (xS : ↑(TranslationQuiver.restrict hS).nonprojective) (p : Quiver.Path ↑((TranslationQuiver.restrict hS).tau xS) ↑xS) (yS : ↑(TranslationQuiver.restrict hS).nonprojective) : (RelationCategory.functor k (meshRelations (MeshCoefficients.restrict hS c))).map (rowP hS xS p yS) = ScalarMeshCategory.row (MeshCoefficients.restrict hS c) xS p yS

theorem MultiplicativeBasisDeformations.inclRow_rowP {k : Type u} [CommRing 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) [DecidablePred fun (x : V) => x ∈ S] [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] [DecidablePred fun (x : V) => x ∈ Q.nonprojective] [Fintype V] (xS : ↑(TranslationQuiver.restrict hS).nonprojective) (p : Quiver.Path ↑((TranslationQuiver.restrict hS).tau xS) ↑xS) : inclRow hS c (rowP hS xS p) = ScalarMeshCategory.row c (TranslationQuiver.restrictNonproj hS xS) ((FullSub.incl S).mapPath p)

theorem MultiplicativeBasisDeformations.rowP_mem {k : Type u} [CommRing k] {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {S : Set V} (hS : Q.IsTauClosed S) [DecidablePred fun (x : V) => x ∈ S] [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] [DecidablePred fun (x : V) => x ∈ Q.nonprojective] [Fintype V] {m : ℕ} (xS : ↑(TranslationQuiver.restrict hS).nonprojective) (p : Quiver.Path ↑((TranslationQuiver.restrict hS).tau xS) ↑xS) (hp : p.length = m + 1) (yS : ↑(TranslationQuiver.restrict hS).nonprojective) : rowP hS xS p yS ∈ LinearPaths.degreePart (m + 1) ↑((TranslationQuiver.restrict hS).tau yS) ↑yS

def MultiplicativeBasisDeformations.inclRows {V : Type v} [Quiver V] {Q : TranslationQuiver V} {S : Set V} (hS : Q.IsTauClosed S) (ST : ScalarMeshCategory.RowSet (TranslationQuiver.restrict hS)) : ScalarMeshCategory.RowSet Q

The rows of Q_S as rows of Q.

theorem MultiplicativeBasisDeformations.two_rowClass_of_restrict {k : Type u} [CommRing 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) [DecidablePred fun (x : V) => x ∈ S] [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] [DecidablePred fun (x : V) => x ∈ Q.nonprojective] [Fintype V] {m : ℕ} (hout : ∀ (x : ↑Q.nonprojective) (w : Quiver.Path ↑(Q.tau x) ↑x), w.length = m + 1 → ↑x ∈ S → (∃ v ∈ w.vertices, v ∉ S) → ScalarMeshCategory.row c x w ∈ ScalarMeshCategory.imageD c m) (xS : ↑(TranslationQuiver.restrict hS).nonprojective) (wS : Quiver.Path ↑((TranslationQuiver.restrict hS).tau xS) ↑xS) (hwS : wS.length = m + 1) (hT : 2 • ScalarMeshCategory.rowClass (MeshCoefficients.restrict hS c) m xS wS = 0) : 2 • ScalarMeshCategory.rowClass c m (TranslationQuiver.restrictNonproj hS xS) ((FullSub.incl S).mapPath wS) = 0

Rows killed by two transfer from Q_S to Q.

theorem MultiplicativeBasisDeformations.rowClass_mem_rowSpan_of_restrict {k : Type u} [CommRing 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) [DecidablePred fun (x : V) => x ∈ S] [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] [DecidablePred fun (x : V) => x ∈ Q.nonprojective] [Fintype V] {m : ℕ} (hout : ∀ (x : ↑Q.nonprojective) (w : Quiver.Path ↑(Q.tau x) ↑x), w.length = m + 1 → ↑x ∈ S → (∃ v ∈ w.vertices, v ∉ S) → ScalarMeshCategory.row c x w ∈ ScalarMeshCategory.imageD c m) (ST : ScalarMeshCategory.RowSet (TranslationQuiver.restrict hS)) (xS : ↑(TranslationQuiver.restrict hS).nonprojective) (wS : Quiver.Path ↑((TranslationQuiver.restrict hS).tau xS) ↑xS) (hwS : wS.length = m + 1) (hT : ScalarMeshCategory.rowClass (MeshCoefficients.restrict hS c) m xS wS ∈ ScalarMeshCategory.rowSpan (MeshCoefficients.restrict hS c) m ST) : ScalarMeshCategory.rowClass c m (TranslationQuiver.restrictNonproj hS xS) ((FullSub.incl S).mapPath wS) ∈ ScalarMeshCategory.rowSpan c m (inclRows hS ST)

Spanning rows transfer from Q_S to Q.