## Stream: maths

### Topic: linear_independent

#### Johan Commelin (Feb 28 2019 at 10:36):

If my goal is linear_independent K s,
how do I turn this into the statement that the coefficient a_i is zero if sum a_i s_i = 0?
This part of the API seems to do lots of abstract stuff, but I'm missing this down to earth condition.

#### Johan Commelin (Feb 28 2019 at 10:37):

Maybe it is hidden in 5 layers of defeqs, but that doesn't seem user friendly to me.

#### Johan Commelin (Feb 28 2019 at 10:56):

@Kenny Lau Any hints?

oh no

#### Kenny Lau (Feb 28 2019 at 11:01):

iirc the lemma isn’t there

#### Johannes Hölzl (Feb 28 2019 at 11:35):

There is linear_independent_iffand lc.total is the sum operator

#### Johannes Hölzl (Feb 28 2019 at 11:36):

by the way, I'm working on adding the linear structure on the function (pi) space & for finsupp if you need this

#### Johan Commelin (Feb 28 2019 at 14:56):

I'm feeling really miserable today. People have said that it is a sobering thought that Lean does not know complex analysis. Well, as far as I know Lean also doesn't know anything about finite-dimensional vector spaces. And that's quite depressing.
I've tried to prove that V and its dual have the same dimension, and I get stuck in a maze of complicated definitions that don't fit in my brain-RAM. It probably means that I haven't understood the API for linear maps and modules... I'm not sure if that says something about me, or about the API.

#### Mario Carneiro (Feb 28 2019 at 15:24):

Do we have the dual vector space?

#### Patrick Massot (Feb 28 2019 at 15:26):

If we have linear maps and the instance saying that a field is a vector space over itself then we have duals, right?

#### Mario Carneiro (Feb 28 2019 at 15:27):

right. I'm trying to reconstruct the proof Johan is talking about

#### Mario Carneiro (Feb 28 2019 at 15:28):

what's the basis for the dual space?

#### Patrick Massot (Feb 28 2019 at 15:28):

I agree that the status of linear algebra in mathlib is much more depressing than the status of complex analysis. But we need to make choices, we can't work on everything at the same time

#### Patrick Massot (Feb 28 2019 at 15:28):

If you have a basis for the original space then you get the dual basis

#### Mario Carneiro (Feb 28 2019 at 15:28):

do you have to invent an inner product to define the dual basis

no

#### Patrick Massot (Feb 28 2019 at 15:29):

If the basis is (e_1, ..., e_n) then the dual basis is defined by l_i(e_j) = 1 if i =j, 0 otherwise

#### Patrick Massot (Feb 28 2019 at 15:29):

You need to know that a linear map can be specified by specifying it on a basis

#### Mario Carneiro (Feb 28 2019 at 15:30):

okay. We have that though

#### Mario Carneiro (Feb 28 2019 at 15:30):

I think it's called constr

#### Mario Carneiro (Feb 28 2019 at 15:30):

But this isn't always a basis, right? in infinite dimensions it breaks down

#### Patrick Massot (Feb 28 2019 at 15:31):

You don't talk about basis in infinite dimension, this would be a bad idea

#### Mario Carneiro (Feb 28 2019 at 15:31):

So we have a dual_basis function that takes any basis and makes a lin ind set in the dual space

#### Mario Carneiro (Feb 28 2019 at 15:31):

and if the original space is f.d then it's also a basis

yes

#### Patrick Massot (Feb 28 2019 at 15:33):

In infinite dimensions the dual tends to be bigger than the original space

#### Mario Carneiro (Feb 28 2019 at 15:33):

oh right, I just remembered that I had plans to redo linear_independent because it uses sets instead of families

ooh

#### Patrick Massot (Feb 28 2019 at 15:34):

That would be nice

#### Mario Carneiro (Feb 28 2019 at 15:34):

it's a lot more natural for everything except zorn's lemma

#### Mario Carneiro (Feb 28 2019 at 15:34):

but that's just one proof

#### Patrick Massot (Feb 28 2019 at 15:35):

