mathlib documentation

algebra.category.FinVect

The category of finite dimensional vector spaces #

This introduces FinVect K, the category of finite dimensional vector spaces on a field K. It is implemented as a full subcategory on a subtype of Module K. We first create the instance as a category, then as a monoidal category and then as a rigid monoidal category.

Future work #

def FinVect (K : Type u) [field K] :
Type (u+1)

Define FinVect as the subtype of Module.{u} K of finite dimensional vector spaces.

Equations
@[instance]
def FinVect.has_coe_to_sort (K : Type u) [field K] :
@[instance]
@[instance]
def FinVect.finite_dimensional (K : Type u) [field K] (V : FinVect K) :
@[instance]
def FinVect.inhabited (K : Type u) [field K] :
Equations
@[instance]
def FinVect.Module.has_coe (K : Type u) [field K] :
Equations
theorem FinVect.coe_comp (K : Type u) [field K] {U V W : FinVect K} (f : U V) (g : V W) :
(f g) = g f
def FinVect.FinVect_dual (K : Type u) [field K] (V : FinVect K) :

The dual module is the dual in the rigid monoidal category FinVect K.

Equations
@[instance]
Equations

The coevaluation map is defined in linear_algebra.coevaluation.

Equations
def FinVect.FinVect_evaluation (K : Type u) [field K] (V : FinVect K) :

The evaluation morphism is given by the contraction map.

Equations
@[simp]
theorem FinVect.FinVect_evaluation_apply (K : Type u) [field K] (V : FinVect K) (f : (FinVect.FinVect_dual K V)) (x : V) :