Formalising the GAGA theorem in Lean4

• A WIP blueprint can be found at here
• The corresponding pdf version can be found here
• The corresponding documentation can be found here