instance VecSemisimple.simple_of_k (k : Type u) [Field k] : CategoryTheory.Simple (FGModuleCat.of k k)

The ground field k, viewed as a one-dimensional vector space, is a simple object in FGModuleCat k: every monomorphism into it from a nonzero object is an iso.

theorem VecSemisimple.nontrivial_of_not_isZero (k : Type u) [Field k] (X : FGModuleCat k) (h : ¬CategoryTheory.Limits.IsZero X) : Nontrivial ↑X

An object X of FGModuleCat k that is not categorically zero is nontrivial as a vector space, i.e. it contains a nonzero element.

theorem VecSemisimple.ofHom_toSpanSingleton_ne_zero (k : Type u) [Field k] (X : FGModuleCat k) (v : ↑X) (hv : v ≠ 0) : FGModuleCat.ofHom (LinearMap.toSpanSingleton k (↑X) v) ≠ 0

The morphism k ⟶ X sending 1 to a nonzero vector v ∈ X is itself nonzero in FGModuleCat k.

theorem VecSemisimple.mono_ofHom_toSpanSingleton (k : Type u) [Field k] (X : FGModuleCat k) (v : ↑X) (hv : v ≠ 0) : CategoryTheory.Mono (FGModuleCat.ofHom (LinearMap.toSpanSingleton k (↑X) v))

The morphism k ⟶ X sending 1 to a nonzero vector v ∈ X is a monomorphism in FGModuleCat k, since c ↦ c • v is injective when v ≠ 0.

noncomputable def VecSemisimple.simple_iso_of_k (k : Type u) [Field k] (X : FGModuleCat k) [CategoryTheory.Simple X] : X ≅ FGModuleCat.of k k

Every simple object X in FGModuleCat k is isomorphic to the ground field k, since a nonzero vector spans a one-dimensional subspace which then forces an iso.

def VecSemisimple.ofHomAddHom (k : Type u) [Field k] (X Y : FGModuleCat k) : (↑X →ₗ[k] ↑Y) →+ (X ⟶ Y)

The additive map sending a k-linear map X →ₗ[k] Y to its packaging as a morphism X ⟶ Y in FGModuleCat k.

instance VecSemisimple.isSemisimpleCategory_vec (k : Type u) [Field k] : TensorCategories.IsSemisimpleCategory (FGModuleCat k)

FGModuleCat k is a semisimple category: every finite-dimensional k-vector space splits as a direct sum of dim_k(X) copies of the simple object k.

instance VecSemisimple.hasFinitelyManySimples_vec (k : Type u) [Field k] : TensorCategories.HasFinitelyManySimples (FGModuleCat k)

FGModuleCat k has finitely many isomorphism classes of simple objects, in fact exactly one: every simple object is isomorphic to the ground field k.

instance VecInstances.fusionCategory_vec (k : Type u) [Field k] : TensorCategories.FusionCategory k (Vec k)

Vec k = FGModuleCat k is a fusion category over k: it is a finite, semisimple, rigid k-linear tensor category whose unit has endomorphism algebra k.