Show that dual of a vector space is a vector space

Stream: new members

[Hank]

As a practice, I defined my own version of the dual of a vector space in the code below. I want to show that the dual is indeed a C-module, but I don't know how. I saw the instance LinearMap.addCommMonoid in Mathlib4 doc and felt that I should use it in some way. I can also fill in all the methods that an instance of the class AddCommMonoid requires, but there are many of them, so I think there should be an lazier approach.

import Mathlib
open Complex Module LinearAlgebra

def dual (V : Type u) [AddCommMonoid V] [Module ℂ V] :=
  -- have h : Module ℂ ℂ := inferInstance
  LinearMap (RingHom.id ℂ) V ℂ

instance (V : Type u) [AddCommMonoid V] [Module ℂ V] : AddCommMonoid (dual V) := sorry

-- this line needs the above instance for AddCommMonoid
instance (V : Type u) [AddCommMonoid V] [Module ℂ V] : Module ℂ (dual V) := sorry

[Johan Commelin]

Voila: this is reusing the existing instances in Mathlib for LinearMap.

noncomputable
instance (V : Type u) [AddCommMonoid V] [Module ℂ V] : AddCommMonoid (dual V) := by
  unfold dual
  infer_instance

-- this line needs the above instance for AddCommMonoid
noncomputable
instance (V : Type u) [AddCommMonoid V] [Module ℂ V] : Module ℂ (dual V) := by
  unfold dual
  infer_instance

[Kevin Buzzard]

If you used abbrev dual instead of def dual then typeclass inference would just work and you wouldn't even need to unfold.

[Kevin Buzzard]

Also note that V \to\_l[\C] \C is notation for LinearMap (RingHom.id \C) V \C