dealing with multiple instanciation

Stream: maths

[Simon Andreys]

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]

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]

I mean that V is a K-module

[Eric Wieser]

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]

I got a error message :
invalid definition, a declaration named 'module' has already been declared

[Eric Wieser]

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

[Eric Wieser]

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]

Typically you'd work within a namespace anyway

[Eric Wieser]

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

[Simon Andreys]

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]

Does switching your instance to semimodule help?

[Kevin Buzzard]

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

[Simon Andreys]

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]

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]

Yes, your problem is indeed f

[Eric Wieser]

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

[Kevin Buzzard]

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]

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]

:-(

[Reid Barton]

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

[Reid Barton]

Also, I predict this will get awkward very quickly.

[Reid Barton]

I mean, more awkward :upside_down:

[Simon Andreys]

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]

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]

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

[Reid Barton]

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]

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

[Kevin Buzzard]

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]

I suppose you could also attach f to the polynomial type instead

[Kevin Buzzard]

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

[Simon Andreys]

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.