Documentation

TauCeti.Algebra.Category.FGModuleCat.Rigid

Left duals of finite-dimensional vector spaces #

The algebraic dual is both a left and a right dual in FGModuleCat K. Mathlib supplies the right pairing. Here the left pairing is obtained from the right pairing of the dual space by CategoryTheory.exactPairingCongrRight, using FGModuleCat.dualEvalIso for the classical double-dual evaluation isomorphism. In particular this choice does not use a braiding to construct the left dual. Its evaluation is the usual contraction, and its adjoint mates are ordinary transposes.

For Mathlib's right pairing, FGModuleCat.evaluation_hom_hom and FGModuleCat.coevaluation_hom_hom record that its evaluation and coevaluation are the contraction contractLeft and the coevaluation coevaluation of linear algebra.

The resulting LeftRigidCategory and RigidCategory instances also give rigidity of categories of group actions through Mathlib's existing instances.

source
@[instance_reducible]
noncomputable def FGModuleCat.leftExactPairing (K : Type u) [Field K] (V : FGModuleCat K) :
CategoryTheory.ExactPairing (dual K V) V

The left exact pairing of a vector space with its algebraic dual, transported from the right exact pairing of the dual along the double-dual evaluation isomorphism.

Instances For
    source
    @[instance_reducible]
    noncomputable instance FGModuleCat.leftDual (K : Type u) [Field K] (V : FGModuleCat K) :
    CategoryTheory.HasLeftDual V

    The left dual of a finite-dimensional vector space is its algebraic dual.

    source
    @[instance_reducible]
    noncomputable instance FGModuleCat.leftRigidCategory (K : Type u) [Field K] :
    CategoryTheory.LeftRigidCategory (FGModuleCat K)

    Finite-dimensional vector spaces have canonical left duals.

    source
    @[instance_reducible]
    noncomputable instance FGModuleCat.rigidCategory (K : Type u) [Field K] :
    CategoryTheory.RigidCategory (FGModuleCat K)

    Finite-dimensional vector spaces form a rigid category, with algebraic duals on both sides.

    source
    @[simp]
    theorem FGModuleCat.leftDual_eq {K : Type u} [Field K] (V : FGModuleCat K) :
    ᘁV = dual K V

    The chosen left dual is the algebraic dual used for the right dual.

    source
    @[simp]
    theorem FGModuleCat.evaluation_hom_hom {K : Type u} [Field K] (V : FGModuleCat K) :
    ModuleCat.Hom.hom (ε_ V Vᘁ).hom = contractLeft K ↑V

    Right evaluation is the contraction of a linear functional with a vector.

    source
    @[simp]
    theorem FGModuleCat.coevaluation_hom_hom {K : Type u} [Field K] (V : FGModuleCat K) :
    ModuleCat.Hom.hom (η_ V Vᘁ).hom = coevaluation K ↑V

    Right coevaluation is the coevaluation of linear algebra.

    source
    @[simp]
    theorem FGModuleCat.leftEvaluation_apply {K : Type u} [Field K] (V : FGModuleCat K) (x : ↑V) (f : Module.Dual K ↑V) :
    (ModuleCat.Hom.hom (ε_ (ᘁV) V).hom) (x ⊗ₜ[K] f) = f x

    Left evaluation is ordinary evaluation of a linear functional.

    source
    @[simp]
    theorem FGModuleCat.leftCoevaluation_hom {K : Type u} [Field K] (V : FGModuleCat K) :
    ModuleCat.Hom.hom (η_ (ᘁV) V).hom = LinearMap.lTensor (Module.Dual K ↑V) ↑(Module.evalEquiv K ↑V).symm ∘ₗ coevaluation K (Module.Dual K ↑V)

    Left coevaluation is coevaluation of the dual, with its double-dual factor identified with the original space by inverse evaluation.

    source
    @[simp]
    theorem FGModuleCat.leftAdjointMate_hom {K : Type u} [Field K] {V W : FGModuleCat K} (f : V ⟶ W) :
    ModuleCat.Hom.hom (ᘁf).hom = (ModuleCat.Hom.hom f.hom).dualMap

    A left adjoint mate evaluates a functional by precomposition with the original map.