Zulip Chat Archive

Stream: maths

Topic: Is the Langlands program a program?


view this post on Zulip 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 Gal(Qp/Qp)\mathrm{Gal}(\overline{\mathbb{Q}}_p/\mathbb{Q}_p), a Galois group invoving the algebraic closure of the pp-adic numbers. The other side involves actions of GLn(Qp)\mathrm{GL}_n(\mathbb{Q}_p) on infinite-dimensional complex vector spaces. Is this already enough to conclude that this is impossible constructively?

view this post on Zulip 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?

view this post on Zulip Kevin Buzzard (Jun 17 2019 at 14:07):

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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Jun 17 2019 at 14:07):

Right. But what about Q_p?

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Chris Hughes (Jun 17 2019 at 16:08):

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

view this post on Zulip Chris Hughes (Jun 17 2019 at 16:10):

The \overline doesn't work

view this post on Zulip Kevin Buzzard (Jun 17 2019 at 16:10):

Let's assume Q\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.

view this post on Zulip Chris Hughes (Jun 17 2019 at 16:11):

The padic norm is computable right?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Jun 17 2019 at 16:12):

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

view this post on Zulip Kevin Buzzard (Jun 17 2019 at 16:12):

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

view this post on Zulip Kevin Buzzard (Jun 17 2019 at 16:14):

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

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip Johan Commelin (Jun 17 2019 at 16:22):

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

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Jun 17 2019 at 16:26):

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

view this post on Zulip Chris Hughes (Jun 17 2019 at 16:27):

They are.

view this post on Zulip Chris Hughes (Jun 17 2019 at 16:27):

But inv isn't

view this post on Zulip Johan Commelin (Jun 17 2019 at 16:27):

Aha.

view this post on Zulip Kevin Buzzard (Jun 17 2019 at 16:27):

I thought that anything uncountable was uncomputable almost by definition.

view this post on Zulip Chris Hughes (Jun 17 2019 at 16:27):

What about nat -> nat?

view this post on Zulip Kevin Buzzard (Jun 17 2019 at 16:27):

What does it mean for the reals to be computable?

view this post on Zulip Chris Hughes (Jun 17 2019 at 16:27):

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

view this post on Zulip Chris Hughes (Jun 17 2019 at 16:28):

I think anything uncountable has non decidable equality.

view this post on Zulip 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.

view this post on Zulip Kenny Lau (Jun 17 2019 at 16:29):

What does it mean for the reals to be computable?

a type is always comuptable.

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Jun 17 2019 at 16:30):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Jun 17 2019 at 16:46):

ooh I'd not thought of it like that.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Andrew Ashworth (Jun 17 2019 at 17:37):

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

view this post on Zulip Andrew Ashworth (Jun 17 2019 at 17:37):

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

view this post on Zulip Chris Hughes (Jun 17 2019 at 17:45):

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

view this post on Zulip Mario Carneiro (Jun 17 2019 at 20:13):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Chris Hughes (Jun 17 2019 at 21:46):

Is the algebraic closure just the direct limit of that?

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Jun 17 2019 at 21:46):

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

view this post on Zulip Chris Hughes (Jun 17 2019 at 21:48):

Oh yes. This is why we need Zorn.

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Jun 17 2019 at 22:03):

it is still pretty sketchy

view this post on Zulip Mario Carneiro (Jun 17 2019 at 22:03):

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

view this post on Zulip Mario Carneiro (Jun 17 2019 at 22:03):

Maybe Milne has something to say about it?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Reid Barton (Jun 17 2019 at 22:06):

or any joint upper bound

view this post on Zulip Mario Carneiro (Jun 17 2019 at 22:06):

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

view this post on Zulip Mario Carneiro (Jun 17 2019 at 22:06):

i.e. there is a field that embeds both

view this post on Zulip Reid Barton (Jun 17 2019 at 22:07):

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

view this post on Zulip Reid Barton (Jun 17 2019 at 22:07):

like, literal set inclusion that's a field homomorphism

view this post on Zulip Mario Carneiro (Jun 17 2019 at 22:07):

I don't think there is a fixed universe here

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Jun 17 2019 at 22:09):

maybe you have to allow taking quotients of the subsets?

view this post on Zulip Mario Carneiro (Jun 17 2019 at 22:11):

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

view this post on Zulip Mario Carneiro (Jun 17 2019 at 22:11):

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

view this post on Zulip Kevin Buzzard (Jun 17 2019 at 22:14):

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Jun 17 2019 at 22:14):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip David Michael Roberts (Jun 17 2019 at 22:19):

For example, in Z[i]\mathbb{Z}[i] we have (2+i)(2i)=5(2+i)(2-i)=5 and the factors are coprime. So to extend the 5-adic norm to Q(i)\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?

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Jun 17 2019 at 22:20):

