# mathlibdocumentation

algebra.category.FinVect

# The category of finite dimensional vector spaces #

This introduces FinVect K, the category of finite dimensional vector spaces over a field K. It is implemented as a full subcategory on a subtype of Module K, which inherits monoidal and symmetric structure as finite_dimensional K is a monoidal predicate. We also provide a right rigid monoidal category instance.

@[protected, instance]
@[protected, instance]
def closed_predicate_finite_dimensional (K : Type u) [field K] :
@[protected, instance]
def FinVect.monoidal_category (K : Type u) [field K] :
@[protected, instance]
def FinVect.large_category (K : Type u) [field K] :
@[protected, instance]
def FinVect.symmetric_category (K : Type u) [field K] :
@[protected, instance]
def FinVect.concrete_category (K : Type u) [field K] :
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
Instances for FinVect
@[protected, instance]
def FinVect.monoidal_closed (K : Type u) [field K] :
@[protected, instance]
def FinVect.finite_dimensional (K : Type u) [field K] (V : FinVect K) :
(V.obj)
@[protected, instance]
def FinVect.inhabited (K : Type u) [field K] :
Equations
def FinVect.of (K : Type u) [field K] (V : Type u) [ V] [ V] :

Lift an unbundled vector space to FinVect K.

Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[simp]
theorem FinVect.ihom_obj (K : Type u) [field K] (V W : FinVect K) :
W = ((V.obj) →ₗ[K] (W.obj))
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
Instances for FinVect.FinVect_dual
noncomputable def FinVect.FinVect_coevaluation (K : Type u) [field K] (V : FinVect K) :

The coevaluation map is defined in linear_algebra.coevaluation.

Equations
theorem FinVect.FinVect_coevaluation_apply_one (K : Type u) [field K] (V : FinVect K) :
= finset.univ.sum (λ (i : (V.obj))), (V.obj)) i ⊗ₜ[K] (V.obj)).coord i)
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 : V).obj)) (x : (V.obj)) :
(f ⊗ₜ[K] x) = f.to_fun x
@[protected, instance]
noncomputable def FinVect.exact_pairing (K : Type u) [field K] (V : FinVect K) :
Equations
@[protected, instance]
noncomputable def FinVect.right_dual (K : Type u) [field K] (V : FinVect K) :
Equations
@[protected, instance]
noncomputable def FinVect.right_rigid_category (K : Type u) [field K] :
Equations
def FinVect.iso_to_linear_equiv {K : Type u} [field K] {V W : FinVect K} (i : V W) :

Converts and isomorphism in the category FinVect to a linear_equiv between the underlying vector spaces.

Equations
theorem FinVect.iso.conj_eq_conj {K : Type u} [field K] {V W : FinVect K} (i : V W) (f : category_theory.End V) :
(i.conj) f = f
@[simp]
theorem linear_equiv.to_FinVect_iso_hom {K : Type u} [field K] {V W : Type u} [ V] [ V] [ W] [ W] (e : V ≃ₗ[K] W) :
@[simp]
theorem linear_equiv.to_FinVect_iso_inv {K : Type u} [field K] {V W : Type u} [ V] [ V] [ W] [ W] (e : V ≃ₗ[K] W) :
def linear_equiv.to_FinVect_iso {K : Type u} [field K] {V W : Type u} [ V] [ V] [ W] [ W] (e : V ≃ₗ[K] W) :
V W

Converts a linear_equiv to an isomorphism in the category FinVect.

Equations