How to express dual linear maps?

Stream: new members

[Xipan Xiao]

I was trying to prove that the double dual of a (finite dimensional) linear space is isomorphic to itself cannonically. However I was unable to even work out the statement itself, let alone a proof. The statement I tried is like:

import Mathlib

open CategoryTheory

universe u

variable (k : Type u) [Field k]

noncomputable def doubleDual (k : Type*) [Field k] : ModuleCat k ⥤ ModuleCat k where
  obj X := ModuleCat.of k (Module.Dual k (Module.Dual k X))
  map {X Y} (f : X ⟶ Y) := ModuleCat.ofHom (LinearMap.dualMap (LinearMap.dualMap f))

But the type of f doesn't match:

application type mismatch
LinearMap.dualMap f
argument
f
has type
X ⟶ Y : Type ?u.23
but is expected to have type
↑X →ₗ[k] ↑Y : Type ?u.23

I have no idea how to construct something with a type like ↑X →ₗ[k] ↑Y, what do these arrows even mean? I even don't know how to search the source code to find symbols like this to understand it.
And is there a category type like LinearSpace or VectorSpace I can use directly, instead of ModuleCat k?

Thanks very much for being patience with these beginner's questions.

[Luigi Massacci]

I would suggest looking at Ch. 9 of #mil to see how to do linear algebra in lean. I don't think it covers duals, but at least you wouldn't have ended up with ModuleCat (assuming you didn't purposefully want to state the theorem categorically)

[Luigi Massacci]

As for the actual theorem you want, @loogle Module.Finite, Module.Free, |- Module.IsReflexive ?_ ?_

[loogle]

:search: Module.IsReflexive.of_finite_of_free

[Luigi Massacci]

Nice, first try :tada:

[Jason Reed]

The up-arrows are coercions which also surprised me as a beginner. In emacs when they appeared in the goal view, I wasn't able to jump-to-definition on them, but I think vscode does make that possible.

[Jason Reed]

Ah, I see it is possible in lean 4 web to click on the up-arrow in the goal view and see its docstring, explaining that it is a coercion

[Xipan Xiao]

I do need a category since I'm trying to prove that the double dual as a functor, is naturally isomorphic to the identity functor.

[Kevin Buzzard]

Then you can't useModuleCat because this has no finiteness hypotheses so it won't be a natural isomorphism.

[Kevin Buzzard]

Wait -- how can a functor be a natural isomorphism? A natural transformation between functors can be a natural isomorphism.

[Kevin Buzzard]

PS

import Mathlib

open CategoryTheory

universe u

variable (k : Type u) [Field k]

noncomputable def doubleDual (k : Type*) [Field k] : ModuleCat k ⥤ ModuleCat k where
  obj X := ModuleCat.of k (Module.Dual k (Module.Dual k X))
  map {X Y} (f : X ⟶ Y) := ModuleCat.ofHom (LinearMap.dualMap (LinearMap.dualMap f.hom))

fixes it. X and Y are terms (they're objects of a category). ↑X and ↑Y are types (with k-module structures). The definition of the hom sets in the category ModuleCat is

structure Hom (M N : ModuleCat.{v} R) where
  private mk ::
  /-- The underlying linear map. -/
  hom' : M →ₗ[R] N

In other words, to make a term of type X ⟶ Y you give a linear map ↑X →ₗ[k] ↑Y, but these things are not equal, there is a function which passes from one to the other, which is why you can't use f and need to use f.hom. Note that you used ofHom to go the other way around when you reconstructed the dual of the dual of f as a map from the object X to the object Y; this moves from the linear map back to the morphism.

[Aaron Liu]

Kevin Buzzard said:

Wait -- how can a functor be a natural isomorphism? A natural transformation between functors can be a natural isomorphism.

I guess the statement is that the functor is naturally isomorphic with the identity?

[Kevin Buzzard]

As part of the data of a natural transformation from I (the identity functor) to DD (the double-dual functor) (on the category of fd k-vector spaces) you have to give morphisms from $V$ to $V^{**}$ for all $V$. Here's an exercise I did when I was writing my "canonical" paper: how about the morphism from $V$ to $V^{**}$ sending $v$ to $f\mapsto -f(v)$? Is this a natural isomorphism?

[Kevin Buzzard]

I was trying to figure out if I could argue that such a natural transformation could be regarded as "canonical".

[Xipan Xiao]

I guess the statement is that the functor is naturally isomorphic with the identity?

Exactly. Thank you for fixing the statement. :-)

[Xipan Xiao]

Then you can't useModuleCat because this has no finiteness hypotheses so it won't be a natural isomorphism.

How can I add the finiteness condition in the doubleDual statement?

[Kevin Buzzard]

