Zulip Chat Archive

Stream: new members

Topic: independent columns


view this post on Zulip Julian Berman (Dec 22 2020 at 04:18):

Is there something like set which gives all families rather than sets? Context is:

  import data.matrix.notation
  import linear_algebra.linear_independent

  def A : matrix _ _  := ![
    ![1, 0, 0, 1, 0, 0, 0],
    ![0, 1, 0, 1, 1, 1, 0],
    ![0, 0, 1, 0, 1, 1, 0]
  ]

  def I := {x : set (fin 7) // linear_independent (fin 3  ) (λ i : x, A.transpose i)}

-- which I don't know is correct yet, I'm trying to say a type of "all collections of indices whose columns in A are linearly independent", but I see linearly_independent is telling me to start with families rather than sets if I can, so is there a thing that given fin 7 will give me all of those maps directly, or am I doing that the way that's expected? (Including whether transposing is the way I'm supposed to pull off columns?)

view this post on Zulip Johan Commelin (Dec 22 2020 at 06:04):

@Julian Berman The code compiles, right?
I think you want to replace (fin 3 → ℚ) with , because you presumably want the columns to be linearly independent over the rationals. Otherwise, this seems like the way to go, to me.

view this post on Zulip Julian Berman (Dec 22 2020 at 06:24):

ah of course -- thanks. It does indeed compile, I just wasn't sure (besides whether it was idiomatic) if that was the right type (e.g. I couldn't yet prove that column 7 isn't in any set despite finding linear_independent.ne_zero -- probably I'm close though, will give it another shot in the morning, thanks for the confirmation!.

view this post on Zulip Julian Berman (Dec 22 2020 at 14:43):

OK managed to get a little bit closer but I think my issue is struggling a bit to prove things about a subtype (or perhaps I'm confused about how to pull an element out of the set there)...

I'm not sure how to proceed from:

  example :  i : I, (6 : fin 7)  i.val := begin
    intro i,
    have h := linear_independent.ne_zero i.property,
    /-
    2 goals
    i : I,
    h : (λ (i_1 : ↥(i.val)), A.transpose ↑i_1) ?m_1 ≠ 0
    ⊢ 6 ∉ i.val

    i : I
    ⊢ ↥(i.val)
    -/
end

I need to basically pass 6 into h right? Is that what specialize is for?

view this post on Zulip Patrick Massot (Dec 22 2020 at 15:26):

The main source of trouble here is a bad implicit argument on docs#linear_independent.ne_zero.

view this post on Zulip Patrick Massot (Dec 22 2020 at 15:27):

You should start with:

import data.matrix.notation
import linear_algebra.linear_independent

def A : matrix _ _  := ![
  ![1, 0, 0, 1, 0, 0, 0],
  ![0, 1, 0, 1, 1, 1, 0],
  ![0, 0, 1, 0, 1, 1, 0]
]

def I := {x : set (fin 7) // linear_independent (fin 3  ) (λ i : x, A.transpose i)}

lemma linear_independent.ne_zero' {ι R M: Type*} {v : ι  M} [ring R] [add_comm_group M]
  [module R M] [nontrivial R] (i : ι) (h : linear_independent R v) : v i  0 :=
h.ne_zero

example :  i : I, (6 : fin 7)  i.val := begin
  intros i H,
  apply i.property.ne_zero' (⟨6, H : i.val),
  dsimp only,

end

And then open a PR fixing that broken binder.

view this post on Zulip Patrick Massot (Dec 22 2020 at 15:28):

The difference between linear_independent.ne_zero' and linear_independent.ne_zero is the i argument is explicit.

view this post on Zulip Julian Berman (Dec 22 2020 at 15:38):

Aha... thank you! Will do.


Last updated: May 15 2021 at 00:39 UTC