Zulip Chat Archive

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?

Kevin Buzzard (Jun 22 2020 at 20:01):

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

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.

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

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

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.

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]?

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.

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

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!

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

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