my splitting field construction is 100% constructive

view this post on Zulip Mario Carneiro (Jun 17 2019 at 22:21):

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

view this post on Zulip Mario Carneiro (Jun 17 2019 at 22:21):

it's defined just above at that link

view this post on Zulip 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 PQ2PQ^2 for two different primes PP and QQ 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.

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Jun 17 2019 at 22:23):

You don't, and I did

view this post on Zulip Mario Carneiro (Jun 17 2019 at 22:24):

it's just the real order on the cantor set

view this post on Zulip Reid Barton (Jun 17 2019 at 22:24):

how is it decidable?

view this post on Zulip Mario Carneiro (Jun 17 2019 at 22:24):

because ZFC

view this post on Zulip Mario Carneiro (Jun 17 2019 at 22:24):

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

view this post on Zulip Reid Barton (Jun 17 2019 at 22:24):

Oh I thought we were trying to be totally constructive

view this post on Zulip 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)

view this post on Zulip Mario Carneiro (Jun 17 2019 at 22:25):

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

view this post on Zulip Mario Carneiro (Jun 17 2019 at 22:25):

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

view this post on Zulip Kevin Buzzard (Jun 17 2019 at 22:25):

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

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Jun 17 2019 at 22:26):

Oh, I did: the very bottom thing.

view this post on Zulip Mario Carneiro (Jun 17 2019 at 22:26):

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

view this post on Zulip Reid Barton (Jun 17 2019 at 22:27):

I'm assuming constructive means "with no axioms"

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Jun 17 2019 at 22:27):

Define the completion of the 𝑝-adic rationals.

This is "completion" in what sense??

view this post on Zulip Mario Carneiro (Jun 17 2019 at 22:27):

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

view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Jun 17 2019 at 22:28):

padic numbers

view this post on Zulip Kevin Buzzard (Jun 17 2019 at 22:28):

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

view this post on Zulip Mario Carneiro (Jun 17 2019 at 22:28):

I believe so

view this post on Zulip Kevin Buzzard (Jun 17 2019 at 22:28):

OK got it.

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Jun 17 2019 at 22:31):

what does Ind-valued mean?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Jun 17 2019 at 22:39):

and this takes the place of constructive definition in lean

view this post on Zulip 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

view this post on Zulip David Michael Roberts (Jun 17 2019 at 22:42):

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

view this post on Zulip Mario Carneiro (Jun 17 2019 at 22:42):

what is Ind- then?

view this post on Zulip David Michael Roberts (Jun 17 2019 at 22:46):

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

view this post on Zulip 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.

view this post on Zulip 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...

view this post on Zulip 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?

view this post on Zulip Johan Commelin (Jun 18 2019 at 07:53):

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

view this post on Zulip Johan Commelin (Jun 18 2019 at 07:53):

So you don't actually build Qp-bar

view this post on Zulip Johan Commelin (Jun 18 2019 at 07:53):

Just some substitute that is hopefully good enough in practice.

view this post on Zulip Johan Commelin (Jun 18 2019 at 07:54):

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

view this post on Zulip Mario Carneiro (Jun 18 2019 at 07:54):

You still have to prove that a colimit sequence exists

view this post on Zulip Mario Carneiro (Jun 18 2019 at 07:54):

or directed set

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Jun 18 2019 at 07:58):

I'm not sure this is turning into a program

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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".

view this post on Zulip Mario Carneiro (Jun 18 2019 at 08:05):

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

view this post on Zulip Mario Carneiro (Jun 18 2019 at 08:05):

hence the suggestion to use an increasing sequence of finite sets

view this post on Zulip Mario Carneiro (Jun 18 2019 at 08:05):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Jun 18 2019 at 08:09):

like something you could put in a CAS

view this post on Zulip 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.

view this post on Zulip David Michael Roberts (Jun 18 2019 at 08:10):

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

view this post on Zulip 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.

view this post on Zulip David Michael Roberts (Jun 18 2019 at 08:10):

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

view this post on Zulip Mario Carneiro (Jun 18 2019 at 08:11):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Jun 18 2019 at 08:15):

Is it possible to enumerate the maximal ideals?

view this post on Zulip Kevin Buzzard (Jun 18 2019 at 08:15):

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

view this post on Zulip Mario Carneiro (Jun 18 2019 at 08:16):

Assume everything is countable and labeled

view this post on Zulip Kevin Buzzard (Jun 18 2019 at 08:16):

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

view this post on Zulip Kevin Buzzard (Jun 18 2019 at 08:16):

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

view this post on Zulip Mario Carneiro (Jun 18 2019 at 08:16):

why do you think there are finitely many maximal ideals?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Jun 18 2019 at 08:18):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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