Zulip Chat Archive

Stream: general

Topic: Riesz extension thm


Yury G. Kudryashov (Mar 10 2020 at 03:15):

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

Yury G. Kudryashov (Mar 10 2020 at 03:16):

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

Johan Commelin (Mar 11 2020 at 07:34):

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 (Mar 11 2020 at 07:44):

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 (Mar 11 2020 at 07:44):

Yes, I want to prove it.

Yury G. Kudryashov (Mar 11 2020 at 07:44):

I should've formulated this sorry in Q1.

Patrick Massot (Mar 11 2020 at 07:48):

We should probably resurrect the Hahn-Banach thread.

Yury G. Kudryashov (Mar 11 2020 at 07:49):

We had a Hahn-Banach thread?

Mario Carneiro (Mar 11 2020 at 07:49):

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

Mario Carneiro (Mar 11 2020 at 07:49):

(for Q1)

Patrick Massot (Mar 11 2020 at 07:49):

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

Patrick Massot (Mar 11 2020 at 07:50):

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

Yury G. Kudryashov (Mar 11 2020 at 07:50):

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

Mario Carneiro (Mar 11 2020 at 07:51):

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

Mario Carneiro (Mar 11 2020 at 07:51):

I think constr may do something similar to this

Yury G. Kudryashov (Mar 11 2020 at 07:55):

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

Patrick Massot (Mar 11 2020 at 07:56):

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 (Mar 11 2020 at 08:01):

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 (Mar 11 2020 at 08:02):

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

Patrick Massot (Mar 11 2020 at 08:02):

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

Kevin Buzzard (Mar 11 2020 at 09:37):

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 VWV\oplus W to N by adding, and then show that VWV\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 (Mar 19 2020 at 19:09):

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

Yury G. Kudryashov (Mar 19 2020 at 19:10):

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

Kevin Buzzard (Mar 19 2020 at 19:10):

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


Last updated: Dec 20 2023 at 11:08 UTC