independent columns

Stream: new members

[Julian Berman]

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]

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

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]

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]

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

[Patrick Massot]

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.

[Patrick Massot]

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

[Julian Berman]

Aha... thank you! Will do.