Let's do more elementary maths since Jeremy opened the way with calculus. But not too elementary, I just spend one hour teaching how to "prove" the equivalence of five definitions of "convex polygon", I will never ever try to Lean that "proof"

#### Patrick Massot (Feb 28 2019 at 15:36):

I makes me think we need a Johannes countdown topic. I think we are getting dangerously close, and we still don't have integrals

#### Johan Commelin (Feb 28 2019 at 15:57):

Sorry, I was away for a while, because someone entered my office. Now I need to catch a train, so I will just dump the contents of my depression in this chat:

/-
Authors: Johan Commelin
-/

import linear_algebra.dimension linear_algebra.tensor_product
import set_theory.ordinal
noncomputable theory

local attribute [instance] classical.prop_decidable

section
variables (R : Type*) (M : Type*)
variables [comm_ring R] [add_comm_group M] [module R M]

def module.dual := M →ₗ[R] R

open module

instance : add_comm_group (dual R M) :=
by delta dual; apply_instance

instance : module R (dual R M) :=
by delta dual; apply_instance

def eval : M →ₗ[R] (dual R (dual R M)) := linear_map.id.flip

variables {R} {M}
def pairing : (dual R M) → M → R := λ (f : M →ₗ[R] R) m, f m

end

namespace is_basis
variables {K : Type*} {V : Type*}
variables [discrete_field K] [add_comm_group V] [vector_space K V]
variables {B : set V} (h : is_basis K B)
include h
open vector_space module submodule linear_map cardinal

def dual : set (module.dual K V) :=
{f : V →ₗ[K] K | ∃ v ∈ B, f v = 1 ∧ ∀ w ∈ B, w ≠ v → f w = 0}

def dual_elem (v : V) : module.dual K V :=
h.constr $λ w, if w = v then 1 else 0 lemma dual_elem_mem (v ∈ B) : h.dual_elem v ∈ h.dual := begin use [v,H], split; intros; erw [constr_basis]; simp *, end lemma mem_dual_iff (f : module.dual K V) : f ∈ h.dual ↔ ∃ v ∈ B, f = h.dual_elem v := begin split; intro H; rcases H with ⟨v, hv, H⟩, { use [v,hv], apply h.ext, intros w hw, erw [constr_basis _ hw], split_ifs with hwv, { rw hwv, exact H.1 }, { apply H.2 w hw hwv, } }, { rw H, apply h.dual_elem_mem v hv } end lemma dual_elem_eq_repr (v ∈ B) (w : V) : pairing (h.dual_elem v) w = h.repr w v := _ def to_dual : V →ₗ[K] module.dual K V := h.constr$ λ v, h.dual_elem v

lemma to_dual_ker : h.to_dual.ker = ⊥ :=
begin
ext v,
split,
{ rw [mem_ker, mem_bot],
intro hv,
sorry },
{ rw mem_bot, intro h, simp [h], }
end

-- lemma lc_dual_elem (l : lc K (module.dual K V))
-- (hl : ∀ (f : module.dual K V), f ∉ h.dual → l f = 0)
-- (v : V) (hv : v ∈ B) :
--   l (h.dual_elem v hv) = (pairing K V).to_fun
--     ((lc.total K (module.dual K V)).to_fun l) v :=
-- begin
--   have := lc.total_apply l,
--   change ((lc.total K (module.dual K V)).to_fun l) = _ at this,
--   erw this, clear this,
--   erw finsupp.apply_sum,
--   revert hl,
--   apply finsupp.induction l,
--   { intro hl,
--     rw [finsupp.zero_apply, finsupp.sum_zero_index],
--     symmetry,
--     apply zero_apply v, },
--   { intros f k l' _ _ IH hl',
--         finsupp.sum_single_index],
--     { congr' 1,
--       by_cases H : f ∈ h.dual,
--         { rw [finsupp.single_apply, smul_apply],
--           split_ifs with hf,
--           { rw [hf, dual_elem, constr_basis _ hv], simp, },
--           sorry },
--         {  }
--        } } }
-- end

