Object quotients of scalar mesh categories

graded-category.tex (eq:mesh-object-quotient) and Subsection 5.2 (mesh-deformations.tex).

• The retraction kQ → kQ_S maps the mesh ideal of Q into that of Q_S (restrict_mem_meshIdealSub): a mesh relation based in S restricts to the mesh relation of Q_S, and one based outside S consists of paths through vertices outside S, which the retraction kills.
• In the object quotient C/[D], a morphism of kQ vanishes exactly when it lies in the mesh ideal plus the paths through D (objectQuotient_map_eq_zero_iff).

theorem MultiplicativeBasisDeformations.FullSub.restrict_eq_zero_of_mem_outside {k : Type u} [Field k] {V : Type v} [Quiver V] [(x : V) → Fintype ((y : V) × (y ⟶ x))] {S : Set V} {a b : FullSub S} {o : LinearPaths.obj a.val ⟶ LinearPaths.obj b.val} (ho : o ∈ outside k S a.val b.val) : (restrict k a b) o = 0

theorem MultiplicativeBasisDeformations.restrict_meshRelation {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) (x : ↑(TranslationQuiver.restrict hS).nonprojective) : (FullSub.restrict k ↑((TranslationQuiver.restrict hS).tau x) ↑x) (meshRelation c (TranslationQuiver.restrictNonproj hS x)) = meshRelation (MeshCoefficients.restrict hS c) x

theorem MultiplicativeBasisDeformations.restrict_comp_meshRelation_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 : FullSub S} (x : ↑(TranslationQuiver.restrict hS).nonprojective) (u : LinearPaths.obj a.val ⟶ LinearPaths.obj ↑(Q.tau (TranslationQuiver.restrictNonproj hS x))) (u' : LinearPaths.obj ↑(TranslationQuiver.restrictNonproj hS x) ⟶ LinearPaths.obj b.val) : (FullSub.restrict k a b) (CategoryTheory.CategoryStruct.comp u (CategoryTheory.CategoryStruct.comp (meshRelation c (TranslationQuiver.restrictNonproj hS x)) u')) ∈ meshIdealSub (MeshCoefficients.restrict hS c) (LinearPaths.obj a) (LinearPaths.obj b)

theorem MultiplicativeBasisDeformations.restrict_mem_meshIdealSub {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} {f : LinearPaths.obj a.val ⟶ LinearPaths.obj b.val} (hf : f ∈ meshIdealSub c (LinearPaths.obj a.val) (LinearPaths.obj b.val)) : (FullSub.restrict k a b) f ∈ meshIdealSub (MeshCoefficients.restrict hS c) (LinearPaths.obj a) (LinearPaths.obj b)

The retraction maps the mesh ideal of Q into the mesh ideal of Q_S.

noncomputable def MultiplicativeBasisDeformations.through {V : Type v} [Quiver V] (k : Type u) [Field k] (D : Set V) (x y : V) : Submodule k (LinearPaths.obj x ⟶ LinearPaths.obj y)

The paths through some vertex of D, spanned in kQ.

theorem MultiplicativeBasisDeformations.outside_eq_through {k : Type u} [Field k] {V : Type v} [Quiver V] [(x : V) → Fintype ((y : V) × (y ⟶ x))] {S : Set V} (x y : V) : FullSub.outside k S x y = through k Sᶜ x y

theorem MultiplicativeBasisDeformations.path_comp_mem_through {k : Type u} [Field k] {V : Type v} [Quiver V] [(x : V) → Fintype ((y : V) × (y ⟶ x))] {D : Set V} {x s y : V} (hs : s ∈ D) (p : Quiver.Path x s) (q : Quiver.Path s y) : LinearPaths.path (p.comp q) ∈ through k D x y

theorem MultiplicativeBasisDeformations.comp_mem_through {k : Type u} [Field k] {V : Type v} [Quiver V] [(x : V) → Fintype ((y : V) × (y ⟶ x))] {D : Set V} {x s y : V} (hs : s ∈ D) (U : LinearPaths.obj x ⟶ LinearPaths.obj s) (W : LinearPaths.obj s ⟶ LinearPaths.obj y) : CategoryTheory.CategoryStruct.comp U W ∈ through k D x y

@[reducible, inline]

noncomputable abbrev MultiplicativeBasisDeformations.oqFunctor {k : Type u} [Field k] {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) (D : Set V) : CategoryTheory.Functor (LinearPaths k V) (ScalarMeshCategory.ObjectQuotient c D)

The functor kQ → C(Q,c)/[D].

theorem MultiplicativeBasisDeformations.oqFunctor_map_eq_zero_iff {k : Type u} [Field k] {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) (D : Set V) {x y : V} (f : LinearPaths.obj x ⟶ LinearPaths.obj y) : (oqFunctor c D).map f = 0 ↔ f ∈ meshIdealSub c (LinearPaths.obj x) (LinearPaths.obj y) ⊔ through k D x y

The object quotient on kQ: a morphism of kQ vanishes in C/[D] exactly when it lies in the mesh ideal plus the paths through D.

theorem MultiplicativeBasisDeformations.oqFunctor_map_surjective {k : Type u} [Field k] {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) (D : Set V) {x y : V} (g : (oqFunctor c D).obj (LinearPaths.obj x) ⟶ (oqFunctor c D).obj (LinearPaths.obj y)) : ∃ (f : LinearPaths.obj x ⟶ LinearPaths.obj y), (oqFunctor c D).map f = g

