# Zulip Chat Archive

## Stream: maths

### Topic: dealing with multiple instanciation

#### Simon Andreys (Nov 25 2020 at 11:39):

I'm considering a vector space V on a field K, with a given endomorphism f : V->V, and I want to use the structure of K[X] module on V defined by P.v=P(f).v for a polynomial P and v in V. The problem is that V is already an instance of a module (it is a K-module) , so I can't just define

```
instance : module (polynomial K) V:=
{
smul:=λ p, polynomial.aeval f p,
...
}
```

What is the standard way to deal with this situation ? Should I define some other `add_comm_group`

W with a group equivalence with V and define the K[X] module structure on W ? Is there a less tedious way to do that ?

#### Eric Wieser (Nov 25 2020 at 11:41):

V is already an instance of a module

What do you mean by this? Are you saying there is a `module (polynomial K) V`

instance already, or just some other `module _ V`

instance? If so, what is `_`

?

#### Simon Andreys (Nov 25 2020 at 11:42):

I mean that V is a K-module

#### Eric Wieser (Nov 25 2020 at 11:43):

That should be fine, unless mathlib is automatically building a `module (polynomial K) V`

instance behind the scenes because it found `module K V`

...

#### Simon Andreys (Nov 25 2020 at 11:44):

I got a error message :

invalid definition, a declaration named 'module' has already been declared

#### Eric Wieser (Nov 25 2020 at 11:45):

That's a different problem. You need to give your instance a name, or put it in a namespace

#### Eric Wieser (Nov 25 2020 at 11:46):

`instance my_module : module (polynomial K) V := ...`

or

```
namespace my_stuff
instance : module (polynomial K) V := ...
end my_stuff
```

Otherwise you're trying to replace the type `module`

with your instance

#### Eric Wieser (Nov 25 2020 at 11:46):

Typically you'd work within a namespace anyway

#### Eric Wieser (Nov 25 2020 at 11:46):

It's always good to include the error message so that people can un- #xy your problem

#### Simon Andreys (Nov 25 2020 at 11:56):

Ok thanks ! I thought this was a more general problem, but I should've included the error message anyway. The namespace works, but it seems to cause later problem in defining `linear_equiv`

. I have another K[X]-module `kxdivp p0`

and I want to assume that it is linearly equivalent to V :

```
variable (φ : linear_equiv (polynomial K) (kxdivp p0) V)
```

I get the following error message :

```
failed to synthesize type class instance for
K : Type,
_inst_1 : field K,
V : Type,
_inst_2 : add_comm_group V,
_inst_3 : vector_space K V,
f : V →ₗ[K] V,
p0 : polynomial K,
l : K,
n : ℕ
⊢ semimodule (polynomial K) V
```

Maybe this is coming from some semimodule/module problem, but I got no error message from

```
variable (φ : linear_equiv (polynomial K) (kxdivp p0) (kxdivp p0)
```

#### Eric Wieser (Nov 25 2020 at 12:01):

Does switching your instance to `semimodule`

help?

#### Kevin Buzzard (Nov 25 2020 at 12:02):

Posting complete working code will make it much easier to debug what is going on.

#### Simon Andreys (Nov 25 2020 at 12:04):

I still have the same error message. Here is the complete code :

```
import algebra.module.basic algebra.field data.polynomial algebra.polynomial.group_ring_action
variables {K:Type} [field K] {V:Type} [add_comm_group V] [vector_space K V] (f : linear_map K V V)
noncomputable theory
-- The set of endomorphisms on V can be seen as a K-algebra
--#check module.endomorphism_algebra K V
--we use the aeval map P f → P(f) to construct the scalar multiplication (smul) P•v=P(f) v.
-- #check λ (p:polynomial K) (v:V), (polynomial.aeval f p) v
--The construction of the K[X]-module structure on V follows.
--note that f is not a hidden variable and must be repeated hereafter.
namespace vector_space_as_kx_module
open polynomial
instance : semimodule (polynomial K) V:=
{
smul:=λ p, polynomial.aeval f p,
one_smul:=λ v, begin simp, end,
mul_smul:=λ p q v,begin simp, end,
smul_add:=λ p u v, begin simp, end,
smul_zero:=λ p, begin simp, end,
add_smul:=λ p q v, begin simp, end,
zero_smul:=λ v, begin simp, end,
}
--GOAL now show that if V≃ K[X]/ (X-λ)^k (as K[X]-modules) then there is a K-basis of V in which the matrix of f is a Jordan block.
--look for K[X]/(P), module isomorphism, basis and matrix.
/-
#check linear_equiv (polynomial K)
#check ideal.quotient
#check {p:polynomial K | p=X}
#check ideal.span {p:polynomial K|p=X}
#check (ideal.span {p:polynomial K|p=X}).quotient
-/
--first we define kxdivp_as_kx_module, the module K[X]/(P) on K[X].
variables (p0 :polynomial K)
def idealp:=ideal.span {q:polynomial K|q=p0 }
def kxdivp:=(idealp p0).quotient
instance : comm_ring $ kxdivp p0 :=ideal.quotient.comm_ring (idealp p0)
instance : module (polynomial K) (kxdivp p0) :=
{
smul:=λ q,λ v, (ideal.quotient.mk (idealp p0) q)*v ,
one_smul:=λ v, begin simp, end,
mul_smul:=λ p q v,begin simp, rw mul_assoc, end,
smul_add:=λ p u v, begin simp, rw mul_add, end,
smul_zero:=λ p, begin simp, end,
add_smul:=λ p q v, begin simp, rw add_mul, end,
zero_smul:=λ v, begin simp, end,
}
--then we fix l:K and we assume that K[X]/(X-l)^n ≃ V
variables (l: K) (n:nat)
variable (φ : linear_equiv (polynomial K) (kxdivp p0) V)
#check V
end vector_space_as_kx_module
```

