The category algebra of a finite family of objects

Construction 2.8 and the proof of Proposition 2.10 (graded-category.tex): "Put G = ⊕_{X ∈ ob C} X and Λ = End_{add C}(G)^{op}. For X in add C, the right Λ-modules R_X = C(G, X) are projective". For objects F x (x ∈ ι) of a k-linear category we realize Λ as ⊕_{x,y} C(F x, F y) with the product in path order ((a b)_{xz} = ∑_y a_{xy} ≫ b_{yz}: first a, then b). The paper's right Λ-modules are then left modules over this ring; R_X = (C(F y, X))_y with (a · m)_x = ∑_y a_{xy} ≫ m_y. The algebra A₀ of Construction 2.8 is the category algebra of the projective labels.

def MultiplicativeBasisDeformations.CatAlg.Alg {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] {ι : Type} (F : ι → 𝒞) : Type w

The category algebra ⊕_{x,y} C(F x, F y).

@[instance_reducible]

instance MultiplicativeBasisDeformations.CatAlg.instAddCommGroupAlg {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] {ι : Type} (F : ι → 𝒞) : AddCommGroup (Alg F)

@[instance_reducible]

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

theorem MultiplicativeBasisDeformations.CatAlg.ext {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} {a b : Alg F} (h : ∀ (x y : ι), a x y = b x y) : a = b

theorem MultiplicativeBasisDeformations.CatAlg.ext_iff {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} {a b : Alg F} : a = b ↔ ∀ (x y : ι), a x y = b x y

@[simp]

theorem MultiplicativeBasisDeformations.CatAlg.add_apply {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} (a b : Alg F) (x y : ι) : (a + b) x y = a x y + b x y

@[simp]

theorem MultiplicativeBasisDeformations.CatAlg.zero_apply {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} (x y : ι) : 0 x y = 0

@[simp]

theorem MultiplicativeBasisDeformations.CatAlg.neg_apply {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} (a : Alg F) (x y : ι) : (-a) x y = -a x y

@[simp]

theorem MultiplicativeBasisDeformations.CatAlg.sub_apply {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} (a b : Alg F) (x y : ι) : (a - b) x y = a x y - b x y

@[simp]

theorem MultiplicativeBasisDeformations.CatAlg.smul_apply {k : Type u} [Field k] {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] [CategoryTheory.Linear k 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} (c : k) (a : Alg F) (x y : ι) : (c • a) x y = c • a x y

theorem MultiplicativeBasisDeformations.CatAlg.sum_apply {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} {κ : Type u_1} (s : Finset κ) (f : κ → Alg F) (x y : ι) : (∑ i ∈ s, f i) x y = ∑ i ∈ s, f i x y

def MultiplicativeBasisDeformations.CatAlg.idTo {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] {ι : Type} [DecidableEq ι] {F : ι → 𝒞} (x y : ι) : F x ⟶ F y

The identity of F x, as a morphism F x ⟶ F y when x = y.

@[simp]

theorem MultiplicativeBasisDeformations.CatAlg.idTo_self {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} (x : ι) : idTo x x = CategoryTheory.CategoryStruct.id (F x)

theorem MultiplicativeBasisDeformations.CatAlg.idTo_ne {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} {x y : ι} (h : x ≠ y) : idTo x y = 0

@[instance_reducible]

instance MultiplicativeBasisDeformations.CatAlg.instMulAlg {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] {ι : Type} [Fintype ι] {F : ι → 𝒞} : Mul (Alg F)

@[instance_reducible]

instance MultiplicativeBasisDeformations.CatAlg.instOneAlg {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] {ι : Type} [DecidableEq ι] {F : ι → 𝒞} : One (Alg F)

theorem MultiplicativeBasisDeformations.CatAlg.mul_apply {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} (a b : Alg F) (x z : ι) : (a * b) x z = ∑ y : ι, CategoryTheory.CategoryStruct.comp (a x y) (b y z)

theorem MultiplicativeBasisDeformations.CatAlg.one_apply {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} (x y : ι) : 1 x y = idTo x y

theorem MultiplicativeBasisDeformations.CatAlg.sum_idTo_comp {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} {X : 𝒞} (x : ι) (f : (y : ι) → F y ⟶ X) : ∑ y : ι, CategoryTheory.CategoryStruct.comp (idTo x y) (f y) = f x

theorem MultiplicativeBasisDeformations.CatAlg.sum_comp_idTo {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} {X : 𝒞} (z : ι) (f : (y : ι) → X ⟶ F y) : ∑ y : ι, CategoryTheory.CategoryStruct.comp (f y) (idTo y z) = f z

theorem MultiplicativeBasisDeformations.CatAlg.sum_comp_idTo_alg {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} (a : Alg F) (x z : ι) : ∑ r : ι, CategoryTheory.CategoryStruct.comp (a x r) (idTo r z) = a x z

