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 #

Show that FinVect K is a symmetric monoidal category.

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

FinVect K = {V // finite_dimensional K ↥V}

@[protected, instance]

def FinVect.has_coe_to_sort (K : Type u) [field K] :

has_coe_to_sort (FinVect K) (Type u)

@[protected, instance]

def FinVect.category (K : Type u) [field K] :

category_theory.category (FinVect K)

@[protected, instance]

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

finite_dimensional K ↥V

@[protected, instance]

def FinVect.inhabited (K : Type u) [field K] :

inhabited (FinVect K)

Equations

FinVect.inhabited K = {default := ⟨Module.of K K semiring.to_module, _⟩}

@[protected, instance]

def FinVect.Module.has_coe (K : Type u) [field K] :

has_coe (FinVect K) (Module K)

Equations

FinVect.Module.has_coe K = {coe := λ (V : FinVect K), V.val}

@[protected]

theorem FinVect.coe_comp (K : Type u) [field K] {U V W : FinVect K} (f : U ⟶ V) (g : V ⟶ W) :

⇑(f ≫ g) = ⇑g ∘ ⇑f

@[protected, instance]

def FinVect.monoidal_category (K : Type u) [field K] :

category_theory.monoidal_category (FinVect K)

Equations

FinVect.monoidal_category K = category_theory.monoidal_category.full_monoidal_subcategory (λ (V : Module K), finite_dimensional K ↥V) _ _

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

FinVect.FinVect_dual K V = ⟨Module.of K (module.dual K ↥V) (module.dual.module K ↥V), _⟩

@[protected, instance]

def FinVect.FinVect_dual.has_coe_to_fun (K : Type u) [field K] (V : FinVect K) :

has_coe_to_fun ↥(FinVect.FinVect_dual K V) (λ (_x : ↥(FinVect.FinVect_dual K V)), ↥V → K)

Equations

FinVect.FinVect_dual.has_coe_to_fun K V = {coe := λ (v : ↥(FinVect.FinVect_dual K V)), id (λ (v : ↥V →ₗ[K] K), ⇑v) v}

noncomputable def FinVect.FinVect_coevaluation (K : Type u) [field K] (V : FinVect K) :

𝟙_ (FinVect K) ⟶ V ⊗ FinVect.FinVect_dual K V

The coevaluation map is defined in linear_algebra.coevaluation.

Equations

FinVect.FinVect_coevaluation K V = coevaluation K ↥V

theorem FinVect.FinVect_coevaluation_apply_one (K : Type u) [field K] (V : FinVect K) :

⇑(FinVect.FinVect_coevaluation K V) 1 = ∑ (i : ↥(basis.of_vector_space_index K ↥V)), ⇑(basis.of_vector_space K ↥V) i ⊗ₜ[K] (basis.of_vector_space K ↥V).coord i

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

FinVect.FinVect_dual K V ⊗ V ⟶ 𝟙_ (FinVect K)

The evaluation morphism is given by the contraction map.

Equations

FinVect.FinVect_evaluation K V = contract_left K ↥V

@[simp]

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

⇑(FinVect.FinVect_evaluation K V) (f ⊗ₜ[K] x) = ⇑f x

@[protected, instance]

noncomputable def FinVect.exact_pairing (K : Type u) [field K] (V : FinVect K) :

category_theory.exact_pairing V (FinVect.FinVect_dual K V)

Equations

FinVect.exact_pairing K V = {coevaluation := FinVect.FinVect_coevaluation K V, evaluation := FinVect.FinVect_evaluation K V, coevaluation_evaluation' := _, evaluation_coevaluation' := _}

@[protected, instance]

noncomputable def FinVect.right_dual (K : Type u) [field K] (V : FinVect K) :

category_theory.has_right_dual V

Equations

FinVect.right_dual K V = category_theory.has_right_dual.mk (FinVect.FinVect_dual K V)

@[protected, instance]

noncomputable def FinVect.right_rigid_category (K : Type u) [field K] :

category_theory.right_rigid_category (FinVect K)

Equations

FinVect.right_rigid_category K = category_theory.right_rigid_category.mk