closed graph theorem

Stream: Is there code for X?

[Cameron Torrance]

is there proof that a linear map between two banach space is continuous iff its graph is closed (or some generalisation) ?

[Scott Morrison]

Not yet.

[Anatole Dedecker]

But we do have the Banach isomorphism theorem, so it should be pretty straightforward

[Kevin Buzzard]

I hope that the p-adic version is included because this is fundamental for nonarchimedean analysis. The only reference I know for the p-adic case is Bourbaki -- even Bosch-Guentzer-Remmert refer the reader to Bourbaki and it's essentially the only place where the book is not self-contained (unless you count references to exotic counterexamples which are not needed in the main arguments but which clarify what implies what).

[Anatole Dedecker]

Wait is there a version that does not work with p-adics ?

[Kevin Buzzard]

Sure, the version where you start "let V be a Banach space over the reals or complexes. Then...". For many people, Banach space := Banach space over the reals or complexes. I have a fear of is_R_or_C. Where is is_R_or_C_or_p-adic? ;-)

[Jireh Loreaux]

Is there a case where you really want one of those three? I mean, most of the time don't you just want nondiscrete_normed_field and complete_space?

[Damiano Testa]

is_R_or_C_or_p-adic or is_R_or_p-adic are precisely the possibilities for the completions of a number field. There is a statement where you really want one of those three (or two)! :stuck_out_tongue_wink:

[Anatole Dedecker]

Cameron Torrance said:

is there proof that a linear map between two banach space is continuous iff its graph is closed (or some generalisation) ?

Do you want to add it or do you need it ? I can make a PR quickly if you want, we have all the necessary ingredients

[Cameron Torrance]

Anatole Dedecker said:

Cameron Torrance said:

is there proof that a linear map between two banach space is continuous iff its graph is closed (or some generalisation) ?

Do you want to add it or do you need it ? I can make a PR quickly if you want, we have all the necessary ingredients

Just needed it

[Anatole Dedecker]

Ok, I'll make a PR then !

[Kevin Buzzard]

@Jireh Loreaux the story in arithmetic is that we're all agreed that $\mathbb{Q}$ and $\mathbb{Q}(i)$ are global fields, and we think we want the completions of global fields to be local fields, but we don't really know what a local field is! The reals and complexes, or, more precisely, normed fields which are isomorphic to the complexes (sometimes we don't know which way is up) are sometimes called local fields or archimedean local fields, but some authors use local field to mean nonarchimedean local field. Some proofs really do really on the nonarchimedean property of the norm. And then there's the issue that some people allow nonarch local fields with infinite residue field and others don't, depending on whether they're doing something geometric (where it often doesn't matter) or arithmetic (where it can be crucial). Langlands goes out of his way to make "unified" statements whenever he can, including the reals, p-adics, and characteristic p local fields, and their finite extensions, but often in the proofs you split into cases depending on whether the norm is nonarchimedean or not. It's a bit of a mess :-/ In nonarchimedean analysis we care much less about finiteness of residue field and then the situation is much closer to what you describe, typically you just need completeness and the existence of an element of norm strictly between 0 and 1 so you can scale. The open mapping theorem comes under that category because it's analytic rather than arithmetic.

[Jireh Loreaux]

@Kevin Buzzard Thanks for that description! That's the other side of the mathematical world for me (at least from my limited perspective), so it's good to learn a bit about what matters and why.

[Anatole Dedecker]

#14265

[Anatole Dedecker]

The main theorem in this PR (linear_map.continuous_of_is_closed_graph) is quite slow to compile, and I can't understand why (heavy rfl maybe ?) so if anyone wants to have a look that would be great