Zulip Chat Archive

Stream: Is there code for X?

Topic: fdvs lemmas


view this post on Zulip Kevin Buzzard (Jun 22 2020 at 19:57):

Can we for example proof that if V is a 9-dimensional vector space, and X and Y are two 5-dimensional subspaces, then X \cap Y is non-zero? I'm happy to do the work proving the lemma but I don't know where to start. Do we have dim(X+Y)=dim(X)+dim(Y)-dim(X \cap Y)? Is it some statement about cardinals instead of naturals?

view this post on Zulip Kevin Buzzard (Jun 22 2020 at 20:01):

Oh great, search works :-) I am now reading linear_algebra.finite_dimensional

view this post on Zulip Kevin Buzzard (Jun 22 2020 at 21:09):

meh, the thing I want is only proved for arbitrary vector spaces as far as I can see. The API is good enough to prove the finite-dimensional case; maybe I should add it though.

view this post on Zulip Jalex Stark (Jun 22 2020 at 21:33):

from reading the docs in that file, it seems like "port more stuff from cardinal dimension" is a goal, so probably your lemma should be PRed

view this post on Zulip Kevin Buzzard (Jun 22 2020 at 21:43):

A mathematics lecturer with no Lean background was asking me about this lemma -- they wanted to know if this sort of thing was possible in Lean. Here's the proof I knocked up for them :

-- boilerplate -- ignore for now
import tactic
import linear_algebra.finite_dimensional

open vector_space
open finite_dimensional
open submodule

-- Let's prove that if V is a 9-dimensional vector space, and X and Y are 5-dimensional subspaces
-- then X ∩ Y is non-zero

theorem five_inter_five_in_nine_is_nonzero
-- let K be a field
(K : Type) [field K]

-- let V be a finite-dimensional vector space over K
(V : Type) [add_comm_group V] [vector_space K V] (hVfin : finite_dimensional K V)

-- and let's assume V is 9-dimensional
-- (note that dim will return a cardinal! findim returns a natural number)
(hV : findim K V = 9)

-- Let X and Y be subspaces of V
(X Y : subspace K V)

-- and let's assume they're both 5-dimensional
(hX : findim K X = 5)
(hY : findim K Y = 5)

-- then X ∩ Y isn't 0
: X  Y  

-- Proof
:= begin
-- I will give a proof which uses *the current state of mathlib*.
-- Note that mathlib can be changed, and other lemmas can be proved,
-- and notation can be created, which will make this proof much more
-- recognisable to undergraduates

-- The key lemma from the library we'll need is that dim(X + Y) + dim(X ∩ Y) = dim(X)+dim(Y)
have key : dim K (X  Y) + dim K (X  Y) = dim K X + dim K Y := dim_sup_add_dim_inf_eq X Y,

-- Unfortunately this is only proved in the library, right now, for arbitrary vector
-- spaces (i.e no finite dimension assumptions). This can be fixed, by adding the
-- finite-dimensional version. The point is that there's an invisible map from natural
-- numbers to cardinals, but it is a map; key is currently a statement about cardinals.

-- Because the lemma is not proved for finite-dimensional spaces, I have to
-- deduce it from the cardinal version
repeat {rw findim_eq_dim at key},
norm_cast at key,

-- `key` is now a statement about natural numbers. It says dim(X+Y)+dim(X∩Y)=dim(X)+dim(Y)
-- Now let's substitute in the hypothesis that dim(X)=dim(Y)=5
rw hX at key, rw hY at key,

-- so now we know dim(X+Y)+dim(X∩Y)=10.

-- Let's now turn to the proof of the theorem.
-- Let's prove it by contradiction. Assume X∩Y is 0
intro hXY,

-- then we know dim(X+Y) + dim(0) = 10
rw hXY at key,

-- and dim(0) = 0
rw findim_bot at key,

-- so the dimension of X+Y is 10

norm_num at key,

-- But the dimension of a subspace is at most the dimension of a space

have key2 : findim K (X  Y)  findim K V := findim_le (X  Y),

-- and now we can get our contradiction by just doing linear arithmetic
linarith,


end

view this post on Zulip Kevin Buzzard (Jun 22 2020 at 21:47):

I don't have time to PR this tonight, but this is an attempt to show a mathematician interested in using Lean for teaching how to a question on his problem sheet, so the easier on the eye we can make it the better.

view this post on Zulip Yakov Pechersky (Jun 22 2020 at 21:54):

Why do you set the hVfin : finite_dimensional K V as opposed to [finite_dimensional K V]?

view this post on Zulip Yakov Pechersky (Jun 22 2020 at 21:55):

It's a bit confusing, because your other hypotheses h* are equalities, and X Y are terms of a type, but hVfin is a hypothesis but not an equality.

view this post on Zulip Chris Hughes (Jun 22 2020 at 22:13):

Is it worth renaming findim to dim and using infindim for infinite dimension. How often does reasoning about infinite dimension come up? My guess is not that much

view this post on Zulip Kevin Buzzard (Jun 22 2020 at 23:10):

@Yakov Pechersky I've never used that stuff before -- if it was a class I missed it, it's just an error on my part. Thanks!

view this post on Zulip Kevin Buzzard (Jun 22 2020 at 23:11):

I think this stuff about dimensions was written by Mario when he was under the impression that ordinals and cardinals were actually used by mathematicians

view this post on Zulip Kevin Buzzard (Jun 22 2020 at 23:14):

I think there's also an argument for card being the finite one (sending infinite sets/types to zero) and infincard being the cardinal one. I might be biased here, I never see cardinals in number theory, perhaps they show up in other courses. It's perhaps worth noting that cardinals are defined in the Imperial curriculum in an optional 3rd year logic course which is not a prerequisite for any other course

view this post on Zulip Scott Morrison (Jun 23 2020 at 00:03):

I like this proposal to give the cardinal valued versions the clumsier names!

view this post on Zulip Mario Carneiro (Jun 23 2020 at 00:34):

that's fine with me. In the original version there was no findim at all, the idea was to use dim and coercion

view this post on Zulip Mario Carneiro (Jun 23 2020 at 00:34):

I believe the case of countably infinite dimension comes up reasonably often

view this post on Zulip Mario Carneiro (Jun 23 2020 at 00:35):

e.g. Hilbert spaces

view this post on Zulip Mario Carneiro (Jun 23 2020 at 00:36):

Uncountably infinite dimension is mostly only useful for choicy constructions like Hamel bases

view this post on Zulip Jalex Stark (Jun 23 2020 at 00:36):

i think you don't use dimension-based arguments very much in that context, precisely because cardinal arithmetic isn't strong enough to help you

view this post on Zulip Mario Carneiro (Jun 23 2020 at 00:36):

No, but you need to be able to say "this has dimension omega"

view this post on Zulip Jalex Stark (Jun 23 2020 at 00:36):

for sure

view this post on Zulip Mario Carneiro (Jun 23 2020 at 00:37):

we ended up defining "this has dimension < omega" as a typeclass because it makes sense

view this post on Zulip Mario Carneiro (Jun 23 2020 at 00:38):

But I think in more general circumstances it is more useful to be able to reason about free modules than bases directly

view this post on Zulip Jalex Stark (Jun 23 2020 at 00:38):

I'm arguing only in favor of "findim gets used much more than dim" (and therefore deserves the shorter names)


Last updated: May 17 2021 at 14:12 UTC