Hahn-Banach corollaries

Stream: general

[Ruben Van de Velde]

Hahn-Banach is now proved over $\R$ and $\mathbb C$, and a couple of corollaries over $\R$. I verified that the proofs work just as well over $\mathbb C$, but I imagine it wouldn't be desirable to copy/paste everything - how'd I approach generalizing them?

[Heather Macbeth]

I thought about this briefly, but am (very) glad that someone else is doing it!

[Heather Macbeth]

I think it's not clear whether it would be more efficient to (A) deduce those $\mathbb{C}$-corollaries from the $\mathbb{R}$-versions of the corollaries of $\mathbb{R}$-Hahn-Banach, or (B) deduce them from your $\mathbb{C}$-version of Hahn-Banach

[Heather Macbeth]

What do you think?

[Heather Macbeth]

By the way, something I was wondering is whether part of the work can be done for any extension field of $\mathbb{R}$, and not just for $\mathbb{C}$?

[Heather Macbeth]

Also -- could you also carry out over $\mathbb{C}$ the isometric inclusion of a normed space in its double dual? That is the motivation for the corollaries.

[Kevin Buzzard]

In the Langlands program we sometimes work over R-bar, an algebraic closure of R with no fixed choice of sqrt (-1)

[Jalex Stark]

what is this object?

[Johan Commelin]

Just complex but without choosing I

[Jalex Stark]

what does "choose" mean?

[Johan Commelin]

complex has a distinguished generator, or equivalently orientation, by it's construction

[Johan Commelin]

Somehow I is a bit more special than -I

[Johan Commelin]

Kevin is talking about a version where you cannot call one of them more special than the other.

[Jalex Stark]

gotcha

[Kevin Buzzard]

The two square roots of -1 just don't have names, in some sense they are indistinguishable

[Jalex Stark]

the whole theory is modded out by swapping the square roots

[Jalex Stark]

so geometrically it's like a halfspace?

[Kevin Buzzard]

It's isomorphic to C but in two ways

[Kevin Buzzard]

The roots are distinct but nobody chose one to make it special

[Kevin Buzzard]

When you're arguing functorially it's sometimes important

[Kevin Buzzard]

Or perhaps psychologically useful, I'm not sure

[Jalex Stark]

i am happy to believe that even though i can't fill in the details

[Kevin Buzzard]

You can imagine a category with two objects and an isomorphism between them

[Kevin Buzzard]

And then you make a diagram with a copy of the complex numbers on each object and make the isomorphism be complex conjugation and then you take the limit of the diagram

[Scott Morrison]

(and then carefully erase from your memory the "names" of the two objects in that category that you had to give them when you summoned them from the void...)

[Ruben Van de Velde]

Heather Macbeth said:

I think it's not clear whether it would be more efficient to (A) deduce those $\mathbb{C}$-corollaries from the $\mathbb{R}$-versions of the corollaries of $\mathbb{R}$-Hahn-Banach, or (B) deduce them from your $\mathbb{C}$-version of Hahn-Banach

(B) seems easier; just replacing $\R \to \mathbb C$ in the proofs works out fine. Wondering how to do it without copy/pasting though; I'm guessing defining some sort of "Hahn-Banach holds over this field" property?

Heather Macbeth said:

By the way, something I was wondering is whether part of the work can be done for any extension field of $\mathbb{R}$, and not just for $\mathbb{C}$?

No idea :)

Heather Macbeth said:

Also -- could you also carry out over $\mathbb{C}$ the isometric inclusion of a normed space in its double dual? That is the motivation for the corollaries.

Something in this direction? (Pretty rough proof - I've only convinced Lean it's true, not understood it.)

[Ruben Van de Velde]

Kevin Buzzard said:

In the Langlands program we sometimes work over R-bar, an algebraic closure of R with no fixed choice of sqrt (-1)

Is there anything in mathlib about this?

[Kevin Buzzard]

Mathlib only has C. Once it has algebraic closures one will be able to prove things about R-bar though. But R-bar and C are isomorphic, it's not a mysterious new object, it's just a different way of thinking about an old object. It's like comparing an n-dimensional vector space with R^n. Sometimes the different point of view can help. It might just be psychological. Whenever I see an R-bar I can choose an isomorphism with C. Sometimes it's best not to though, like sometimes you don't need to choose a basis of V.

[Ruben Van de Velde]

Oh, @Heather Macbeth I didn't notice you'd already done the inclusion in the double dual in dual.lean; will take a look at some point

[Heather Macbeth]

But not over $\mathbb{C}$, so you should add that!

[Heather Macbeth]

Ruben Van de Velde said:

Wondering how to do it without copy/pasting though; I'm guessing defining some sort of "Hahn-Banach holds over this field" property?

Having looked at your branch and seen how directly the proofs adapt, this seems like the right answer!

[Heather Macbeth]

Ruben Van de Velde said:

Heather Macbeth said:

By the way, something I was wondering is whether part of the work can be done for any extension field of $\mathbb{R}$, and not just for $\mathbb{C}$?

No idea :)

But the point I am making here is that maybe we already have a "Hahn-Banach holds over this field" property, and that property is "is a (finite?) extension field of $\mathbb{R}$".

[Heather Macbeth]

or (perhaps easier given the available lemmas) "is a (finite?) algebra over $\mathbb{R}$". By the way, @Yury G. Kudryashov , have you seen this discussion?