Dual Functor

Stream: Is there code for X?

[Success Moses]

Is there code for the dual functor?

In fun (M : ModuleCat R) => Dual R M, I got error message "failed to synthesize Module R M"

import Mathlib.LinearAlgebra.Dual.Defs

open CategoryTheory Module

variable {R : Type} [Ring R] [CommSemiring R]

example : (ModuleCat R) ⥤ (ModuleCat R) := by
  refine {obj := ?_, map := ?_, map_id := ?_, map_comp := ?_}
  · exact fun M => Dual R M -- failed to synthesize `Module R M`
  · sorry -- dualMap
  · aesop
  · aesop

[Kevin Buzzard]

You don't want [Ring R] [CommSemiring R] -- that means "put two unrelated ring structures on R" and will quickly lead to confusion.

[Kim Morrison]

We really really need a linter for this.

[Success Moses]

It worked for [CommRing]. Thanks

variable {R : Type} [CommRing R]

example : (ModuleCat R) ⥤ (ModuleCat R) := by
  refine {obj := ?_, map := ?_, map_id := ?_, map_comp := ?_}
  · exact fun M => ModuleCat.of _ <| Dual R M

[Joël Riou]

The functor you are considering is contravariant: you need to define it as (ModuleCat R)ᵒᵖ ⥤ ModuleCat R.
It is unclear we need to add this definition, because it can be obtained as follows:

import Mathlib.Algebra.Category.ModuleCat.Monoidal.Closed

universe u

open CategoryTheory MonoidalClosed

variable (R : Type u) [CommRing R]

#check internalHom.flip.obj (ModuleCat.of R R)

Because of the way the type of morphisms in ModuleCat is packaged, this is not exactly the functor you are defining on objects, but it is naturally equivalent.