Zulip Chat Archive

Stream: maths

Topic: linear_independent


view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Feb 28 2019 at 10:56):

@Kenny Lau Any hints?

view this post on Zulip Kenny Lau (Feb 28 2019 at 11:00):

oh no

view this post on Zulip Kenny Lau (Feb 28 2019 at 11:01):

iirc the lemma isn’t there

view this post on Zulip Johannes Hölzl (Feb 28 2019 at 11:35):

There is linear_independent_iffand lc.total is the sum operator

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Feb 28 2019 at 15:24):

Do we have the dual vector space?

view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Feb 28 2019 at 15:27):

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

view this post on Zulip Mario Carneiro (Feb 28 2019 at 15:28):

what's the basis for the dual space?

view this post on Zulip 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

view this post on Zulip Patrick Massot (Feb 28 2019 at 15:28):

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

view this post on Zulip Mario Carneiro (Feb 28 2019 at 15:28):

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

view this post on Zulip Patrick Massot (Feb 28 2019 at 15:28):

no

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Feb 28 2019 at 15:30):

okay. We have that though

view this post on Zulip Mario Carneiro (Feb 28 2019 at 15:30):

I think it's called constr

view this post on Zulip Mario Carneiro (Feb 28 2019 at 15:30):

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

view this post on Zulip Patrick Massot (Feb 28 2019 at 15:31):

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Feb 28 2019 at 15:31):

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

view this post on Zulip Patrick Massot (Feb 28 2019 at 15:32):

yes

view this post on Zulip Patrick Massot (Feb 28 2019 at 15:33):

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

view this post on Zulip 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

view this post on Zulip Patrick Massot (Feb 28 2019 at 15:33):

ooh

view this post on Zulip Patrick Massot (Feb 28 2019 at 15:34):

That would be nice

view this post on Zulip Mario Carneiro (Feb 28 2019 at 15:34):

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

view this post on Zulip Mario Carneiro (Feb 28 2019 at 15:34):

but that's just one proof

view this post on Zulip 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"

view this post on Zulip 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

view this post on Zulip 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:

/-
Copyright (c) 2019 Johan Commelin. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
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',
--     rw [finsupp.add_apply, IH, finsupp.sum_add_index,
--         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

view this post on Zulip Patrick Massot (Feb 28 2019 at 16:03):

Indeed there are too many sets in this story

view this post on Zulip 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...

view this post on Zulip Mario Carneiro (Feb 28 2019 at 16:42):

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

view this post on Zulip Mario Carneiro (Feb 28 2019 at 16:44):

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

view this post on Zulip Kevin Buzzard (Feb 28 2019 at 17:07):

Differentiation is a science, integration is an art.

view this post on Zulip 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)

view this post on Zulip Johannes Hölzl (Feb 28 2019 at 17:34):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Johannes Hölzl (Feb 28 2019 at 17:38):

Ah, that's what mem_dual is for

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Feb 28 2019 at 17:40):

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

view this post on Zulip Johannes Hölzl (Feb 28 2019 at 17:40):

the coercion into functions worked quiet well for me

view this post on Zulip Johannes Hölzl (Feb 28 2019 at 17:41):

I had more problems with the decidability instance required for finsupp

view this post on Zulip Johan Commelin (Feb 28 2019 at 18:09):

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

view this post on Zulip Johan Commelin (Feb 28 2019 at 18:09):

You can see the hackery in the code dump above.

view this post on Zulip 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,

view this post on Zulip Johan Commelin (Feb 28 2019 at 18:10):

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

view this post on Zulip 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