# Zulip Chat Archive

## Stream: maths

### Topic: Is the Langlands program a program?

#### Kevin Buzzard (Jun 17 2019 at 12:50):

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 (Jun 17 2019 at 14:06):

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 (Jun 17 2019 at 14:07):

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

#### Chris Hughes (Jun 17 2019 at 14:07):

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

#### Kevin Buzzard (Jun 17 2019 at 14:07):

Right. But what about Q_p?

#### Chris Hughes (Jun 17 2019 at 14:09):

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

#### Chris Hughes (Jun 17 2019 at 14:11):

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 (Jun 17 2019 at 15:41):

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 (Jun 17 2019 at 16:08):

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 (Jun 17 2019 at 16:10):

The `\overline`

doesn't work

#### Kevin Buzzard (Jun 17 2019 at 16:10):

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 (Jun 17 2019 at 16:11):

The padic norm is computable right?

#### Kevin Buzzard (Jun 17 2019 at 16:11):

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 (Jun 17 2019 at 16:12):

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 (Jun 17 2019 at 16:12):

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 (Jun 17 2019 at 16:12):

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

#### Kevin Buzzard (Jun 17 2019 at 16:14):

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 (Jun 17 2019 at 16:14):

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 (Jun 17 2019 at 16:21):

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 (Jun 17 2019 at 16:22):

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 (Jun 17 2019 at 16:22):

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 (Jun 17 2019 at 16:22):

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

#### Johan Commelin (Jun 17 2019 at 16:26):

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

#### Chris Hughes (Jun 17 2019 at 16:27):

They are.

#### Chris Hughes (Jun 17 2019 at 16:27):

But `inv`

isn't

#### Johan Commelin (Jun 17 2019 at 16:27):

Aha.

#### Kevin Buzzard (Jun 17 2019 at 16:27):

I thought that anything uncountable was uncomputable almost by definition.

#### Chris Hughes (Jun 17 2019 at 16:27):

What about `nat -> nat`

?

#### Kevin Buzzard (Jun 17 2019 at 16:27):

What does it mean for the reals to be computable?

#### Chris Hughes (Jun 17 2019 at 16:27):

I guess it means `+`

, `*`

and `-`

are computable.

#### Chris Hughes (Jun 17 2019 at 16:28):

I think anything uncountable has non decidable equality.

#### Kevin Buzzard (Jun 17 2019 at 16:29):

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

#### Kenny Lau (Jun 17 2019 at 16:29):

What does it mean for the reals to be computable?

a type is always comuptable.

#### Johan Commelin (Jun 17 2019 at 16:30):

I think anything uncountable has non decidable equality.

Ok, and I guess this means that for uncountable fields `inv`

will be noncomputable.

#### Johan Commelin (Jun 17 2019 at 16:30):

I'm quite sure that `inv`

