Theorems · Definition · category theory

FGModuleCat.FGModuleCatCoevaluation

(K : Type u) →
  [inst : Field K] →
    (V : FGModuleCat K) →
      CategoryTheory.MonoidalCategoryStruct.tensorUnit (FGModuleCat K) ⟶
        CategoryTheory.MonoidalCategoryStruct.tensorObj V (FGModuleCat.FGModuleCatDual K V)

The coevaluation map is defined in LinearAlgebra.coevaluation.

Defined in: Mathlib.Algebra.Category.FGModuleCat.Basic
Cited by: 1 results in Mathlib
Foundations: Depth 102 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: Field

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites11

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Quiver.Homstatement · cited by 32,603
Fieldstatement and proof · cited by 7,404
CategoryTheory.MonoidalCategoryStruct.tensorObjstatement · cited by 3,106
ModuleCatstatement · cited by 1,429
CategoryTheory.MonoidalCategoryStruct.tensorUnitstatement · cited by 1,384
ModuleCat.isFGstatement · cited by 53
FGModuleCatstatement and proof · cited by 52
FGModuleCat.carrierproof · cited by 28
CategoryTheory.ConcreteCategory.ofHomproof · cited by 18
FGModuleCat.FGModuleCatDualstatement · cited by 5
coevaluationproof · cited by 4

Cited by1

Results whose statement or proof uses this declaration.

FGModuleCat.FGModuleCatCoevaluation_apply_onestatement · cited by 0