Is the Langlands program a program?

Stream: maths

[Kevin Buzzard]

The local Langlands conjectures for GL_n state the existence of a canonical bijection between some set and some other set of the same cardinality. The word "canonical" here was initially defined to mean "we would like the bijection to have the following ten properties, and possibly some other properties too if we think of any that look useful and which we didn't mention yet". It is now a theorem that there is exactly one bijection with these ten properties, so we're all good.

I am interested in whether it is possible to turn the bijection into a computer program. Let me be more precise. I am kind of suspecting that it is not possible to do this, because I am kind of suspecting that it not even possible to define the two sides. But my understanding of this stuff is still hazy.

One side involves continuous group homomorphisms from the group $\mathrm{Gal}(\overline{\mathbb{Q}}_p/\mathbb{Q}_p)$, a Galois group invoving the algebraic closure of the $p$-adic numbers. The other side involves actions of $\mathrm{GL}_n(\mathbb{Q}_p)$ on infinite-dimensional complex vector spaces. Is this already enough to conclude that this is impossible constructively?

[Koundinya Vajjha]

I think the proof of the existence of algebraic closure invokes Zorn's lemma somewhere doesn't it? Or is there a constructive variant?

[Kevin Buzzard]

Algebraic closure of a general field requires Zorn. Algebraic closure of the complex numbers does not!

[Chris Hughes]

There's a constructive variant for some fields. I guess Q and finite fields would be possible

[Kevin Buzzard]

Right. But what about Q_p?

[Chris Hughes]

I would say almost certainly, because virtually everything is computable if you define it as a quotient by some horribly undecidable relation.

[Chris Hughes]

Is the question whether it's computable in the sense that addition on reals as quotient of cauchy sequences is computable, or whether it's computable in a practical sense?

[Kevin Buzzard]

The question is whether I can write a program which computes this canonical bijection in theory. I felt like the easiest way of answering it would be to convince myself that one can't even compute the two sets in theory.

[Chris Hughes]

You can definitely compute actions of $\text{GL}_n(\mathbb{Q}_p)$ in theory. I think $\overline{\mathbb{Q}_p}$ is computable as well, you can algebraically close first and then complete right?

[Chris Hughes]

The \overline doesn't work

[Kevin Buzzard]

Let's assume $\overline{\mathbb{Q}}$ is computable. We now want to complete with respect to a norm. But I don't know how to get that norm computably.

[Chris Hughes]

The padic norm is computable right?

[Kevin Buzzard]

The problem is that there are many ways to extend the p-adic norm on the rationals to a norm on its algebraic closure.

[Chris Hughes]

Doesn't matter if the norm is computable, since you only need it to define a relation, which are always computable in Lean.

[Kevin Buzzard]

For example, in $\mathbb{Z}[i]$ we have $(2+i)(2-i)=5$ and the factors are coprime. So to extend the 5-adic norm to $\mathbb{Q}(i)$ you need to decide which one will have valuation 1 and which one valuation 0.

[Kevin Buzzard]

And then you need to make infinitely many other such decisions in a compatible manner.

[Kevin Buzzard]

In ideal-theoretic terms, 5 is no longer prime in $\mathbb{Z}[i]$, it factors into two prime ideals $(2+i)$ and $(2-i)$, and more generally for number field you're going to have to factor the ideal $(5)$ and then choose one of the factors, in a compatible way across all number fields.

[Kevin Buzzard]

There are uncountably many ways of extending the 5-adic norm on the rationals to a norm on the algebraic closure of the rationals.

[Chris Hughes]

Choosing an arbitrary relation is fine according to Lean

def r : ℕ → ℕ → Prop := classical.some (show ∃ r : ℕ → ℕ → Prop,
  equivalence r ∧ ∀ a c b d,
  r a b → r c d → r (a + c) (b + d), from ⟨(=), ⟨eq.refl, λ _ _, eq.symm, λ _ _ _, eq.trans⟩,
    by intros; simp *⟩)

