Full translation subquivers

graded-category.tex (eq:mesh-object-quotient). Let S be a set of vertices closed under τ and τ⁻¹ wherever defined, and Q_S the full translation subquiver on S. In the path category, killing the identities outside S kills exactly the paths through vertices outside S. A mesh relation based in S retains the terms whose middle vertex lies in S; this is the mesh relation of Q_S.

This file provides:

• FullSub S, the full subquiver on S, its inclusion FullSub.incl, and the lift FullSub.liftPath of a path all of whose vertices lie in S;
• the retraction FullSub.restrict : kQ → kQ_S, sending a path to its lift if it stays in S and to zero otherwise; it is multiplicative;
• TranslationQuiver.restrict, the translation quiver structure on FullSub S, and the restricted coefficients.

def MultiplicativeBasisDeformations.FullSub {V : Type v} (S : Set V) : Type v

The full subquiver on a set of vertices (a type synonym, to carry its own quiver structure).

@[instance_reducible]

instance MultiplicativeBasisDeformations.FullSub.instQuiver {V : Type v} [Quiver V] {S : Set V} : Quiver (FullSub S)

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.FullSub.val {V : Type v} {S : Set V} (a : FullSub S) : V

The underlying vertex.

theorem MultiplicativeBasisDeformations.FullSub.val_mem {V : Type v} [Quiver V] {S : Set V} (a : FullSub S) : a.val ∈ S

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.FullSub.mk {V : Type v} {S : Set V} (v : V) (hv : v ∈ S) : FullSub S

The vertex of the subquiver.

theorem MultiplicativeBasisDeformations.FullSub.ext {V : Type v} [Quiver V] {S : Set V} {a b : FullSub S} (h : a.val = b.val) : a = b

@[instance_reducible]

instance MultiplicativeBasisDeformations.FullSub.instDecidableEq {V : Type v} [Quiver V] {S : Set V} [DecidableEq V] : DecidableEq (FullSub S)

@[instance_reducible]

instance MultiplicativeBasisDeformations.FullSub.instFintypeOfDecidablePredMemSet {V : Type v} {S : Set V} [Fintype V] [DecidablePred fun (x : V) => x ∈ S] : Fintype (FullSub S)

@[instance_reducible]

instance MultiplicativeBasisDeformations.FullSub.instDecidableEqHom {V : Type v} [Quiver V] {S : Set V} [(x y : V) → DecidableEq (x ⟶ y)] (a b : FullSub S) : DecidableEq (a ⟶ b)

@[instance_reducible]

instance MultiplicativeBasisDeformations.FullSub.instFintypeHom {V : Type v} [Quiver V] {S : Set V} [(x y : V) → Fintype (x ⟶ y)] (a b : FullSub S) : Fintype (a ⟶ b)

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.FullSub.incl {V : Type v} [Quiver V] (S : Set V) : FullSub S ⥤q V

The inclusion of the full subquiver.

def MultiplicativeBasisDeformations.FullSub.liftPathAux {V : Type v} [Quiver V] {S : Set V} (a : FullSub S) {b : V} (p : Quiver.Path a.val b) (hp : ∀ v ∈ p.vertices, v ∈ S) : Quiver.Path a (mk b ⋯)

Lift a path all of whose vertices lie in S (auxiliary form).

theorem MultiplicativeBasisDeformations.FullSub.incl_mapPath_liftPathAux {V : Type v} [Quiver V] {S : Set V} (a : FullSub S) {b : V} (p : Quiver.Path a.val b) (hp : ∀ v ∈ p.vertices, v ∈ S) : (incl S).mapPath (a.liftPathAux p hp) = p

def MultiplicativeBasisDeformations.FullSub.liftPath {V : Type v} [Quiver V] {S : Set V} (a b : FullSub S) (p : Quiver.Path a.val b.val) (hp : ∀ v ∈ p.vertices, v ∈ S) : Quiver.Path a b

Lift a path all of whose vertices lie in S.

