T is Noetherian paper

Stream: FLT

[Kevin Buzzard]

I really want to get back to getting the proof that T is Noetherian over the line. This will involve finishing the adele project and the Haar character project. Both of these have made substantial progress recently. Unfortunately I have realised that the ball must be in my court right now because there are essentially no unclaimed tasks and yet the theorem is not proved :-) There are sorries with no associated tasks, and occasionally there are arguments with no LaTeX. @Madison Crim I know you've been doing that tensoring with an fp module commutes with arbitrary products; I tried to state the theorem that tensoring with an fp module commutes with restricted products but we're missing some typeclass instances which we need in order to even state this, so I feel like the ball is in my court on this one (this an example of where LaTeX is missing). I would really like to get to this this week, I have quite a quiet week, so hopefully later on this week there will be some more posts in this thread summarising where we are and what needs doing. This will be the first real output of the project.

As I said in my FLT Big Proof talk, I almost feel like I made a mistake here. The proof has motivated a lot of important definitions but all of the theorems we proved were basically known in the 1960s so we could have skipped them. However the advantage of doing what we did was that it showed that our definitions were usable.