# Zulip Chat Archive

## 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 `.val`

s.

#### 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

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

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