Prove that the initial frame Ω is a spectral frame and define its patch
#173
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
martinescardo
approved these changes
Aug 17, 2023
|
@martinescardo This is currently a draft PR but I’m in the process of finalising it. Should be ready to review soon. |
|
Note to self: before proceeding further with this, it‘s probably a good idea to address Issue #168. |
martinescardo
approved these changes
Aug 21, 2023
| → closed-under-binary-meets F ℬ holds | ||
| → let | ||
| ℬ↑ = directify F ℬ | ||
| β↑ = directified-basis-is-basis F ℬ β |
source/Locales/Sierpinski.lagda
Outdated
| (((P (𝟙 {𝓤} , (λ { ⋆ → ⋆ }) , 𝟙-is-prop)) holds) , λ _ → ₁) , {!!} | ||
|
|
||
| ℬ𝕊-is-directed-basis : is-directed-basis (𝒪 𝕊) ℬ𝕊 | ||
| ℬ𝕊-is-directed-basis = {!!} , {!!} |
source/Locales/Sierpinski.lagda
Outdated
| (((P (𝟙 {𝓤} , (λ { ⋆ → ⋆ }) , 𝟙-is-prop)) holds) , λ _ → ₁) , {!!} | ||
|
|
||
| ℬ𝕊-is-directed-basis : is-directed-basis (𝒪 𝕊) ℬ𝕊 | ||
| ℬ𝕊-is-directed-basis = {!!} , {!!} |
source/Locales/Sierpinski.lagda
Outdated
| 𝕊-spectralᴰ = ℬ𝕊 , ℬ𝕊-is-directed-basis , {!!} , {!!} | ||
|
|
||
| 𝕊-is-spectral : is-spectral (𝒪 𝕊) holds | ||
| 𝕊-is-spectral = {!!} |
martinescardo
approved these changes
Aug 21, 2023
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This PR adds a proof that the initial frame
Ωis spectral. This is actually quite easy to prove, except there is a technical problem with showing that the basis is closed under binary meets.Because our definition of spectral locale requires the covering families to be directed, the basis has to be closed under finite joins to ensure that this condition is met. When we do this, however, we end up in a situation where$(x_1 \vee \cdots \vee x_m) \wedge (y_1 \vee \cdots \vee y_n)$ has to be shown to be in the basis, given that each $x_i$ and $y_j$ are basic. This requires a CNF transformation argument that is quite tedious.
One might say that this is a good reason to take out the directedness condition from the definition of spectrality, which I have tried doing in the past. In my experience though, things go much more smoothly if this condition is baked into the definition.