Linear maps out of path categories

A morphism of kQ is a finite linear combination of paths, so any function on paths extends linearly (LinearPaths.extend); if the function is multiplicative on paths, so is its extension (extend_comp). Two instances are used repeatedly:

• a quiver morphism φ induces LinearPaths.mapPaths φ : kQ → kQ', sending a path to its image;
• for a full subquiver, sending a path to its lift when all of its vertices lie in the subquiver, and to zero otherwise, is multiplicative (in FullSubquiver.lean).

noncomputable def MultiplicativeBasisDeformations.LinearPaths.extend {k : Type u} [CommRing k] {V : Type v} [Quiver V] {M : Type u₂} [AddCommGroup M] [Module k M] {x y : V} (g : Quiver.Path x y → M) : (obj x ⟶ obj y) →ₗ[k] M

The linear extension of a function on the paths from x to y.

@[simp]

theorem MultiplicativeBasisDeformations.LinearPaths.extend_path {k : Type u} [CommRing k] {V : Type v} [Quiver V] {M : Type u₂} [AddCommGroup M] [Module k M] {x y : V} (g : Quiver.Path x y → M) (p : Quiver.Path x y) : (extend g) (path p) = g p

theorem MultiplicativeBasisDeformations.LinearPaths.extend_comp {k : Type u} [CommRing k] {V : Type v} [Quiver V] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Preadditive D] [CategoryTheory.Linear k D] (F : V → D) (g : {x y : V} → Quiver.Path x y → (F x ⟶ F y)) (hg : ∀ {x y z : V} (p : Quiver.Path x y) (q : Quiver.Path y z), g (p.comp q) = CategoryTheory.CategoryStruct.comp (g p) (g q)) {x y z : V} (f : obj x ⟶ obj y) (f' : obj y ⟶ obj z) : (extend g) (CategoryTheory.CategoryStruct.comp f f') = CategoryTheory.CategoryStruct.comp ((extend g) f) ((extend g) f')

The linear extension of a multiplicative function on paths is multiplicative.

theorem MultiplicativeBasisDeformations.LinearPaths.extend_mem_of_forall {k : Type u} [CommRing k] {V : Type v} [Quiver V] {x y : V} {M : Type u₂} [AddCommGroup M] [Module k M] (g : Quiver.Path x y → M) (N : Submodule k M) {d : ℕ} (hg : ∀ (p : Quiver.Path x y), p.length = d → g p ∈ N) {f : obj x ⟶ obj y} (hf : f ∈ degreePart d x y) : (extend g) f ∈ N

theorem MultiplicativeBasisDeformations.LinearPaths.length_mapPath {V : Type v} [Quiver V] {W : Type v'} [Quiver W] (φ : V ⥤q W) {x y : V} (p : Quiver.Path x y) : (φ.mapPath p).length = p.length

theorem MultiplicativeBasisDeformations.LinearPaths.vertices_mapPath {V : Type v} [Quiver V] {W : Type v'} [Quiver W] (φ : V ⥤q W) {x y : V} (p : Quiver.Path x y) : (φ.mapPath p).vertices = List.map φ.obj p.vertices

noncomputable def MultiplicativeBasisDeformations.LinearPaths.mapPaths {k : Type u} [CommRing k] {V : Type v} [Quiver V] {W : Type v'} [Quiver W] (φ : V ⥤q W) (x y : V) : (obj x ⟶ obj y) →ₗ[k] obj (φ.obj x) ⟶ obj (φ.obj y)

The linear functor kQ → kQ' induced by a quiver morphism, on Hom spaces.

@[simp]

theorem MultiplicativeBasisDeformations.LinearPaths.mapPaths_path {k : Type u} [CommRing k] {V : Type v} [Quiver V] {W : Type v'} [Quiver W] (φ : V ⥤q W) {x y : V} (p : Quiver.Path x y) : (mapPaths φ x y) (path p) = path (φ.mapPath p)

theorem MultiplicativeBasisDeformations.LinearPaths.mapPaths_comp {k : Type u} [CommRing k] {V : Type v} [Quiver V] {W : Type v'} [Quiver W] (φ : V ⥤q W) {x y z : V} (f : obj x ⟶ obj y) (f' : obj y ⟶ obj z) : (mapPaths φ x z) (CategoryTheory.CategoryStruct.comp f f') = CategoryTheory.CategoryStruct.comp ((mapPaths φ x y) f) ((mapPaths φ y z) f')

theorem MultiplicativeBasisDeformations.LinearPaths.mapPaths_arrow {k : Type u} [CommRing k] {V : Type v} [Quiver V] {W : Type v'} [Quiver W] (φ : V ⥤q W) {x y : V} (a : x ⟶ y) : (mapPaths φ x y) (arrow a) = arrow (φ.map a)

theorem MultiplicativeBasisDeformations.LinearPaths.mapPaths_mem_degreePart {k : Type u} [CommRing k] {V : Type v} [Quiver V] {W : Type v'} [Quiver W] (φ : V ⥤q W) {d : ℕ} {x y : V} {f : obj x ⟶ obj y} (hf : f ∈ degreePart d x y) : (mapPaths φ x y) f ∈ degreePart d (φ.obj x) (φ.obj y)