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]
Equations
- monoidal_predicate_finite_dimensional K = {prop_id' := _, prop_tensor' := _}
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
Define FinVect as the subtype of Module.{u} K of finite dimensional vector spaces.
Equations
- FinVect K = {V // finite_dimensional K ↥V}
Instances for FinVect
@[protected, instance]
@[protected, instance]
@[protected, instance]
Equations
- FinVect.inhabited K = {default := ⟨Module.of K K semiring.to_module, _⟩}
def
FinVect.of
(K : Type u)
[field K]
(V : Type u)
[add_comm_group V]
[module K V]
[finite_dimensional K V] :
FinVect K
Lift an unbundled vector space to FinVect K.
Equations
- FinVect.of K V = ⟨Module.of K V _inst_3, _⟩
@[protected, instance]
def
FinVect.Module.category_theory.has_forget₂
(K : Type u)
[field K] :
category_theory.has_forget₂ (FinVect K) (Module K)
Equations
@[protected, instance]
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' := _}
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), _⟩
Instances for FinVect.FinVect_dual
Instances for ↥FinVect.FinVect_dual
@[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)
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
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)), ⇑(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
@[simp]
theorem
FinVect.FinVect_evaluation_apply
(K : Type u)
[field K]
(V : FinVect K)
(f : ↥(FinVect.FinVect_dual K V))
(x : ↥V) :
@[protected, instance]
Equations
- FinVect.exact_pairing K V = {coevaluation := FinVect.FinVect_coevaluation K V, evaluation := FinVect.FinVect_evaluation K V, coevaluation_evaluation' := _, evaluation_coevaluation' := _}
@[protected, instance]
Equations
@[protected, instance]
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) :
@[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) :
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' := _}