Multiplicative bases

MultiplicativeBasisDeformations.Refinements.PathRealize

Realizing the path category by chosen arrows (toward Proposition 12.8) #

Given morphisms g a : F y ⟶ F x of a k-linear category for the arrows a : y ⟶ x of a quiver, paths are realized by composition (pathR) and the k-linear path category kQ by linear extension (realizeR); the realization is a functor (realizeR_comp). This is the realization kQ → ℳ by lifted arrows of deformation-refinements.tex.

source
def MultiplicativeBasisDeformations.PathReal.pathR {V : Type} [Quiver V] {𝒞 : Type u_2} [CategoryTheory.Category.{u_3, u_2} 𝒞] {F : V → 𝒞} (g : {y x : V} → (y ⟶ x) → (F y ⟶ F x)) {x y : V} :
Quiver.Path x y → (F x ⟶ F y)

The realization of a path.

Instances For
    source
    @[simp]
    theorem MultiplicativeBasisDeformations.PathReal.pathR_nil {V : Type} [Quiver V] {𝒞 : Type u_2} [CategoryTheory.Category.{u_3, u_2} 𝒞] [CategoryTheory.Preadditive 𝒞] {F : V → 𝒞} (g : {y x : V} → (y ⟶ x) → (F y ⟶ F x)) {x : V} :
    pathR (fun {y x : V} => g) Quiver.Path.nil = CategoryTheory.CategoryStruct.id (F x)
    source
    @[simp]
    theorem MultiplicativeBasisDeformations.PathReal.pathR_cons {V : Type} [Quiver V] {𝒞 : Type u_2} [CategoryTheory.Category.{u_3, u_2} 𝒞] [CategoryTheory.Preadditive 𝒞] {F : V → 𝒞} (g : {y x : V} → (y ⟶ x) → (F y ⟶ F x)) {x y z : V} (p : Quiver.Path x y) (a : y ⟶ z) :
    pathR (fun {y x : V} => g) (p.cons a) = CategoryTheory.CategoryStruct.comp (pathR (fun {y x : V} => g) p) (g a)
    source
    theorem MultiplicativeBasisDeformations.PathReal.pathR_comp {V : Type} [Quiver V] {𝒞 : Type u_2} [CategoryTheory.Category.{u_3, u_2} 𝒞] [CategoryTheory.Preadditive 𝒞] {F : V → 𝒞} (g : {y x : V} → (y ⟶ x) → (F y ⟶ F x)) {x y z : V} (p : Quiver.Path x y) (q : Quiver.Path y z) :
    pathR (fun {y x : V} => g) (p.comp q) = CategoryTheory.CategoryStruct.comp (pathR (fun {y x : V} => g) p) (pathR (fun {y x : V} => g) q)
    source
    theorem MultiplicativeBasisDeformations.PathReal.pathR_toPath {V : Type} [Quiver V] {𝒞 : Type u_2} [CategoryTheory.Category.{u_3, u_2} 𝒞] [CategoryTheory.Preadditive 𝒞] {F : V → 𝒞} (g : {y x : V} → (y ⟶ x) → (F y ⟶ F x)) {x y : V} (a : x ⟶ y) :
    pathR (fun {y x : V} => g) a.toPath = g a
    source
    noncomputable def MultiplicativeBasisDeformations.PathReal.realizeR (k : Type u_1) [Field k] {V : Type} [Quiver V] {𝒞 : Type u_2} [CategoryTheory.Category.{u_3, u_2} 𝒞] [CategoryTheory.Preadditive 𝒞] [CategoryTheory.Linear k 𝒞] {F : V → 𝒞} (g : {y x : V} → (y ⟶ x) → (F y ⟶ F x)) (x y : V) :
    (LinearPaths.obj x ⟶ LinearPaths.obj y) →ₗ[k] F x ⟶ F y

    The realization of the path category.

    Instances For
      source
      theorem MultiplicativeBasisDeformations.PathReal.realizeR_path {k : Type u_1} [Field k] {V : Type} [Quiver V] {𝒞 : Type u_2} [CategoryTheory.Category.{u_3, u_2} 𝒞] [CategoryTheory.Preadditive 𝒞] [CategoryTheory.Linear k 𝒞] {F : V → 𝒞} (g : {y x : V} → (y ⟶ x) → (F y ⟶ F x)) {x y : V} (p : Quiver.Path x y) :
      (realizeR k (fun {y x : V} => g) x y) (LinearPaths.path p) = pathR (fun {y x : V} => g) p
      source
      theorem MultiplicativeBasisDeformations.PathReal.realizeR_arrow {k : Type u_1} [Field k] {V : Type} [Quiver V] {𝒞 : Type u_2} [CategoryTheory.Category.{u_3, u_2} 𝒞] [CategoryTheory.Preadditive 𝒞] [CategoryTheory.Linear k 𝒞] {F : V → 𝒞} (g : {y x : V} → (y ⟶ x) → (F y ⟶ F x)) {x y : V} (a : x ⟶ y) :
      (realizeR k (fun {y x : V} => g) x y) (LinearPaths.arrow a) = g a
      source
      theorem MultiplicativeBasisDeformations.PathReal.realizeR_comp {k : Type u_1} [Field k] {V : Type} [Quiver V] {𝒞 : Type u_2} [CategoryTheory.Category.{u_3, u_2} 𝒞] [CategoryTheory.Preadditive 𝒞] [CategoryTheory.Linear k 𝒞] {F : V → 𝒞} (g : {y x : V} → (y ⟶ x) → (F y ⟶ F x)) {x y z : V} (f : LinearPaths.obj x ⟶ LinearPaths.obj y) (h : LinearPaths.obj y ⟶ LinearPaths.obj z) :
      (realizeR k (fun {y x : V} => g) x z) (CategoryTheory.CategoryStruct.comp f h) = CategoryTheory.CategoryStruct.comp ((realizeR k (fun {y x : V} => g) x y) f) ((realizeR k (fun {y x : V} => g) y z) h)