@[reducible, inline]

abbrev VecInstances.Vec (k : Type u) [Ring k] : Type (u + 1)

Vec k is the category of finite-dimensional k-vector spaces, modeled in mathlib by FGModuleCat k.

instance VecInstances.hasFiniteBiproducts_vec (k : Type u) [Field k] : CategoryTheory.Limits.HasFiniteBiproducts (Vec k)

Vec k has all finite biproducts, obtained from existence of finite products.

noncomputable def VecInstances.subobjectOrderEmbedding (k : Type u) [Field k] (X : Vec k) : CategoryTheory.Subobject X ↪o Submodule k ↑X

The order embedding from subobjects of X in Vec k to submodules of the underlying k-module, built by composing the forgetful functor with mathlib's subobjectModule equivalence.

theorem VecInstances.hasFiniteLength_vec (k : Type u) [Field k] (X : Vec k) : TensorCategories.HasFiniteLength X

Every object of Vec k has finite length: its subobject lattice is both well-founded and inverse well-founded.

instance VecInstances.locallyFiniteCategory_vec (k : Type u) [Field k] : TensorCategories.LocallyFiniteCategory k (Vec k)

Vec k is locally finite (Definition 1.12.1): finite-dimensional hom-spaces and finite-length objects.

instance VecInstances.multitensorCategory_vec (k : Type u) [Field k] : TensorCategories.MultitensorCategory k (Vec k)

Vec k is a multitensor category in the sense of Definition 1.12.3.

theorem VecInstances.linearMap_eq_of_apply_one (k : Type u) [Field k] (f g : k →ₗ[k] k) (h : f 1 = g 1) : f = g

Two k-linear endomorphisms of k are equal iff they agree on the multiplicative identity.

noncomputable def VecInstances.endUnitAlgHom (k : Type u) [Field k] : CategoryTheory.End (CategoryTheory.MonoidalCategoryStruct.tensorUnit (FGModuleCat k)) →ₐ[k] k

The k-algebra homomorphism End(𝟙_ Vec) →ₐ[k] k sending an endomorphism f to f(1), witnessing the identification of End(𝟙_ Vec) with k.

noncomputable def VecInstances.endUnitAlgEquiv (k : Type u) [Field k] : CategoryTheory.End (CategoryTheory.MonoidalCategoryStruct.tensorUnit (FGModuleCat k)) ≃ₐ[k] k

The k-algebra isomorphism End(𝟙_ Vec) ≃ₐ[k] k, upgrading endUnitAlgHom into a bijection. This realizes End(𝟙) ≅ k for Vec_k.

instance VecInstances.tensorCategory_vec (k : Type u) [Field k] : TensorCategories.TensorCategory k (Vec k)

Vec k is a tensor category in the sense of Definition 1.12.3: a multitensor category whose unit-endomorphism algebra is k.

@[reducible, inline]

noncomputable abbrev VecInstances.def_1_12_3_endUnit_iso (k : Type u) [Field k] : CategoryTheory.End (CategoryTheory.MonoidalCategoryStruct.tensorUnit (FGModuleCat k)) ≃ₐ[k] k

Convenient alias for Definition 1.12.3: the canonical isomorphism End(𝟙_ Vec_k) ≅ k.