Zulip Chat Archive

Stream: maths

Topic: vector spaces vs modules over a field


view this post on Zulip Johan Commelin (Jun 18 2018 at 07:25):

I have a module over a field. How do I upgrade it to a vector_space? We can't have a generic instance, because we would immediately get loops (every vector_space is already a module).

view this post on Zulip Johan Commelin (Jun 18 2018 at 07:26):

I really wish this would be transparent, because there is no content at all.

view this post on Zulip Chris Hughes (Jun 18 2018 at 09:18):

Something like this?

import linear_algebra.basic

variables {F : Type*} [field F] {M : Type*} [m : module F M]

instance Mvector_space : vector_space F M := {..m}

view this post on Zulip Gabriel Ebner (Jun 18 2018 at 09:20):

Maybe make vector_space a reducible definition for module?

view this post on Zulip Johan Commelin (Jun 18 2018 at 09:25):

@Chris Hughes That is tricky right? Because then we get cycles in the type class system.

view this post on Zulip Johan Commelin (Jun 18 2018 at 09:25):

@Gabriel Ebner How do I make a class reducible?

view this post on Zulip Chris Hughes (Jun 18 2018 at 09:28):

I agree it does seem a little silly. I'm not sure we'd get cycles any more than we would by any other use of extends. This is a little weird because there aren't any extra axioms, but extends is used all the time without any problems.

view this post on Zulip Chris Hughes (Jun 18 2018 at 09:29):

In fact just making what I just wrote a global instance is probably a good idea.

view this post on Zulip Gabriel Ebner (Jun 18 2018 at 09:29):

Not class, just @[reducible] def vector_space (α : Type u) (β : Type v) [field α] := module α β

view this post on Zulip Johan Commelin (Jun 18 2018 at 09:30):

But then we can't use the type class instance anymore...

view this post on Zulip Johan Commelin (Jun 18 2018 at 09:31):

Chris, Hmmm, I thought introducing cycles was a bad idea. I think we try to avoid them.

view this post on Zulip Johan Commelin (Jun 18 2018 at 09:31):

extends does not introduce cycles. So I don't understand your point.

view this post on Zulip Chris Hughes (Jun 18 2018 at 09:34):

The definition of vector_space just extends module with no extra axioms. So it won't introduce cycles.

view this post on Zulip Chris Hughes (Jun 18 2018 at 09:34):

If extends doesn't introduce cycles.

view this post on Zulip Gabriel Ebner (Jun 18 2018 at 09:34):

@Chris Hughes There is the cycle module -> vector_space -> module.

view this post on Zulip Gabriel Ebner (Jun 18 2018 at 09:35):

(If you add the instance.)

view this post on Zulip Chris Hughes (Jun 18 2018 at 09:35):

Oh I see.

view this post on Zulip Gabriel Ebner (Jun 18 2018 at 09:35):

@Johan Commelin I just tried replacing the vector_space class by a definition and everything seems to work. Why do you think it would break type class instances?

view this post on Zulip Johan Commelin (Jun 18 2018 at 09:37):

I mean, then I can't any longer write {V : Type} [vector_space real V] in my theorems. Right?

view this post on Zulip Johan Commelin (Jun 18 2018 at 09:37):

Because the [] only work for classes.

view this post on Zulip Chris Hughes (Jun 18 2018 at 09:38):

Maybe it will just interpret it as module real V

view this post on Zulip Johan Commelin (Jun 18 2018 at 09:38):

The reason that nothing breaks after your change, is because mathlib has not really used vector spaces yet. It only defines them...

view this post on Zulip Johan Commelin (Jun 18 2018 at 09:39):

Chris, hmm, that might be true! Then it might work!

view this post on Zulip Johan Commelin (Jun 18 2018 at 09:41):

@Gabriel Ebner Ok, I see that in fact on the line below there is already [vector_space ...] and it seems to work. You are right. Thanks!

view this post on Zulip Mario Carneiro (Jun 18 2018 at 11:42):

IIRC I set this up before (vector_space as reducible def) and @Johannes Hölzl reverted it to the current wrapper class style, so there was probably a reason although I forget what it is.

view this post on Zulip Mario Carneiro (Jun 18 2018 at 11:43):

I think the preferred solution is just to have instances of vector_space for all your vector spaces

view this post on Zulip Johan Commelin (Jun 18 2018 at 11:47):

Ok, but aren't you scared that this creates cycles?

view this post on Zulip Mario Carneiro (Jun 18 2018 at 11:47):

Chris's instance will create cycles. I'm not suggesting that

view this post on Zulip Johan Commelin (Jun 18 2018 at 11:48):

Or, you mean, explicitly saying

instance foobar : vector_space real V := {}

view this post on Zulip Johan Commelin (Jun 18 2018 at 11:48):

whenever V is a module over the reals.

view this post on Zulip Mario Carneiro (Jun 18 2018 at 11:48):

depends on what V is there

view this post on Zulip Mario Carneiro (Jun 18 2018 at 11:48):

if V is an arbitrary module over the reals, then no

view this post on Zulip Mario Carneiro (Jun 18 2018 at 11:49):

if you replace V with my_R_vec then yes

view this post on Zulip Mario Carneiro (Jun 18 2018 at 11:50):

If you want to deal with an arbitrary real vector space, the assumption should say vector_space not module

view this post on Zulip Chris Hughes (Jun 18 2018 at 11:50):

What happens if you have something like a vector space instance for polynomials over a field, but also a module instance for polynomials over a ring. Then you have cycles.

view this post on Zulip Mario Carneiro (Jun 18 2018 at 11:50):

no

view this post on Zulip Mario Carneiro (Jun 18 2018 at 11:50):

that's perfectly okay

view this post on Zulip Mario Carneiro (Jun 18 2018 at 11:50):

that's a diamond not a cycle

view this post on Zulip Mario Carneiro (Jun 18 2018 at 11:51):

and the defeq constraint will be easy to satisfy here

view this post on Zulip Johan Commelin (Jun 18 2018 at 11:55):

Mario, I am defining Lie algebras. They are modules over a ring with extra data and properties. But if my ring happens to be a field, then I want to prove extra things about my Lie algebras (using things like dimension etc...). How should I explain to Lean that if I have [field R] I want to upgrade my [lie_algebra L] to a [vector_space R L] instead of just the module R L that it extends?

view this post on Zulip Mario Carneiro (Jun 18 2018 at 11:59):

you can have an instance for that

view this post on Zulip Mario Carneiro (Jun 18 2018 at 11:59):

instance [field R] [lie_algebra L] : vector_space R L

view this post on Zulip Johan Commelin (Jun 18 2018 at 12:01):

ok, I see

view this post on Zulip Johan Commelin (Jun 18 2018 at 12:01):

That's a good solution, I guess (-;

view this post on Zulip Johannes Hölzl (Jun 18 2018 at 18:53):

I don't remember why I changed it to a class maybe I had a problem in combination with the inout parameter. We can change it back and see what happens.


Last updated: May 11 2021 at 16:22 UTC