Translation quivers and scalar mesh categories

Definitions 2.3 and 2.4 of the manuscript (graded-category.tex).

• The k-linear path category of a quiver is Free k (Paths Q): morphisms x ⟶ y are finite linear combinations of paths from x to y, and p ≫ q is the path p followed by q. This matches the manuscript's left-to-right path products.
• A quotient of the path category by the two-sided ideal linearly generated by a family of relations is RelationCategory.
• A translation quiver carries a bijection τ from the nonprojective onto the noninjective vertices, and mates σ a : τ x ⟶ y for every arrow a : y ⟶ x with x nonprojective. The mate bijection is recorded separately for each pair (x, y); this is the same as one bijection from the arrows ending at nonprojective vertices onto the arrows starting at noninjective vertices with the stated endpoints.
• The scalar mesh category C(Q,c) is the quotient by the mesh relations r_x = ∑_{a : y → x} c_{x,a} (σ a) a.

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.LinearPaths (k : Type u) (V : Type v) : Type v

The k-linear path category of the quiver V.

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.LinearPaths.obj {k : Type u} {V : Type v} (x : V) : LinearPaths k V

The vertex x, as an object of the linear path category.

noncomputable def MultiplicativeBasisDeformations.LinearPaths.path {k : Type u} [CommRing k] {V : Type v} [Quiver V] {x y : V} (p : Quiver.Path x y) : obj x ⟶ obj y

The morphism of the linear path category given by a single path.

noncomputable def MultiplicativeBasisDeformations.LinearPaths.arrow {k : Type u} [CommRing k] {V : Type v} [Quiver V] {x y : V} (a : x ⟶ y) : obj x ⟶ obj y

The morphism of the linear path category given by a single arrow.

noncomputable def MultiplicativeBasisDeformations.LinearPaths.degreePart {k : Type u} [CommRing k] {V : Type v} [Quiver V] (n : ℕ) (x y : V) : Submodule k (obj x ⟶ obj y)

The path-degree-n part of kQ(x, y): the span of the paths of length n.