#### Simon Andreys (Nov 25 2020 at 12:08):

Maybe the issue is with the variable f ? How can I specify that f is the linear map I want to use to construct the K[X]-module structure ?

#### Eric Wieser (Nov 25 2020 at 12:19):

Yes, your problem is indeed `f`

#### Eric Wieser (Nov 25 2020 at 12:19):

If `instance`

s have arguments, then they can't be found by type-class resolution

#### Kevin Buzzard (Nov 25 2020 at 13:10):

Yeah. There's supposed to be one instance per class, and here you want a family of instances parametrised by f which is unfortunately not what the type class system was designed to do :-(

#### Simon Andreys (Nov 25 2020 at 13:18):

Thank you for your help ! I should've thought of it earlier, it's not the first time I'm confused by an implicit argument. I struggled a bit to see how to specify `f`

, I came up with the following: I give the name `Vmodule`

to the instance of `module (polynomial K) V`

and then I can declare the variable `\phi`

with

```
variable (φ : @linear_equiv (polynomial K) (kxdivp p0) V _ _ _ _ (vector_space_as_kx_module.Vmodule f) )
```

strangely I have to specify the namespace "vector_space_as_kx_module" here although I am already in the namespace, I suppose this prevent some issues with unnamed instances.

#### Kevin Buzzard (Nov 25 2020 at 13:18):

:-(

#### Reid Barton (Nov 25 2020 at 13:18):

Yeah, I think you always have to use the full name for instances.

#### Reid Barton (Nov 25 2020 at 13:19):

Also, I predict this will get awkward very quickly.

#### Reid Barton (Nov 25 2020 at 13:19):

I mean, more awkward :upside_down:

#### Simon Andreys (Nov 25 2020 at 13:25):

Okay I will try using "def" instead of instance in this case, hopefully this doesn't get even more awkward. @Kevin Buzzard why the sad face ?

#### Kevin Buzzard (Nov 25 2020 at 13:44):

Because what you're doing is mathematically completely reasonable but it's going to be a pain to do here because of design decisions which are usually correct but are in this case incorrect

#### Eric Wieser (Nov 25 2020 at 13:46):

You could create a new type that wraps V and attaches f

#### Reid Barton (Nov 25 2020 at 13:47):

A more common approach in Lean is to define something like `def kx_module (V) (f : linear_map K V V) : Type := V`

and put the `K[X]`

-module instance on that instead, but it's also not perfect

#### Eric Wieser (Nov 25 2020 at 13:47):

`def fV (f : ...) := V`

#### Kevin Buzzard (Nov 25 2020 at 13:48):

You can make a cute little function (indeed you already have) which takes f as an input and spits out the module instance you want, but now you're going to have to feed it into the system every time you want to use it. You could I guess use a type alias instead. In maths we might write $V_f$ for $V$ with the $K[X]$-action coming from $f$.

#### Eric Wieser (Nov 25 2020 at 13:48):

I suppose you could also attach `f`

to the polynomial type instead

#### Kevin Buzzard (Nov 25 2020 at 13:49):

Having typed that message on my phone i now see that several other people said it too :-)

#### Simon Andreys (Nov 25 2020 at 13:54):

Ok thank you everyone ! As you may have guessed my long-term goal is the Jordan normal form, though this part was mostly a warm-up before I get started with torsion PID modules. I'll try the `def fV f :=V`

solution and see how it goes to prove that if there is a \phi linear equivalence with K[X]/((x-l)^n) then f is a Jordan block in the relevant basis.

Last updated: May 18 2021 at 07:19 UTC