mathlib documentation

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]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
def FinVect.finite_dimensional (K : Type u) [field K] (V : FinVect K) :
@[protected, instance]
def FinVect.inhabited (K : Type u) [field K] :
Equations
def FinVect.of (K : Type u) [field K] (V : Type u) [add_comm_group V] [module K V] [finite_dimensional K V] :

Lift an unbundled vector space to FinVect K.

Equations
@[simp]
theorem FinVect.ihom_obj (K : Type u) [field K] (V W : FinVect K) :
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
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).obj)) (x : (V.obj)) :
@[protected, instance]
noncomputable def FinVect.right_dual (K : Type u) [field K] (V : FinVect 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) :
@[simp]
theorem linear_equiv.to_FinVect_iso_hom {K : Type u} [field K] {V W : Type u} [add_comm_group V] [module K V] [finite_dimensional K V] [add_comm_group W] [module K W] [finite_dimensional K W] (e : V ≃ₗ[K] W) :
@[simp]
theorem linear_equiv.to_FinVect_iso_inv {K : Type u} [field K] {V W : Type u} [add_comm_group V] [module K V] [finite_dimensional K V] [add_comm_group W] [module K W] [finite_dimensional K W] (e : V ≃ₗ[K] W) :
def linear_equiv.to_FinVect_iso {K : Type u} [field K] {V W : Type u} [add_comm_group V] [module K V] [finite_dimensional K V] [add_comm_group W] [module K W] [finite_dimensional K W] (e : V ≃ₗ[K] W) :

Converts a linear_equiv to an isomorphism in the category FinVect.

Equations