You'll have to make the appropriate category yourself if we don't have it

[Kevin Buzzard]

docs#FDRep

[Kevin Buzzard]

docs#FGModuleCat

[Kevin Buzzard]

There it is, we have it, use that

[Xipan Xiao]

With the help from this thread, copilot, chatgpt and the usage of exact? I was finally able to finish the proof. I'm sharing the finished code here, and I guess there are still room to improve. Thank you all so much.

import Mathlib

open CategoryTheory

variable (k : Type*) [Field k]

def doubleDual : FGModuleCat k ⥤ FGModuleCat k where
  obj V := FGModuleCat.of k (Module.Dual k (Module.Dual k V))
  map f := FGModuleCat.ofHom (LinearMap.dualMap (LinearMap.dualMap f.hom))

instance instFiniteOfFGModuleCat (V : FGModuleCat k) : Module.Finite k V.obj := V.property

def identityFDVec : FGModuleCat k ⥤ FGModuleCat k where
  obj := id
  map := id

-- The natural transformation η, from the identity functor to the double dual functor.
def η (V : FGModuleCat k) : V ⟶ (FGModuleCat.of k (Module.Dual k (Module.Dual k V))) :=
  FGModuleCat.ofHom {
    toFun := fun v => {
      toFun := fun g => g v,
      map_add' := fun g₁ g₂ => by simp,
      map_smul' := fun a g => by simp,
    },
    map_add' := fun v₁ v₂ => by ext; simp,
    map_smul' := fun a v => by ext; simp,
  }

-- The underlying mapping of the inverse of the natural transformation η
noncomputable def η_inv_fun (V : FGModuleCat k)
  (f : Module.Dual k (Module.Dual k V)) : V :=
  let b := Basis.ofVectorSpace k (↑V)
  ∑ i, f (b.coord i) • b i

-- Verifies that η_inv_fun is a linear map: additions are preserved.
lemma η_inv_is_additive (V : FGModuleCat k)
    (f g : Module.Dual k (Module.Dual k V)) :
    η_inv_fun k V (f + g) = η_inv_fun k V f + η_inv_fun k V g := by
  let b := Basis.ofVectorSpace k (↑V)
  simp only [η_inv_fun]
  have h : ∀ i, (f + g) (b.coord i) • b i = f (b.coord i) • b i + g (b.coord i) • b i := by
    intro i
    exact add_smul (f (b.coord i)) (g (b.coord i)) (b i)
  rw [Finset.sum_congr rfl (fun i hi => h i), ← Finset.sum_add_distrib]

-- Verifies that η_inv_fun is a linear map: commutation of scalar multiplication.
lemma η_inv_commutes_scalar_mul (V : FGModuleCat k)
    (a : k) (f : Module.Dual k (Module.Dual k V)) :
    η_inv_fun k V (a • f) = a • η_inv_fun k V f := by
  let b := Basis.ofVectorSpace k (↑V)
  simp only [η_inv_fun]
  have h : ∀ i, (a • f) (b.coord i) • b i = a • f (b.coord i) • b i := by
    intro i
    exact smul_assoc a (f (b.coord i)) (b i)
  rw [Finset.sum_congr rfl (fun i hi => h i), Finset.smul_sum]

-- The inverse of the natural transformation η.
noncomputable def η_inv (V : FGModuleCat k) :
    FGModuleCat.of k (Module.Dual k (Module.Dual k V)) ⟶ V :=
  FGModuleCat.ofHom {
    toFun := η_inv_fun k V,
    map_add' := η_inv_is_additive k V,
    map_smul' := η_inv_commutes_scalar_mul k V,
  }

-- Applying η followed by η_inv gives the identity on V.
lemma η_inv_cancels_η (V : FGModuleCat k) : η k V ≫ η_inv k V = 𝟙 V := by
  ext x
  dsimp [η, η_inv, η_inv_fun]
  exact Basis.sum_repr (Basis.ofVectorSpace k ↑V) x

-- Applying η_inv followed by η gives the identity on the double dual of V.
lemma η_cancels_η_inv(V : FGModuleCat k) :
    η_inv k V ≫ η k V = 𝟙 (FGModuleCat.of k (Module.Dual k (Module.Dual k V))) := by
  ext f g
  dsimp [η, η_inv, η_inv_fun]
  let b := Basis.ofVectorSpace k (↑V)
  calc
    g (∑ i, f (b.coord i) • b i)
      = ∑ i, g (f (b.coord i) • b i) := by simp
    _ = ∑ i, f (b.coord i) • g (b i) := by simp
    _ = ∑ i, g (b i) • f (b.coord i) := by
      apply Finset.sum_congr rfl
      intro i _
      exact mul_comm (f (b.coord i)) (g (b i))
    _ = ∑ i, f (g (b i) • b.coord i) := by simp only [LinearMap.map_smul]
    _ = f (∑ i, g (b i) • b.coord i) := by
      exact Eq.symm (map_sum f (fun x ↦ g (b x) • b.coord x) Finset.univ)
    _ = f g := by rw [Basis.sum_dual_apply_smul_coord b g]