instance X_setoid : setoid ℕ := ⟨r, (classical.some_spec r._proof_1).1⟩

def X : Type := quotient ⟨r, (classical.some_spec r._proof_1).1⟩

--computable
def add : X → X → X := λ a b, quotient.lift_on₂ a b
  (λ a b, ⟦a + b⟧)
  (λ a b c d hab hcd,
    quotient.sound $ (classical.some_spec r._proof_1).2 _ _ _ _ hab hcd)

[Johan Commelin]

You can definitely compute actions of $\text{GL}_n(\mathbb{Q}_p)$ in theory. I think $\overline{\mathbb{Q}_p}$ is computable as well, you can algebraically close first and then complete right?

Nope, $\overline{\mathbb{Q}_p}$ is not complete.

[Kevin Buzzard]

If we completed Q-bar then we could define Q_p-bar as the stuff in the completion which was algebraic over Q_p.

[Kevin Buzzard]

But I'm not convinced we can complete Q-bar yet. However Chris' add post is a bit discomboulating.

[Johan Commelin]

I'm completely confused. Why aren't the reals computable in Lean...

[Chris Hughes]

They are.

[Chris Hughes]

But inv isn't

[Johan Commelin]

Aha.

[Kevin Buzzard]

I thought that anything uncountable was uncomputable almost by definition.

[Chris Hughes]

What about nat -> nat?

[Kevin Buzzard]

What does it mean for the reals to be computable?

[Chris Hughes]

I guess it means +, * and - are computable.

[Chris Hughes]

I think anything uncountable has non decidable equality.

[Kevin Buzzard]

I know what it means for a function nat -> nat to be computable. For more general domains I am a bit confused.

[Kenny Lau]

What does it mean for the reals to be computable?

a type is always comuptable.

[Johan Commelin]

I think anything uncountable has non decidable equality.

Ok, and I guess this means that for uncountable fields inv will be noncomputable.

[Johan Commelin]

I'm quite sure that inv is used somewhere in Langlands (-;

[Chris Hughes]

No, because as Kenny showed you can make more or less any field computable, by defining it as some quotient of field expressions.

[Kevin Buzzard]

Types: That is true in the sense that you don't have to put noncomputable in front of it in Lean. But I think I established in the computability thread that there are proofs which are noncomputable in the sense that you can't write a program, but Lean would let you mark them as computable because Lean doesn't generate bytecode for theorems becuase of impredicabilitvity or whatever it's called.

[Chris Hughes]

I think if you want that sort of computability, you have to never use any of the 3 axioms. And avoiding quot.sound might be hard.

[Kevin Buzzard]

ooh I'd not thought of it like that.

[Kevin Buzzard]

Without the quotient axiom one can still build quotients, but the universal property isn't computable because you have to choose an element in an equivalence class. The axiom doesn't magically make things computable.

[Andrew Ashworth]

I'm not sure what definition of computable is being used here but whatever real numbers as Cauchy sequences are, they are definitely not thought of as computable in general. Of course in certain cases you can compute with real numbers, and do useful things with them (Brouwer / Bishop) style.

[Andrew Ashworth]

here's a recent paper (2019!) about computable analysis

[Andrew Ashworth]

https://hal.inria.fr/hal-02088293/document

[Chris Hughes]

The definition used is "Lean does not demand that I mark the definition noncomputable"

[Mario Carneiro]

This MSE question of mine might be helpful for defining $\overline{\mathbb{Q}_p}$: Proving existence of $\overline{\mathbb{Q}_p}$ without AC

[Kevin Buzzard]

Consider the subset relation on finite extensions of Qp. This is a directed set, because we can take the union of two finite extensions to get another finite extension.

I don't follow this part. What is a finite extension of Q_p? It doesn't seem like even a set to me, let alone a directed set. If it's a set of isomorphism classes, then one can't take the union of two finite extensions (by which I assume you mean the field generated by the union) because this is not an isomorphism-invariant thing. For example, within the complexes, the field generated by Q(a) and Q(b) if a^3=b^3=2 depends on whether a and b are equal cube roots of 2 or unequal ones.

