Linear endofunctors of finite-dimensional vector spaces

A linear endofunctor of finite-dimensional vector spaces has a canonical evaluation map

F(k) ⊗ V → F(V).

It sends x ⊗ v to the image of x under F applied to the linear map k → V, a ↦ a • v. This is the natural comparison needed to upgrade the finite-string detector calculation at the ground field to a natural functorial statement.

def MagnitudeConjecture.FiniteVectorSpace.pointMap {k : Type u} [Field k] (V : FGModuleCat k) (v : ↑V) : FGModuleCat.of k k ⟶ V

A vector, regarded as the linear map from the ground field which sends 1 to that vector.

@[simp]

theorem MagnitudeConjecture.FiniteVectorSpace.pointMap_apply {k : Type u} [Field k] (V : FGModuleCat k) (v : ↑V) (a : k) : (ModuleCat.Hom.hom (pointMap V v).hom) a = a • v

@[simp]

theorem MagnitudeConjecture.FiniteVectorSpace.pointMap_add {k : Type u} [Field k] (V : FGModuleCat k) (v w : ↑V) : pointMap V (v + w) = pointMap V v + pointMap V w

@[simp]

theorem MagnitudeConjecture.FiniteVectorSpace.pointMap_smul {k : Type u} [Field k] (V : FGModuleCat k) (r : k) (v : ↑V) : pointMap V (r • v) = r • pointMap V v

def MagnitudeConjecture.FiniteVectorSpace.functorEvaluationBilinear {k : Type u} [Field k] (F : CategoryTheory.Functor (FGModuleCat k) (FGModuleCat k)) [F.Additive] [CategoryTheory.Functor.Linear k F] (V : FGModuleCat k) : ↑(F.obj (FGModuleCat.of k k)) →ₗ[k] ↑V →ₗ[k] ↑(F.obj V)

The bilinear evaluation pairing associated to a linear endofunctor.

def MagnitudeConjecture.FiniteVectorSpace.functorEvaluation {k : Type u} [Field k] (F : CategoryTheory.Functor (FGModuleCat k) (FGModuleCat k)) [F.Additive] [CategoryTheory.Functor.Linear k F] (V : FGModuleCat k) : CategoryTheory.MonoidalCategoryStruct.tensorObj (F.obj (FGModuleCat.of k k)) V ⟶ F.obj V

The canonical evaluation map F(k) ⊗ V → F(V) of a linear endofunctor.

@[simp]

theorem MagnitudeConjecture.FiniteVectorSpace.functorEvaluation_tmul {k : Type u} [Field k] (F : CategoryTheory.Functor (FGModuleCat k) (FGModuleCat k)) [F.Additive] [CategoryTheory.Functor.Linear k F] (V : FGModuleCat k) (x : ↑(F.obj (FGModuleCat.of k k))) (v : ↑V) : (ModuleCat.Hom.hom (functorEvaluation F V).hom) (x ⊗ₜ[k] v) = (ModuleCat.Hom.hom (F.map (pointMap V v)).hom) x

def MagnitudeConjecture.FiniteVectorSpace.functorEvaluationNatTrans {k : Type u} [Field k] (F : CategoryTheory.Functor (FGModuleCat k) (FGModuleCat k)) [F.Additive] [CategoryTheory.Functor.Linear k F] : CategoryTheory.MonoidalCategory.tensorLeft (F.obj (FGModuleCat.of k k)) ⟶ F

Evaluation is natural in the finite-dimensional coefficient space.

@[simp]

theorem MagnitudeConjecture.FiniteVectorSpace.hom_hom_sum {k : Type u} [Field k] {ι : Type u_1} [Fintype ι] {V W : FGModuleCat k} (f : ι → (V ⟶ W)) : ModuleCat.Hom.hom (∑ i : ι, f i).hom = ∑ i : ι, ModuleCat.Hom.hom (f i).hom

