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.
Equations
- monoidal_predicate_finite_dimensional K = {prop_id' := _, prop_tensor' := _}
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
Equations
- FinVect.inhabited K = {default := ⟨Module.of K K semiring.to_module, _⟩}
Lift an unbundled vector space to FinVect K
.
Equations
- FinVect.of K V = ⟨Module.of K V _inst_3, _⟩
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 = ⟨Module.of K (module.dual K ↥V) (module.dual.module K ↥V), _⟩
Instances for FinVect.FinVect_dual
Instances for ↥FinVect.FinVect_dual
The coevaluation map is defined in linear_algebra.coevaluation
.
Equations
The evaluation morphism is given by the contraction map.
Equations
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' := _}