## Stream: general

### Topic: FinVect

#### Antoine Labelle (May 25 2022 at 02:06):

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 (May 25 2022 at 02:52):

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

#### Scott Morrison (May 25 2022 at 04:52):

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

#### Scott Morrison (May 25 2022 at 04:53):

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

#### Antoine Labelle (May 25 2022 at 13:13):

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 (May 25 2022 at 13:14):

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

#### Antoine Labelle (May 25 2022 at 13:16):

I think Scott's proposition makes sense too

#### Adam Topaz (May 25 2022 at 13:22):

Your code is not working for me

What is failing?

#### Adam Topaz (May 25 2022 at 13:23):

Oh, just a namespace missing and a noncomputable flag.

#### Adam Topaz (May 25 2022 at 13:23):

it's okay I added them on my end

#### Scott Morrison (May 25 2022 at 13:30):

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

#### Scott Morrison (May 25 2022 at 13:31):

Probably just before the example on line 53.

#### Scott Morrison (May 25 2022 at 13:31):

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 (May 25 2022 at 13:33):

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 (May 25 2022 at 13:34):

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 (May 25 2022 at 13:35):

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

#### Antoine Labelle (May 25 2022 at 13:41):

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

#### Antoine Labelle (May 25 2022 at 13:47):

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 (May 25 2022 at 13:48):

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.

Last updated: Aug 03 2023 at 10:10 UTC