search

martinescardo / TypeTopology

Logical manifestations of topological concepts, and other things, via the univalent point of view.
GNU General Public License v3.0
220 stars 40 forks source link

Prove that the locale of spectra is a spectral locale #258

Closed ayberkt closed 3 months ago

ayberkt commented 3 months ago

This PR adds the proof that the locale of spectra over a distributive lattice L is a spectral locale.

It was proved in PR #251 that this locale is compact, so to show spectrality, it remained to construct proofs of the following.

  1. Compact opens form a directed basis.
  2. Compact opens are closed under binary meets.
  3. The type of compact opens is small.

This PR adds all three of these proofs, hence concluding that the frame of ideals defines a spectral locale.