worries about `is_R_or_C`

Stream: maths

[Kevin Buzzard]

I've moaned about this to several people both online and offline but let me try and get my thoughts straight about what concerns me with is_R_or_C. Maybe I'm worrying about nothing. tl;dr: putting an is_R_or_C structure on a field is losing information which is sometimes (but not always) important.

In the Langlands Philosophy is sometimes said to relate algebra to analysis, although of course this is over-selling it: it only relates some part of algebra to some part of analysis. On the analysis side, at least in the classical Langlands philosophy, one is considering representations of things like real Lie groups (objects with reasonable finiteness properties) on things like Hilbert spaces (typically infinite-dimensional). On the algebra side, one is considering representations of things like Galois groups (typically infinite and wild) on finite-dimensional spaces (e.g. cohomology groups).

The story started off with class field theory, which was developed over 100 years ago. Back then the Galois groups showing up were the absolute Galois group of a number field $K$, i.e. $\mathrm{Gal}(\overline{K}/K)$, where $K=\mathbb{Q}$ or a finite extension such as $\mathbb{Q}(i)$. Later on the $p$-adic numbers were discovered, and people found that the proofs could be simplified if you developed a theory for $K$ a completion of a number field with respect to a nontrivial valuation first (similarly to how you first prove theorems about $\mathbb{R}^n$ and then about manifolds). The Langlands philosophy has as input not just a local or global field $K$ but also an algebraic group $G$ defined over $K$, and re-interprets class field theory as "the Langlands philosophy for $GL_1$".

In mathematics we've learnt over the years not to break symmetry if we don't have to, e.g.150 years ago people were studying matrices but now we study linear maps, because we can develop the theory of linear algebra without having to pick a basis. If $K$ is an abstract number field, such as the field $\mathbb{Q}[X]/(X^3-2)$ obtained by adjoining a cube root of 2 to the rationals, then $K$ will have lots of $p$-adic completions but it also has two archimedean completions, coming from the following two norms on $K$: the first comes from embedding $K$ into $\mathbb{R}$ by sending this abstract cube root of 2 to the real $2^{1/3}$ and then applying the usual norm on $\mathbb{R}$, and the second embeds $K$ in $\mathbb{C}$ by sending the abstract cube root of 2 to either one of the complex non-real cube roots of 2 and then uses the usual norm on $\mathbb{C}$. Note that because $|z|=|\overline{z}|$ it doesn't matter which complex cube root we choose. A general number field can be written as $\mathbb{Q}[X]/(f(X))$ where $f\in\mathbb{Q}[X]$ is irreducible, and the number of archimedean completions of $K$ is equal to the number of irreducible factors of $f$ considered as a polynomial in $\mathbb{R}[X]$, with the degree 1 factors giving "real completions" of $K$, all isomorphic to $\mathbb{R}$, and the degree 2 factors giving these completions which are isomorphic to the complexes. Note however that the completion of a number field at a complex place is not "equal" to $\mathbb{C}$, it is merely a field containing a copy of the reals and having degree 2 over that field; it does not contain a canonical square root of $-1$. Because we're interested in the Langlands philosophy for number fields, and we want to study number fields by studying them locally, we see that when one is setting up the local theory it might be wise to take this into account and to develop some parts of mathematics for this field which I call $\overline{\mathbb{R}}$, an algebraic closure of the reals with two square roots of $-1$ which in some sense are indistinguishable. Fixing an isomorphism of a complex completion of a number field with $\mathbb{C}$ is just like picking a basis -- historically popular, but often not necessary, and indeed it even impedes development of some parts of the theory because it's not a natural thing to do so it can cause some noise when one is attempting to do "functorial" things.