noncomputable def MultiplicativeBasisDeformations.oqEquiv {k : Type u} [Field k] {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) (D : Set V) (x y : V) : ((LinearPaths.obj x ⟶ LinearPaths.obj y) ⧸ meshIdealSub c (LinearPaths.obj x) (LinearPaths.obj y) ⊔ through k D x y) ≃ₗ[k] (oqFunctor c D).obj (LinearPaths.obj x) ⟶ (oqFunctor c D).obj (LinearPaths.obj y)

The Hom spaces of C/[D], as quotients of the Hom spaces of kQ.

theorem MultiplicativeBasisDeformations.through_mono {k : Type u} [Field k] {V : Type v} [Quiver V] [(x : V) → Fintype ((y : V) × (y ⟶ x))] {D D' : Set V} (h : D ⊆ D') (x y : V) : through k D x y ≤ through k D' x y

theorem MultiplicativeBasisDeformations.restrict_mem_through {k : Type u} [Field k] {V : Type v} [Quiver V] [(x : V) → Fintype ((y : V) × (y ⟶ x))] {S : Set V} {D : Set (FullSub S)} {a b : FullSub S} {f : LinearPaths.obj a.val ⟶ LinearPaths.obj b.val} (hf : f ∈ through k (FullSub.val '' D ∪ Sᶜ) a.val b.val) : (FullSub.restrict k a b) f ∈ through k D a b

theorem MultiplicativeBasisDeformations.inclL_mem_through {k : Type u} [Field k] {V : Type v} [Quiver V] [(x : V) → Fintype ((y : V) × (y ⟶ x))] {S : Set V} {D : Set (FullSub S)} {a b : FullSub S} {f : LinearPaths.obj a ⟶ LinearPaths.obj b} (hf : f ∈ through k D a b) : (FullSub.inclL k a b) f ∈ through k (FullSub.val '' D ∪ Sᶜ) a.val b.val

theorem MultiplicativeBasisDeformations.mem_sup_through_iff {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) {D : Set (FullSub S)} {a b : FullSub S} (f : LinearPaths.obj a.val ⟶ LinearPaths.obj b.val) : f ∈ meshIdealSub c (LinearPaths.obj a.val) (LinearPaths.obj b.val) ⊔ through k (FullSub.val '' D ∪ Sᶜ) a.val b.val ↔ (FullSub.restrict k a b) f ∈ meshIdealSub (MeshCoefficients.restrict hS c) (LinearPaths.obj a) (LinearPaths.obj b) ⊔ through k D a b

eq:mesh-object-quotient: between vertices of S, a morphism of kQ vanishes in C/[val D ∪ Sᶜ] exactly when its restriction vanishes in C(Q_S)/[D].

theorem MultiplicativeBasisDeformations.restrict_surjective {k : Type u} [Field k] {V : Type v} [Quiver V] [(x : V) → Fintype ((y : V) × (y ⟶ x))] {S : Set V} (a b : FullSub S) : Function.Surjective ⇑(FullSub.restrict k a b)

noncomputable def MultiplicativeBasisDeformations.restrictQuotEquiv {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) (D : Set (FullSub S)) (a b : FullSub S) : ((LinearPaths.obj a.val ⟶ LinearPaths.obj b.val) ⧸ meshIdealSub c (LinearPaths.obj a.val) (LinearPaths.obj b.val) ⊔ through k (FullSub.val '' D ∪ Sᶜ) a.val b.val) ≃ₗ[k] (LinearPaths.obj a ⟶ LinearPaths.obj b) ⧸ meshIdealSub (MeshCoefficients.restrict hS c) (LinearPaths.obj a) (LinearPaths.obj b) ⊔ through k D a b

eq:mesh-object-quotient on Hom spaces between vertices of S.

theorem MultiplicativeBasisDeformations.path_nil_eq_id {k : Type u} [Field k] {V : Type v} [Quiver V] [(x : V) → Fintype ((y : V) × (y ⟶ x))] (x : V) : LinearPaths.path Quiver.Path.nil = CategoryTheory.CategoryStruct.id (LinearPaths.obj x)

theorem MultiplicativeBasisDeformations.oq_id_ne_zero_iff {k : Type u} [Field k] {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) (D : Set V) (x : V) : CategoryTheory.CategoryStruct.id (ScalarMeshCategory.ObjectQuotient.obj c D x) ≠ 0 ↔ CategoryTheory.CategoryStruct.id (LinearPaths.obj x) ∉ meshIdealSub c (LinearPaths.obj x) (LinearPaths.obj x) ⊔ through k D x x

theorem MultiplicativeBasisDeformations.oq_id_eq_zero_of_mem {k : Type u} [Field k] {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) (D : Set V) {x : V} (hx : x ∈ D) : CategoryTheory.CategoryStruct.id (ScalarMeshCategory.ObjectQuotient.obj c D x) = 0

theorem MultiplicativeBasisDeformations.brickHypothesis_restrict {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) (h : ScalarMeshCategory.BrickHypothesis c) : ScalarMeshCategory.BrickHypothesis (MeshCoefficients.restrict hS c)

Object quotients of C(Q_S) are object quotients of C(Q) (Subsection 5.2): the brick hypothesis passes to a τ-closed full subquiver.

theorem MultiplicativeBasisDeformations.finiteDimensional_restrict {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) (hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)) (a b : FullSub S) : FiniteDimensional k (ScalarMeshCategory.obj (MeshCoefficients.restrict hS c) a ⟶ ScalarMeshCategory.obj (MeshCoefficients.restrict hS c) b)

The scalar mesh category of a τ-closed full subquiver is finite-dimensional if C(Q, c) is (graded-category.tex).