[Chris Hughes]

Subsets of nat \times polynomial Q_p with random field structures such that Q_p embeds into them with order by subset such that inclusion is a field hom.

[Chris Hughes]

Is the algebraic closure just the direct limit of that?

[Kevin Buzzard]

We can't then take the (field generated by the) union of two random extensions, at least not without further work.

I am concerned that we need some form of countable choice to make this work.

[Kevin Buzzard]

I don't see how we have finite joins yet.

[Chris Hughes]

Oh yes. This is why we need Zorn.

[Mario Carneiro]

I should warn you that my knowledge of algebraic number theory was extremely sketchy when I wrote that Q

[Mario Carneiro]

it is still pretty sketchy

[Mario Carneiro]

rereading it, I had the same question about unions of field extensions

[Mario Carneiro]

Maybe Milne has something to say about it?

[Mario Carneiro]

I think it is true that finite field extensions are a directed set though, because that claim doesn't imply uniqueness of the join

[Mario Carneiro]

there may be multiple ways to make the field extensions compatible, but there should be at least one way

[Reid Barton]

I don't understand, with Chris's description of the order, how two different copies of Q(sqrt 2) could have any join

[Reid Barton]

or any joint upper bound

[Mario Carneiro]

two copies of Q(sqrt 2) have join Q(sqrt 2)

[Mario Carneiro]

i.e. there is a field that embeds both

[Reid Barton]

But they are different subsets of the fixed universe and the ordering was supposedly containment

[Reid Barton]

like, literal set inclusion that's a field homomorphism

[Mario Carneiro]

I don't think there is a fixed universe here

[Reid Barton]

I was going with

Subsets of nat \times polynomial Q_p with random field structures such that Q_p embeds into them with order by subset such that inclusion is a field hom.

[Mario Carneiro]

maybe you have to allow taking quotients of the subsets?

[Mario Carneiro]

I don't think "order by subset" works very well when the field structures are random

[Mario Carneiro]

You can make chains pretty well, but you don't get a directed set

[Kevin Buzzard]

I think one might need countable choice to pull this off.

[Mario Carneiro]

I did actually work this out in metamath, but only as far as the definitions so I'm not totally sure it all works

[Mario Carneiro]

http://us2.metamath.org/mpeuni/mmtheorems269.html#ccp

[Mario Carneiro]

The actual construction is very straightforward - it's just the splitting field of an increasing sequence of finite sets that covers polynomial ZZ

[Kevin Buzzard]

The general problem is as follows. If L and M are random finite field extensions of K, then LM is not a thing. If we regard L and M as subsets of K-bar then LM is definitely a thing, but if L and M are just random things defined up to isomorphism, then different embeddings of L and M into K-bar might give rise to completely different LM's, fields that don't even have the same degree over K for example. An analogous problem is that the "intersection" of L and M is not a well-defined thing until you embed into K-bar, but if L and M are not normal extensions then there will be more than one image in K-bar so the intersection might change.

[David Michael Roberts]

For example, in $\mathbb{Z}[i]$ we have $(2+i)(2-i)=5$ and the factors are coprime. So to extend the 5-adic norm to $\mathbb{Q}(i)$ you need to decide which one will have valuation 1 and which one valuation 0.

Do the two choices of valuation give isomorphic valued fields? Does one get a diagram of all possible choices of valued field extensions?

[Kevin Buzzard]

The actual construction is very straightforward - it's just the splitting field of an increasing sequence of finite sets that covers polynomial ZZ

Splitting fields are defined up to isomorphism but not unique isomorphism, so if you have an abstract splitting field of f then you have to make a choice when you're embedding it into an abstract splitting field of fg. I'm not ruling out the possibility that ther's some way of making all these choices consistently somehow though in the specific case of the p-adics.

[Mario Carneiro]

my splitting field construction is 100% constructive

[Mario Carneiro]

it requires a total order on the base set to make random choices

[Mario Carneiro]

