Zulip Chat Archive

Stream: new members

Topic: Zero-dimensional vector space


Heather Macbeth (Jun 09 2020 at 01:53):

Where in mathlib is this fact? I tried library_search, but it timed out!

import linear_algebra.dimension

variables (𝕜 : Type*) [field 𝕜]
variables (E : Type*) [add_comm_group E] [vector_space 𝕜 E]

example (x : E) (h : vector_space.dim 𝕜 E = 0) : x = 0 := sorry

Scott Morrison (Jun 09 2020 at 03:09):

I wouldn't be particularly surprised if this isn't in mathlib yet. :-)

Heather Macbeth (Jun 09 2020 at 03:25):

Well, that would explain it! :)

Heather Macbeth (Jun 09 2020 at 03:27):

By the way, is there a predefined instance for the zero-dimensional vector space? The closest I could find on a quick pass is for the zero-dimensional subspace of a given vector space.

Scott Morrison (Jun 09 2020 at 03:30):

Maybe this should go in punit_instances.lean?

Scott Morrison (Jun 09 2020 at 03:31):

Maybe actually it's already there, since vector_space = module.

Scott Morrison (Jun 09 2020 at 03:31):

So just use punit as the underlying type.

Scott Morrison (Jun 09 2020 at 03:32):

But there won't be a finite_dimensional R punit instance yet, or the calculation of its dimension. :-)

Heather Macbeth (Jun 09 2020 at 03:33):

Aha, thank you. This punit is new to me.

Heather Macbeth (Jun 09 2020 at 03:35):

Will any zero-dimensional vector space over K be definitionally equal to module K punit ?

Heather Macbeth (Jun 09 2020 at 03:36):

Or will there only be an isomorphism?

Scott Morrison (Jun 09 2020 at 03:36):

only an iso

Scott Morrison (Jun 09 2020 at 03:36):

the underlying type could be any one element type

Scott Morrison (Jun 09 2020 at 03:38):

I guess one could derive a vector_space K V from unique V?

Scott Morrison (Jun 09 2020 at 03:38):

That would probably be evil to add to typeclass search, however.

Heather Macbeth (Jun 09 2020 at 03:40):

Could you explain your last comment? I don't know the unique V syntax, and it's not very searchable :)

Scott Morrison (Jun 09 2020 at 03:47):

Oh, there is a typeclass unique, that asserts that a type has exactly one elements.

Scott Morrison (Jun 09 2020 at 03:47):

src#unique

Scott Morrison (Jun 09 2020 at 03:48):

It's effectively a "this thing is equivalent to punit" typeclass.

Scott Morrison (Jun 09 2020 at 03:48):

While one could in principle prove instance vector_space_of_unique (V : Type*) [unique V] : vector_space K V := ...

Scott Morrison (Jun 09 2020 at 03:49):

(possibly by transporting the vector space structure from punit?!)

Scott Morrison (Jun 09 2020 at 03:49):

I don't think this would be a good use of typeclass search.

Scott Morrison (Jun 09 2020 at 03:50):

Because _every_ time someone looked for a vector_space K V instance now for some V, Lean would go off and see if it could produce unique V.

Heather Macbeth (Jun 09 2020 at 03:51):

I think I understand. Yes, it seems like a bad idea :)

Heather Macbeth (Jun 09 2020 at 03:52):

You are fixing the dimension somehow?

Heather Macbeth (Jun 09 2020 at 03:52):

i.e., this would be the fact about the uniqueness up to isomorphism of a vector space of fixed dimension?

Scott Morrison (Jun 09 2020 at 03:56):

no --- [unique V] is just saying that the type V itself has exactly one element. Nothing I've been saying is related to "uniqueness up to isomorphism of a vector space of fixed dimension", except for the much easier statement "uniqueness up to isomorphism of a vector space with one element".

Heather Macbeth (Jun 09 2020 at 03:59):

Oh, I see now what you mean by unique meaning "this thing is equivalent to punit". Thanks!


Last updated: Dec 20 2023 at 11:08 UTC