The intersection of two 5-dimensional subspaces in 9-dimensional space is non-zero

vectorspace.lean

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