FinVect

Stream: general

[Antoine Labelle]

With the current definitions, a morphism f : V ⟶ W where V W : FinVect K is a linear map from V.val to W.val. On the other hand, it is difficult to work with the module V.val because finite_dimensional K V.val is currently not found by apply_instance (docs#FinVect.finite_dimensional only give us an instance of finite_dimensional K V).
Hence if I want to work with FinVect I have two options: either I add an instance finite_dimensional K V.val and work with linear maps between things of type Module K, or I add something like FinVect.to_linear_map (f : V ⟶ W) : V →ₗ[K] W and work with linear maps between things of type FinVect K.
I would appreciate any thoughts on this, which option should be preferred and why?

[Adam Topaz]

Can you give a concrete example where you run into an issue?

[Scott Morrison]

I wonder if we could use a custom structure for FinVect instead of subtype, to avoid these pesky .vals.

[Scott Morrison]

But yes, a concrete example of this problem would be great.

[Antoine Labelle]

Here's the concrete example that led me this issue.

import representation_theory.fdRep
import linear_algebra.trace

universes u
variables {k G : Type u} [field k] [monoid G] (V W : fdRep k G)

def character (g : G) := linear_map.trace k V (V.ρ g)

lemma char_tensor : (V ⊗ W).character = V.character * W.character :=
by { ext g, convert linear_map.trace_tensor_product' (V.ρ g) (W.ρ g) } --fails because `module.finite k V.V.val` instance missing

With this definition the character is the trace of V.ρ g which is a linear map from V.V.val to itself, and I can't prove anything about this since V.V.val doesn't have a finite_dimensional instance.

[Antoine Labelle]

So either I add that instance or I define it as a linear map from V.V to itself.

[Antoine Labelle]

I think Scott's proposition makes sense too

[Adam Topaz]

Your code is not working for me

[Antoine Labelle]

What is failing?

[Adam Topaz]

Oh, just a namespace missing and a noncomputable flag.

[Adam Topaz]

it's okay I added them on my end

[Scott Morrison]

Just add the line def ρ (V : fdRep k G) : G →* (V →ₗ[k] V) := V.ρ in fdRep.lean.

[Scott Morrison]

Probably just before the example on line 53.

[Scott Morrison]

This will fix your problem, and is a good idea anyway. It just provides a synonym for Action.ρ but which uses the coercion rather than going via subtype.val.

[Adam Topaz]

HEre's some code to illustrate the issue:

import representation_theory.fdRep
import linear_algebra.trace

universes u
variables (k : Type u) [field k]

open category_theory

@[derive [large_category, λ α, has_coe_to_sort α (Sort*)]]
def FinVect' := { V : Module.{u} k // finite_dimensional k V }

namespace FinVect'
instance finite_dimensional (V : FinVect' k) : finite_dimensional k V := V.prop
end FinVect'

example (V W : FinVect' k) (f : V ⟶ V) (g : W ⟶ W) : true :=
begin
  have := linear_map.trace_tensor_product' f g,  -- fails
end

@[derive [λ α, has_coe_to_sort α (Sort*)]]
def FinVect'' := { V : Module.{u} k // finite_dimensional k V }

namespace FinVect''
instance finite_dimensional (V : FinVect'' k) : finite_dimensional k V := V.prop

instance : category (FinVect'' k) :=
{ hom := λ V W, V →ₗ[k] W,
  id := λ _, linear_map.id,
  comp := λ _ _ _ f g, g.comp f,
  id_comp' := sorry,
  comp_id' := sorry,
  assoc' := sorry }

end FinVect''

example (V W : FinVect'' k) (f : V ⟶ V) (g : W ⟶ W) : true :=
begin
  have := linear_map.trace_tensor_product' f g,
end

[Adam Topaz]

Yeah, so it seems that the issue is precisely because the coercion to sort is not used to define the morphisms in the category structure.

[Scott Morrison]

@Adam Topaz, I think in your last example you need to delete the -- fails!

[Antoine Labelle]

Ok thanks, I think that would solve my issue. But there's still a general issue with FinVect, right?

[Antoine Labelle]

Also I think that might introduce another issue: I want to use docs#Action.iso.conj_ρ to prove that isomorphic objects of fdRep have the same character, but I don't think it works on the new definition of ρ. I'm not sure though.

[Adam Topaz]

I don't know if this is necessarily an issue with FinVect. It's a fairly common issue we have (not just with FinVect) that it can be annoying to go back and forth between the unbundled world of typeclasses and the bundled world of category theory. We could fix small issues here and there, but it's a more pervasive problem that should be given more serious thought.