lemma dual_is_basis (B : set V) (h : is_basis K B) (hfin : dim K V < omega) :
is_basis K (h.dual) :=
begin
split,
{ sorry },
-- { rw [linear_independent_iff],
--   intros l hl H,
--   ext f,
--   by_cases hf : f ∈ h.dual,
--   { rw lc.total_apply at H,
--     rw mem_dual_iff at hf,
--     rcases hf with ⟨v, hv, hf⟩,
--     rw hf,
--     sorry },
--   { rw [lc.mem_supported'] at hl,
--     apply hl f hf, } },
{ apply le_antisymm,
{ simp },
{ intros x hx,

sorry } }
end

end is_basis

lemma eval_ker : (eval K V).ker = ⊥ :=
begin
ext,
split,
{ rw [mem_ker, mem_bot],
intro h,
sorry },
{ rw mem_bot, intro h, simp [h], }
end

end


#### Patrick Massot (Feb 28 2019 at 16:03):

Indeed there are too many sets in this story

#### Johan Commelin (Feb 28 2019 at 16:16):

By the way, today's xkcd is also about depressing elementary topics: https://xkcd.com/2117/
Maybe this can cheer us up a bit...

#### Mario Carneiro (Feb 28 2019 at 16:42):

the definition of is_basis.dual is definitely not going to be easy to work with

#### Mario Carneiro (Feb 28 2019 at 16:44):

BTW I think that XKCD is a great example of why decidability matters in mathematics

#### Kevin Buzzard (Feb 28 2019 at 17:07):

Differentiation is a science, integration is an art.

#### Johannes Hölzl (Feb 28 2019 at 17:33):

@Johan Commelin I'm currently preparing a push for the vector space structure of the function space and for finsupp: https://github.com/johoelzl/mathlib/commits/master (specially https://github.com/johoelzl/mathlib/commit/c83c049126030c524cf63e70273635b5d9f26476 and https://github.com/johoelzl/mathlib/commit/592e3c7a2dfbd5826919b4605559d35d4d75938f)

#### Johannes Hölzl (Feb 28 2019 at 17:34):

I don't know if any of this material might help for your proof

#### Johannes Hölzl (Feb 28 2019 at 17:37):

Instead of defining is_basis.dual directly, it might be easier to use the image of dual_elem

#### Johan Commelin (Feb 28 2019 at 17:38):

Hmm, I don't think that's where the problems are... the iff that I prove afterwards let's you move between the two.

#### Johannes Hölzl (Feb 28 2019 at 17:38):

Ah, that's what mem_dual is for

#### Johan Commelin (Feb 28 2019 at 17:39):

It's just that I'm running into many type class errors because it doesn't know how to coerce a linear map into a function. And then I manually add .to_fun and it typechecks, but then all sorts of rw and simp don't trigger. And it's just a pain.

#### Johan Commelin (Feb 28 2019 at 17:40):

It also made me a bit worried about if bundling + coercions is a good idea...

#### Johannes Hölzl (Feb 28 2019 at 17:40):

the coercion into functions worked quiet well for me

#### Johannes Hölzl (Feb 28 2019 at 17:41):

I had more problems with the decidability instance required for finsupp

#### Johan Commelin (Feb 28 2019 at 18:09):

I couldn't apply lc.total _ _ to an l : lc in theorem statements.

#### Johan Commelin (Feb 28 2019 at 18:09):

You can see the hackery in the code dump above.

#### Johan Commelin (Feb 28 2019 at 18:09):

-- lemma lc_dual_elem (l : lc K (module.dual K V))
-- (hl : ∀ (f : module.dual K V), f ∉ h.dual → l f = 0)
-- (v : V) (hv : v ∈ B) :
--   l (h.dual_elem v hv) = (pairing K V).to_fun
--     ((lc.total K (module.dual K V)).to_fun l) v :=
-- begin
--   have := lc.total_apply l,
--   change ((lc.total K (module.dual K V)).to_fun l) = _ at this,
--   erw this, clear this,


#### Johan Commelin (Feb 28 2019 at 18:10):

I have to write ((lc.total K (module.dual K V)).to_fun l

#### Johan Commelin (Feb 28 2019 at 18:10):

And then the first 3 lines of the proof are hackery to get lc.total_apply working.

Last updated: May 10 2021 at 07:15 UTC