Functorial qcqs-schemes #1086
Functorial qcqs-schemes #1086
Conversation
| fun theIso = ε A .fst | ||
| inv theIso = yonedaᴾ 𝔸¹ A .fun | ||
| rightInv theIso α = ℤFUNCTOR .⋆IdL _ ∙ yonedaᴾ 𝔸¹ A .leftInv α | ||
| leftInv theIso a = path -- I get yellow otherwise | ||
| where | ||
| path : yonedaᴾ 𝔸¹ A .fun ((idTrans (Sp .F-ob A)) ●ᵛ yonedaᴾ 𝔸¹ A .inv a) ≡ a | ||
| path = cong (yonedaᴾ 𝔸¹ A .fun) (ℤFUNCTOR .⋆IdL _) ∙ yonedaᴾ 𝔸¹ A .rightInv a | ||
| snd (Γ⊣SpCounitEquiv A) = ε A .snd | ||
| snd (𝓞⊣SpCounitEquiv A) = ε A .snd | ||
|
|
||
|
|
||
| -- Affine schemes |
There was a problem hiding this comment.
∃[ A ∈ CommRing ℓ ] NatIso (Sp .F-ob A) X could just be a sigma type,because this will always be a subsingleton.
|
I don't fully understand what happened to the commit history here. @mzeuner Did you rebase but then also merge? Because some commits (such as "cleanup affine scheme") appear twice now (as 947871f and as f4f95b6). Github still shows 107 files changed. But when I look at the diff locally ( |
|
I don't really understand how this happened either. |
|
Ah, I see. |
mzeuner
force-pushed
the
FuncQCQSSchemes
branch
from
8b6d276 to
f4f95b6
Compare
|
Ok, I reset to the commit before the merge and force-pushed, now everything looks much better. |
|
Ok, nice! I merge it. |
This PR builds on (#1082).
It proves that the Zariski coverage on
CommRing^opis subcanonical, i.e. that representables are Zariski sheaves.Quasi-compact, quasi-separated schemes are defined as Zariski sheaves that have a finite affine cover by compact open subfunctors. Subcanonicity is then used to show that affine schemes (i.e. representables) are qcqs-schemes.