it's defined just above at that link

[Kevin Buzzard]

Do the two choices of valuation give isomorphic valued fields? Does one get a diagram of all possible choices of valued field extensions?

Yes, complex conjugation gives an isomorphism in this case. For a non-Galois extension though the valuations might not be isomorphic, e.g. 5 can factor as $PQ^2$ for two different primes $P$ and $Q$ and then the two valuations will definitely be different (they will have different "ramification degree"). For a finite extension of Q there's just a finite set of extensions of the p-adic valuation. For a finite Galois extension they're all Galois conjugate (this is not immediately obvious but it's true), i.e. you can move from any one to another one by applying an automorphism of the field. In the limit there are uncountably many and I don't know what a diagram is, but they might well be acted on transitively by the absolute galois group of the rationals.

[Reid Barton]

I don't think you can define any total order on Q_p though. Maybe it depends on exactly what you need out of the total order

[Mario Carneiro]

You don't, and I did

[Mario Carneiro]

it's just the real order on the cantor set

[Reid Barton]

how is it decidable?

[Mario Carneiro]

because ZFC

[Mario Carneiro]

I don't know whether that matters in this context though

[Reid Barton]

Oh I thought we were trying to be totally constructive

[Kevin Buzzard]

What link are we supposed to be looking at? Mario is your argument still that Q_p-bar can be made constructively (whatever that means when we're talking about uncountable objects)

[Mario Carneiro]

5 years ago I was just trying to do the construction in ZF

[Mario Carneiro]

The metamath link contains a list of definitions with comments on every line

[Kevin Buzzard]

So we're allowed AC? I am still so confused about what constructive means.

[Kevin Buzzard]

The link I followed just gave me a definition of Q_p, not Q_p-bar. Maybe I missed something.

[Kevin Buzzard]

Oh, I did: the very bottom thing.

[Mario Carneiro]

df-qp is Q_p, df-qpa is Q_p-bar

[Reid Barton]

I'm assuming constructive means "with no axioms"

[Mario Carneiro]

ZF is not quite the same thing as lean-constructive, but they are surprisingly similar in the broad strokes

[Kevin Buzzard]

Define the completion of the 𝑝-adic rationals.

This is "completion" in what sense??

[Mario Carneiro]

df-qpa is algebraic completion, df-cp is metric completion

[Kevin Buzzard]

Whatever are the "p-adic rationals"? Are they the rationals with the p-adic metric, or the p-adic numbers?

[Mario Carneiro]

padic numbers

[Kevin Buzzard]

By "algebraic completion" do you mean what mathematicians call "algebraic closure"?

[Mario Carneiro]

I believe so

[Kevin Buzzard]

OK got it.

[David Michael Roberts]

Oh, yes, I forgot the analogy with covering spaces, whereby one might not have a 'good enough' action by deck transformations (analogous to non-Galois field extns). So maybe I mean this: consider the algebraic closure not as a single field, but as an 'Ind-valued field' (or similar), whereby one has all the valued finite extensions and all the ways they map to each other. Maybe a stupid and known-to-fail idea, but my category theorist's nose leads me that way.

[Mario Carneiro]

what does Ind-valued mean?

[Mario Carneiro]

To clarify on constructivism in metamath: We have LEM from the very beginning - it's built on classical logic. But AC is an axiom, and metamath tracks axioms, so we try to minimize its use when possible. It's not intuitionistic mathematics, it's just ZF

[Mario Carneiro]

There is a separate database devoted to developing intuitionistic mathematics, but I don't think it's likely to discover anything that hasn't already been done in Coq and Agda and the other constructive proof assistants

[Mario Carneiro]

When you want to avoid AC, you start worrying about whether certain sets are "definable", not merely proven to exist

[Mario Carneiro]

and this takes the place of constructive definition in lean

[Mario Carneiro]

For example, from the well ordering theorem there is a well order of the real numbers, but there is (provably in the metatheory) no definable well order of the reals

[David Michael Roberts]

Ind-(valued field), not (Ind-valued) field.

[Mario Carneiro]

what is Ind- then?

[David Michael Roberts]

https://ncatlab.org/nlab/show/ind-object

[Kevin Buzzard]

You can take the class of all finite extensions of Q equipped with a valuation extending the p-adic valuation. But in general you can have more than one morphism between two objects.

[David Michael Roberts]

Sure, but you can have more than one embedding of a finite extension of Q (sans valuation) into larger extensions of Q (ditto). Somehow it all works out. I'm surely missing details, and not using the right words... Instead of Qbar one could work with the Ind-field that is all the finite extensions of Q, maybe?? Awful, since we know we can construct Qbar, but on the geometric side people think about pro-étale covers...

[Kevin Buzzard]

I don't understand how to take the limit without using choice. Say I have two directions to go at each stage. How can I find a way to the end without choice?

[Johan Commelin]

I think if you work with an Ind-field you don't actually take the limit.

[Johan Commelin]

So you don't actually build Qp-bar

[Johan Commelin]

Just some substitute that is hopefully good enough in practice.

[Johan Commelin]

@David Michael Roberts Correct me if I'm wrong :up:

[Mario Carneiro]

You still have to prove that a colimit sequence exists

[Mario Carneiro]

or directed set

[Mario Carneiro]

and in this case the actual taking of the colimit isn't a problem, because the necessary colimits exist in whatever category this is

[Kevin Buzzard]

I'm not sure this is turning into a program

[Kevin Buzzard]

Taking some big colimit in the category of rings, and then getting a field out of it by choosing a random maximal ideal (to quotient out by) is where choice strikes if you do it this way

[David Michael Roberts]

@Johan Commelin correct. _Don't_ take the colimit. Work with the Ind-field, much as one would work with eg the pro-group of automorphisms.

[Johan Commelin]

@David Michael Roberts But I guess that for some applications you will need to know that the colimit exists, right?

[Johan Commelin]

and in this case the actual taking of the colimit isn't a problem, because the necessary colimits exist in whatever category this is

The existence is a proof, hence irrelevant. But taking the colimit requires choices. I still don't see how to do that "canonically".

[Mario Carneiro]

If you can make it the colimit of a sequence, then you can pick an order

[Mario Carneiro]

hence the suggestion to use an increasing sequence of finite sets

[Mario Carneiro]

where the order is based on an arbitrary total order on Qp

[David Michael Roberts]

In practice, one might only work in some collection of intermediate extension (cf the Stacks project proving that one only ever needs small categories of schemes, given some initial schemes of interest). One would need to prove the theory required to actually trace through ordinary results that use an actual construction-using-Choice, but people seem to be having fun with eg condensed objects these days, which is not too dissimilar.

[Mario Carneiro]

I think it is pretty likely that Cp is an avoidable convenience, but then again so are most infinite sets. That doesn't mean I want to do formalization that way

[Mario Carneiro]

To actually answer Kevin's question, the better place to investigate is how people actually do computations on Cp

[Mario Carneiro]

like something you could put in a CAS

[Kevin Buzzard]

hence the suggestion to use an increasing sequence of finite sets

What I don't understand with the "increasing sequence of finite sets and order based on arbitrary total order" approch is that even if you stick to splitting fields, you will still have to choose a map from each splitting field to the next one up.

[David Michael Roberts]

Yes, surely people don't work with actual elements of some enormous topological ring.

[Kevin Buzzard]

like something you could put in a CAS

People don't do computations with C_p, nobody really understands it. People prove theorems about it.

[David Michael Roberts]

@Kevin Buzzard don't choose :-) use them all.

[Mario Carneiro]

Given two finite extensions, does there exist a common finite extension embedding both?

[Mario Carneiro]

People don't do computations with C_p, nobody really understands it. People prove theorems about it.

I think that's pretty clear evidence that Cp is not meant to be computable

[Kevin Buzzard]

Kevin Buzzard don't choose :-) use them all.

Right.

Yes, surely people don't work with actual elements of some enormous topological ring.

Right.

So the question is: although people don't actually ever talk about elements or whatever, the Langlands philosophy (in this case just class field theory) says "here are two sets, there is a bijection between them. Yes, the elements of one of the sets can be described as "group homomorphisms", even though nobody has ever seen an element of one of the groups in question -- but this doesn't matter". My question is whether this bijection can ever be a computer program.

[Mario Carneiro]

For the bijection itself to be a computer program, you need computable representations of both sides and a program that transforms one representation to the other. But it's also possible that one is a concrete computable type and the other is some noncomputable mess, and the bijection is saying that the noncomputable mess has a "nice" representation

[Kevin Buzzard]

Given two finite extensions, does there exist a common finite extension embedding both?

In some sense there is more than one. Given the two finite extensions, you can tensor product them together, and this gives you a ring not a field. The ring has finitely many maximal ideals; you can just choose one, and quotient out by it, and there is a common finite extension extending both.

[Mario Carneiro]

Is it possible to enumerate the maximal ideals?

[Kevin Buzzard]

In general, I doubt it. In the case of the p-adic numbers -- maybe.

[Mario Carneiro]

Assume everything is countable and labeled

[Kevin Buzzard]

I just don't know. I've not really thought about this kind of question before.

[Kevin Buzzard]

I've never had to avoid AC throughout my entire adult life.

[Mario Carneiro]

why do you think there are finitely many maximal ideals?

[Kevin Buzzard]

If our base field is K, of characteristic 0, and L and M are finite extensions of K, then L tensor M is a finite direct sum of finite extensions of K.

[Kevin Buzzard]

This follows from some sort of chinese remainder argument. We can write M=K[X]/f(X) with f irreducible, and then L tensor M is just L[X]/f(X) where now f might not be irreducible any more, but it only has finitely many factors.

[Kevin Buzzard]

We have to choose a factor. Of course we also have to choose f.

[Mario Carneiro]

I forget how irreducibility / factor finding algorithm works, but assuming you can calculate that for integer polynomials, I think that does the job

[Simon Pepin Lehalleur]

Is class field theory a program in the sense that you mean? It certainly involves uncountable sets, and arbitrary p-adic numbers, including non-computable ones. On the other hand, doesn't the inductive structure of the local langlands correspondance imply that it should be computable "modulo class field theory" (more precisely, modulo the local langlands correspondence for characters of Levi subgroups)? Do I remember correctly that the number of supercuspidal representations of fixed central character and conductor are finite?

Also, the computability aspects of a group and of its isomorphism classes of representations (of some type) can be very different. For instance, the unitary group U(n) is uncomputable in some sense, since the real numbers are, but its finite-dimensional continuous representations are described by highest weight theory and are computable.

[Kevin Buzzard]

I'm trying to work this out Simon. It's a weird question (in the sense that I've never cared about it before and none of my friends care about this question either). I think that I still don't really understand the question yet. I seem to have several competing definitions of computability in my head.

[Kevin Buzzard]

The only reason I'm asking at all is that I wrote this blog post saying that proofs were not programs and then a bunch of constructivists on Twitter told me that I wasn't trying hard enough.

[David Michael Roberts]

a bunch of constructivists on Twitter told me that I wasn't trying hard enough.

They are probably right, but don't take it personally. Prior to Bishop's book on constructive analysis (which is a gem), people thought constructivist ideas were too weak to do any analysis, and were fixated on things like 'all functions are continuous'. Turns out there's no real issue, the trick is arriving at classically equivalent definitions that have constructive content.

[David Michael Roberts]

Is class field theory a program in the sense that you mean? It certainly involves uncountable sets, and arbitrary p-adic numbers, including non-computable ones. On the other hand, doesn't the inductive structure of the local langlands correspondance imply that it should be computable "modulo class field theory"

Colin McLarty gave a talk at the Association for Symbolic Logic meeting last year titled "Class field theory in exponential function arithmetic (EFA)", and EFA is an incredibly weak system.