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]

def monoidal_predicate_finite_dimensional (K : Type u) [field K] :

category_theory.monoidal_category.monoidal_predicate (λ (V : Module K), finite_dimensional K ↥V)

@[protected, instance]

def closed_predicate_finite_dimensional (K : Type u) [field K] :

category_theory.monoidal_category.closed_predicate (λ (V : Module K), finite_dimensional K ↥V)

@[protected, instance]

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

category_theory.monoidal_category (FinVect K)

@[protected, instance]

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

category_theory.large_category (FinVect K)

@[protected, instance]

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

category_theory.symmetric_category (FinVect K)

@[protected, instance]

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

category_theory.concrete_category (FinVect 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

FinVect K = category_theory.full_subcategory (λ (V : Module K), finite_dimensional K ↥V)

Instances for FinVect

@[protected, instance]

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

category_theory.monoidal_closed (FinVect K)

@[protected, instance]

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

finite_dimensional K ↥(V.obj)

@[protected, instance]

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

inhabited (FinVect K)

Equations

FinVect.inhabited K = {default := {obj := Module.of K K semiring.to_module, property := _}}

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

FinVect.of K V = {obj := Module.of K V _inst_3, property := _}

@[protected, instance]

def FinVect.Module.category_theory.has_forget₂ (K : Type u) [field K] :

category_theory.has_forget₂ (FinVect K) (Module K)

Equations

FinVect.Module.category_theory.has_forget₂ K = id (category_theory.full_subcategory.has_forget₂ (λ (V : Module K), finite_dimensional K ↥V))

@[protected, instance]

def FinVect.category_theory.forget₂.category_theory.full (K : Type u) [field K] :

category_theory.full (category_theory.forget₂ (FinVect K) (Module K))

Equations

FinVect.category_theory.forget₂.category_theory.full K = {preimage := λ (X Y : FinVect K) (f : (category_theory.forget₂ (FinVect K) (Module K)).obj X ⟶ (category_theory.forget₂ (FinVect K) (Module K)).obj Y), f, witness' := _}

@[simp]

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

(category_theory.ihom V).obj W = FinVect.of K (↥(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

FinVect.FinVect_dual K V = {obj := Module.of K (module.dual K ↥(V.obj)) (module.dual.module K ↥(V.obj)), property := _}

Instances for FinVect.FinVect_dual

FinVect.exact_pairing

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.obj)

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

⇑(FinVect.FinVect_coevaluation K V) 1 = finset.univ.sum (λ (i : ↥(basis.of_vector_space_index K ↥(V.obj))), ⇑(basis.of_vector_space K ↥(V.obj)) i ⊗ₜ[K] (basis.of_vector_space K ↥(V.obj)).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.obj)

@[simp]

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

⇑(FinVect.FinVect_evaluation K V) (f ⊗ₜ[K] x) = f.to_fun 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

def FinVect.iso_to_linear_equiv {K : Type u} [field K] {V W : FinVect K} (i : V ≅ W) :

↥(V.obj) ≃ₗ[K] ↥(W.obj)

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

Equations

FinVect.iso_to_linear_equiv i = ((category_theory.forget₂ (FinVect K) (Module K)).map_iso i).to_linear_equiv

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 = ⇑((FinVect.iso_to_linear_equiv i).conj) f

@[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) :

e.to_FinVect_iso.hom = e.to_linear_map

@[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) :

e.to_FinVect_iso.inv = e.symm.to_linear_map

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) :

FinVect.of K V ≅ FinVect.of K W

Converts a linear_equiv to an isomorphism in the category FinVect.

Equations

e.to_FinVect_iso = {hom := e.to_linear_map, inv := e.symm.to_linear_map, hom_inv_id' := _, inv_hom_id' := _}