Riesz extension thm

Stream: general

[Yury G. Kudryashov]

Hi, I'm trying to formalize M. Riesz extension theorem, and I have a few questions, see #2120

[Yury G. Kudryashov]

Two of them should probably go to #maths but Q3 "Why elaboration of the step takes so long?" probably should go here.

[Johan Commelin]

I will also ask a question about Q1 here... what do you mean with it? :wink:
Do you want to replace the sorry with a proof, or do you want to add it as an assumption somehow?

[Yury G. Kudryashov]

This sorry says that if you have a vector subspace p, a vector x ∉ p, a linear map f : s → V, and y : V, then you can extend f to linear a linear map s ⊔ span {x} → V such that f x = y.

[Yury G. Kudryashov]

Yes, I want to prove it.

[Yury G. Kudryashov]

I should've formulated this sorry in Q1.

[Patrick Massot]

We should probably resurrect the Hahn-Banach thread.

[Yury G. Kudryashov]

We had a Hahn-Banach thread?

[Mario Carneiro]

what's the problem? It seems llike you've stated the theorem just fine.

[Mario Carneiro]

(for Q1)

[Patrick Massot]

https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Hahn-Banach

[Patrick Massot]

It's a very short thread, you should read it entirely

[Yury G. Kudryashov]

I did hope that someone with a better knowledge of linear_algebra/ directory will point me to a helpful lemma.

[Mario Carneiro]

Oh I see, you want the Q to already have a solution in mathlib

[Mario Carneiro]

I think constr may do something similar to this

[Yury G. Kudryashov]

@Patrick Massot I read the thread. I'll try to read the gist tomorrow.

[Patrick Massot]

It would be nice to have Hahn-Banach in mathlib as well. I'm not saying we should use this proof, which was mostly a SSReflect translation experiment, but we should have some proof.

[Yury G. Kudryashov]

I was going to follow https://en.wikipedia.org/wiki/M._Riesz_extension_theorem both for M. Riesz extension theorem and Hahn-Banach theorem.

[Patrick Massot]

Sure, they are very much related, that's why I pointed out my old Hahn-Banach work.

[Patrick Massot]

Because the extension and induction work is the main part of Marie's work.

[Kevin Buzzard]

For the vector space lemma, could one make the following definition: if M,N are R-modules and V,W are submodules of M, and you have R-linear maps V -> N and W -> N which agree on V intersect W then you can get a map from V \lub W to N. Maybe computer scientists have a name for this map? And then you show that it agrees with the given maps on V and W. You could first define a map from $V\oplus W$ to N by adding, and then show that $V\cap W$ embedded anti-diagonally is the kernel of the surjection to V \lub W. This seems like the sort of lemma which should be in mathlib.

[Yury G. Kudryashov]

@Kevin Buzzard I made it only for the case of empty intersection. I'll see if I can generalize it.

[Yury G. Kudryashov]

BTW, the proof works now (at least it worked before merging master).

[Kevin Buzzard]

Nice! It's good to see maths I remember from UG appearing in Lean