def VecCategoricalFusionData.homLinearEquiv (k : Type u) [Field k] (X Y : FGModuleCat k) : (X ⟶ Y) ≃ₗ[k] ↑X →ₗ[k] ↑Y

The k-linear equivalence between morphisms in FGModuleCat k and the underlying linear maps between their carriers.

theorem VecCategoricalFusionData.vec_hom_finrank (k : Type u) [Field k] : Module.finrank k (FGModuleCat.of k k ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj (FGModuleCat.of k k) (FGModuleCat.of k k)) = 1

The dimension of Hom(k, k ⊗ k) over k (computed inside FGModuleCat k) is one, reflecting the fact that k ⊗ k ≅ k is simple in Vec.

@[implicit_reducible]

instance VecCategoricalFusionData.instCategoricalFusionDataFGModuleCat (k : Type u) [Field k] : CategoricalFusionData k (FGModuleCat k)

FGModuleCat k is a categorical fusion category with the single simple object k, trivial fusion rules (k ⊗ k = k), and self-dual involution. This packages Vec_k as the rank-one fusion category.