# 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):

#### 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 `transport`

ing 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