Random Fermat's Last Theorem observation: the bridge between analysis and algebra in it is nonconstructive.

Chris Birkbeck, a post-doc at UCL, has been making modular forms in Lean. He defined them, unsurprisingly, as holomorphic functions on the upper half plane with some cute symmetry properties. So I started thinking "ooh what could we do with modular forms?"

And when I start thinking more arithmetically and wondering if we could cut out the subspace of the Jacobian by a newform and make an elliptic curve, I realised that in alg geom that only worked with a totally different definition of a modular forms -- some section of a sheaf.

So of course we now need to start thinking about using GAGA because we would like to relate the definition of a modular form in complex analysis (where all the harmonic analysis happens) to the definition in complex algebraic geometry (which is where the alg geom kicks in)

So this is called Serre's GAGA principle, and the proof is a beautiful piece of dévissage, you start with projective varieties like modular curves, then you reduce to projective n-space and then you reduce to powers of the canonical twisting sheaf and then you compute.

Serre's GAGA principle says that the analytic and algebraic definitions of a modular form are the same, and the way it does it is that it says "there's an obvious injective map from the algebra to the analysis, because polynomials are diffrntiable". So STP this map is surjective.

And right at the bottom of the proof in GAGA the proof is "because these vector spaces have the same dimension"

So the way you get the algebraic object (the modular form in the sense used by Wiles throughout his paper) from the analytic object (the modular form which Langlands gives in return for the 3-torsion of the Frey curve) is a cheat if you're a constructivist

You know the algebraic object exists because the analytic object Langlands gave you is in a complex vector space which you are assured you have a basis for.

I only noticed this through discussions with Jujian Zhang about these matters. Thanks Jujian.