Define linear function from matrix

Stream: maths

[Abhimanyu Pallavi Sudhir]

How can I construct in Lean the linear transformation (as a function) given by an (infinite) set of vectors (in ℕ → ℝ), a proof that they are linearly independent, and their images?

On the subtype of ℕ → ℝ that is their span, of course.

[Abhimanyu Pallavi Sudhir]

I'm not very familiar with the linear_algebra in mathlib.

[Abhimanyu Pallavi Sudhir]

Oh I guess it's to_lin.

[Abhimanyu Pallavi Sudhir]

Or eval.

[Kevin Buzzard]

The linear transformation on what? Their span?

[Kevin Buzzard]

PS are you in the same room as me?

[Abhimanyu Pallavi Sudhir]

Yes.

[Abhimanyu Pallavi Sudhir]

And yes.

[Abhimanyu Pallavi Sudhir]

Apparently matrices don't work.

[Abhimanyu Pallavi Sudhir]

Because they're finite.

[Abhimanyu Pallavi Sudhir]

At least there must be a way to define a linear map from basis elements even if we were defining it on the entire space and not a subspace.

[Mario Carneiro]

The setup confuses me. What is the type of the input and output?

[Abhimanyu Pallavi Sudhir]

The type of the input is a submodule of ℕ → ℝ (given as the span of a set). The type of the output is ℝ as a module.

[Mario Carneiro]

is ℕ → ℝ the vector space or is it a countable family over ℝ?

[Abhimanyu Pallavi Sudhir]

It's the vector space.

[Abhimanyu Pallavi Sudhir]

But the map is defined only on a subtype of it.

[Abhimanyu Pallavi Sudhir]

The set of vectors is something like 1/(n+m) : m \in \nat

[Mario Carneiro]

what map? you only have a submodule

[Abhimanyu Pallavi Sudhir]

Right, but I can make it a subtype and it would still be a module.

[Johan Commelin]

@Abhimanyu Pallavi Sudhir If I understand you correctly, you don't really care about the vector space

[Johan Commelin]

So you have some family v : \iota → V of vectors

[Johan Commelin]

And you have a proof that they are linearly independent.

[Johan Commelin]

And you have a family f : \iota → W of "images"

[Johan Commelin]

And now you want the map from the span of the v i to W, that maps v i to f i.

[Johan Commelin]

Is that correct?

[Abhimanyu Pallavi Sudhir]

Yes.

[Abhimanyu Pallavi Sudhir]

Chris tells me linear_independent.repr is what I'm looking for.

[Abhimanyu Pallavi Sudhir]

I'm having a look at it.

[Johan Commelin]

I think that's right