theorem MultiplicativeBasisDeformations.FullSub.incl_mapPath_liftPath {V : Type v} [Quiver V] {S : Set V} {a b : FullSub S} (p : Quiver.Path a.val b.val) (hp : ∀ v ∈ p.vertices, v ∈ S) : (incl S).mapPath (a.liftPath b p hp) = p

theorem MultiplicativeBasisDeformations.FullSub.vertices_incl_mapPath {V : Type v} [Quiver V] {S : Set V} {a b : FullSub S} (p : Quiver.Path a b) (v : V) : v ∈ ((incl S).mapPath p).vertices → v ∈ S

theorem MultiplicativeBasisDeformations.FullSub.liftPath_incl_mapPath {V : Type v} [Quiver V] {S : Set V} {a b : FullSub S} (p : Quiver.Path a b) : a.liftPath b ((incl S).mapPath p) ⋯ = p

theorem MultiplicativeBasisDeformations.FullSub.length_liftPath {V : Type v} [Quiver V] {S : Set V} {a b : FullSub S} (p : Quiver.Path a.val b.val) (hp : ∀ v ∈ p.vertices, v ∈ S) : (a.liftPath b p hp).length = p.length

theorem MultiplicativeBasisDeformations.FullSub.incl_mapPath_injective {V : Type v} [Quiver V] {S : Set V} {a b : FullSub S} {p q : Quiver.Path a b} (h : (incl S).mapPath p = (incl S).mapPath q) : p = q

theorem MultiplicativeBasisDeformations.FullSub.mem_vertices_comp_iff {V : Type v} [Quiver V] {S : Set V} {a b c : V} (p : Quiver.Path a b) (q : Quiver.Path b c) : (∀ v ∈ (p.comp q).vertices, v ∈ S) ↔ (∀ v ∈ p.vertices, v ∈ S) ∧ ∀ v ∈ q.vertices, v ∈ S

theorem MultiplicativeBasisDeformations.FullSub.liftPath_comp {V : Type v} [Quiver V] {S : Set V} {a b c : FullSub S} (p : Quiver.Path a.val b.val) (q : Quiver.Path b.val c.val) (hp : ∀ v ∈ p.vertices, v ∈ S) (hq : ∀ v ∈ q.vertices, v ∈ S) (hpq : ∀ v ∈ (p.comp q).vertices, v ∈ S) : a.liftPath c (p.comp q) hpq = (a.liftPath b p hp).comp (b.liftPath c q hq)

noncomputable def MultiplicativeBasisDeformations.FullSub.outside {V : Type v} [Quiver V] (k : Type u) [CommRing k] (S : Set V) (x y : V) : Submodule k (LinearPaths.obj x ⟶ LinearPaths.obj y)

The paths through some vertex outside S, spanned in kQ.

noncomputable def MultiplicativeBasisDeformations.FullSub.restrictPath {V : Type v} [Quiver V] {S : Set V} (k : Type u) [CommRing k] {a b : FullSub S} (p : Quiver.Path a.val b.val) : LinearPaths.obj a ⟶ LinearPaths.obj b

A path of Q between vertices of S, restricted to Q_S: its lift if it stays in S, and zero otherwise.

noncomputable def MultiplicativeBasisDeformations.FullSub.restrict {V : Type v} [Quiver V] {S : Set V} (k : Type u) [CommRing k] (a b : FullSub S) : (LinearPaths.obj a.val ⟶ LinearPaths.obj b.val) →ₗ[k] LinearPaths.obj a ⟶ LinearPaths.obj b

The retraction kQ → kQ_S on Hom spaces between vertices of S.

theorem MultiplicativeBasisDeformations.FullSub.restrictPath_comp {V : Type v} [Quiver V] {S : Set V} (k : Type u) [CommRing k] {a b c : FullSub S} (p : Quiver.Path a.val b.val) (q : Quiver.Path b.val c.val) : restrictPath k (p.comp q) = CategoryTheory.CategoryStruct.comp (restrictPath k p) (restrictPath k q)

