## Stream: Is there code for X?

### Topic: fdvs lemmas

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

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

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

#### Scott Morrison (Jun 23 2020 at 00:03):

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

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

#### Mario Carneiro (Jun 23 2020 at 00:34):

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

#### Mario Carneiro (Jun 23 2020 at 00:35):

e.g. Hilbert spaces

#### Mario Carneiro (Jun 23 2020 at 00:36):

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

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

#### Mario Carneiro (Jun 23 2020 at 00:36):

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

for sure

#### Mario Carneiro (Jun 23 2020 at 00:37):

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

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

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