Number theory over function fields

Stream: maths

[Gihan Marasingha]

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]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Gihan Marasingha]

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]

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]

Thanks for the advice @Kevin Buzzard!