## Stream: new members

### Topic: linear independent

#### Alena Gusakov (Apr 04 2023 at 17:17):

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 (Apr 04 2023 at 17:25):

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

#### Alena Gusakov (Apr 04 2023 at 17:26):

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 (Apr 04 2023 at 17:27):

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 (Apr 04 2023 at 17:29):

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 (Apr 04 2023 at 17:30):

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 (Apr 04 2023 at 17:31):

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

#### Yaël Dillies (Apr 04 2023 at 17:33):

I think docs#linear_independent.image_of_comp is one direction.

#### Alena Gusakov (Apr 04 2023 at 17:33):

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 (Apr 09 2023 at 10:23):

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

Last updated: Dec 20 2023 at 11:08 UTC