Zulip Chat Archive

Stream: maths

Topic: Number theory over function fields


Gihan Marasingha (May 07 2020 at 16:52):

I'd like to get more involved and plan to take on a research MSc student to help formalise results in number theory over function fields. For example, proving quadratic reciprocity, the Riemann Hypothesis, etc. in this setting.

Two questions for the experienced members:
1) Has any of this been done? I can't see it in mathlib, but perhaps I'm not looking hard enough.
2) In your opinion, is it a reasonable goal for an MSc dissertation?

Thanks!

Johan Commelin (May 07 2020 at 16:56):

I don't think we have anything in that direction. I'm not aware of anything involving function fields.

Johan Commelin (May 07 2020 at 16:56):

It depends very much on how much maths the student knows and how much experience they have with formalising maths.

Johan Commelin (May 07 2020 at 16:56):

If they don't have any prior experience... it might go well, but it might also be very tough.

Gihan Marasingha (May 07 2020 at 17:01):

Thanks @Johan Commelin. That's good to know. I can make a start to see how challenging it's likely to be before the start of the academic year in September.

Kevin Buzzard (May 07 2020 at 17:22):

There is also no theory of Dedekind domains AFAIK, e.g. the fact that integrally closed 1-dimensional domains have the property that non-zero ideals factor uniquely into primes.

I think it's a super thing to do for an MSc dissertation. It's kind of high-risk high-gain, because there's a chance the student won't get anywhere (I've had students in the past where I have had to write 50% of the code myself, before they could get going), but if they do something then it's probably worth publishing. For preparation you might want to try and find the simplest route to each major theorem. I would very much like to work on general commutative algebra (e.g. Nullstellensatz etc) over the summer.

Gihan Marasingha (May 07 2020 at 17:25):

Thanks for the advice @Kevin Buzzard!


Last updated: Dec 20 2023 at 11:08 UTC