## Stream: new members

### Topic: independent columns

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

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

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

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

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

#### Patrick Massot (Dec 22 2020 at 15:27):

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.

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

#### Julian Berman (Dec 22 2020 at 15:38):

Aha... thank you! Will do.

Last updated: May 15 2021 at 00:39 UTC