Formalising Hochster's Theorem

Stream: maths

[Fangming Li (John)]

Hello everyone! I have successfully formalised Hochster's Theorem: every spectral topological space is homeomorphic to the prime spectrum of a commutative ring. Here is the link to my repository: https://github.com/FMLJohn/Hochster.

The theorem has been stated as the following, which can be found in Hochster/Section7.lean:

theorem exists_nonempty_homeomorph (X : Type u) [TopologicalSpace X] [SpectralSpace X] :
    ∃ R : Type u, ∃ _ : CommRing R, Nonempty (X ≃ₜ PrimeSpectrum R) := ...

[Kevin Buzzard]

Congratulations! You might be the first human I've met who has read the proof :-)