-- The natural isomorphism between the identity functor and the double dual functor.
noncomputable def doubleDualIso : identityFDVec k ≅ doubleDual k := NatIso.ofComponents
    (fun V => {
      hom := η k V,
      inv := η_inv k V,
      hom_inv_id := η_inv_cancels_η k V,
      inv_hom_id := η_cancels_η_inv k V,
    })
    (by
      intros X Y f
      dsimp [doubleDual, η]
      rfl
    )

[Kevin Buzzard]

eta is a natural transformation, not the natural transformation. You can put function inputs before the := like this:

-- The natural transformation η, from the identity functor to the double dual functor.
def η (V : FGModuleCat k) : V ⟶ (FGModuleCat.of k (Module.Dual k (Module.Dual k V))) :=
  FGModuleCat.ofHom {
    toFun v := {
      toFun g := g v
      map_add' g₁ g₂ := by simp
      map_smul' a g := by simp
    }
    map_add' v₁ v₂ := by ext; simp
    map_smul' a v := by ext; simp
  }

and you can delete all the commas (they're lean 3 isms).

[Kevin Buzzard]

You have reinvented the wheel with η_inv_fun; we have the isomorphism between V and its double-dual in the f.d. case already, it's

variable (V : FGModuleCat k) in
#check Module.evalEquiv k V

which applies because docs#Module.instIsReflexiveOfFiniteOfProjective says that a finite projective module is reflexive, and a module over a field is automatically projective. Of course this doesn't matter, no doubt you learnt something writing this stuff, and to be quite honest when I was learning this stuff I found exercises like this a lot of fun whether or not they were already in mathlib.

Great job for getting this calculation out!

[Xipan Xiao]

ah! Thank you so much for this new information. I think I got a much simplified proof:

import Mathlib

open CategoryTheory

variable (k : Type*) [Field k]

def doubleDual : FGModuleCat k ⥤ FGModuleCat k where
  obj V := FGModuleCat.of k (Module.Dual k (Module.Dual k V))
  map f := FGModuleCat.ofHom (LinearMap.dualMap (LinearMap.dualMap f.hom))

instance instFiniteOfFGModuleCat (V : FGModuleCat k) : Module.Finite k V.obj := V.property

def identityFDVec : FGModuleCat k ⥤ FGModuleCat k where
  obj := id
  map := id

noncomputable def doubleDualIso : identityFDVec k ≅ doubleDual k :=
  NatIso.ofComponents
    (fun V =>
      { hom := FGModuleCat.ofHom (Module.evalEquiv k V).toLinearMap
        inv := FGModuleCat.ofHom (Module.evalEquiv k V).symm.toLinearMap
        hom_inv_id := by ext; apply (Module.evalEquiv k V).symm_apply_apply
        inv_hom_id := by ext; apply (Module.evalEquiv k V).apply_symm_apply })
    (by intros X Y f; ext; rfl)

[Kevin Buzzard]

Yeah that looks great! Well done!

[Kevin Buzzard]

Now can do you my exercise about whether $v\mapsto(f\mapsto-f(v))$ is also a natural isomorphism?

[Xipan Xiao]

I think so, for it is the composition of η: V ⟶ V** and -1: V** ⟶V**, which is obviously a linear bijection. The naturality part also follows trivially from the original isomorphism: you just replace η with -η in the commutative diagram, since everything is linear, the equation still holds (by just timing -1 from both sides).

[Kevin Buzzard]

So now can you explain why $v\mapsto(f\mapsto f(v))$ is said by some people to be "canonical" but $v\mapsto(f\mapsto-f(v))$ is somehow not?

Bonus questions: can you write down all of the natural isomorphisms between the identity and your functor?

[Xipan Xiao]

Two linear isomorphisms from f, g: V \to W induces an automorphism f \circ g^{-1} of V. So nature isomorphisms differ by an automorphism of V (or V**) with η. If we want to find "all" of them, we can compose η with something from GL(n) to get another one, and there is nothing else. But this involves a choice of something from GL(n). I guess we call the one "canonical" because we chose the identity from GL(n).

[Aaron Liu]

But you have to define it on all spaces, not just the ones of dimension n

[Xipan Xiao]

ah then there is no so many choices, just two of them: id and -id?

[Aaron Liu]

You can do k • id for all invertible k in the scalar field

[Aaron Liu]

and I think you can get more with strong enough choice