Dual representables and injective copresentations

For the category algebra Λ of a family F, the dual representable J_p = (D C(F p, F q))_q is the module D(e_p Λ) (in the manuscript's right-module notation D(Λ e_p), graded-category.tex). A functional λ on a module X gives θ_λ : X → J_p, θ_λ(x)_q(h) = λ(h · x). Every finite-dimensional module embeds into a finite sum of the J_p, which gives the injective copresentations used in Lemma 2.9.

def MultiplicativeBasisDeformations.CatAlg.DRep {k : Type u} [Field k] {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] [CategoryTheory.Linear k 𝒞] {ι : Type} (F : ι → 𝒞) (p : ι) : Type (max w u)

The dual representable J_p.

@[instance_reducible]

instance MultiplicativeBasisDeformations.CatAlg.instAddCommGroupDRep {k : Type u} [Field k] {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] [CategoryTheory.Linear k 𝒞] {ι : Type} (F : ι → 𝒞) (p : ι) : AddCommGroup (DRep F p)

@[instance_reducible]

instance MultiplicativeBasisDeformations.CatAlg.instModuleDRep {k : Type u} [Field k] {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] [CategoryTheory.Linear k 𝒞] {ι : Type} (F : ι → 𝒞) (p : ι) : Module k (DRep F p)

instance MultiplicativeBasisDeformations.CatAlg.instFiniteDimensionalDRepOfHom {k : Type u} [Field k] {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] [CategoryTheory.Linear k 𝒞] {ι : Type} [Fintype ι] (F : ι → 𝒞) (p : ι) [∀ (x y : ι), FiniteDimensional k (F x ⟶ F y)] : FiniteDimensional k (DRep F p)

@[simp]

theorem MultiplicativeBasisDeformations.CatAlg.DRep.add_apply {k : Type u} [Field k] {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] [CategoryTheory.Linear k 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} {p : ι} (φ ψ : DRep F p) (q : ι) : (φ + ψ) q = φ q + ψ q

@[simp]

theorem MultiplicativeBasisDeformations.CatAlg.DRep.zero_apply {k : Type u} [Field k] {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] [CategoryTheory.Linear k 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} {p : ι} (q : ι) : 0 q = 0

@[simp]

theorem MultiplicativeBasisDeformations.CatAlg.DRep.smulk_apply {k : Type u} [Field k] {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] [CategoryTheory.Linear k 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} {p : ι} (c : k) (φ : DRep F p) (q : ι) : (c • φ) q = c • φ q

def MultiplicativeBasisDeformations.CatAlg.postL {k : Type u} [Field k] {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] [CategoryTheory.Linear k 𝒞] {X Y Z : 𝒞} (g : Y ⟶ Z) : (X ⟶ Y) →ₗ[k] X ⟶ Z

Postcomposition, as a linear map.

@[simp]

theorem MultiplicativeBasisDeformations.CatAlg.postL_apply {k : Type u} [Field k] {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] [CategoryTheory.Linear k 𝒞] {X Y Z : 𝒞} (g : Y ⟶ Z) (h : X ⟶ Y) : (postL g) h = CategoryTheory.CategoryStruct.comp h g

@[instance_reducible]

instance MultiplicativeBasisDeformations.CatAlg.instSMulAlgDRep {k : Type u} [Field k] {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] [CategoryTheory.Linear k 𝒞] {ι : Type} [Fintype ι] {F : ι → 𝒞} (p : ι) : SMul (Alg F) (DRep F p)

theorem MultiplicativeBasisDeformations.CatAlg.DRep.smul_apply {k : Type u} [Field k] {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] [CategoryTheory.Linear k 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} {p : ι} (a : Alg F) (φ : DRep F p) (q : ι) (h : F p ⟶ F q) : ((a • φ) q) h = ∑ r : ι, (φ r) (CategoryTheory.CategoryStruct.comp h (a q r))

theorem MultiplicativeBasisDeformations.CatAlg.DRep.ext {k : Type u} [Field k] {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] [CategoryTheory.Linear k 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} {p : ι} {φ ψ : DRep F p} (h : ∀ (q : ι) (x : F p ⟶ F q), (φ q) x = (ψ q) x) : φ = ψ

theorem MultiplicativeBasisDeformations.CatAlg.DRep.ext_iff {k : Type u} [Field k] {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] [CategoryTheory.Linear k 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} {p : ι} {φ ψ : DRep F p} : φ = ψ ↔ ∀ (q : ι) (x : F p ⟶ F q), (φ q) x = (ψ q) x

@[instance_reducible]

instance MultiplicativeBasisDeformations.CatAlg.instModuleAlgDRep {k : Type u} [Field k] {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] [CategoryTheory.Linear k 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} (p : ι) : Module (Alg F) (DRep F p)

instance MultiplicativeBasisDeformations.CatAlg.instIsScalarTowerAlgDRep {k : Type u} [Field k] {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] [CategoryTheory.Linear k 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} (p : ι) : IsScalarTower k (Alg F) (DRep F p)

def MultiplicativeBasisDeformations.CatAlg.elemAt {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] {ι : Type} [DecidableEq ι] {F : ι → 𝒞} (p q : ι) (h : F p ⟶ F q) : Alg F

The element of Λ with the single entry h : F p → F q.

theorem MultiplicativeBasisDeformations.CatAlg.elemAt_mul {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} (p q : ι) (h : F p ⟶ F q) (a : Alg F) : elemAt p q h * a = ∑ r : ι, elemAt p r (CategoryTheory.CategoryStruct.comp h (a q r))

theorem MultiplicativeBasisDeformations.CatAlg.elemAt_id {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} (p : ι) : elemAt p p (CategoryTheory.CategoryStruct.id (F p)) = idem p

theorem MultiplicativeBasisDeformations.CatAlg.elemAt_add {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} (p q : ι) (h h' : F p ⟶ F q) : elemAt p q (h + h') = elemAt p q h + elemAt p q h'

theorem MultiplicativeBasisDeformations.CatAlg.elemAt_smul {k : Type u} [Field k] {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] [CategoryTheory.Linear k 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} (p q : ι) (c : k) (h : F p ⟶ F q) : elemAt p q (c • h) = c • elemAt p q h

def MultiplicativeBasisDeformations.CatAlg.thetaFun {k : Type u} [Field k] {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] [CategoryTheory.Linear k 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} {X : Type u_1} [AddCommGroup X] [Module k X] [Module (Alg F) X] [IsScalarTower k (Alg F) X] (p : ι) (lam : Module.Dual k X) (x : X) : DRep F p

The values of θ_λ.

theorem MultiplicativeBasisDeformations.CatAlg.thetaFun_apply {k : Type u} [Field k] {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] [CategoryTheory.Linear k 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} {X : Type u_1} [AddCommGroup X] [Module k X] [Module (Alg F) X] [IsScalarTower k (Alg F) X] (p : ι) (lam : Module.Dual k X) (x : X) (q : ι) (h : F p ⟶ F q) : (thetaFun p lam x q) h = lam (elemAt p q h • x)

def MultiplicativeBasisDeformations.CatAlg.theta {k : Type u} [Field k] {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] [CategoryTheory.Linear k 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} {X : Type u_1} [AddCommGroup X] [Module k X] [Module (Alg F) X] [IsScalarTower k (Alg F) X] (p : ι) (lam : Module.Dual k X) : X →ₗ[Alg F] DRep F p

θ_λ : X → J_p, θ_λ(x)_q(h) = λ(h · x).

theorem MultiplicativeBasisDeformations.CatAlg.theta_apply {k : Type u} [Field k] {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] [CategoryTheory.Linear k 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} {X : Type u_1} [AddCommGroup X] [Module k X] [Module (Alg F) X] [IsScalarTower k (Alg F) X] (p : ι) (lam : Module.Dual k X) (x : X) (q : ι) (h : F p ⟶ F q) : ((theta p lam) x q) h = lam (elemAt p q h • x)

theorem MultiplicativeBasisDeformations.CatAlg.sum_idem_eq_one {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} : ∑ x : ι, idem x = 1

theorem MultiplicativeBasisDeformations.CatAlg.eq_zero_of_idem {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} {X : Type u_1} [AddCommGroup X] [Module (Alg F) X] {x : X} (h : ∀ (p : ι), idem p • x = 0) : x = 0

theorem MultiplicativeBasisDeformations.CatAlg.exists_embedding {k : Type u} [Field k] {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] [CategoryTheory.Linear k 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} {X : Type u_1} [AddCommGroup X] [Module k X] [Module (Alg F) X] [IsScalarTower k (Alg F) X] [FiniteDimensional k X] : ∃ (n : ℕ) (e : X →ₗ[Alg F] (c : ι × Fin n) → DRep F c.1), Function.Injective ⇑e

Every finite-dimensional module embeds into a finite sum of dual representables.