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_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_zero:=λ p, begin  simp, 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 instances 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.

:-(

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