Zero-dimensional vector space

Stream: new members

[Heather Macbeth]

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]

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

[Heather Macbeth]

Well, that would explain it! :)

[Heather Macbeth]

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]

Maybe this should go in punit_instances.lean?

[Scott Morrison]

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

[Scott Morrison]

So just use punit as the underlying type.

[Scott Morrison]

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

[Heather Macbeth]

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

[Heather Macbeth]

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

[Heather Macbeth]

Or will there only be an isomorphism?

[Scott Morrison]

only an iso

[Scott Morrison]

the underlying type could be any one element type

[Scott Morrison]

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

[Scott Morrison]

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

[Heather Macbeth]

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

[Scott Morrison]

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

[Scott Morrison]

src#unique

[Scott Morrison]

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

[Scott Morrison]

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

[Scott Morrison]

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

[Scott Morrison]

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

[Scott Morrison]

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]

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

[Heather Macbeth]

You are fixing the dimension somehow?

[Heather Macbeth]

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

[Scott Morrison]

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]

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