theorem MultiplicativeBasisDeformations.CatAlg.sum_idTo_comp_alg {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} (a : Alg F) (q z : ι) : ∑ t : ι, CategoryTheory.CategoryStruct.comp (idTo q t) (a t z) = a q z

@[instance_reducible]

instance MultiplicativeBasisDeformations.CatAlg.instRingAlg {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} : Ring (Alg F)

@[instance_reducible]

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

The modules R_X

def MultiplicativeBasisDeformations.CatAlg.Rep {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] {ι : Type} (F : ι → 𝒞) (X : 𝒞) : Type w

R_X = (C(F y, X))_y.

@[instance_reducible]

instance MultiplicativeBasisDeformations.CatAlg.instAddCommGroupRep {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] {ι : Type} {F : ι → 𝒞} (X : 𝒞) : AddCommGroup (Rep F X)

@[instance_reducible]

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

theorem MultiplicativeBasisDeformations.CatAlg.Rep.ext {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} {X : 𝒞} {m n : Rep F X} (h : ∀ (y : ι), m y = n y) : m = n

theorem MultiplicativeBasisDeformations.CatAlg.Rep.ext_iff {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} {X : 𝒞} {m n : Rep F X} : m = n ↔ ∀ (y : ι), m y = n y

theorem MultiplicativeBasisDeformations.CatAlg.Rep.sum_apply {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} {X : 𝒞} {κ : Type u_1} (s : Finset κ) (f : κ → Rep F X) (y : ι) : (∑ i ∈ s, f i) y = ∑ i ∈ s, f i y

@[simp]

theorem MultiplicativeBasisDeformations.CatAlg.Rep.add_apply {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} {X : 𝒞} (m n : Rep F X) (y : ι) : (m + n) y = m y + n y

@[simp]

theorem MultiplicativeBasisDeformations.CatAlg.Rep.zero_apply {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} {X : 𝒞} (y : ι) : 0 y = 0

@[simp]

theorem MultiplicativeBasisDeformations.CatAlg.Rep.sub_apply' {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} {X : 𝒞} (m n : Rep F X) (y : ι) : (m - n) y = m y - n y

@[simp]

theorem MultiplicativeBasisDeformations.CatAlg.Rep.neg_apply' {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} {X : 𝒞} (m : Rep F X) (y : ι) : (-m) y = -m y

@[simp]

theorem MultiplicativeBasisDeformations.CatAlg.Rep.smul_apply' {k : Type u} [Field k] {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] [CategoryTheory.Linear k 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} {X : 𝒞} (c : k) (m : Rep F X) (y : ι) : (c • m) y = c • m y

@[instance_reducible]

instance MultiplicativeBasisDeformations.CatAlg.instSMulAlgRep {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] {ι : Type} [Fintype ι] {F : ι → 𝒞} (X : 𝒞) : SMul (Alg F) (Rep F X)

theorem MultiplicativeBasisDeformations.CatAlg.Rep.smul_apply {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} {X : 𝒞} (a : Alg F) (m : Rep F X) (x : ι) : (a • m) x = ∑ y : ι, CategoryTheory.CategoryStruct.comp (a x y) (m y)

@[instance_reducible]

instance MultiplicativeBasisDeformations.CatAlg.instModuleAlgRep {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} (X : 𝒞) : Module (Alg F) (Rep F X)

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

def MultiplicativeBasisDeformations.CatAlg.repMap {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} {X Y : 𝒞} (f : X ⟶ Y) : Rep F X →ₗ[Alg F] Rep F Y

Postcomposition R_X → R_Y.

@[simp]

theorem MultiplicativeBasisDeformations.CatAlg.repMap_apply {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} {X Y : 𝒞} (f : X ⟶ Y) (m : Rep F X) (y : ι) : (repMap f) m y = CategoryTheory.CategoryStruct.comp (m y) f

Idempotents and the Yoneda lemma

def MultiplicativeBasisDeformations.CatAlg.unit {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] {ι : Type} [DecidableEq ι] {F : ι → 𝒞} (x : ι) : Rep F (F x)

The generator 1_x ∈ R_{F x}.

def MultiplicativeBasisDeformations.CatAlg.colAlg {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] {ι : Type} [DecidableEq ι] {F : ι → 𝒞} (x : ι) (r : Rep F (F x)) : Alg F

The column algebra element of r ∈ R_{F x}: a_{yz} = r_y for z = x.

def MultiplicativeBasisDeformations.CatAlg.idem {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] {ι : Type} [DecidableEq ι] {F : ι → 𝒞} (x : ι) : Alg F

The idempotent e_x.

theorem MultiplicativeBasisDeformations.CatAlg.colAlg_smul_unit {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} (x : ι) (r : Rep F (F x)) : colAlg x r • unit x = r