theorem MultiplicativeBasisDeformations.FullSub.restrict_comp {V : Type v} [Quiver V] {S : Set V} (k : Type u) [CommRing k] {a b c : FullSub S} (f : LinearPaths.obj a.val ⟶ LinearPaths.obj b.val) (g : LinearPaths.obj b.val ⟶ LinearPaths.obj c.val) : (restrict k a c) (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp ((restrict k a b) f) ((restrict k b c) g)

@[reducible, inline]

noncomputable abbrev MultiplicativeBasisDeformations.FullSub.inclL {V : Type v} [Quiver V] {S : Set V} (k : Type u) [CommRing k] (a b : FullSub S) : (LinearPaths.obj a ⟶ LinearPaths.obj b) →ₗ[k] LinearPaths.obj ((incl S).obj a) ⟶ LinearPaths.obj ((incl S).obj b)

The inclusion kQ_S → kQ on Hom spaces.

theorem MultiplicativeBasisDeformations.FullSub.restrict_inclL {V : Type v} [Quiver V] {S : Set V} (k : Type u) [CommRing k] {a b : FullSub S} (f : LinearPaths.obj a ⟶ LinearPaths.obj b) : (restrict k a b) ((inclL k a b) f) = f

theorem MultiplicativeBasisDeformations.FullSub.sub_inclL_restrict_mem {V : Type v} [Quiver V] {S : Set V} (k : Type u) [CommRing k] {a b : FullSub S} (f : LinearPaths.obj a.val ⟶ LinearPaths.obj b.val) : f - (inclL k a b) ((restrict k a b) f) ∈ outside k S a.val b.val

theorem MultiplicativeBasisDeformations.FullSub.outside_comp_mem {V : Type v} [Quiver V] {S : Set V} (k : Type u) [CommRing k] {x y z : V} {f : LinearPaths.obj x ⟶ LinearPaths.obj y} (hf : f ∈ outside k S x y) (g : LinearPaths.obj y ⟶ LinearPaths.obj z) : CategoryTheory.CategoryStruct.comp f g ∈ outside k S x z

theorem MultiplicativeBasisDeformations.FullSub.comp_outside_mem {V : Type v} [Quiver V] {S : Set V} (k : Type u) [CommRing k] {x y z : V} (f : LinearPaths.obj x ⟶ LinearPaths.obj y) {g : LinearPaths.obj y ⟶ LinearPaths.obj z} (hg : g ∈ outside k S y z) : CategoryTheory.CategoryStruct.comp f g ∈ outside k S x z

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

A set of vertices closed under τ and τ⁻¹ wherever they are defined.

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.TranslationQuiver.restrict {V : Type v} [Quiver V] {Q : TranslationQuiver V} {S : Set V} (hS : Q.IsTauClosed S) : TranslationQuiver (FullSub S)

The full translation subquiver Q_S on a τ-closed set S.

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.TranslationQuiver.restrictNonproj {V : Type v} [Quiver V] {Q : TranslationQuiver V} {S : Set V} (hS : Q.IsTauClosed S) (x : ↑(restrict hS).nonprojective) : ↑Q.nonprojective

The vertex of Q, from a nonprojective vertex of Q_S.

theorem MultiplicativeBasisDeformations.TranslationQuiver.restrict_tau_val {V : Type v} [Quiver V] {Q : TranslationQuiver V} {S : Set V} (hS : Q.IsTauClosed S) (x : ↑(restrict hS).nonprojective) : (↑((restrict hS).tau x)).val = ↑(Q.tau (restrictNonproj hS x))

def MultiplicativeBasisDeformations.MeshCoefficients.restrict {k : Type u} [CommRing k] {V : Type v} [Quiver V] {Q : TranslationQuiver V} {S : Set V} (hS : Q.IsTauClosed S) (c : MeshCoefficients k Q) : MeshCoefficients k (TranslationQuiver.restrict hS)

The coefficients of Q, restricted to Q_S.

@[instance_reducible]

noncomputable instance MultiplicativeBasisDeformations.FullSub.instFintypeStar {V : Type v} [Quiver V] {S : Set V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] (x : FullSub S) : Fintype ((y : FullSub S) × (y ⟶ x))