(1/3: Zulip doesn't like posts this long)

[Kevin Buzzard]

Conversely, when one is considering representations of groups like $GL_n(\overline{\mathbb{R}})$ on Hilbert spaces, here it is absolutely essential that the Hilbert spaces are over $\mathbb{C}$! This is a "different" $\mathbb{C}$ in the theory, it's not a completion of a number field, it's some fixed choice of the complex numbers over which we're going to do some representation theory.

Even the most trivial example shows up the difference. If $K$ is a field like $\mathbb{Q}[X](X^2+X+1)$, with complex completion $\overline{\mathbb{R}}$, then on the analysis side of the $GL_1$ case of the Langlands program one wants to consider irreducible complex representations of $\overline{\mathbb{R}}^\times$ and these things will all be one-dimensional, so they correspond to continuous (and hence $C^\infty$) group homomorphisms $\overline{\mathbb{R}}^\times\to\mathbb{C}^\times$. If you've (non-canonically) identified $\overline{\mathbb{R}}$ with $\mathbb{C}$ then you're developing the theory of continuous group homomorphisms $\mathbb{C}^\times\to\mathbb{C}^\times$ and there's an "obvious" such homomorphism, namely the identity function. But this "obvious" homomorphism does not play a special role in the theory, indeed it only looks obvious because one has "picked a basis" and is now being led astray. The morphism which plays a special role in the theory is the norm representation sending $z$ to $z\overline{z}$. Note that this makes sense as a representation of $\overline{\mathbb{R}}^\times$, as complex conjugation is still a thing on $\overline{\mathbb{R}}$: it's the unique non-trivial element of the Galois group $\mathrm{Gal}(\overline{\mathbb{R}}/\mathbb{R})$.

Earlier in my life I spent quite some time unravelling work of other people who were interested in the archimedean local part of the Langlands philosophy and would stick to groups like $GL_n(\mathbb{R})$ and $GL_n(\mathbb{C})$, because they would typically not deal with $GL_n(\overline{\mathbb{R}})$ so one would have to stare at their results and then extract the (often more beautiful) results about $GL_n(\overline{\mathbb{R}})$ from them. This was not always easy. In contrast, in Langlands' original work on representations of real reductive groups he was sometimes careful not to make this choice, and would happily work with $\overline{\mathbb{R}}$. Now mathlib prides itself on working in the "correct generality". As I've said, sometimes is_R_or_C, the typeclass which chooses an isomorphism of a field $k$ with $\mathbb{R}$ or $\mathbb{C}$ (and is in particular data) is definitely sometimes the right thing to do (e.g. when setting up the theory of Hilbert spaces). However it is definitely not always the right thing to do; sometimes one needs a proposition saying "this normed field is a completion of a number field", which could be represented as a Prop-valued is_R_or_Rbar; there are several ways of formalising the concept (e.g. one cheap way would be "I am isomorphic to either $\mathbb{R}$ or $\mathbb{C}$" but there are many others, e.g. "my norm is archimedean and I'm complete with respect to it", where an archimedean norm is defined to be a norm which is not non-archimedean).

(2/3)

[Kevin Buzzard]

What we lose by picking a basis is a far more conceptual way of handling the way that complex conjugation interacts with the theory. One can make constructions associated to a complete archimedean normed field $k$ and then translate these constructions along isomorphisms. If $k$ comes with an [is_R_or_Rbar k] typeclass then there are more isomorphisms from $k$ to $k$ which preserve this typeclass than if it comes with an [is_R_or_C k] typeclass; putting this typeclass on your field early means that there is now the question "how does your construction behave under complex conjugation?" and this now might be some horrible calculation involving finding all the API for how complex conjugation commutes with all the sub-constructions. Langlands argues that this little extra piece of data is sometimes really worth tracking, and picking a basis (by which I mean picking a square root of $-1$) makes this data harder to track. Furthermore the fact that is_R_or_C is a typeclass is very strange to me, because in the fields showing up in this part of mathematics there really isn't just one is_R_or_C structure on e.g. $\mathbb{Q}[X]/(X^2+X+1)\otimes_{\mathbb{Q}}\mathbb{R}$, there are two, and I don't really want to choose either of them.

(3/3)

[Oliver Nash]

Is it fair to say that the real worry is that somebody might start writing lemmas about archimedean completions of number fields using is_R_or_C?

[Kevin Buzzard]

In some sense it's even earlier than that -- I'm worried that people might start writing lemmas about $GL_n(k)$ or $M_n(k)$ with is_R_or_C k. Langlands eats a local or global field, and a (connected reductive) affine algebraic group defined over that field, e.g. GL_n. That's one part of the worry. The other part of the worry is that we're losing information, namely how complex conjugation acts on everything. For example if [is_R_or_C k] and $M\in GL_n(k)$ you can prove that $\overline{det(M)}=det(\overline{M})$ but this statement looks like it needs a proof. With is_R_or_Rbar you can deduce it from the fact that determinant commutes with isomorphisms, but the isomorphism in question doesn't preserve the is_R_or_C structure, and this worries me a bit.

[Filippo A. E. Nuccio]

FWIW, when discussing how to set-up Local CFT with @María Inés de Frutos Fernández we agreed that this was not the right arithmetic notion, precisely because of the choice of the embedding. Would the fact that the unit ball is connected be a good way of determining which kind of valuation we are looking at?

[Kevin Buzzard]

Filippo I don't know which part of my huge message you're talking about!

[Filippo A. E. Nuccio]

I am sorry, I wrote my message answering @Oliver Nash 's precisely in the same moment when you added your last remark. I was answering his. Concerning your long one, I understand very well your concern, and I think it is serious -- but I have no idea for the moment.

[Kevin Buzzard]

Of course what I _should_ do is to just write is_R_or_Rbar and then start experimenting with it!

[Sebastien Gouezel]

Right now, the is_R_or_C structure in mathlib is definitely used to single out i, and use it to do analysis. So, I'd say the current use is not problematic with respect to your message. What you are more worried about, if I understand correctly, is potential uses that are not yet in mathlib. There are two things you can do about that:

• Watch out for PRs and signal when the use of is_R_or_C is not the right one.
• Improve the docstring of is_R_or_C.

[Oliver Nash]

I was about to suggest a doc string warning. I think this could go a long way to helping.

[Oliver Nash]

I think the concept "I have a normed field + an equivalence to either R or C" is not necessarily harmful. Perhaps functional analysis can be setup without this (it would be neat to see an attempt!) but it seems not to do any harm there.

[Oliver Nash]

One final thought: in module theory we allow ourselves to have an extensive API for bases but we are careful that lemmas should be stated in terms of freeness when this is the right concept.

[Eric Wieser]

Right now docs#is_R_or_C is only used for things which are definitionally ℝ or ℂ, not just isomorphic to them, yes?

[Moritz Doll]

is_R_or_C has only two instances and as long as it stays that way we should be fine. One issue I have is that there is no way of proving statements separately for the reals and the complex numbers and then saying that it holds for is_R_or_C

[Moritz Doll]

there are enough theorems in analysis, where the proofs are quite different (or one uses the other), but in the end one wants a unified statement

[Moritz Doll]

I guess that if is_R_or_C had a way of making sure that the only two instances can be $\mathbb{R}$ and $\mathbb{C}$, then that would solve both problems.

[Andrew Yang]

How bad would it be to add the fields K = R \/ K = C and h : K = complex -> h.cast I = complex.I to is_R_or_C?

Edit: You would need more fields to say the other class instances are equal as well.

[Moritz Doll]

I was just experimenting around with it and it works surprisingly well to address my problem, the question is whether it also solves Kevin's worries and whether there are any downsides

[Moritz Doll]

my hacky experiment:

class is_R_or_C_properly (k : Type*) : Prop :=
  (is_R_or_C : k = ℝ ∨ k = ℂ)

lemma is_R_or_C' (k : Type*) [is_R_or_C_properly k] : k = ℝ ∨ k = ℂ := is_R_or_C_properly.is_R_or_C

lemma R_is_true (x : ℝ) : true := by trivial

lemma C_is_true (x : ℂ) : true := by trivial

example (k : Type*) [is_R_or_C_properly k] (x : k) : true :=
begin
  cases (is_R_or_C' k) with h,
  { rw h at x,
    exact R_is_true x },
  rw h at x,
  exact C_is_true x,
end

[Andrew Yang]

You would need the statement about complex.I or else there will be two is_R_or_C ℂ instances if I am not mistaken.
Then it should be possible to get subsingleton (is_R_or_C ℂ) and subsingleton (is_R_or_C ℝ) and you should be able to prove P ℝ -> P ℂ -> is_R_or_C K -> P K.

[Adam Topaz]

As someone who is too lazy to read too much and has never actually used is_R_or_C, can someone explain what was the original intention for such a class?

[Yaël Dillies]

Maybe better to do

induction is_R_or_C : Prop
| of_real : is_R_or_C ℝ
| of_complex : is_R_or_C ℂ

[Moritz Doll]

@Andrew Yang I know, I was just unsure whether rewrite works, I don't claim that my typeclass is good. it was just for experimenting around

[Andrew Yang]

The point of is_R_or_C is to give a unified interface to R and C to define say complex and real inner-product spaces in one go If I am not mistaken. A K = R \/ K = C statement on its own probably doesn't do much.

[Adam Topaz]

I guess my question is whether the choice of $i$ is really needed or whether the action of $Gal(\mathbb{C}|\mathbb{R})$ suffices?

[Adam Topaz]

I can imagine a p-adic analogue which characterizes completions of algebraic extensions of $\mathbb{Q}_p$ as well...

[Kevin Buzzard]

Adam Topaz said:

I guess my question is whether the choice of $i$ is really needed or whether the action of $Gal(\mathbb{C}|\mathbb{R})$ suffices?

Right -- I can envisage $\overline{\mathbb{R}}$-sesquilinear forms :-)

[Moritz Doll]

I have no definitive answer, but my guess would be that we never really need the choice of $i$. I cannot think of a way how that would ever come up.

[Johan Commelin]

There are plenty of formulas in analysis where i shows up in the pen-and-paper treatment, right?

[Johan Commelin]

But maybe those aren't about is_R_or_C type of fields, but about ℂ only.

[Johan Commelin]

Everything containing (2π i)^k, etc...

[Kevin Buzzard]

In the part of Hodge theory which leaks through into algebraic geometry you sometimes only see the group generated by this, which is well defined for Rbar.

[Johan Commelin]

I agree. There are some remarks in Hodge II about how i showing up in the definition of polarization is actually not-a-real-choice. But it's an annoying thing that it even shows up.

[Johan Commelin]

Presumably you can take the kernel of exp and do everything with tensor powers of that kernel. But I'm not sure if that is easier to formalize then the pick-a-basis-2πi-and-check-that-it-doesnt-matter-route.

[Junyan Xu]

Andrew Yang said:

You would need the statement about complex.I or else there will be two is_R_or_C ℂ instances if I am not mistaken.
Then it should be possible to get subsingleton (is_R_or_C ℂ) and subsingleton (is_R_or_C ℝ) and you should be able to prove P ℝ -> P ℂ -> is_R_or_C K -> P K.

Among the data fields of docs#is_R_or_C, star_ring, normed_algebra and complete_space all depend on nontrivially_normed_field, so it's gonna be tricky. I imagine you need to first prove some extensionality lemma with heterogeneous equality ...

[Jireh Loreaux]

FYI: soon is_R_or_C will extend densely_normed_field (see #15657)

[Eric Wieser]

A related remark; there was one place where I had to use is_R_or_C because I couldn't use inner_product_space and normed_algebra at the same time.

[Johan Commelin]

One thing I would like to see (but I don't yet know how) is a tiny sub-version of is_R_or_C that only concerns the algebra (no topology, and in particular no completeness). Because in number theory this would mean https://en.wikipedia.org/wiki/Totally_real_field and https://en.wikipedia.org/wiki/CM-field. A lot of theory about hermitian forms etc can be set up in that generality, and is useful in number theory.

[Johan Commelin]

My gut feeling is that we might be able to set up a few nice mixin classes. But I don't have a design/proposal yet.

[Kevin Buzzard]

Right, but this is a different issue. You certainly wouldn't be choosing a square root of -1 there!

[Johan Commelin]

It's different but related. If we are redesigning/extending these classes, I think it is good to keep this in mind.

[Johan Commelin]

We have a nice library about quadratic forms in large generality. I think it would be good to develop the hermitian library in the right generality as well. And thinking about that might help carving out the right set of is_R_or_C-related classes. We probably want a hierarchy/family of 3 or 4 such classes.

[Chris Hughes]

I'm just curious how these problems actually manifest themselves in Lean. If we were doing HoTT, we would have the problem that the notion of equality on Sigma k, Is_R_or_C k would be the wrong one, but we're not doing HoTT and we can use whichever isomorphism notion we want.

The only issue is maybe there would be type class diamonds somewhere where you end up with non def-eq instances because the chosen square root of minu one is different, but I don't see where that would be a problem.

I also don't see the non-canonical maps as a problem. We already have choices of maps into things like algebraic closures and you just have to understand that these maps are not natural when you use them. I think to be honest, the first thing we would do with our is_R_or_Rbar is use Classical.choice to pick an I.

My view is that mathematician care about this on paper because they're implicitly assuming some meta theorem similar to univalence or parametricity. Classical.choice breaks univalence and Classical.decEq breaks parametricity so we can't really use these meta theorems in mathlib very easily anyway, and for this reason, I don't think these considerations are relevant to us.

[Chris Hughes]

To prove constructions are isomorphism invariant in Lean, you will have to do the work whatever construction you choose and you won't be able to handwave something about not making any choices like you can on paper.

[Chris Hughes]

Did I accidentally reply to a year old thread? Oops