theorem MultiplicativeBasisDeformations.CatAlg.colAlg_add {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} (x : ι) (r s : Rep F (F x)) : colAlg x (r + s) = colAlg x r + colAlg x s

theorem MultiplicativeBasisDeformations.CatAlg.colAlg_smul {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} (x : ι) (a : Alg F) (r : Rep F (F x)) : colAlg x (a • r) = a * colAlg x r

theorem MultiplicativeBasisDeformations.CatAlg.colAlg_smul' {k : Type u} [Field k] {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] [CategoryTheory.Linear k 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} (x : ι) (c : k) (r : Rep F (F x)) : colAlg x (c • r) = c • colAlg x r

theorem MultiplicativeBasisDeformations.CatAlg.idem_mul_idem {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} (x : ι) : idem x * idem x = idem x

theorem MultiplicativeBasisDeformations.CatAlg.hom_ext {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} {M : Type u_1} [AddCommGroup M] [Module (Alg F) M] {x : ι} {φ ψ : Rep F (F x) →ₗ[Alg F] M} (h : φ (unit x) = ψ (unit x)) : φ = ψ

Yoneda: maps out of R_{F x} are determined by the image of 1_x.

def MultiplicativeBasisDeformations.CatAlg.ofElem {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} {M : Type u_1} [AddCommGroup M] [Module (Alg F) M] (x : ι) (m : M) : Rep F (F x) →ₗ[Alg F] M

The map R_{F x} → M with 1_x ↦ m.

theorem MultiplicativeBasisDeformations.CatAlg.ofElem_unit {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} {M : Type u_1} [AddCommGroup M] [Module (Alg F) M] (x : ι) (m : M) : (ofElem x m) (unit x) = idem x • m

theorem MultiplicativeBasisDeformations.CatAlg.ofElem_apply {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} {M : Type u_1} [AddCommGroup M] [Module (Alg F) M] (x : ι) (m : M) (r : Rep F (F x)) : (ofElem x m) r = colAlg x r • m

theorem MultiplicativeBasisDeformations.CatAlg.eq_ofElem {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} {M : Type u_1} [AddCommGroup M] [Module (Alg F) M] {x : ι} (φ : Rep F (F x) →ₗ[Alg F] M) : φ = ofElem x (φ (unit x))

Every map out of R_{F x} is ofElem of the image of 1_x.

theorem MultiplicativeBasisDeformations.CatAlg.idem_smul_rep {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} {X : 𝒞} (x : ι) (m : Rep F X) (y : ι) : (idem x • m) y = if y = x then m y else 0

theorem MultiplicativeBasisDeformations.CatAlg.unit_comp_apply {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} {X : 𝒞} (x : ι) (f : F x ⟶ X) : (repMap f) (unit x) x = f

theorem MultiplicativeBasisDeformations.CatAlg.smul_unit_component {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} {X : 𝒞} (x : ι) (φ : Rep F (F x) →ₗ[Alg F] Rep F X) (y : ι) : φ (unit x) y = CategoryTheory.CategoryStruct.comp (idTo y x) (φ (unit x) x)

theorem MultiplicativeBasisDeformations.CatAlg.eq_repMap {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} {X : 𝒞} {x : ι} (φ : Rep F (F x) →ₗ[Alg F] Rep F X) : φ = repMap (φ (unit x) x)

Yoneda for representables: Hom(R_{F x}, R_X) = C(F x, X).

theorem MultiplicativeBasisDeformations.CatAlg.repMap_injective {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} {X : 𝒞} {x : ι} {f g : F x ⟶ X} (h : repMap f = repMap g) : f = g

theorem MultiplicativeBasisDeformations.CatAlg.repMap_comp {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} {X Y Z : 𝒞} (f : X ⟶ Y) (g : Y ⟶ Z) : repMap (CategoryTheory.CategoryStruct.comp f g) = repMap g ∘ₗ repMap f

theorem MultiplicativeBasisDeformations.CatAlg.repMap_add {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} {X Y : 𝒞} (f g : X ⟶ Y) : repMap (f + g) = repMap f + repMap g

theorem MultiplicativeBasisDeformations.CatAlg.repMap_sum {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} {X Y : 𝒞} {κ : Type u_2} (s : Finset κ) (f : κ → (X ⟶ Y)) : repMap (∑ i ∈ s, f i) = ∑ i ∈ s, repMap (f i)

theorem MultiplicativeBasisDeformations.CatAlg.repMap_zero {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} {X Y : 𝒞} : repMap 0 = 0

theorem MultiplicativeBasisDeformations.CatAlg.repMap_smul_apply {k : Type u} [Field k] {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] [CategoryTheory.Linear k 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} {X Y : 𝒞} (c : k) (f : X ⟶ Y) (m : Rep F X) : (repMap (c • f)) m = c • (repMap f) m