Revisiting Stone duality for bitopological spaces: III. The biO ⊣ bipt adjunction and the patch frame

In part II, I defined simple lax biframes and simple biframes, and I argued that simple biframes are the same thing as the biframes of Banaschewski, Brümmer and Hardie. We will pursue the idea of using simple biframes as an analogue of Stone duals of bitopological spaces, through an adjunction biO ⊣ bipt. This leads to a notion of bisobrification, which coincides with the notion of 2-sobrification I had talked about in a previous post. I will take the opportunity to show a bit formally why simple biframes and Banaschewski-Brümmer-Hardie biframes are the same thing, by exhibiting an actual equivalence of categories. We will finally see how the notion of patch topology transfers over to simple biframes (or Banaschewski-Brümmer-Hardie biframes, for which the notion is built-in), how the patch and (bi)point constructions commute, and how the patch and (bi)sobrification commute. Read the full post.