linear independent

Stream: new members

[Alena Gusakov]

Hi all,
This might be a little bit of a dumb question but I'm trying to understand the design of linear_independent and how to use it. I'm trying to use some of the existing lemmas for matroid proofs, but I keep tripping up on the two different ways that a set of vectors can be expressed and I'm not really sure which to use, how to go between them, etc. More specifically, I'm trying to talk about the image of a function $\phi : E \rightarrow (ι → 𝔽)$ that maps into a set of vectors, and we have

linear_independent 𝔽 (coe : (φ '' X) → (ι → 𝔽))

but also we can express it like

linear_independent 𝔽 (λ (e : X), φ (e : E))

For example, I want to use

lemma finrank_span_set_eq_card (s : set V) [fintype s]
  (hs : linear_independent K (coe : s → V)) :
  finrank K (span K s) = s.to_finset.card

which clearly uses the coe expression.

[Johan Commelin]

@Alena Gusakov can you say a bit more about what X is?

[Alena Gusakov]

Johan Commelin said:

Alena Gusakov can you say a bit more about what X is?

Sure! X is just an arbitrary set E, where E is just a type for now (in our case it's the ground set of the matroid but I don't think that is necessary to know)

[Johan Commelin]

Is it important that X is a set E? Or is it useful to think about X as an "indexed family of elements of E"?

[Alena Gusakov]

I suppose you could view it as an indexed family of elements, but in the definition I have it as a set currently, I can provide an MWE if that helps!

[Johan Commelin]

If you can explain in a words a bit of the background that might also help. What is the intuitive meaning/role of X?

[Johan Commelin]

Is it supposed to be a basis? Or a random set? Where does it come from? How is it used?

[Yaël Dillies]

I think docs#linear_independent.image_of_comp is one direction.

[Alena Gusakov]

Johan Commelin said:

Is it supposed to be a basis? Or a random set? Where does it come from? How is it used?

So X is an arbitrary set of elements in a representable matroid, through which I'm trying to write some helper lemmas about the relationship between independence of a set in a matroid and linear independence of its representation. I.e. if a set X is independent in matroid E, then when you take its representation over some field $\mathbb{F}$ (which will be a set of vectors in some vector space over $\mathbb{F}$) you get a linearly independent set, and if it's not independent then the representation will not be linearly independent.

[Yaël Dillies]

For future reference, the lemma Alena was looking for is docs#linear_independent_image