def MultiplicativeBasisDeformations.RelationCategory (k : Type u) [CommRing k] {C : Type v} [CategoryTheory.Category.{w, v} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (R : (X Y : C) → Set (X ⟶ Y)) : Type v

The quotient of a linear category by the two-sided ideal linearly generated by the relations R.

@[instance_reducible]

instance MultiplicativeBasisDeformations.instCategoryRelationCategory (k : Type u) [CommRing k] {C : Type v} [CategoryTheory.Category.{w, v} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (R : (X Y : C) → Set (X ⟶ Y)) : CategoryTheory.Category.{w, v} (RelationCategory k R)

@[instance_reducible]

instance MultiplicativeBasisDeformations.instPreadditiveRelationCategory (k : Type u) [CommRing k] {C : Type v} [CategoryTheory.Category.{w, v} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (R : (X Y : C) → Set (X ⟶ Y)) : CategoryTheory.Preadditive (RelationCategory k R)

@[instance_reducible]

instance MultiplicativeBasisDeformations.instLinearRelationCategory (k : Type u) [CommRing k] {C : Type v} [CategoryTheory.Category.{w, v} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (R : (X Y : C) → Set (X ⟶ Y)) : CategoryTheory.Linear k (RelationCategory k R)

def MultiplicativeBasisDeformations.RelationCategory.functor (k : Type u) [CommRing k] {C : Type v} [CategoryTheory.Category.{w, v} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (R : (X Y : C) → Set (X ⟶ Y)) : CategoryTheory.Functor C (RelationCategory k R)

The quotient functor onto a relation category.

instance MultiplicativeBasisDeformations.instFullRelationCategoryFunctor (k : Type u) [CommRing k] {C : Type v} [CategoryTheory.Category.{w, v} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (R : (X Y : C) → Set (X ⟶ Y)) : (RelationCategory.functor k R).Full

instance MultiplicativeBasisDeformations.instAdditiveRelationCategoryFunctor (k : Type u) [CommRing k] {C : Type v} [CategoryTheory.Category.{w, v} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (R : (X Y : C) → Set (X ⟶ Y)) : (RelationCategory.functor k R).Additive

instance MultiplicativeBasisDeformations.instLinearRelationCategoryFunctor (k : Type u) [CommRing k] {C : Type v} [CategoryTheory.Category.{w, v} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (R : (X Y : C) → Set (X ⟶ Y)) : CategoryTheory.Functor.Linear k (RelationCategory.functor k R)

structure MultiplicativeBasisDeformations.TranslationQuiver (V : Type v) [Quiver V] : Type (max v w)

Definition 2.3 (def:translation-quiver). A translation quiver structure on the quiver V.

• nonprojective : Set V

  The nonprojective vertices.

• noninjective : Set V

  The noninjective vertices.

• tau : ↑self.nonprojective ≃ ↑self.noninjective

  The translation, a bijection from nonprojective onto noninjective vertices.

• mate (x : ↑self.nonprojective) (y : V) : (y ⟶ ↑x) ≃ (↑(self.tau x) ⟶ y)

  The mate bijection: σ a : τ x ⟶ y for a : y ⟶ x.

def MultiplicativeBasisDeformations.TranslationQuiver.IsStable {V : Type v} [Quiver V] (Q : TranslationQuiver V) : Prop

A translation quiver is stable if every vertex is nonprojective and noninjective.

def MultiplicativeBasisDeformations.HasAtMostOneArrow (V : Type v) [Quiver V] : Prop

At most one arrow between each ordered pair of vertices.

def MultiplicativeBasisDeformations.MeshCoefficients (k : Type u) [CommRing k] {V : Type v} [Quiver V] (Q : TranslationQuiver V) : Type (max (max v w) u)

A coefficient system: a nonzero scalar c_{x,a} for each nonprojective vertex x and each arrow a ending at x.

noncomputable def MultiplicativeBasisDeformations.meshRelation {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) : LinearPaths.obj ↑(Q.tau x) ⟶ LinearPaths.obj ↑x

The mesh relation r_x = ∑_{a : y → x} c_{x,a} (σ a) a at a nonprojective vertex x.

def MultiplicativeBasisDeformations.meshRelations {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) : Set (X ⟶ Y)

The family of all mesh relations, indexed by their endpoints.

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.ScalarMeshCategory (k : Type u) [CommRing k] {V : Type v} [Quiver V] (Q : TranslationQuiver V) [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) : Type v

Definition 2.4 (def:scalar-mesh-category). The scalar mesh category C(Q, c) = kQ / ⟨r_x : x nonprojective⟩.

@[reducible, inline]

noncomputable abbrev MultiplicativeBasisDeformations.ScalarMeshCategory.obj {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 : V) : ScalarMeshCategory k Q c

The vertex x as an object of C(Q, c).

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

The path-degree-n part C_n(x, y) of the scalar mesh category, the image of the paths of length n.

theorem MultiplicativeBasisDeformations.RelationCategory.functor_map_eq_zero_iff {k : Type u'} [CommRing k] {C : Type v'} [CategoryTheory.Category.{w', v'} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (R : (X Y : C) → Set (X ⟶ Y)) {X Y : C} (f : X ⟶ Y) : (functor k R).map f = 0 ↔ f ∈ (CategoricalIdeal.HomIdeal.linearSpan k R).hom X Y

The quotient functor onto a relation category kills exactly the generated ideal.

theorem MultiplicativeBasisDeformations.RelationCategory.functor_map_surjective {k : Type u'} [CommRing k] {C : Type v'} [CategoryTheory.Category.{w', v'} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (R : (X Y : C) → Set (X ⟶ Y)) {X Y : C} (g : (functor k R).obj X ⟶ (functor k R).obj Y) : ∃ (f : X ⟶ Y), (functor k R).map f = g