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.
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)
Equations
- FinVect.inhabited K = {default := {obj := Module.of K K semiring.to_module, property := _}}
Lift an unbundled vector space to FinVect K
.
Equations
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 = {obj := Module.of K (module.dual K ↥(V.obj)) (module.dual.module K ↥(V.obj)), property := _}
Instances for FinVect.FinVect_dual
The coevaluation map is defined in linear_algebra.coevaluation
.
Equations
- FinVect.FinVect_coevaluation K V = coevaluation K ↥(V.obj)
The evaluation morphism is given by the contraction map.
Equations
- FinVect.FinVect_evaluation K V = contract_left K ↥(V.obj)
Equations
- FinVect.exact_pairing K V = {coevaluation := FinVect.FinVect_coevaluation K V, evaluation := FinVect.FinVect_evaluation K V, coevaluation_evaluation' := _, evaluation_coevaluation' := _}
Equations
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
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' := _}