Zulip Chat Archive

Stream: maths

Topic: finite_dimensional assumption


view this post on Zulip Patrick Lutz (Sep 21 2020 at 23:52):

Why does findim_top (documentation) require that the vector space is finite_dimensional? If I'm understanding things correctly, it should be true in general. Is it because it's only coincidentally true if the vector space is finite dimensional (because it depends on the arbitrary decision of how to define findim for infinite dimensional vector spaces) and therefore it's bad to prove it? For reference, findim_top says

theorem findim_top [finite_dimensional K V] : findim K ( : submodule K V) = findim K V

In general, when mathlib includes arbitrary definitions meant to make a function total (like dividing by zero, or findim of infinite dimensional vector spaces), when is it reasonable to prove theorems that only work because of some particular details of that arbitrary definition?

view this post on Zulip Patrick Lutz (Sep 21 2020 at 23:53):

Also sorry if "maths" is not the right stream for this question. I wasn't really sure which stream it belonged in. Maybe "new members" but I feel like at some point I should stop posting questions there.

view this post on Zulip Mario Carneiro (Sep 21 2020 at 23:53):

I assume the author didn't bother to consider the infinite dimensional case

view this post on Zulip Patrick Lutz (Sep 21 2020 at 23:53):

Is it reasonable for me to add it?

view this post on Zulip Mario Carneiro (Sep 21 2020 at 23:54):

sure

view this post on Zulip Patrick Lutz (Sep 21 2020 at 23:54):

I want to add some lemmas about dimensions of subalgebras and this will make it slightly easier

view this post on Zulip Mario Carneiro (Sep 21 2020 at 23:55):

I assume findim is some operator applied to dim? If so the proof should be easy if you have dim K top = dim K V

view this post on Zulip Patrick Lutz (Sep 21 2020 at 23:57):

Yeah, that's true


Last updated: May 09 2021 at 11:09 UTC