noncomputable def MagnitudeConjecture.FiniteVectorSpace.coordinateMap {k : Type u} [Field k] {ι : Type u_1} [Fintype ι] (V : FGModuleCat k) (b : Module.Basis ι k ↑V) (i : ι) : V ⟶ FGModuleCat.of k k

A basis coordinate, bundled as a morphism to the ground field.

@[simp]

theorem MagnitudeConjecture.FiniteVectorSpace.coordinateMap_apply {k : Type u} [Field k] {ι : Type u_1} [Fintype ι] (V : FGModuleCat k) (b : Module.Basis ι k ↑V) (i : ι) (v : ↑V) : (ModuleCat.Hom.hom (coordinateMap V b i).hom) v = (b.repr v) i

theorem MagnitudeConjecture.FiniteVectorSpace.sum_coordinateMap_comp_pointMap_eq_id {k : Type u} [Field k] {ι : Type u_1} [Fintype ι] (V : FGModuleCat k) (b : Module.Basis ι k ↑V) : ∑ i : ι, CategoryTheory.CategoryStruct.comp (coordinateMap V b i) (pointMap V (b i)) = CategoryTheory.CategoryStruct.id V

The rank-one maps supplied by a finite basis sum to the identity.

noncomputable def MagnitudeConjecture.FiniteVectorSpace.functorEvaluationSection {k : Type u} [Field k] (F : CategoryTheory.Functor (FGModuleCat k) (FGModuleCat k)) [F.Additive] [CategoryTheory.Functor.Linear k F] (V : FGModuleCat k) : F.obj V ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj (F.obj (FGModuleCat.of k k)) V

A basis-dependent right inverse to the basis-free evaluation map. Its only role is to prove that evaluation is an isomorphism.

@[simp]

theorem MagnitudeConjecture.FiniteVectorSpace.functorEvaluationSection_apply {k : Type u} [Field k] (F : CategoryTheory.Functor (FGModuleCat k) (FGModuleCat k)) [F.Additive] [CategoryTheory.Functor.Linear k F] (V : FGModuleCat k) (y : ↑(F.obj V)) : (ModuleCat.Hom.hom (functorEvaluationSection F V).hom) y = ∑ i : Fin (Module.finrank k ↑V), (ModuleCat.Hom.hom (F.map (coordinateMap V (Module.finBasis k ↑V) i)).hom) y ⊗ₜ[k] (Module.finBasis k ↑V) i

theorem MagnitudeConjecture.FiniteVectorSpace.functorEvaluationSection_comp_evaluation {k : Type u} [Field k] (F : CategoryTheory.Functor (FGModuleCat k) (FGModuleCat k)) [F.Additive] [CategoryTheory.Functor.Linear k F] (V : FGModuleCat k) : CategoryTheory.CategoryStruct.comp (functorEvaluationSection F V) (functorEvaluation F V) = CategoryTheory.CategoryStruct.id (F.obj V)

The basis section is a right inverse of the canonical evaluation map.

theorem MagnitudeConjecture.FiniteVectorSpace.functorEvaluation_bijective {k : Type u} [Field k] (F : CategoryTheory.Functor (FGModuleCat k) (FGModuleCat k)) [F.Additive] [CategoryTheory.Functor.Linear k F] (V : FGModuleCat k) : Function.Bijective ⇑(ModuleCat.Hom.hom (functorEvaluation F V).hom)

The canonical evaluation map of an additive linear endofunctor is bijective on every finite-dimensional vector space.

noncomputable def MagnitudeConjecture.FiniteVectorSpace.functorEvaluationNatIso {k : Type u} [Field k] (F : CategoryTheory.Functor (FGModuleCat k) (FGModuleCat k)) [F.Additive] [CategoryTheory.Functor.Linear k F] : CategoryTheory.MonoidalCategory.tensorLeft (F.obj (FGModuleCat.of k k)) ≅ F

Finite-dimensional Eilenberg--Watts over a field: an additive linear endofunctor is naturally isomorphic to tensoring with its value on the ground field.