Project idea: Stone duality

Stream: LFTCM 2024

[Sam van G]

I will suggest a number of projects related to Stone duality in my talk , you can look at the very last slide if you want spoilers! And come talk to me.

[Sam van G]

List of possible projects (see my talk this afternoon for details):

1. Cut down the sober-spatial equivalence
2. Complete the proof of Birkhoff's theorem
3. The various equivalent definitions of profinite types
4. Work towards the Mile-Stones
5. For the brave: (Finite) Hochster's theorem
6. Priestley duality
7. Open mapping theorem and semantic interpolation

[Florent Schaffhauser]

Sam van G said:

I will suggest a number of projects related to Stone duality in my talk , you can look at the very last slide if you want spoilers! And come talk to me.

Great talk! Could you please upload a [handout] version of your slides?

[Sam van G]

Thanks @Flo (Florent Schaffhauser) ! Done, and corrected a few typos.

[Taiba]

Sam van G said:

List of possible projects (see my talk this afternoon for details):

1. Cut down the sober-spatial equivalence
2. Complete the proof of Birkhoff's theorem
3. The various equivalent definitions of profinite types
4. Work towards the Mile-Stones
5. For the brave: (Finite) Hochster's theorem
6. Priestley duality
7. Open mapping theorem and semantic interpolation

Hi, I'm actually working on the formalisation of stone duality, would you like to talk about it sometime?

[Sam van G]

Sure! Come find me any time today

[Sam van G]

Just now, I pushed a commit to our repository that makes

def Equiv : Profinite ≌ BoolAlgᵒᵖ

sorry-free. See further this message.