is used somewhere in Langlands (-;

#### Chris Hughes (Jun 17 2019 at 16:31):

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 (Jun 17 2019 at 16:31):

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 (Jun 17 2019 at 16:39):

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 (Jun 17 2019 at 16:46):

ooh I'd not thought of it like that.

#### Kevin Buzzard (Jun 17 2019 at 16:47):

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 (Jun 17 2019 at 17:33):

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 (Jun 17 2019 at 17:37):

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

#### Andrew Ashworth (Jun 17 2019 at 17:37):

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

#### Chris Hughes (Jun 17 2019 at 17:45):

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

"

#### Mario Carneiro (Jun 17 2019 at 20:13):

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 (Jun 17 2019 at 21:35):

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 (Jun 17 2019 at 21:43):

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 (Jun 17 2019 at 21:46):

Is the algebraic closure just the direct limit of that?

#### Kevin Buzzard (Jun 17 2019 at 21:46):

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 (Jun 17 2019 at 21:46):

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

#### Chris Hughes (Jun 17 2019 at 21:48):

Oh yes. This is why we need Zorn.

#### Mario Carneiro (Jun 17 2019 at 22:03):

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

#### Mario Carneiro (Jun 17 2019 at 22:03):

it is still pretty sketchy

#### Mario Carneiro (Jun 17 2019 at 22:03):

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

#### Mario Carneiro (Jun 17 2019 at 22:03):

Maybe Milne has something to say about it?

#### Mario Carneiro (Jun 17 2019 at 22:04):

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 (Jun 17 2019 at 22:05):

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

#### Reid Barton (Jun 17 2019 at 22:05):

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 (Jun 17 2019 at 22:06):

or any joint upper bound

#### Mario Carneiro (Jun 17 2019 at 22:06):

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

#### Mario Carneiro (Jun 17 2019 at 22:06):

i.e. there is a field that embeds both

#### Reid Barton (Jun 17 2019 at 22:07):

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

#### Reid Barton (Jun 17 2019 at 22:07):

like, literal set inclusion that's a field homomorphism

#### Mario Carneiro (Jun 17 2019 at 22:07):

I don't think there is a fixed universe here

#### Reid Barton (Jun 17 2019 at 22:07):

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 (Jun 17 2019 at 22:09):

maybe you have to allow taking quotients of the subsets?

#### Mario Carneiro (Jun 17 2019 at 22:11):

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

#### Mario Carneiro (Jun 17 2019 at 22:11):

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

#### Kevin Buzzard (Jun 17 2019 at 22:14):

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

#### Mario Carneiro (Jun 17 2019 at 22:14):

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 (Jun 17 2019 at 22:14):

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

#### Mario Carneiro (Jun 17 2019 at 22:18):

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 (Jun 17 2019 at 22:18):

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 (Jun 17 2019 at 22:19):

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 (Jun 17 2019 at 22:20):

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 (Jun 17 2019 at 22:20):

my splitting field construction is 100% constructive

#### Mario Carneiro (Jun 17 2019 at 22:21):

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

#### Mario Carneiro (Jun 17 2019 at 22:21):

it's defined just above at that link

#### Kevin Buzzard (Jun 17 2019 at 22:23):

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 (Jun 17 2019 at 22:23):

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 (Jun 17 2019 at 22:23):

You don't, and I did

#### Mario Carneiro (Jun 17 2019 at 22:24):

it's just the real order on the cantor set

#### Reid Barton (Jun 17 2019 at 22:24):

how is it decidable?

#### Mario Carneiro (Jun 17 2019 at 22:24):

because ZFC

#### Mario Carneiro (Jun 17 2019 at 22:24):

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

#### Reid Barton (Jun 17 2019 at 22:24):

Oh I thought we were trying to be totally constructive

#### Kevin Buzzard (Jun 17 2019 at 22:25):

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 (Jun 17 2019 at 22:25):

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

#### Mario Carneiro (Jun 17 2019 at 22:25):

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

#### Kevin Buzzard (Jun 17 2019 at 22:25):

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

#### Kevin Buzzard (Jun 17 2019 at 22:26):

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

#### Kevin Buzzard (Jun 17 2019 at 22:26):

Oh, I did: the very bottom thing.

#### Mario Carneiro (Jun 17 2019 at 22:26):

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

#### Reid Barton (Jun 17 2019 at 22:27):

I'm assuming constructive means "with no axioms"

#### Mario Carneiro (Jun 17 2019 at 22:27):

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

#### Kevin Buzzard (Jun 17 2019 at 22:27):

Define the completion of the 𝑝-adic rationals.

This is "completion" in what sense??

#### Mario Carneiro (Jun 17 2019 at 22:27):

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

#### Kevin Buzzard (Jun 17 2019 at 22:27):

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

#### Mario Carneiro (Jun 17 2019 at 22:28):

padic numbers

#### Kevin Buzzard (Jun 17 2019 at 22:28):

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

#### Mario Carneiro (Jun 17 2019 at 22:28):

I believe so

#### Kevin Buzzard (Jun 17 2019 at 22:28):

OK got it.

#### David Michael Roberts (Jun 17 2019 at 22:31):

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 (Jun 17 2019 at 22:31):

what does Ind-valued mean?

#### Mario Carneiro (Jun 17 2019 at 22:34):

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 (Jun 17 2019 at 22:36):

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 (Jun 17 2019 at 22:38):

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

#### Mario Carneiro (Jun 17 2019 at 22:39):

and this takes the place of constructive definition in lean

#### Mario Carneiro (Jun 17 2019 at 22:40):

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 (Jun 17 2019 at 22:42):

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

#### Mario Carneiro (Jun 17 2019 at 22:42):

what is Ind- then?

#### David Michael Roberts (Jun 17 2019 at 22:46):

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

#### Kevin Buzzard (Jun 18 2019 at 07:44):

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 (Jun 18 2019 at 07:52):

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 (Jun 18 2019 at 07:52):

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 (Jun 18 2019 at 07:53):

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

#### Johan Commelin (Jun 18 2019 at 07:53):

So you don't actually build `Qp-bar`

#### Johan Commelin (Jun 18 2019 at 07:53):

Just some substitute that is hopefully good enough in practice.

#### Johan Commelin (Jun 18 2019 at 07:54):

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

#### Mario Carneiro (Jun 18 2019 at 07:54):

You still have to prove that a colimit sequence exists

#### Mario Carneiro (Jun 18 2019 at 07:54):

or directed set

#### Mario Carneiro (Jun 18 2019 at 07:55):

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 (Jun 18 2019 at 07:58):

I'm not sure this is turning into a program

#### Kevin Buzzard (Jun 18 2019 at 07:58):

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 (Jun 18 2019 at 08:02):

@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 (Jun 18 2019 at 08:03):

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

#### Johan Commelin (Jun 18 2019 at 08:04):

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 (Jun 18 2019 at 08:05):

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

#### Mario Carneiro (Jun 18 2019 at 08:05):

hence the suggestion to use an increasing sequence of finite sets

#### Mario Carneiro (Jun 18 2019 at 08:05):

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

#### David Michael Roberts (Jun 18 2019 at 08:07):

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 (Jun 18 2019 at 08:08):

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 (Jun 18 2019 at 08:09):

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

#### Mario Carneiro (Jun 18 2019 at 08:09):

like something you could put in a CAS

#### Kevin Buzzard (Jun 18 2019 at 08:10):

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 (Jun 18 2019 at 08:10):

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

#### Kevin Buzzard (Jun 18 2019 at 08:10):

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 (Jun 18 2019 at 08:10):

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

#### Mario Carneiro (Jun 18 2019 at 08:11):

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

#### Mario Carneiro (Jun 18 2019 at 08:11):

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 (Jun 18 2019 at 08:13):

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 (Jun 18 2019 at 08:15):

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 (Jun 18 2019 at 08:15):

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 (Jun 18 2019 at 08:15):

Is it possible to enumerate the maximal ideals?

#### Kevin Buzzard (Jun 18 2019 at 08:15):

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

#### Mario Carneiro (Jun 18 2019 at 08:16):

Assume everything is countable and labeled

#### Kevin Buzzard (Jun 18 2019 at 08:16):

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

#### Kevin Buzzard (Jun 18 2019 at 08:16):

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

#### Mario Carneiro (Jun 18 2019 at 08:16):

why do you think there are finitely many maximal ideals?

#### Kevin Buzzard (Jun 18 2019 at 08:17):

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 (Jun 18 2019 at 08:18):

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 (Jun 18 2019 at 08:18):

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

#### Mario Carneiro (Jun 18 2019 at 08:21):

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 (Jun 18 2019 at 08:35):

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 (Jun 18 2019 at 08:37):

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 (Jun 18 2019 at 08:37):

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 (Jun 18 2019 at 08:50):

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 (Jun 20 2019 at 01:43):

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.

Last updated: May 10 2021 at 23:11 UTC