Zulip Chat Archive

Stream: maths

Topic: Define linear function from matrix


view this post on Zulip Abhimanyu Pallavi Sudhir (Nov 14 2019 at 17:23):

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.

view this post on Zulip Abhimanyu Pallavi Sudhir (Nov 14 2019 at 17:27):

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

view this post on Zulip Abhimanyu Pallavi Sudhir (Nov 14 2019 at 17:28):

Oh I guess it's to_lin.

view this post on Zulip Abhimanyu Pallavi Sudhir (Nov 14 2019 at 17:29):

Or eval.

view this post on Zulip Kevin Buzzard (Nov 14 2019 at 17:31):

The linear transformation on what? Their span?

view this post on Zulip Kevin Buzzard (Nov 14 2019 at 17:31):

PS are you in the same room as me?

view this post on Zulip Abhimanyu Pallavi Sudhir (Nov 14 2019 at 17:32):

Yes.

view this post on Zulip Abhimanyu Pallavi Sudhir (Nov 14 2019 at 17:32):

And yes.

view this post on Zulip Abhimanyu Pallavi Sudhir (Nov 14 2019 at 17:41):

Apparently matrices don't work.

view this post on Zulip Abhimanyu Pallavi Sudhir (Nov 14 2019 at 17:42):

Because they're finite.

view this post on Zulip Abhimanyu Pallavi Sudhir (Nov 14 2019 at 17:43):

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.

view this post on Zulip Mario Carneiro (Nov 14 2019 at 17:45):

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

view this post on Zulip Abhimanyu Pallavi Sudhir (Nov 14 2019 at 17:48):

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.

view this post on Zulip Mario Carneiro (Nov 14 2019 at 17:49):

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

view this post on Zulip Abhimanyu Pallavi Sudhir (Nov 14 2019 at 17:49):

It's the vector space.

view this post on Zulip Abhimanyu Pallavi Sudhir (Nov 14 2019 at 17:49):

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

view this post on Zulip Abhimanyu Pallavi Sudhir (Nov 14 2019 at 17:50):

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

view this post on Zulip Mario Carneiro (Nov 14 2019 at 17:50):

what map? you only have a submodule

view this post on Zulip Abhimanyu Pallavi Sudhir (Nov 14 2019 at 17:50):

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

view this post on Zulip Johan Commelin (Nov 14 2019 at 17:54):

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

view this post on Zulip Johan Commelin (Nov 14 2019 at 17:54):

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

view this post on Zulip Johan Commelin (Nov 14 2019 at 17:54):

And you have a proof that they are linearly independent.

view this post on Zulip Johan Commelin (Nov 14 2019 at 17:54):

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

view this post on Zulip Johan Commelin (Nov 14 2019 at 17:55):

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

view this post on Zulip Johan Commelin (Nov 14 2019 at 17:56):

Is that correct?

view this post on Zulip Abhimanyu Pallavi Sudhir (Nov 14 2019 at 17:56):

Yes.

view this post on Zulip Abhimanyu Pallavi Sudhir (Nov 14 2019 at 17:56):

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

view this post on Zulip Abhimanyu Pallavi Sudhir (Nov 14 2019 at 17:56):

I'm having a look at it.

view this post on Zulip Johan Commelin (Nov 14 2019 at 17:56):

I think that's right


Last updated: May 12 2021 at 08:14 UTC