Transfer of the mesh derivative to a τ-closed full subquiver #
Proof of Proposition 5.1 (prop:periodic-localization), last paragraph, and
eq:mesh-object-quotient. For a τ-closed set S, the inclusion
kQ_S → kQ sends the mesh relation of Q_S at x to the mesh relation of
Q at x minus its terms through middle vertices outside S
(inclL_meshRelation_sub_mem). Hence the inclusion maps the mesh ideal of
Q_S into the mesh ideal of Q plus the paths through vertices outside S
(inclL_mem_ideal_sup_outside).
Consequently, if D_m(C(Q_S)) is surjective and the rows through vertices
outside S are already in the image of D_m(C(Q)), then every row at a vertex
of S is in that image (row_mem_imageD_of_restrict).
@[reducible, inline]
noncomputable abbrev
MultiplicativeBasisDeformations.meshIdealSub
{k : Type u}
[CommRing k]
{V : Type v}
[Quiver V]
{Q : TranslationQuiver V}
[(x : V) → Fintype ((y : V) × (y ⟶ x))]
(c : MeshCoefficients k Q)
(X Y : LinearPaths k V)
:
Submodule k (X ⟶ Y)
The mesh ideal of C(Q, c), as a submodule of the Hom spaces of kQ.
Instances For
theorem
MultiplicativeBasisDeformations.meshRelation_mem_meshIdealSub
{k : Type u}
[CommRing k]
{V : Type v}
[Quiver V]
{Q : TranslationQuiver V}
[(x : V) → Fintype ((y : V) × (y ⟶ x))]
(c : MeshCoefficients k Q)
(x : ↑Q.nonprojective)
:
meshRelation c x ∈ meshIdealSub c (LinearPaths.obj ↑(Q.tau x)) (LinearPaths.obj ↑x)
theorem
MultiplicativeBasisDeformations.path_mem_outside
{k : Type u}
[CommRing k]
{V : Type v}
[Quiver V]
[(x : V) → Fintype ((y : V) × (y ⟶ x))]
{S : Set V}
{x y : V}
(p : Quiver.Path x y)
{v : V}
(hv : v ∈ p.vertices)
(hvS : v ∉ S)
:
LinearPaths.path p ∈ FullSub.outside k S x y
noncomputable def
MultiplicativeBasisDeformations.inclMesh
{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)
(x : ↑(TranslationQuiver.restrict hS).nonprojective)
:
LinearPaths.obj ↑(Q.tau (TranslationQuiver.restrictNonproj hS x)) ⟶ LinearPaths.obj ↑(TranslationQuiver.restrictNonproj hS x)
The image in kQ of the mesh relation of Q_S at x.
Instances For
theorem
MultiplicativeBasisDeformations.inclL_meshRelation_sub_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)
(c : MeshCoefficients k Q)
(x : ↑(TranslationQuiver.restrict hS).nonprojective)
:
inclMesh hS c x - meshRelation c (TranslationQuiver.restrictNonproj hS x) ∈ FullSub.outside k S ↑(Q.tau (TranslationQuiver.restrictNonproj hS x)) ↑(TranslationQuiver.restrictNonproj hS x)
The mesh relation of Q_S maps to the mesh relation of Q, up to the terms
with middle vertex outside S.
theorem
MultiplicativeBasisDeformations.inclL_mem_ideal_sup_outside
{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)
{a b : FullSub S}
{f : LinearPaths.obj a ⟶ LinearPaths.obj b}
(hf : f ∈ meshIdealSub (MeshCoefficients.restrict hS c) (LinearPaths.obj a) (LinearPaths.obj b))
:
(FullSub.inclL k a b) f ∈ meshIdealSub c (LinearPaths.obj a.val) (LinearPaths.obj b.val) ⊔ FullSub.outside k S a.val b.val
The inclusion maps the mesh ideal of Q_S into the mesh ideal of Q plus
the paths through vertices outside S.
theorem
MultiplicativeBasisDeformations.proj_mem_span_outside
{k : Type u}
[CommRing k]
{V : Type v}
[Quiver V]
[(x : V) → Fintype ((y : V) × (y ⟶ x))]
{S : Set V}
{x y : V}
(d : ℕ)
{o : LinearPaths.obj x ⟶ LinearPaths.obj y}
(ho : o ∈ FullSub.outside k S x y)
:
(LinearPaths.proj d x y) o ∈ Submodule.span k
{f : LinearPaths.obj x ⟶ LinearPaths.obj y | ∃ (p : Quiver.Path x y), p.length = d ∧ (∃ v ∈ p.vertices, v ∉ S) ∧ f = LinearPaths.path p}
@[reducible, inline]
abbrev
MultiplicativeBasisDeformations.PathFamily
{k : Type u}
[CommRing k]
{V : Type v}
[Quiver V]
(S : Set V)
:
Type (max (max (max w v) v) (max u v) w)
A family of morphisms of kQ_S parallel to the arrows of Q_S.
Instances For
noncomputable def
MultiplicativeBasisDeformations.liftFamily
{k : Type u}
[CommRing k]
{V : Type v}
[Quiver V]
{Q : TranslationQuiver V}
[(x : V) → Fintype ((y : V) × (y ⟶ x))]
{S : Set V}
(c : MeshCoefficients k Q)
[DecidablePred fun (x : V) => x ∈ S]
(F : PathFamily S)
:
Extend a family on Q_S by zero to a family on Q.
Instances For
theorem
MultiplicativeBasisDeformations.liftFamily_mem
{k : Type u}
[CommRing k]
{V : Type v}
[Quiver V]
{Q : TranslationQuiver V}
[(x : V) → Fintype ((y : V) × (y ⟶ x))]
{S : Set V}
(c : MeshCoefficients k Q)
[DecidablePred fun (x : V) => x ∈ S]
{m : ℕ}
(F : PathFamily S)
(hF : ∀ (b : (u : FullSub S) × (v : FullSub S) × (u ⟶ v)), F b ∈ LinearPaths.degreePart m b.fst b.snd.fst)
:
liftFamily c F ∈ ScalarMeshCategory.familiesDeg c m
noncomputable def
MultiplicativeBasisDeformations.derivPath
{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)
(F : PathFamily S)
(x : ↑(TranslationQuiver.restrict hS).nonprojective)
:
LinearPaths.obj ↑((TranslationQuiver.restrict hS).tau x) ⟶ LinearPaths.obj ↑x
The derivative of a family on Q_S, computed in kQ_S.
Instances For
theorem
MultiplicativeBasisDeformations.map_derivPath
{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]
(F : PathFamily S)
(x : ↑(TranslationQuiver.restrict hS).nonprojective)
:
(RelationCategory.functor k (meshRelations (MeshCoefficients.restrict hS c))).map (derivPath hS c F x) = ScalarMeshCategory.meshDerivative (MeshCoefficients.restrict hS c)
(fun (b : (x : FullSub S) × (y : FullSub S) × (x ⟶ y)) =>
(RelationCategory.functor k (meshRelations (MeshCoefficients.restrict hS c))).map (F b))
x
noncomputable def
MultiplicativeBasisDeformations.inclDeriv
{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)
(F : PathFamily S)
(x : ↑(TranslationQuiver.restrict hS).nonprojective)
:
LinearPaths.obj ↑(Q.tau (TranslationQuiver.restrictNonproj hS x)) ⟶ LinearPaths.obj ↑(TranslationQuiver.restrictNonproj hS x)
The image in kQ of derivPath.
Instances For
theorem
MultiplicativeBasisDeformations.meshDerivative_liftFamily
{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]
(F : PathFamily S)
(x : ↑(TranslationQuiver.restrict hS).nonprojective)
:
ScalarMeshCategory.meshDerivative c (liftFamily c F) (TranslationQuiver.restrictNonproj hS x) = (RelationCategory.functor k (meshRelations c)).map (inclDeriv hS c F x)
theorem
MultiplicativeBasisDeformations.meshDerivative_liftFamily_of_not_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)
(c : MeshCoefficients k Q)
[DecidablePred fun (x : V) => x ∈ S]
(F : PathFamily S)
(x : ↑Q.nonprojective)
(hx : ↑x ∉ S)
:
ScalarMeshCategory.meshDerivative c (liftFamily c F) x = 0
theorem
MultiplicativeBasisDeformations.derivPath_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)
(c : MeshCoefficients k Q)
[DecidablePred fun (x : V) => x ∈ S]
{m : ℕ}
(F : PathFamily S)
(hF : ∀ (b : (u : FullSub S) × (v : FullSub S) × (u ⟶ v)), F b ∈ LinearPaths.degreePart m b.fst b.snd.fst)
(x : ↑(TranslationQuiver.restrict hS).nonprojective)
:
derivPath hS c F x ∈ LinearPaths.degreePart (m + 1) ↑((TranslationQuiver.restrict hS).tau x) ↑x
theorem
MultiplicativeBasisDeformations.single_mem_imageD_of_mem_sup
{k : Type u}
[CommRing k]
{V : Type v}
[Quiver V]
{Q : TranslationQuiver V}
[(x : V) → Fintype ((y : V) × (y ⟶ x))]
{S : Set V}
(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]
{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)
(x : ↑Q.nonprojective)
(hx : ↑x ∈ S)
{G : LinearPaths.obj ↑(Q.tau x) ⟶ LinearPaths.obj ↑x}
(hG : G ∈ meshIdealSub c (LinearPaths.obj ↑(Q.tau x)) (LinearPaths.obj ↑x) ⊔ FullSub.outside k S ↑(Q.tau x) ↑x)
(hGd : G ∈ LinearPaths.degreePart (m + 1) ↑(Q.tau x) ↑x)
:
Pi.single x ((RelationCategory.functor k (meshRelations c)).map G) ∈ ScalarMeshCategory.imageD c m
A degree-(m+1) element of the mesh ideal of Q plus the paths outside S
gives a combination of rows through vertices outside S.
theorem
MultiplicativeBasisDeformations.row_mem_imageD_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 : ℕ}
(hsurj : ScalarMeshCategory.MeshDerivativeSurjective (MeshCoefficients.restrict hS c) 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)
(x : ↑Q.nonprojective)
(hx : ↑x ∈ S)
(w : Quiver.Path ↑(Q.tau x) ↑x)
(hw : w.length = m + 1)
:
ScalarMeshCategory.row c x w ∈ ScalarMeshCategory.imageD c m
Proposition 5.1, transfer to a τ-closed subquiver
(prop:periodic-localization, last paragraph). If D_m(C(Q_S)) is surjective
and every row through a vertex outside S is in the image of D_m(C(Q)), then
every row at a vertex of S is in that image.