diff --git a/Cubical/AlgebraicGeometry/Functorial/ZFunctors/Base.agda b/Cubical/AlgebraicGeometry/Functorial/ZFunctors/Base.agda new file mode 100644 index 000000000..852474364 --- /dev/null +++ b/Cubical/AlgebraicGeometry/Functorial/ZFunctors/Base.agda @@ -0,0 +1,245 @@ +{- + + A ℤ-functor is just a functor from rings to sets. + + NOTE: we consider the functor category [ Ring ℓ , Set ℓ ] for some universe level ℓ + and not [ Ring ℓ , Set (ℓ+1) ] as is done in + "Introduction to Algebraic Geometry and Algebraic Groups" + by Demazure & Gabriel! + + The category of ℤ-functors contains the category of (qcqs-) schemes + as a full subcategory and satisfies a "universal property" + similar to the one of schemes: + + There is a coadjunction 𝓞 ⊣ᵢ Sp + (relative to the inclusion i : CommRing ℓ → CommRing (ℓ+1)) + between the "global sections functor" 𝓞 + and the fully-faithful embedding of affines Sp, + whose counit is a natural isomorphism + +-} + +{-# OPTIONS --safe --lossy-unification #-} +module Cubical.AlgebraicGeometry.Functorial.ZFunctors.Base where + +open import Cubical.Foundations.Prelude +open import Cubical.Foundations.Equiv +open import Cubical.Foundations.Isomorphism +open import Cubical.Foundations.Function +open import Cubical.Foundations.Powerset +open import Cubical.Foundations.HLevels + +open import Cubical.Functions.FunExtEquiv + +open import Cubical.Data.Sigma +open import Cubical.Data.Nat using (ℕ) + +open import Cubical.Algebra.Ring +open import Cubical.Algebra.CommRing + +open import Cubical.Categories.Category renaming (isIso to isIsoC) +open import Cubical.Categories.Functor +open import Cubical.Categories.Instances.Sets +open import Cubical.Categories.Instances.CommRings +open import Cubical.Categories.Instances.Functors +open import Cubical.Categories.NaturalTransformation +open import Cubical.Categories.Yoneda +open import Cubical.Categories.Site.Sheaf +open import Cubical.Categories.Site.Instances.ZariskiCommRing + +open import Cubical.HITs.PropositionalTruncation as PT + + +open Category hiding (_∘_) + + +module _ {ℓ : Level} where + + open Functor + open NatTrans + open CommRingStr ⦃...⦄ + open IsRingHom + + + -- using the naming conventions of Demazure & Gabriel + ℤFunctor = Functor (CommRingsCategory {ℓ = ℓ}) (SET ℓ) + ℤFUNCTOR = FUNCTOR (CommRingsCategory {ℓ = ℓ}) (SET ℓ) + + -- Yoneda in the notation of Demazure & Gabriel, + -- uses that double op is original category definitionally + Sp : Functor (CommRingsCategory {ℓ = ℓ} ^op) ℤFUNCTOR + Sp = YO {C = (CommRingsCategory {ℓ = ℓ} ^op)} + + isAffine : (X : ℤFunctor) → Type (ℓ-suc ℓ) + isAffine X = ∃[ A ∈ CommRing ℓ ] NatIso (Sp .F-ob A) X + -- TODO: 𝔸¹ ≅ Sp ℤ[x] and 𝔾ₘ ≅ Sp ℤ[x,x⁻¹] ≅ D(x) ↪ 𝔸¹ as first examples of affine schemes + + -- a ℤ-functor that is a sheaf wrt the Zariski coverage is called local + isLocal : ℤFunctor → Type (ℓ-suc ℓ) + isLocal X = isSheaf zariskiCoverage X + + -- the forgetful functor + -- aka the affine line + -- (aka the representable of ℤ[x]) + 𝔸¹ : ℤFunctor + 𝔸¹ = ForgetfulCommRing→Set + + -- the global sections functor + 𝓞 : Functor ℤFUNCTOR (CommRingsCategory {ℓ = ℓ-suc ℓ} ^op) + fst (F-ob 𝓞 X) = X ⇒ 𝔸¹ + + -- ring struncture induced by internal ring object 𝔸¹ + N-ob (CommRingStr.0r (snd (F-ob 𝓞 X))) A _ = 0r + where instance _ = A .snd + N-hom (CommRingStr.0r (snd (F-ob 𝓞 X))) φ = funExt λ _ → sym (φ .snd .pres0) + + N-ob (CommRingStr.1r (snd (F-ob 𝓞 X))) A _ = 1r + where instance _ = A .snd + N-hom (CommRingStr.1r (snd (F-ob 𝓞 X))) φ = funExt λ _ → sym (φ .snd .pres1) + + N-ob ((snd (F-ob 𝓞 X) CommRingStr.+ α) β) A x = α .N-ob A x + β .N-ob A x + where instance _ = A .snd + N-hom ((snd (F-ob 𝓞 X) CommRingStr.+ α) β) {x = A} {y = B} φ = funExt path + where + instance + _ = A .snd + _ = B .snd + path : ∀ x → α .N-ob B (X .F-hom φ x) + β .N-ob B (X .F-hom φ x) + ≡ φ .fst (α .N-ob A x + β .N-ob A x) + path x = α .N-ob B (X .F-hom φ x) + β .N-ob B (X .F-hom φ x) + ≡⟨ cong₂ _+_ (funExt⁻ (α .N-hom φ) x) (funExt⁻ (β .N-hom φ) x) ⟩ + φ .fst (α .N-ob A x) + φ .fst (β .N-ob A x) + ≡⟨ sym (φ .snd .pres+ _ _) ⟩ + φ .fst (α .N-ob A x + β .N-ob A x) ∎ + + N-ob ((snd (F-ob 𝓞 X) CommRingStr.· α) β) A x = α .N-ob A x · β .N-ob A x + where instance _ = A .snd + N-hom ((snd (F-ob 𝓞 X) CommRingStr.· α) β) {x = A} {y = B} φ = funExt path + where + instance + _ = A .snd + _ = B .snd + path : ∀ x → α .N-ob B (X .F-hom φ x) · β .N-ob B (X .F-hom φ x) + ≡ φ .fst (α .N-ob A x · β .N-ob A x) + path x = α .N-ob B (X .F-hom φ x) · β .N-ob B (X .F-hom φ x) + ≡⟨ cong₂ _·_ (funExt⁻ (α .N-hom φ) x) (funExt⁻ (β .N-hom φ) x) ⟩ + φ .fst (α .N-ob A x) · φ .fst (β .N-ob A x) + ≡⟨ sym (φ .snd .pres· _ _) ⟩ + φ .fst (α .N-ob A x · β .N-ob A x) ∎ + + N-ob ((CommRingStr.- snd (F-ob 𝓞 X)) α) A x = - α .N-ob A x + where instance _ = A .snd + N-hom ((CommRingStr.- snd (F-ob 𝓞 X)) α) {x = A} {y = B} φ = funExt path + where + instance + _ = A .snd + _ = B .snd + path : ∀ x → - α .N-ob B (X .F-hom φ x) ≡ φ .fst (- α .N-ob A x) + path x = - α .N-ob B (X .F-hom φ x) ≡⟨ cong -_ (funExt⁻ (α .N-hom φ) x) ⟩ + - φ .fst (α .N-ob A x) ≡⟨ sym (φ .snd .pres- _) ⟩ + φ .fst (- α .N-ob A x) ∎ + + CommRingStr.isCommRing (snd (F-ob 𝓞 X)) = makeIsCommRing + isSetNatTrans + (λ _ _ _ → makeNatTransPath (funExt₂ λ A _ → A .snd .CommRingStr.+Assoc _ _ _)) + (λ _ → makeNatTransPath (funExt₂ λ A _ → A .snd .CommRingStr.+IdR _)) + (λ _ → makeNatTransPath (funExt₂ λ A _ → A .snd .CommRingStr.+InvR _)) + (λ _ _ → makeNatTransPath (funExt₂ λ A _ → A .snd .CommRingStr.+Comm _ _)) + (λ _ _ _ → makeNatTransPath (funExt₂ λ A _ → A .snd .CommRingStr.·Assoc _ _ _)) + (λ _ → makeNatTransPath (funExt₂ λ A _ → A .snd .CommRingStr.·IdR _)) + (λ _ _ _ → makeNatTransPath (funExt₂ λ A _ → A .snd .CommRingStr.·DistR+ _ _ _)) + (λ _ _ → makeNatTransPath (funExt₂ λ A _ → A .snd .CommRingStr.·Comm _ _)) + + -- action on natural transformations + fst (F-hom 𝓞 α) = α ●ᵛ_ + pres0 (snd (F-hom 𝓞 α)) = makeNatTransPath (funExt₂ λ _ _ → refl) + pres1 (snd (F-hom 𝓞 α)) = makeNatTransPath (funExt₂ λ _ _ → refl) + pres+ (snd (F-hom 𝓞 α)) _ _ = makeNatTransPath (funExt₂ λ _ _ → refl) + pres· (snd (F-hom 𝓞 α)) _ _ = makeNatTransPath (funExt₂ λ _ _ → refl) + pres- (snd (F-hom 𝓞 α)) _ = makeNatTransPath (funExt₂ λ _ _ → refl) + + -- functoriality of 𝓞 + F-id 𝓞 = RingHom≡ (funExt λ _ → makeNatTransPath (funExt₂ λ _ _ → refl)) + F-seq 𝓞 _ _ = RingHom≡ (funExt λ _ → makeNatTransPath (funExt₂ λ _ _ → refl)) + + + +-- There is a coadjunction 𝓞 ⊣ᵢ Sp +-- (relative to the inclusion i : CommRing ℓ → CommRing (ℓ+1)) +-- between the "global sections functor" 𝓞 +-- and the fully-faithful embedding of affines Sp, +-- whose counit is a natural isomorphism +module AdjBij {ℓ : Level} where + + open Functor + open NatTrans + open Iso + open IsRingHom + + private module _ {A : CommRing ℓ} {X : ℤFunctor {ℓ}} where + _♭ : CommRingHom A (𝓞 .F-ob X) → X ⇒ Sp .F-ob A + fst (N-ob (φ ♭) B x) a = φ .fst a .N-ob B x + + pres0 (snd (N-ob (φ ♭) B x)) = cong (λ y → y .N-ob B x) (φ .snd .pres0) + pres1 (snd (N-ob (φ ♭) B x)) = cong (λ y → y .N-ob B x) (φ .snd .pres1) + pres+ (snd (N-ob (φ ♭) B x)) _ _ = cong (λ y → y .N-ob B x) (φ .snd .pres+ _ _) + pres· (snd (N-ob (φ ♭) B x)) _ _ = cong (λ y → y .N-ob B x) (φ .snd .pres· _ _) + pres- (snd (N-ob (φ ♭) B x)) _ = cong (λ y → y .N-ob B x) (φ .snd .pres- _) + + N-hom (φ ♭) ψ = funExt (λ x → RingHom≡ (funExt λ a → funExt⁻ (φ .fst a .N-hom ψ) x)) + + + -- the other direction is just precomposition modulo Yoneda + _♯ : X ⇒ Sp .F-ob A → CommRingHom A (𝓞 .F-ob X) + fst (α ♯) a = α ●ᵛ yonedaᴾ 𝔸¹ A .inv a + + pres0 (snd (α ♯)) = makeNatTransPath (funExt₂ λ B x → α .N-ob B x .snd .pres0) + pres1 (snd (α ♯)) = makeNatTransPath (funExt₂ λ B x → α .N-ob B x .snd .pres1) + pres+ (snd (α ♯)) _ _ = makeNatTransPath (funExt₂ λ B x → α .N-ob B x .snd .pres+ _ _) + pres· (snd (α ♯)) _ _ = makeNatTransPath (funExt₂ λ B x → α .N-ob B x .snd .pres· _ _) + pres- (snd (α ♯)) _ = makeNatTransPath (funExt₂ λ B x → α .N-ob B x .snd .pres- _) + + + -- the two maps are inverse to each other + ♭♯Id : ∀ (α : X ⇒ Sp .F-ob A) → ((α ♯) ♭) ≡ α + ♭♯Id _ = makeNatTransPath (funExt₂ λ _ _ → RingHom≡ (funExt (λ _ → refl))) + + ♯♭Id : ∀ (φ : CommRingHom A (𝓞 .F-ob X)) → ((φ ♭) ♯) ≡ φ + ♯♭Id _ = RingHom≡ (funExt λ _ → makeNatTransPath (funExt₂ λ _ _ → refl)) + + + -- we get a relative adjunction 𝓞 ⊣ᵢ Sp + -- with respect to the inclusion i : CommRing ℓ → CommRing (ℓ+1) + 𝓞⊣SpIso : {A : CommRing ℓ} {X : ℤFunctor {ℓ}} + → Iso (CommRingHom A (𝓞 .F-ob X)) (X ⇒ Sp .F-ob A) + fun 𝓞⊣SpIso = _♭ + inv 𝓞⊣SpIso = _♯ + rightInv 𝓞⊣SpIso = ♭♯Id + leftInv 𝓞⊣SpIso = ♯♭Id + + 𝓞⊣SpNatℤFunctor : {A : CommRing ℓ} {X Y : ℤFunctor {ℓ}} (α : X ⇒ Sp .F-ob A) (β : Y ⇒ X) + → (β ●ᵛ α) ♯ ≡ (𝓞 .F-hom β) ∘cr (α ♯) + 𝓞⊣SpNatℤFunctor _ _ = RingHom≡ (funExt (λ _ → makeNatTransPath (funExt₂ (λ _ _ → refl)))) + + 𝓞⊣SpNatCommRing : {X : ℤFunctor {ℓ}} {A B : CommRing ℓ} + (φ : CommRingHom A (𝓞 .F-ob X)) (ψ : CommRingHom B A) + → (φ ∘cr ψ) ♭ ≡ (φ ♭) ●ᵛ Sp .F-hom ψ + 𝓞⊣SpNatCommRing _ _ = makeNatTransPath (funExt₂ λ _ _ → RingHom≡ (funExt (λ _ → refl))) + + -- the counit is an equivalence + private + ε : (A : CommRing ℓ) → CommRingHom A ((𝓞 ∘F Sp) .F-ob A) + ε A = (idTrans (Sp .F-ob A)) ♯ + + 𝓞⊣SpCounitEquiv : (A : CommRing ℓ) → CommRingEquiv A ((𝓞 ∘F Sp) .F-ob A) + fst (𝓞⊣SpCounitEquiv A) = isoToEquiv theIso + where + theIso : Iso (A .fst) ((𝓞 ∘F Sp) .F-ob A .fst) + 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 diff --git a/Cubical/AlgebraicGeometry/Functorial/ZFunctors/CompactOpen.agda b/Cubical/AlgebraicGeometry/Functorial/ZFunctors/CompactOpen.agda new file mode 100644 index 000000000..d24abaf8b --- /dev/null +++ b/Cubical/AlgebraicGeometry/Functorial/ZFunctors/CompactOpen.agda @@ -0,0 +1,382 @@ +{- + + The definition of compact open subfunctors of a ℤ-functor X: + + U ↪ Sp(A) is compact open if it is given by a f.g. ideal of A, + i.e. if ∃ f₁, ... ,fₙ : A s.t. for all rings B: + U(B) = { φ : Hom(A,B) | ⟨ φf₁ , ... , φfₙ ⟩ = B } + + U ↪ X is compact open, if pulling back along any A-valued point + Sp(A) → X gives a compact open of Sp(A). + + By observing that compact open subfunctors of affine schemes + are in 1-1 correspondence with radicals of f.g. ideals, + we get that compact open subfunctors are classified by the + ℤ-functor that sends a ring to its Zariski lattice. + +-} + + +{-# OPTIONS --safe --lossy-unification #-} +module Cubical.AlgebraicGeometry.Functorial.ZFunctors.CompactOpen where + +open import Cubical.Foundations.Prelude +open import Cubical.Foundations.Equiv +open import Cubical.Foundations.Isomorphism +open import Cubical.Foundations.Function +open import Cubical.Foundations.Powerset +open import Cubical.Foundations.HLevels + + +open import Cubical.Functions.FunExtEquiv + +open import Cubical.Data.Sigma +open import Cubical.Data.Nat using (ℕ) + +open import Cubical.Data.FinData + +open import Cubical.Algebra.Ring +open import Cubical.Algebra.CommRing +open import Cubical.Algebra.CommRing.Localisation +open import Cubical.Algebra.CommRing.RadicalIdeal +open import Cubical.Algebra.Semilattice +open import Cubical.Algebra.Lattice +open import Cubical.Algebra.DistLattice +open import Cubical.Algebra.DistLattice.BigOps + +open import Cubical.AlgebraicGeometry.ZariskiLattice.Base +open import Cubical.AlgebraicGeometry.ZariskiLattice.UniversalProperty +open import Cubical.AlgebraicGeometry.ZariskiLattice.Properties +open import Cubical.AlgebraicGeometry.Functorial.ZFunctors.Base + +open import Cubical.Categories.Category renaming (isIso to isIsoC) +open import Cubical.Categories.Functor +open import Cubical.Categories.Instances.CommRings +open import Cubical.Categories.Instances.DistLattice +open import Cubical.Categories.Instances.DistLattices +open import Cubical.Categories.Site.Coverage +open import Cubical.Categories.Site.Sheaf +open import Cubical.Categories.Site.Instances.ZariskiCommRing +open import Cubical.Categories.NaturalTransformation +open import Cubical.Categories.Yoneda + +open import Cubical.HITs.PropositionalTruncation as PT +open import Cubical.HITs.SetQuotients as SQ + +open import Cubical.Relation.Binary.Order.Poset + + +module _ {ℓ : Level} where + + open Iso + open Functor + open NatTrans + open NatIso + open DistLatticeStr ⦃...⦄ + open CommRingStr ⦃...⦄ + open IsRingHom + open IsLatticeHom + open ZarLat + open ZarLatUniversalProp + + -- the Zariski lattice functor classifying compact open subobjects + ZarLatFun : ℤFunctor {ℓ = ℓ} + F-ob ZarLatFun A = ZL A , SQ.squash/ + F-hom ZarLatFun φ = inducedZarLatHom φ .fst + F-id ZarLatFun {A} = cong fst (inducedZarLatHomId A) + F-seq ZarLatFun φ ψ = cong fst (inducedZarLatHomSeq φ ψ) + + -- this is a separated presheaf + -- (TODO: prove this a sheaf) + isSeparatedZarLatFun : isSeparated zariskiCoverage ZarLatFun + isSeparatedZarLatFun A (unimodvec n f 1∈⟨f₁,⋯,fₙ⟩) u w uRest≡wRest = + u ≡⟨ sym (∧lLid _) ⟩ + 1l ∧l u ≡⟨ congL _∧l_ D1≡⋁Dfᵢ ⟩ + (⋁ (D A ∘ f)) ∧l u ≡⟨ ⋁Meetldist _ _ ⟩ + ⋁ (λ i → D A (f i) ∧l u) ≡⟨ ⋁Ext Dfᵢ∧u≡Dfᵢ∧w ⟩ + ⋁ (λ i → D A (f i) ∧l w) ≡⟨ sym (⋁Meetldist _ _) ⟩ + (⋁ (D A ∘ f)) ∧l w ≡⟨ congL _∧l_ (sym D1≡⋁Dfᵢ) ⟩ + 1l ∧l w ≡⟨ ∧lLid _ ⟩ + w ∎ + where + open Join (ZariskiLattice A) + open JoinSemilattice (Lattice→JoinSemilattice (DistLattice→Lattice (ZariskiLattice A))) + using (IndPoset) + open LatticeTheory (DistLattice→Lattice (ZariskiLattice A)) + open PosetStr (IndPoset .snd) + open IsSupport (isSupportD A) + open RadicalIdeal A + instance + _ = A .snd + _ = ZariskiLattice A .snd + + D1≡⋁Dfᵢ : 1l ≡ ⋁ (D A ∘ f) + D1≡⋁Dfᵢ = is-antisym _ _ + (supportRadicalIneq f 1r (∈→∈√ _ _ 1∈⟨f₁,⋯,fₙ⟩)) + (1lRightAnnihilates∨l _) + + Dfᵢ∧u≡Dfᵢ∧w : ∀ i → D A (f i) ∧l u ≡ D A (f i) ∧l w + Dfᵢ∧u≡Dfᵢ∧w i = + D A (f i) ∧l u + ≡⟨ sym (cong fst (funExt⁻ (cong fst toLocToDown≡ToDown) u)) ⟩ + locToDownHom .fst (inducedZarLatHom /1AsCommRingHom .fst u) .fst + ≡⟨ cong (λ x → locToDownHom .fst x .fst) (uRest≡wRest i) ⟩ + locToDownHom .fst (inducedZarLatHom /1AsCommRingHom .fst w) .fst + ≡⟨ cong fst (funExt⁻ (cong fst toLocToDown≡ToDown) w) ⟩ + D A (f i) ∧l w ∎ + where + open InvertingElementsBase.UniversalProp A (f i) + open LocDownSetIso A (f i) + + CompactOpen : ℤFunctor → Type (ℓ-suc ℓ) + CompactOpen X = X ⇒ ZarLatFun + + -- the induced subfunctor + ⟦_⟧ᶜᵒ : {X : ℤFunctor} (U : CompactOpen X) → ℤFunctor + F-ob (⟦_⟧ᶜᵒ {X = X} U) A = (Σ[ x ∈ X .F-ob A .fst ] U .N-ob A x ≡ D A 1r) + , isSetΣSndProp (X .F-ob A .snd) λ _ → squash/ _ _ + where instance _ = snd A + F-hom (⟦_⟧ᶜᵒ {X = X} U) {x = A} {y = B} φ (x , Ux≡D1) = (X .F-hom φ x) , path + where + instance + _ = A .snd + _ = B .snd + open IsLatticeHom + path : U .N-ob B (X .F-hom φ x) ≡ D B 1r + path = U .N-ob B (X .F-hom φ x) ≡⟨ funExt⁻ (U .N-hom φ) x ⟩ + ZarLatFun .F-hom φ (U .N-ob A x) ≡⟨ cong (ZarLatFun .F-hom φ) Ux≡D1 ⟩ + ZarLatFun .F-hom φ (D A 1r) ≡⟨ inducedZarLatHom φ .snd .pres1 ⟩ + D B 1r ∎ + F-id (⟦_⟧ᶜᵒ {X = X} U) = funExt (λ x → Σ≡Prop (λ _ → squash/ _ _) + (funExt⁻ (X .F-id) (x .fst))) + F-seq (⟦_⟧ᶜᵒ {X = X} U) φ ψ = funExt (λ x → Σ≡Prop (λ _ → squash/ _ _) + (funExt⁻ (X .F-seq φ ψ) (x .fst))) + + + isAffineCompactOpen : {X : ℤFunctor} (U : CompactOpen X) → Type (ℓ-suc ℓ) + isAffineCompactOpen U = isAffine ⟦ U ⟧ᶜᵒ + + + -- the (big) dist. lattice of compact opens + CompOpenDistLattice : Functor ℤFUNCTOR (DistLatticesCategory {ℓ = ℓ-suc ℓ} ^op) + fst (F-ob CompOpenDistLattice X) = CompactOpen X + + -- lattice structure induce by internal lattice object ZarLatFun + N-ob (DistLatticeStr.0l (snd (F-ob CompOpenDistLattice X))) A _ = 0l + where instance _ = ZariskiLattice A .snd + N-hom (DistLatticeStr.0l (snd (F-ob CompOpenDistLattice X))) _ = funExt λ _ → refl + + N-ob (DistLatticeStr.1l (snd (F-ob CompOpenDistLattice X))) A _ = 1l + where instance _ = ZariskiLattice A .snd + N-hom (DistLatticeStr.1l (snd (F-ob CompOpenDistLattice X))) {x = A} {y = B} φ = funExt λ _ → path + where + instance + _ = A .snd + _ = B .snd + _ = ZariskiLattice B .snd + path : D B 1r ≡ D B (φ .fst 1r) ∨l 0l + path = cong (D B) (sym (φ .snd .pres1)) ∙ sym (∨lRid _) + + N-ob ((snd (F-ob CompOpenDistLattice X) DistLatticeStr.∨l U) V) A x = U .N-ob A x ∨l V .N-ob A x + where instance _ = ZariskiLattice A .snd + N-hom ((snd (F-ob CompOpenDistLattice X) DistLatticeStr.∨l U) V) {x = A} {y = B} φ = funExt path + where + instance + _ = ZariskiLattice A .snd + _ = ZariskiLattice B .snd + path : ∀ x → U .N-ob B (X .F-hom φ x) ∨l V .N-ob B (X .F-hom φ x) + ≡ ZarLatFun .F-hom φ (U .N-ob A x ∨l V .N-ob A x) + path x = U .N-ob B (X .F-hom φ x) ∨l V .N-ob B (X .F-hom φ x) + ≡⟨ cong₂ _∨l_ (funExt⁻ (U .N-hom φ) x) (funExt⁻ (V .N-hom φ) x) ⟩ + ZarLatFun .F-hom φ (U .N-ob A x) ∨l ZarLatFun .F-hom φ (V .N-ob A x) + ≡⟨ sym (inducedZarLatHom φ .snd .pres∨l _ _) ⟩ + ZarLatFun .F-hom φ (U .N-ob A x ∨l V .N-ob A x) ∎ + + N-ob ((snd (F-ob CompOpenDistLattice X) DistLatticeStr.∧l U) V) A x = U .N-ob A x ∧l V .N-ob A x + where instance _ = ZariskiLattice A .snd + N-hom ((snd (F-ob CompOpenDistLattice X) DistLatticeStr.∧l U) V) {x = A} {y = B} φ = funExt path + where + instance + _ = ZariskiLattice A .snd + _ = ZariskiLattice B .snd + path : ∀ x → U .N-ob B (X .F-hom φ x) ∧l V .N-ob B (X .F-hom φ x) + ≡ ZarLatFun .F-hom φ (U .N-ob A x ∧l V .N-ob A x) + path x = U .N-ob B (X .F-hom φ x) ∧l V .N-ob B (X .F-hom φ x) + ≡⟨ cong₂ _∧l_ (funExt⁻ (U .N-hom φ) x) (funExt⁻ (V .N-hom φ) x) ⟩ + ZarLatFun .F-hom φ (U .N-ob A x) ∧l ZarLatFun .F-hom φ (V .N-ob A x) + ≡⟨ sym (inducedZarLatHom φ .snd .pres∧l _ _) ⟩ + ZarLatFun .F-hom φ (U .N-ob A x ∧l V .N-ob A x) ∎ + + DistLatticeStr.isDistLattice (snd (F-ob CompOpenDistLattice X)) = makeIsDistLattice∧lOver∨l + isSetNatTrans + (λ _ _ _ → makeNatTransPath (funExt₂ + (λ A _ → ZariskiLattice A .snd .DistLatticeStr.∨lAssoc _ _ _))) + (λ _ → makeNatTransPath (funExt₂ (λ A _ → ZariskiLattice A .snd .DistLatticeStr.∨lRid _))) + (λ _ _ → makeNatTransPath (funExt₂ (λ A _ → ZariskiLattice A .snd .DistLatticeStr.∨lComm _ _))) + (λ _ _ _ → makeNatTransPath (funExt₂ + (λ A _ → ZariskiLattice A .snd .DistLatticeStr.∧lAssoc _ _ _))) + (λ _ → makeNatTransPath (funExt₂ (λ A _ → ZariskiLattice A .snd .DistLatticeStr.∧lRid _))) + (λ _ _ → makeNatTransPath (funExt₂ (λ A _ → ZariskiLattice A .snd .DistLatticeStr.∧lComm _ _))) + (λ _ _ → makeNatTransPath (funExt₂ -- don't know why ∧lAbsorb∨l doesn't work + (λ A _ → ZariskiLattice A .snd .DistLatticeStr.absorb _ _ .snd))) + (λ _ _ _ → makeNatTransPath (funExt₂ -- same here + (λ A _ → ZariskiLattice A .snd .DistLatticeStr.∧l-dist-∨l _ _ _ .fst))) + + -- (contravariant) action on morphisms + fst (F-hom CompOpenDistLattice α) = α ●ᵛ_ + pres0 (snd (F-hom CompOpenDistLattice α)) = makeNatTransPath (funExt₂ λ _ _ → refl) + pres1 (snd (F-hom CompOpenDistLattice α)) = makeNatTransPath (funExt₂ λ _ _ → refl) + pres∨l (snd (F-hom CompOpenDistLattice α)) _ _ = makeNatTransPath (funExt₂ λ _ _ → refl) + pres∧l (snd (F-hom CompOpenDistLattice α)) _ _ = makeNatTransPath (funExt₂ λ _ _ → refl) + + -- functoriality + F-id CompOpenDistLattice = LatticeHom≡f _ _ + (funExt λ _ → makeNatTransPath (funExt₂ λ _ _ → refl)) + F-seq CompOpenDistLattice _ _ = LatticeHom≡f _ _ + (funExt λ _ → makeNatTransPath (funExt₂ λ _ _ → refl)) + + + -- useful lemmas + module _ (X : ℤFunctor) where + open isIsoC + private instance _ = (CompOpenDistLattice .F-ob X) .snd + + compOpenTopNatIso : NatIso X ⟦ 1l ⟧ᶜᵒ + N-ob (trans compOpenTopNatIso) _ φ = φ , refl + N-hom (trans compOpenTopNatIso) _ = funExt λ _ → Σ≡Prop (λ _ → squash/ _ _) refl + inv (nIso compOpenTopNatIso B) = fst + sec (nIso compOpenTopNatIso B) = funExt λ _ → Σ≡Prop (λ _ → squash/ _ _) refl + ret (nIso compOpenTopNatIso B) = funExt λ _ → refl + + + module _ (X : ℤFunctor) where + open isIsoC + open Join (CompOpenDistLattice .F-ob X) + open JoinSemilattice (Lattice→JoinSemilattice (DistLattice→Lattice (CompOpenDistLattice .F-ob X))) + open PosetStr (IndPoset .snd) hiding (_≤_) + open LatticeTheory ⦃...⦄ + private instance _ = (CompOpenDistLattice .F-ob X) .snd + + compOpenGlobalIncl : (U : CompactOpen X) → ⟦ U ⟧ᶜᵒ ⇒ X + N-ob (compOpenGlobalIncl U) A = fst + N-hom (compOpenGlobalIncl U) φ = refl + + compOpenIncl : {U V : CompactOpen X} → V ≤ U → ⟦ V ⟧ᶜᵒ ⇒ ⟦ U ⟧ᶜᵒ + N-ob (compOpenIncl {U = U} {V = V} V≤U) A (x , Vx≡D1) = x , path + where + instance + _ = A .snd + _ = ZariskiLattice A .snd + _ = DistLattice→Lattice (ZariskiLattice A) + path : U .N-ob A x ≡ D A 1r + path = U .N-ob A x ≡⟨ funExt⁻ (funExt⁻ (cong N-ob (sym V≤U)) A) x ⟩ + V .N-ob A x ∨l U .N-ob A x ≡⟨ cong (_∨l U .N-ob A x) Vx≡D1 ⟩ + D A 1r ∨l U .N-ob A x ≡⟨ 1lLeftAnnihilates∨l _ ⟩ + D A 1r ∎ + N-hom (compOpenIncl V≤U) φ = funExt λ x → Σ≡Prop (λ _ → squash/ _ _) refl + + -- this is essentially U∧_ + compOpenDownHom : (U : CompactOpen X) + → DistLatticeHom (CompOpenDistLattice .F-ob X) + (CompOpenDistLattice .F-ob ⟦ U ⟧ᶜᵒ) + compOpenDownHom U = CompOpenDistLattice .F-hom (compOpenGlobalIncl U) + + module _ {U V : CompactOpen X} (V≤U : V ≤ U) where + -- We need this separate definition to avoid termination checker issues, + -- but we don't understand why. + private + compOpenDownHomFun : (A : CommRing ℓ) + → ⟦ V ⟧ᶜᵒ .F-ob A .fst + → ⟦ compOpenDownHom U .fst V ⟧ᶜᵒ .F-ob A .fst + compOpenDownHomFun A v = (compOpenIncl V≤U ⟦ A ⟧) v , snd v + + compOpenDownHomNatIso : NatIso ⟦ V ⟧ᶜᵒ ⟦ compOpenDownHom U .fst V ⟧ᶜᵒ + N-ob (trans compOpenDownHomNatIso) = compOpenDownHomFun + N-hom (trans compOpenDownHomNatIso) _ = + funExt λ _ → Σ≡Prop (λ _ → squash/ _ _) (Σ≡Prop (λ _ → squash/ _ _) refl) + inv (nIso compOpenDownHomNatIso A) ((x , Ux≡D1) , Vx≡D1) = x , Vx≡D1 + sec (nIso compOpenDownHomNatIso A) = + funExt λ _ → Σ≡Prop (λ _ → squash/ _ _) (Σ≡Prop (λ _ → squash/ _ _) refl) + ret (nIso compOpenDownHomNatIso A) = funExt λ _ → Σ≡Prop (λ _ → squash/ _ _) refl + + compOpenInclId : ∀ {U : CompactOpen X} → compOpenIncl (is-refl U) ≡ idTrans ⟦ U ⟧ᶜᵒ + compOpenInclId = makeNatTransPath (funExt₂ (λ _ _ → Σ≡Prop (λ _ → squash/ _ _) refl)) + + compOpenInclSeq : ∀ {U V W : CompactOpen X} (U≤V : U ≤ V) (V≤W : V ≤ W) + → compOpenIncl (is-trans _ _ _ U≤V V≤W) + ≡ compOpenIncl U≤V ●ᵛ compOpenIncl V≤W + compOpenInclSeq _ _ = makeNatTransPath + (funExt₂ (λ _ _ → Σ≡Prop (λ _ → squash/ _ _) refl)) + + + -- the structure sheaf + private COᵒᵖ = (DistLatticeCategory (CompOpenDistLattice .F-ob X)) ^op + + strDLSh : Functor COᵒᵖ (CommRingsCategory {ℓ = ℓ-suc ℓ}) + F-ob strDLSh U = 𝓞 .F-ob ⟦ U ⟧ᶜᵒ + F-hom strDLSh U≥V = 𝓞 .F-hom (compOpenIncl U≥V) + F-id strDLSh = cong (𝓞 .F-hom) compOpenInclId ∙ 𝓞 .F-id + F-seq strDLSh _ _ = cong (𝓞 .F-hom) (compOpenInclSeq _ _) ∙ 𝓞 .F-seq _ _ + + + -- important lemma + -- Compact opens of Zariski sheaves are sheaves + presLocalCompactOpen : (X : ℤFunctor) (U : CompactOpen X) → isLocal X → isLocal ⟦ U ⟧ᶜᵒ + presLocalCompactOpen X U isLocalX R um@(unimodvec _ f _) = isoToIsEquiv isoU + where + open Coverage zariskiCoverage + open InvertingElementsBase R + instance _ = R .snd + + fᵢCoverR = covers R .snd um + + isoX : Iso (X .F-ob R .fst) (CompatibleFamily X fᵢCoverR) + isoX = equivToIso (elementToCompatibleFamily _ _ , isLocalX R um) + + compatibleFamIncl : (CompatibleFamily ⟦ U ⟧ᶜᵒ fᵢCoverR) → (CompatibleFamily X fᵢCoverR) + compatibleFamIncl fam = (fst ∘ fst fam) + , λ i j B φ ψ φψComm → cong fst (fam .snd i j B φ ψ φψComm) + + compatibleFamIncl≡ : ∀ (y : Σ[ x ∈ X .F-ob R .fst ] U .N-ob R x ≡ D R 1r) + → compatibleFamIncl (elementToCompatibleFamily ⟦ U ⟧ᶜᵒ fᵢCoverR y) + ≡ elementToCompatibleFamily X fᵢCoverR (y .fst) + compatibleFamIncl≡ y = CompatibleFamily≡ _ _ _ _ λ _ → refl + + isoU : Iso (Σ[ x ∈ X .F-ob R .fst ] U .N-ob R x ≡ D R 1r) + (CompatibleFamily ⟦ U ⟧ᶜᵒ fᵢCoverR) + fun isoU = elementToCompatibleFamily _ _ + fst (inv isoU fam) = isoX .inv (compatibleFamIncl fam) + snd (inv isoU fam) = -- U (x) ≡ D(1) + -- knowing that U(x/1)¸≡ D(1) in R[1/fᵢ] + let x = isoX .inv (compatibleFamIncl fam) in + isSeparatedZarLatFun R um (U .N-ob R x) (D R 1r) + λ i → let open UniversalProp (f i) + instance _ = R[1/ (f i) ]AsCommRing .snd in + + inducedZarLatHom /1AsCommRingHom .fst (U .N-ob R x) + + ≡⟨ funExt⁻ (sym (U .N-hom /1AsCommRingHom)) x ⟩ + + U .N-ob R[1/ (f i) ]AsCommRing (X .F-hom /1AsCommRingHom x) + + ≡⟨ cong (U .N-ob R[1/ f i ]AsCommRing) + (funExt⁻ (cong fst (isoX .rightInv (compatibleFamIncl fam))) i) ⟩ + + U .N-ob R[1/ (f i) ]AsCommRing (fam .fst i .fst) + + ≡⟨ fam .fst i .snd ⟩ + + D R[1/ (f i) ]AsCommRing 1r + + ≡⟨ sym (inducedZarLatHom /1AsCommRingHom .snd .pres1) ⟩ + + inducedZarLatHom /1AsCommRingHom .fst (D R 1r) ∎ + + rightInv isoU fam = + Σ≡Prop (λ _ → isPropIsCompatibleFamily _ _ _) + (funExt λ i → Σ≡Prop (λ _ → squash/ _ _) + (funExt⁻ (cong fst + (isoX .rightInv (compatibleFamIncl fam))) i)) + leftInv isoU y = Σ≡Prop (λ _ → squash/ _ _) + (cong (isoX .inv) (compatibleFamIncl≡ y) + ∙ isoX .leftInv (y .fst)) diff --git a/Cubical/AlgebraicGeometry/Functorial/ZFunctors/OpenSubscheme.agda b/Cubical/AlgebraicGeometry/Functorial/ZFunctors/OpenSubscheme.agda new file mode 100644 index 000000000..83dab7931 --- /dev/null +++ b/Cubical/AlgebraicGeometry/Functorial/ZFunctors/OpenSubscheme.agda @@ -0,0 +1,201 @@ +{- + + Compact open subfunctors of qcqs-schemes are qcqs-schemes (TODO!!!) + The proof proceeds by + 1. Defining standard/basic compact opens of affines and proving that they are affine + 2. Proving that arbitrary compact opens of affines are qcqs-schemes + +-} + +{-# OPTIONS --safe --lossy-unification #-} +module Cubical.AlgebraicGeometry.Functorial.ZFunctors.OpenSubscheme where + +open import Cubical.Foundations.Prelude +open import Cubical.Foundations.Equiv +open import Cubical.Foundations.Isomorphism +open import Cubical.Foundations.Function +open import Cubical.Foundations.Powerset +open import Cubical.Foundations.HLevels + + +open import Cubical.Functions.FunExtEquiv + +open import Cubical.Data.Sigma +open import Cubical.Data.Nat using (ℕ) + +open import Cubical.Data.FinData + +open import Cubical.Algebra.Ring +open import Cubical.Algebra.CommRing +open import Cubical.Algebra.CommRing.Localisation +open import Cubical.Algebra.Semilattice +open import Cubical.Algebra.Lattice +open import Cubical.Algebra.DistLattice +open import Cubical.Algebra.DistLattice.BigOps + +open import Cubical.AlgebraicGeometry.ZariskiLattice.Base +open import Cubical.AlgebraicGeometry.ZariskiLattice.UniversalProperty +open import Cubical.AlgebraicGeometry.ZariskiLattice.Properties +open import Cubical.AlgebraicGeometry.Functorial.ZFunctors.Base +open import Cubical.AlgebraicGeometry.Functorial.ZFunctors.CompactOpen +open import Cubical.AlgebraicGeometry.Functorial.ZFunctors.QcQsScheme + +open import Cubical.Categories.Category renaming (isIso to isIsoC) +open import Cubical.Categories.Functor + +open import Cubical.Categories.Site.Instances.ZariskiCommRing +open import Cubical.Categories.NaturalTransformation +open import Cubical.Categories.Yoneda + + +open import Cubical.HITs.PropositionalTruncation as PT +open import Cubical.HITs.SetQuotients as SQ + +open import Cubical.Relation.Binary.Order.Poset + + +-- standard affine opens +module StandardOpens {ℓ : Level} (R : CommRing ℓ) (f : R .fst) where + + open Iso + open Functor + open NatTrans + open NatIso + open isIsoC + open DistLatticeStr ⦃...⦄ + open CommRingStr ⦃...⦄ + open IsRingHom + open RingHoms + open IsLatticeHom + open ZarLat + + open InvertingElementsBase R + open UniversalProp f + + private module ZL = ZarLatUniversalProp + + private + instance + _ = R .snd + + D : CompactOpen (Sp ⟅ R ⟆) + D = yonedaᴾ ZarLatFun R .inv (ZL.D R f) + + SpR[1/f]≅⟦Df⟧ : NatIso (Sp .F-ob R[1/ f ]AsCommRing) ⟦ D ⟧ᶜᵒ + N-ob (trans SpR[1/f]≅⟦Df⟧) B φ = (φ ∘r /1AsCommRingHom) , ∨lRid _ ∙ path + where + open CommRingHomTheory φ + open IsSupport (ZL.isSupportD B) + instance + _ = B .snd + _ = ZariskiLattice B .snd + + isUnitφ[f/1] : φ .fst (f /1) ∈ B ˣ + isUnitφ[f/1] = RingHomRespInv (f /1) ⦃ S/1⊆S⁻¹Rˣ f ∣ 1 , sym (·IdR f) ∣₁ ⦄ + + path : ZL.D B (φ .fst (f /1)) ≡ 1l + path = supportUnit _ isUnitφ[f/1] + + N-hom (trans SpR[1/f]≅⟦Df⟧) _ = funExt λ _ → Σ≡Prop (λ _ → squash/ _ _) (RingHom≡ refl) + + inv (nIso SpR[1/f]≅⟦Df⟧ B) (φ , Dφf≡D1) = invElemUniversalProp B φ isUnitφf .fst .fst + where + instance _ = ZariskiLattice B .snd + isUnitφf : φ .fst f ∈ B ˣ + isUnitφf = unitLemmaZarLat B (φ $r f) (sym (∨lRid _) ∙ Dφf≡D1) + + sec (nIso SpR[1/f]≅⟦Df⟧ B) = + funExt λ _ → Σ≡Prop (λ _ → squash/ _ _) (RingHom≡ (invElemUniversalProp _ _ _ .fst .snd)) + ret (nIso SpR[1/f]≅⟦Df⟧ B) = + funExt λ φ → cong fst (invElemUniversalProp B (φ ∘r /1AsCommRingHom) _ .snd (φ , refl)) + + isAffineD : isAffineCompactOpen D + isAffineD = ∣ R[1/ f ]AsCommRing , SpR[1/f]≅⟦Df⟧ ∣₁ + + +-- compact opens of affine schemes are qcqs-schemes +module _ {ℓ : Level} (R : CommRing ℓ) (W : CompactOpen (Sp ⟅ R ⟆)) where + + open StandardOpens + + open Iso + open Functor + open NatTrans + open NatIso + open isIsoC + open DistLatticeStr ⦃...⦄ + open CommRingStr ⦃...⦄ + open PosetStr ⦃...⦄ + open IsRingHom + open RingHoms + open IsLatticeHom + open ZarLat + + open JoinSemilattice (Lattice→JoinSemilattice (DistLattice→Lattice (CompOpenDistLattice .F-ob (Sp .F-ob R)))) using (IndPoset; ind≤bigOp) + open InvertingElementsBase R + open Join + open JoinMap + open AffineCover + private module ZL = ZarLatUniversalProp + + private + instance + _ = R .snd + _ = ZariskiLattice R .snd + _ = CompOpenDistLattice .F-ob (Sp .F-ob R) .snd + _ = CompOpenDistLattice .F-ob ⟦ W ⟧ᶜᵒ .snd + _ = IndPoset .snd + + w : ZL R + w = yonedaᴾ ZarLatFun R .fun W + + -- yoneda is a lattice homomorphsim + isHomYoneda : IsLatticeHom (DistLattice→Lattice (ZariskiLattice R) .snd) + (yonedaᴾ ZarLatFun R .inv) + (DistLattice→Lattice (CompOpenDistLattice ⟅ Sp ⟅ R ⟆ ⟆) .snd) + pres0 isHomYoneda = makeNatTransPath (funExt₂ (λ _ _ → refl)) + pres1 isHomYoneda = + makeNatTransPath (funExt₂ (λ _ φ → inducedZarLatHom φ .snd .pres1)) + pres∨l isHomYoneda u v = + makeNatTransPath (funExt₂ (λ _ φ → inducedZarLatHom φ .snd .pres∨l u v)) + pres∧l isHomYoneda u v = + makeNatTransPath (funExt₂ (λ _ φ → inducedZarLatHom φ .snd .pres∧l u v)) + + module _ {n : ℕ} + (f : FinVec (fst R) n) + (⋁Df≡W : ⋁ (CompOpenDistLattice ⟅ Sp ⟅ R ⟆ ⟆) (D R ∘ f) ≡ W) where + + Df≤W : ∀ i → D R (f i) ≤ W + Df≤W i = subst (D R (f i) ≤_) ⋁Df≡W (ind≤bigOp (D R ∘ f) i) + + toAffineCover : AffineCover ⟦ W ⟧ᶜᵒ + AffineCover.n toAffineCover = n + U toAffineCover i = compOpenDownHom (Sp ⟅ R ⟆) W .fst (D R (f i)) + covers toAffineCover = sym (pres⋁ (compOpenDownHom (Sp ⟅ R ⟆) W) (D R ∘ f)) + ∙ cong (compOpenDownHom (Sp ⟅ R ⟆) W .fst) ⋁Df≡W + ∙ makeNatTransPath (funExt₂ (λ _ → snd)) + isAffineU toAffineCover i = + ∣ _ , seqNatIso (SpR[1/f]≅⟦Df⟧ R (f i)) (compOpenDownHomNatIso _ (Df≤W i)) ∣₁ + + module _ {n : ℕ} + (f : FinVec (fst R) n) + (⋁Df≡w : ⋁ (ZariskiLattice R) (ZL.D R ∘ f) ≡ w) where + + private + ⋁Df≡W : ⋁ (CompOpenDistLattice ⟅ Sp ⟅ R ⟆ ⟆) (D R ∘ f) ≡ W + ⋁Df≡W = sym (pres⋁ (_ , isHomYoneda) (ZL.D R ∘ f)) + ∙ cong (yonedaᴾ ZarLatFun R .inv) ⋁Df≡w + ∙ yonedaᴾ ZarLatFun R .leftInv W + + makeAffineCoverCompOpenOfAffine : AffineCover ⟦ W ⟧ᶜᵒ + makeAffineCoverCompOpenOfAffine = toAffineCover f ⋁Df≡W + + hasAffineCoverCompOpenOfAffine : hasAffineCover ⟦ W ⟧ᶜᵒ + hasAffineCoverCompOpenOfAffine = PT.map truncHelper ([]surjective w) + where + truncHelper : Σ[ n,f ∈ Σ ℕ (FinVec (fst R)) ] [ n,f ] ≡ w → AffineCover ⟦ W ⟧ᶜᵒ + truncHelper ((n , f) , [n,f]≡w) = makeAffineCoverCompOpenOfAffine f (ZL.⋁D≡ R f ∙ [n,f]≡w) + + isQcQsSchemeCompOpenOfAffine : isQcQsScheme ⟦ W ⟧ᶜᵒ + fst isQcQsSchemeCompOpenOfAffine = presLocalCompactOpen _ _ (isSubcanonicalZariskiCoverage R) + snd isQcQsSchemeCompOpenOfAffine = hasAffineCoverCompOpenOfAffine diff --git a/Cubical/AlgebraicGeometry/Functorial/ZFunctors/QcQsScheme.agda b/Cubical/AlgebraicGeometry/Functorial/ZFunctors/QcQsScheme.agda new file mode 100644 index 000000000..d8f9a77c2 --- /dev/null +++ b/Cubical/AlgebraicGeometry/Functorial/ZFunctors/QcQsScheme.agda @@ -0,0 +1,82 @@ +{- + + A qcqs-scheme is a ℤ-functor that is local (a Zariski-sheaf) + and has an affine cover, where the notion of cover is given + by the lattice structure of compact open subfunctors + +-} + +{-# OPTIONS --safe --lossy-unification #-} +module Cubical.AlgebraicGeometry.Functorial.ZFunctors.QcQsScheme where + +open import Cubical.Foundations.Prelude +open import Cubical.Foundations.Equiv +open import Cubical.Foundations.Isomorphism +open import Cubical.Foundations.Function +open import Cubical.Foundations.Powerset +open import Cubical.Foundations.HLevels + + +open import Cubical.Functions.FunExtEquiv + +open import Cubical.Data.Sigma +open import Cubical.Data.Nat using (ℕ) + +open import Cubical.Data.FinData + +open import Cubical.Algebra.CommRing +open import Cubical.Algebra.Semilattice +open import Cubical.Algebra.Lattice +open import Cubical.Algebra.DistLattice +open import Cubical.Algebra.DistLattice.BigOps + +open import Cubical.AlgebraicGeometry.Functorial.ZFunctors.Base +open import Cubical.AlgebraicGeometry.Functorial.ZFunctors.CompactOpen + +open import Cubical.Categories.Category renaming (isIso to isIsoC) +open import Cubical.Categories.Functor +open import Cubical.Categories.Site.Instances.ZariskiCommRing + +open import Cubical.HITs.PropositionalTruncation as PT + + +module _ {ℓ : Level} (X : ℤFunctor {ℓ = ℓ}) where + open Functor + open DistLatticeStr ⦃...⦄ + open Join (CompOpenDistLattice .F-ob X) + open JoinSemilattice (Lattice→JoinSemilattice (DistLattice→Lattice (CompOpenDistLattice .F-ob X))) + private instance _ = (CompOpenDistLattice .F-ob X) .snd + + + record AffineCover : Type (ℓ-suc ℓ) where + field + n : ℕ + U : FinVec (CompactOpen X) n + covers : ⋁ U ≡ 1l -- TODO: equivalent to X ≡ ⟦ ⋁ U ⟧ᶜᵒ + isAffineU : ∀ i → isAffineCompactOpen (U i) + + hasAffineCover : Type (ℓ-suc ℓ) + hasAffineCover = ∥ AffineCover ∥₁ + + +module _ {ℓ : Level} where + -- definition of quasi-compact, quasi-separated schemes + isQcQsScheme : ℤFunctor → Type (ℓ-suc ℓ) + isQcQsScheme X = isLocal X × hasAffineCover X + + -- affine schemes are qcqs-schemes + module _ (A : CommRing ℓ) where + open AffineCover + open DistLatticeStr ⦃...⦄ + private instance _ = (CompOpenDistLattice ⟅ Sp ⟅ A ⟆ ⟆) .snd + + -- the canonical one element affine cover of a representable + singlAffineCover : AffineCover (Sp ⟅ A ⟆) + n singlAffineCover = 1 + U singlAffineCover zero = 1l + covers singlAffineCover = ∨lRid _ + isAffineU singlAffineCover zero = ∣ A , compOpenTopNatIso (Sp ⟅ A ⟆) ∣₁ + + isQcQsSchemeAffine : isQcQsScheme (Sp ⟅ A ⟆) + fst isQcQsSchemeAffine = isSubcanonicalZariskiCoverage A + snd isQcQsSchemeAffine = ∣ singlAffineCover ∣₁ diff --git a/Cubical/Algebra/ZariskiLattice/Base.agda b/Cubical/AlgebraicGeometry/ZariskiLattice/Base.agda similarity index 99% rename from Cubical/Algebra/ZariskiLattice/Base.agda rename to Cubical/AlgebraicGeometry/ZariskiLattice/Base.agda index 06bb4f790..273a85f06 100644 --- a/Cubical/Algebra/ZariskiLattice/Base.agda +++ b/Cubical/AlgebraicGeometry/ZariskiLattice/Base.agda @@ -1,5 +1,5 @@ {-# OPTIONS --safe --lossy-unification #-} -module Cubical.Algebra.ZariskiLattice.Base where +module Cubical.AlgebraicGeometry.ZariskiLattice.Base where open import Cubical.Foundations.Prelude diff --git a/Cubical/Algebra/ZariskiLattice/Properties.agda b/Cubical/AlgebraicGeometry/ZariskiLattice/Properties.agda similarity index 97% rename from Cubical/Algebra/ZariskiLattice/Properties.agda rename to Cubical/AlgebraicGeometry/ZariskiLattice/Properties.agda index ba9813b86..3fafe859b 100644 --- a/Cubical/Algebra/ZariskiLattice/Properties.agda +++ b/Cubical/AlgebraicGeometry/ZariskiLattice/Properties.agda @@ -1,5 +1,5 @@ {-# OPTIONS --safe --lossy-unification #-} -module Cubical.Algebra.ZariskiLattice.Properties where +module Cubical.AlgebraicGeometry.ZariskiLattice.Properties where open import Cubical.Foundations.Prelude @@ -25,8 +25,8 @@ open import Cubical.Algebra.Lattice open import Cubical.Algebra.DistLattice open import Cubical.Algebra.DistLattice.Downset -open import Cubical.Algebra.ZariskiLattice.Base -open import Cubical.Algebra.ZariskiLattice.UniversalProperty +open import Cubical.AlgebraicGeometry.ZariskiLattice.Base +open import Cubical.AlgebraicGeometry.ZariskiLattice.UniversalProperty open import Cubical.HITs.SetQuotients as SQ import Cubical.HITs.PropositionalTruncation as PT diff --git a/Cubical/Algebra/ZariskiLattice/StructureSheaf.agda b/Cubical/AlgebraicGeometry/ZariskiLattice/StructureSheaf.agda similarity index 98% rename from Cubical/Algebra/ZariskiLattice/StructureSheaf.agda rename to Cubical/AlgebraicGeometry/ZariskiLattice/StructureSheaf.agda index b70970886..0ca759738 100644 --- a/Cubical/Algebra/ZariskiLattice/StructureSheaf.agda +++ b/Cubical/AlgebraicGeometry/ZariskiLattice/StructureSheaf.agda @@ -8,7 +8,7 @@ -} {-# OPTIONS --safe --lossy-unification #-} -module Cubical.Algebra.ZariskiLattice.StructureSheaf where +module Cubical.AlgebraicGeometry.ZariskiLattice.StructureSheaf where open import Cubical.Foundations.Prelude @@ -56,8 +56,8 @@ open import Cubical.Algebra.Lattice open import Cubical.Algebra.DistLattice open import Cubical.Algebra.DistLattice.Basis open import Cubical.Algebra.DistLattice.BigOps -open import Cubical.Algebra.ZariskiLattice.Base -open import Cubical.Algebra.ZariskiLattice.UniversalProperty +open import Cubical.AlgebraicGeometry.ZariskiLattice.Base +open import Cubical.AlgebraicGeometry.ZariskiLattice.UniversalProperty open import Cubical.Categories.Category.Base hiding (_[_,_]) open import Cubical.Categories.Functor diff --git a/Cubical/Algebra/ZariskiLattice/StructureSheafPullback.agda b/Cubical/AlgebraicGeometry/ZariskiLattice/StructureSheafPullback.agda similarity index 98% rename from Cubical/Algebra/ZariskiLattice/StructureSheafPullback.agda rename to Cubical/AlgebraicGeometry/ZariskiLattice/StructureSheafPullback.agda index 61bc82976..41695c786 100644 --- a/Cubical/Algebra/ZariskiLattice/StructureSheafPullback.agda +++ b/Cubical/AlgebraicGeometry/ZariskiLattice/StructureSheafPullback.agda @@ -9,7 +9,7 @@ -} {-# OPTIONS --safe --lossy-unification #-} -module Cubical.Algebra.ZariskiLattice.StructureSheafPullback where +module Cubical.AlgebraicGeometry.ZariskiLattice.StructureSheafPullback where open import Cubical.Foundations.Prelude @@ -59,8 +59,8 @@ open import Cubical.Algebra.Lattice open import Cubical.Algebra.DistLattice open import Cubical.Algebra.DistLattice.Basis open import Cubical.Algebra.DistLattice.BigOps -open import Cubical.Algebra.ZariskiLattice.Base -open import Cubical.Algebra.ZariskiLattice.UniversalProperty +open import Cubical.AlgebraicGeometry.ZariskiLattice.Base +open import Cubical.AlgebraicGeometry.ZariskiLattice.UniversalProperty open import Cubical.Categories.Category.Base hiding (_[_,_]) open import Cubical.Categories.Functor diff --git a/Cubical/Algebra/ZariskiLattice/UniversalProperty.agda b/Cubical/AlgebraicGeometry/ZariskiLattice/UniversalProperty.agda similarity index 99% rename from Cubical/Algebra/ZariskiLattice/UniversalProperty.agda rename to Cubical/AlgebraicGeometry/ZariskiLattice/UniversalProperty.agda index 4355fe899..53b4fc4f5 100644 --- a/Cubical/Algebra/ZariskiLattice/UniversalProperty.agda +++ b/Cubical/AlgebraicGeometry/ZariskiLattice/UniversalProperty.agda @@ -1,5 +1,5 @@ {-# OPTIONS --safe --lossy-unification #-} -module Cubical.Algebra.ZariskiLattice.UniversalProperty where +module Cubical.AlgebraicGeometry.ZariskiLattice.UniversalProperty where open import Cubical.Foundations.Prelude @@ -40,7 +40,7 @@ open import Cubical.Algebra.DistLattice.Basis open import Cubical.Algebra.DistLattice.BigOps open import Cubical.Algebra.Matrix -open import Cubical.Algebra.ZariskiLattice.Base +open import Cubical.AlgebraicGeometry.ZariskiLattice.Base open import Cubical.HITs.SetQuotients as SQ open import Cubical.HITs.PropositionalTruncation as PT diff --git a/Cubical/Categories/Instances/ZFunctors.agda b/Cubical/Categories/Instances/ZFunctors.agda index faec14ebe..5aef61581 100644 --- a/Cubical/Categories/Instances/ZFunctors.agda +++ b/Cubical/Categories/Instances/ZFunctors.agda @@ -1,795 +1,24 @@ -{- - - The impredicative way to define functorial qcqs-schemes (over Spec(ℤ)) - --} -{-# OPTIONS --safe --lossy-unification #-} +{-# OPTIONS --safe #-} module Cubical.Categories.Instances.ZFunctors where -open import Cubical.Foundations.Prelude -open import Cubical.Foundations.Equiv -open import Cubical.Foundations.Isomorphism -open import Cubical.Foundations.Function -open import Cubical.Foundations.Powerset -open import Cubical.Foundations.HLevels - - -open import Cubical.Functions.FunExtEquiv - -open import Cubical.Data.Sigma -open import Cubical.Data.Nat using (ℕ) - -open import Cubical.Data.FinData - -open import Cubical.Algebra.Ring -open import Cubical.Algebra.CommRing -open import Cubical.Algebra.CommRing.Localisation -open import Cubical.Algebra.CommRing.RadicalIdeal -open import Cubical.Algebra.Semilattice -open import Cubical.Algebra.Lattice -open import Cubical.Algebra.DistLattice -open import Cubical.Algebra.DistLattice.BigOps -open import Cubical.Algebra.ZariskiLattice.Base -open import Cubical.Algebra.ZariskiLattice.UniversalProperty -open import Cubical.Algebra.ZariskiLattice.Properties - -open import Cubical.Categories.Category renaming (isIso to isIsoC) -open import Cubical.Categories.Functor -open import Cubical.Categories.Instances.Sets -open import Cubical.Categories.Instances.CommRings -open import Cubical.Categories.Instances.DistLattice -open import Cubical.Categories.Instances.DistLattices -open import Cubical.Categories.Instances.Functors -open import Cubical.Categories.Site.Cover -open import Cubical.Categories.Site.Coverage -open import Cubical.Categories.Site.Sheaf -open import Cubical.Categories.Site.Instances.ZariskiCommRing -open import Cubical.Categories.NaturalTransformation -open import Cubical.Categories.Yoneda - - -open import Cubical.HITs.PropositionalTruncation as PT -open import Cubical.HITs.SetQuotients as SQ - -open import Cubical.Relation.Binary.Order.Poset - -open Category hiding (_∘_) renaming (_⋆_ to _⋆c_) - -private - variable - ℓ ℓ' ℓ'' : Level - - -module _ {ℓ : Level} where - - open Functor - open NatTrans - open CommRingStr ⦃...⦄ - open IsRingHom - - -- using the naming conventions of Demazure & Gabriel - ℤFunctor = Functor (CommRingsCategory {ℓ = ℓ}) (SET ℓ) - ℤFUNCTOR = FUNCTOR (CommRingsCategory {ℓ = ℓ}) (SET ℓ) - - -- Yoneda in the notation of Demazure & Gabriel, - -- uses that double op is original category definitionally - Sp : Functor (CommRingsCategory {ℓ = ℓ} ^op) ℤFUNCTOR - Sp = YO {C = (CommRingsCategory {ℓ = ℓ} ^op)} - - -- the forgetful functor - -- aka the affine line - -- (aka the representable of ℤ[x]) - 𝔸¹ : ℤFunctor - 𝔸¹ = ForgetfulCommRing→Set - - -- the global sections functor - 𝓞 : Functor ℤFUNCTOR (CommRingsCategory {ℓ = ℓ-suc ℓ} ^op) - fst (F-ob 𝓞 X) = X ⇒ 𝔸¹ - - -- ring struncture induced by internal ring object 𝔸¹ - N-ob (CommRingStr.0r (snd (F-ob 𝓞 X))) A _ = 0r - where instance _ = A .snd - N-hom (CommRingStr.0r (snd (F-ob 𝓞 X))) φ = funExt λ _ → sym (φ .snd .pres0) - - N-ob (CommRingStr.1r (snd (F-ob 𝓞 X))) A _ = 1r - where instance _ = A .snd - N-hom (CommRingStr.1r (snd (F-ob 𝓞 X))) φ = funExt λ _ → sym (φ .snd .pres1) - - N-ob ((snd (F-ob 𝓞 X) CommRingStr.+ α) β) A x = α .N-ob A x + β .N-ob A x - where instance _ = A .snd - N-hom ((snd (F-ob 𝓞 X) CommRingStr.+ α) β) {x = A} {y = B} φ = funExt path - where - instance - _ = A .snd - _ = B .snd - path : ∀ x → α .N-ob B (X .F-hom φ x) + β .N-ob B (X .F-hom φ x) - ≡ φ .fst (α .N-ob A x + β .N-ob A x) - path x = α .N-ob B (X .F-hom φ x) + β .N-ob B (X .F-hom φ x) - ≡⟨ cong₂ _+_ (funExt⁻ (α .N-hom φ) x) (funExt⁻ (β .N-hom φ) x) ⟩ - φ .fst (α .N-ob A x) + φ .fst (β .N-ob A x) - ≡⟨ sym (φ .snd .pres+ _ _) ⟩ - φ .fst (α .N-ob A x + β .N-ob A x) ∎ - - N-ob ((snd (F-ob 𝓞 X) CommRingStr.· α) β) A x = α .N-ob A x · β .N-ob A x - where instance _ = A .snd - N-hom ((snd (F-ob 𝓞 X) CommRingStr.· α) β) {x = A} {y = B} φ = funExt path - where - instance - _ = A .snd - _ = B .snd - path : ∀ x → α .N-ob B (X .F-hom φ x) · β .N-ob B (X .F-hom φ x) - ≡ φ .fst (α .N-ob A x · β .N-ob A x) - path x = α .N-ob B (X .F-hom φ x) · β .N-ob B (X .F-hom φ x) - ≡⟨ cong₂ _·_ (funExt⁻ (α .N-hom φ) x) (funExt⁻ (β .N-hom φ) x) ⟩ - φ .fst (α .N-ob A x) · φ .fst (β .N-ob A x) - ≡⟨ sym (φ .snd .pres· _ _) ⟩ - φ .fst (α .N-ob A x · β .N-ob A x) ∎ - - N-ob ((CommRingStr.- snd (F-ob 𝓞 X)) α) A x = - α .N-ob A x - where instance _ = A .snd - N-hom ((CommRingStr.- snd (F-ob 𝓞 X)) α) {x = A} {y = B} φ = funExt path - where - instance - _ = A .snd - _ = B .snd - path : ∀ x → - α .N-ob B (X .F-hom φ x) ≡ φ .fst (- α .N-ob A x) - path x = - α .N-ob B (X .F-hom φ x) ≡⟨ cong -_ (funExt⁻ (α .N-hom φ) x) ⟩ - - φ .fst (α .N-ob A x) ≡⟨ sym (φ .snd .pres- _) ⟩ - φ .fst (- α .N-ob A x) ∎ - - CommRingStr.isCommRing (snd (F-ob 𝓞 X)) = makeIsCommRing - isSetNatTrans - (λ _ _ _ → makeNatTransPath (funExt₂ λ A _ → A .snd .CommRingStr.+Assoc _ _ _)) - (λ _ → makeNatTransPath (funExt₂ λ A _ → A .snd .CommRingStr.+IdR _)) - (λ _ → makeNatTransPath (funExt₂ λ A _ → A .snd .CommRingStr.+InvR _)) - (λ _ _ → makeNatTransPath (funExt₂ λ A _ → A .snd .CommRingStr.+Comm _ _)) - (λ _ _ _ → makeNatTransPath (funExt₂ λ A _ → A .snd .CommRingStr.·Assoc _ _ _)) - (λ _ → makeNatTransPath (funExt₂ λ A _ → A .snd .CommRingStr.·IdR _)) - (λ _ _ _ → makeNatTransPath (funExt₂ λ A _ → A .snd .CommRingStr.·DistR+ _ _ _)) - (λ _ _ → makeNatTransPath (funExt₂ λ A _ → A .snd .CommRingStr.·Comm _ _)) - - -- action on natural transformations - fst (F-hom 𝓞 α) = α ●ᵛ_ - pres0 (snd (F-hom 𝓞 α)) = makeNatTransPath (funExt₂ λ _ _ → refl) - pres1 (snd (F-hom 𝓞 α)) = makeNatTransPath (funExt₂ λ _ _ → refl) - pres+ (snd (F-hom 𝓞 α)) _ _ = makeNatTransPath (funExt₂ λ _ _ → refl) - pres· (snd (F-hom 𝓞 α)) _ _ = makeNatTransPath (funExt₂ λ _ _ → refl) - pres- (snd (F-hom 𝓞 α)) _ = makeNatTransPath (funExt₂ λ _ _ → refl) - - -- functoriality of 𝓞 - F-id 𝓞 = RingHom≡ (funExt λ _ → makeNatTransPath (funExt₂ λ _ _ → refl)) - F-seq 𝓞 _ _ = RingHom≡ (funExt λ _ → makeNatTransPath (funExt₂ λ _ _ → refl)) - - - --- There is an adjunction 𝓞 ⊣ᵢ Sp --- (relative to the inclusion i : CommRing ℓ → CommRing (ℓ+1)) --- between the "global sections functor" 𝓞 --- and the fully-faithful embedding of affines Sp, --- whose counit is a natural isomorphism -module AdjBij where - - open Functor - open NatTrans - open Iso - open IsRingHom - - private module _ {A : CommRing ℓ} {X : ℤFunctor {ℓ}} where - _♭ : CommRingHom A (𝓞 .F-ob X) → X ⇒ Sp .F-ob A - fst (N-ob (φ ♭) B x) a = φ .fst a .N-ob B x - - pres0 (snd (N-ob (φ ♭) B x)) = cong (λ y → y .N-ob B x) (φ .snd .pres0) - pres1 (snd (N-ob (φ ♭) B x)) = cong (λ y → y .N-ob B x) (φ .snd .pres1) - pres+ (snd (N-ob (φ ♭) B x)) _ _ = cong (λ y → y .N-ob B x) (φ .snd .pres+ _ _) - pres· (snd (N-ob (φ ♭) B x)) _ _ = cong (λ y → y .N-ob B x) (φ .snd .pres· _ _) - pres- (snd (N-ob (φ ♭) B x)) _ = cong (λ y → y .N-ob B x) (φ .snd .pres- _) - - N-hom (φ ♭) ψ = funExt (λ x → RingHom≡ (funExt λ a → funExt⁻ (φ .fst a .N-hom ψ) x)) - - - -- the other direction is just precomposition modulo Yoneda - _♯ : X ⇒ Sp .F-ob A → CommRingHom A (𝓞 .F-ob X) - fst (α ♯) a = α ●ᵛ yonedaᴾ 𝔸¹ A .inv a - - pres0 (snd (α ♯)) = makeNatTransPath (funExt₂ λ B x → α .N-ob B x .snd .pres0) - pres1 (snd (α ♯)) = makeNatTransPath (funExt₂ λ B x → α .N-ob B x .snd .pres1) - pres+ (snd (α ♯)) _ _ = makeNatTransPath (funExt₂ λ B x → α .N-ob B x .snd .pres+ _ _) - pres· (snd (α ♯)) _ _ = makeNatTransPath (funExt₂ λ B x → α .N-ob B x .snd .pres· _ _) - pres- (snd (α ♯)) _ = makeNatTransPath (funExt₂ λ B x → α .N-ob B x .snd .pres- _) - - - -- the two maps are inverse to each other - ♭♯Id : ∀ (α : X ⇒ Sp .F-ob A) → ((α ♯) ♭) ≡ α - ♭♯Id _ = makeNatTransPath (funExt₂ λ _ _ → RingHom≡ (funExt (λ _ → refl))) - - ♯♭Id : ∀ (φ : CommRingHom A (𝓞 .F-ob X)) → ((φ ♭) ♯) ≡ φ - ♯♭Id _ = RingHom≡ (funExt λ _ → makeNatTransPath (funExt₂ λ _ _ → refl)) - - - -- we get a relative adjunction 𝓞 ⊣ᵢ Sp - -- with respect to the inclusion i : CommRing ℓ → CommRing (ℓ+1) - 𝓞⊣SpIso : {A : CommRing ℓ} {X : ℤFunctor {ℓ}} - → Iso (CommRingHom A (𝓞 .F-ob X)) (X ⇒ Sp .F-ob A) - fun 𝓞⊣SpIso = _♭ - inv 𝓞⊣SpIso = _♯ - rightInv 𝓞⊣SpIso = ♭♯Id - leftInv 𝓞⊣SpIso = ♯♭Id - - 𝓞⊣SpNatℤFunctor : {A : CommRing ℓ} {X Y : ℤFunctor {ℓ}} (α : X ⇒ Sp .F-ob A) (β : Y ⇒ X) - → (β ●ᵛ α) ♯ ≡ (𝓞 .F-hom β) ∘cr (α ♯) - 𝓞⊣SpNatℤFunctor _ _ = RingHom≡ (funExt (λ _ → makeNatTransPath (funExt₂ (λ _ _ → refl)))) - - 𝓞⊣SpNatCommRing : {X : ℤFunctor {ℓ}} {A B : CommRing ℓ} - (φ : CommRingHom A (𝓞 .F-ob X)) (ψ : CommRingHom B A) - → (φ ∘cr ψ) ♭ ≡ (φ ♭) ●ᵛ Sp .F-hom ψ - 𝓞⊣SpNatCommRing _ _ = makeNatTransPath (funExt₂ λ _ _ → RingHom≡ (funExt (λ _ → refl))) - - -- the counit is an equivalence - private - ε : (A : CommRing ℓ) → CommRingHom A ((𝓞 ∘F Sp) .F-ob A) - ε A = (idTrans (Sp .F-ob A)) ♯ - - 𝓞⊣SpCounitEquiv : (A : CommRing ℓ) → CommRingEquiv A ((𝓞 ∘F Sp) .F-ob A) - fst (𝓞⊣SpCounitEquiv A) = isoToEquiv theIso - where - theIso : Iso (A .fst) ((𝓞 ∘F Sp) .F-ob A .fst) - 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 - - --- Affine schemes -module _ {ℓ : Level} where - open Functor - - isAffine : (X : ℤFunctor) → Type (ℓ-suc ℓ) - isAffine X = ∃[ A ∈ CommRing ℓ ] NatIso (Sp .F-ob A) X - - -- TODO: 𝔸¹ ≅ Sp ℤ[x] and 𝔾ₘ ≅ Sp ℤ[x,x⁻¹] ≅ D(x) ↪ 𝔸¹ as first examples of affine schemes - - --- The unit is an equivalence iff the ℤ-functor is affine. --- Unfortunately, we can't give a natural transformation --- X ⇒ Sp (𝓞 X), because the latter ℤ-functor lives in a higher universe. --- We can however give terms that look just like the unit, --- giving us an alternative def. of affine ℤ-functors -private module AffineDefs {ℓ : Level} where - open Functor - open NatTrans - open Iso - open IsRingHom - η : (X : ℤFunctor) (A : CommRing ℓ) → X .F-ob A .fst → CommRingHom (𝓞 .F-ob X) A - fst (η X A x) α = α .N-ob A x - pres0 (snd (η X A x)) = refl - pres1 (snd (η X A x)) = refl - pres+ (snd (η X A x)) _ _ = refl - pres· (snd (η X A x)) _ _ = refl - pres- (snd (η X A x)) _ = refl - - -- this is basically a natural transformation - ηObHom : (X : ℤFunctor) {A B : CommRing ℓ} (φ : CommRingHom A B) - → η X B ∘ (X .F-hom φ) ≡ (φ ∘cr_) ∘ η X A - ηObHom X φ = funExt (λ x → RingHom≡ (funExt λ α → funExt⁻ (α .N-hom φ) x)) - - -- can only state equality on object part, but that would be enough - ηHom : {X Y : ℤFunctor} (α : X ⇒ Y) (A : CommRing ℓ) (x : X .F-ob A .fst) - → η Y A (α .N-ob A x) ≡ η X A x ∘cr 𝓞 .F-hom α - ηHom _ _ _ = RingHom≡ refl - - isAffine' : (X : ℤFunctor) → Type (ℓ-suc ℓ) - isAffine' X = ∀ (A : CommRing ℓ) → isEquiv (η X A) - -- TODO: isAffine → isAffine' - - --- compact opens and affine covers -module _ {ℓ : Level} where - - open Iso - open Functor - open NatTrans - open NatIso - open DistLatticeStr ⦃...⦄ - open CommRingStr ⦃...⦄ - open IsRingHom - open IsLatticeHom - open ZarLat - open ZarLatUniversalProp - - -- the Zariski lattice functor classifying compact open subobjects - ZarLatFun : ℤFunctor {ℓ = ℓ} - F-ob ZarLatFun A = ZL A , SQ.squash/ - F-hom ZarLatFun φ = inducedZarLatHom φ .fst - F-id ZarLatFun {A} = cong fst (inducedZarLatHomId A) - F-seq ZarLatFun φ ψ = cong fst (inducedZarLatHomSeq φ ψ) - - -- this is a separated presheaf - -- (TODO: prove this a sheaf) - isSeparatedZarLatFun : isSeparated zariskiCoverage ZarLatFun - isSeparatedZarLatFun A (unimodvec n f 1∈⟨f₁,⋯,fₙ⟩) u w uRest≡wRest = - u ≡⟨ sym (∧lLid _) ⟩ - 1l ∧l u ≡⟨ congL _∧l_ D1≡⋁Dfᵢ ⟩ - (⋁ (D A ∘ f)) ∧l u ≡⟨ ⋁Meetldist _ _ ⟩ - ⋁ (λ i → D A (f i) ∧l u) ≡⟨ ⋁Ext Dfᵢ∧u≡Dfᵢ∧w ⟩ - ⋁ (λ i → D A (f i) ∧l w) ≡⟨ sym (⋁Meetldist _ _) ⟩ - (⋁ (D A ∘ f)) ∧l w ≡⟨ congL _∧l_ (sym D1≡⋁Dfᵢ) ⟩ - 1l ∧l w ≡⟨ ∧lLid _ ⟩ - w ∎ - where - open Join (ZariskiLattice A) - open JoinSemilattice (Lattice→JoinSemilattice (DistLattice→Lattice (ZariskiLattice A))) - using (IndPoset) - open LatticeTheory (DistLattice→Lattice (ZariskiLattice A)) - open PosetStr (IndPoset .snd) - open IsSupport (isSupportD A) - open RadicalIdeal A - instance - _ = A .snd - _ = ZariskiLattice A .snd - - D1≡⋁Dfᵢ : 1l ≡ ⋁ (D A ∘ f) - D1≡⋁Dfᵢ = is-antisym _ _ - (supportRadicalIneq f 1r (∈→∈√ _ _ 1∈⟨f₁,⋯,fₙ⟩)) - (1lRightAnnihilates∨l _) - - Dfᵢ∧u≡Dfᵢ∧w : ∀ i → D A (f i) ∧l u ≡ D A (f i) ∧l w - Dfᵢ∧u≡Dfᵢ∧w i = - D A (f i) ∧l u - ≡⟨ sym (cong fst (funExt⁻ (cong fst toLocToDown≡ToDown) u)) ⟩ - locToDownHom .fst (inducedZarLatHom /1AsCommRingHom .fst u) .fst - ≡⟨ cong (λ x → locToDownHom .fst x .fst) (uRest≡wRest i) ⟩ - locToDownHom .fst (inducedZarLatHom /1AsCommRingHom .fst w) .fst - ≡⟨ cong fst (funExt⁻ (cong fst toLocToDown≡ToDown) w) ⟩ - D A (f i) ∧l w ∎ - where - open InvertingElementsBase.UniversalProp A (f i) - open LocDownSetIso A (f i) - - CompactOpen : ℤFunctor → Type (ℓ-suc ℓ) - CompactOpen X = X ⇒ ZarLatFun - - -- the induced subfunctor - ⟦_⟧ᶜᵒ : {X : ℤFunctor} (U : CompactOpen X) → ℤFunctor - F-ob (⟦_⟧ᶜᵒ {X = X} U) A = (Σ[ x ∈ X .F-ob A .fst ] U .N-ob A x ≡ D A 1r) - , isSetΣSndProp (X .F-ob A .snd) λ _ → squash/ _ _ - where instance _ = snd A - F-hom (⟦_⟧ᶜᵒ {X = X} U) {x = A} {y = B} φ (x , Ux≡D1) = (X .F-hom φ x) , path - where - instance - _ = A .snd - _ = B .snd - open IsLatticeHom - path : U .N-ob B (X .F-hom φ x) ≡ D B 1r - path = U .N-ob B (X .F-hom φ x) ≡⟨ funExt⁻ (U .N-hom φ) x ⟩ - ZarLatFun .F-hom φ (U .N-ob A x) ≡⟨ cong (ZarLatFun .F-hom φ) Ux≡D1 ⟩ - ZarLatFun .F-hom φ (D A 1r) ≡⟨ inducedZarLatHom φ .snd .pres1 ⟩ - D B 1r ∎ - F-id (⟦_⟧ᶜᵒ {X = X} U) = funExt (λ x → Σ≡Prop (λ _ → squash/ _ _) - (funExt⁻ (X .F-id) (x .fst))) - F-seq (⟦_⟧ᶜᵒ {X = X} U) φ ψ = funExt (λ x → Σ≡Prop (λ _ → squash/ _ _) - (funExt⁻ (X .F-seq φ ψ) (x .fst))) - - - isAffineCompactOpen : {X : ℤFunctor} (U : CompactOpen X) → Type (ℓ-suc ℓ) - isAffineCompactOpen U = isAffine ⟦ U ⟧ᶜᵒ - - -- TODO: define basic opens D(f) ↪ Sp A and prove ⟦ D(f) ⟧ᶜᵒ ≅ Sp A[1/f] - - -- the (big) dist. lattice of compact opens - CompOpenDistLattice : Functor ℤFUNCTOR (DistLatticesCategory {ℓ = ℓ-suc ℓ} ^op) - fst (F-ob CompOpenDistLattice X) = CompactOpen X - - -- lattice structure induce by internal lattice object ZarLatFun - N-ob (DistLatticeStr.0l (snd (F-ob CompOpenDistLattice X))) A _ = 0l - where instance _ = ZariskiLattice A .snd - N-hom (DistLatticeStr.0l (snd (F-ob CompOpenDistLattice X))) _ = funExt λ _ → refl - - N-ob (DistLatticeStr.1l (snd (F-ob CompOpenDistLattice X))) A _ = 1l - where instance _ = ZariskiLattice A .snd - N-hom (DistLatticeStr.1l (snd (F-ob CompOpenDistLattice X))) {x = A} {y = B} φ = funExt λ _ → path - where - instance - _ = A .snd - _ = B .snd - _ = ZariskiLattice B .snd - path : D B 1r ≡ D B (φ .fst 1r) ∨l 0l - path = cong (D B) (sym (φ .snd .pres1)) ∙ sym (∨lRid _) - - N-ob ((snd (F-ob CompOpenDistLattice X) DistLatticeStr.∨l U) V) A x = U .N-ob A x ∨l V .N-ob A x - where instance _ = ZariskiLattice A .snd - N-hom ((snd (F-ob CompOpenDistLattice X) DistLatticeStr.∨l U) V) {x = A} {y = B} φ = funExt path - where - instance - _ = ZariskiLattice A .snd - _ = ZariskiLattice B .snd - path : ∀ x → U .N-ob B (X .F-hom φ x) ∨l V .N-ob B (X .F-hom φ x) - ≡ ZarLatFun .F-hom φ (U .N-ob A x ∨l V .N-ob A x) - path x = U .N-ob B (X .F-hom φ x) ∨l V .N-ob B (X .F-hom φ x) - ≡⟨ cong₂ _∨l_ (funExt⁻ (U .N-hom φ) x) (funExt⁻ (V .N-hom φ) x) ⟩ - ZarLatFun .F-hom φ (U .N-ob A x) ∨l ZarLatFun .F-hom φ (V .N-ob A x) - ≡⟨ sym (inducedZarLatHom φ .snd .pres∨l _ _) ⟩ - ZarLatFun .F-hom φ (U .N-ob A x ∨l V .N-ob A x) ∎ - - N-ob ((snd (F-ob CompOpenDistLattice X) DistLatticeStr.∧l U) V) A x = U .N-ob A x ∧l V .N-ob A x - where instance _ = ZariskiLattice A .snd - N-hom ((snd (F-ob CompOpenDistLattice X) DistLatticeStr.∧l U) V) {x = A} {y = B} φ = funExt path - where - instance - _ = ZariskiLattice A .snd - _ = ZariskiLattice B .snd - path : ∀ x → U .N-ob B (X .F-hom φ x) ∧l V .N-ob B (X .F-hom φ x) - ≡ ZarLatFun .F-hom φ (U .N-ob A x ∧l V .N-ob A x) - path x = U .N-ob B (X .F-hom φ x) ∧l V .N-ob B (X .F-hom φ x) - ≡⟨ cong₂ _∧l_ (funExt⁻ (U .N-hom φ) x) (funExt⁻ (V .N-hom φ) x) ⟩ - ZarLatFun .F-hom φ (U .N-ob A x) ∧l ZarLatFun .F-hom φ (V .N-ob A x) - ≡⟨ sym (inducedZarLatHom φ .snd .pres∧l _ _) ⟩ - ZarLatFun .F-hom φ (U .N-ob A x ∧l V .N-ob A x) ∎ - - DistLatticeStr.isDistLattice (snd (F-ob CompOpenDistLattice X)) = makeIsDistLattice∧lOver∨l - isSetNatTrans - (λ _ _ _ → makeNatTransPath (funExt₂ - (λ A _ → ZariskiLattice A .snd .DistLatticeStr.∨lAssoc _ _ _))) - (λ _ → makeNatTransPath (funExt₂ (λ A _ → ZariskiLattice A .snd .DistLatticeStr.∨lRid _))) - (λ _ _ → makeNatTransPath (funExt₂ (λ A _ → ZariskiLattice A .snd .DistLatticeStr.∨lComm _ _))) - (λ _ _ _ → makeNatTransPath (funExt₂ - (λ A _ → ZariskiLattice A .snd .DistLatticeStr.∧lAssoc _ _ _))) - (λ _ → makeNatTransPath (funExt₂ (λ A _ → ZariskiLattice A .snd .DistLatticeStr.∧lRid _))) - (λ _ _ → makeNatTransPath (funExt₂ (λ A _ → ZariskiLattice A .snd .DistLatticeStr.∧lComm _ _))) - (λ _ _ → makeNatTransPath (funExt₂ -- don't know why ∧lAbsorb∨l doesn't work - (λ A _ → ZariskiLattice A .snd .DistLatticeStr.absorb _ _ .snd))) - (λ _ _ _ → makeNatTransPath (funExt₂ -- same here - (λ A _ → ZariskiLattice A .snd .DistLatticeStr.∧l-dist-∨l _ _ _ .fst))) - - -- (contravariant) action on morphisms - fst (F-hom CompOpenDistLattice α) = α ●ᵛ_ - pres0 (snd (F-hom CompOpenDistLattice α)) = makeNatTransPath (funExt₂ λ _ _ → refl) - pres1 (snd (F-hom CompOpenDistLattice α)) = makeNatTransPath (funExt₂ λ _ _ → refl) - pres∨l (snd (F-hom CompOpenDistLattice α)) _ _ = makeNatTransPath (funExt₂ λ _ _ → refl) - pres∧l (snd (F-hom CompOpenDistLattice α)) _ _ = makeNatTransPath (funExt₂ λ _ _ → refl) - - -- functoriality - F-id CompOpenDistLattice = LatticeHom≡f _ _ - (funExt λ _ → makeNatTransPath (funExt₂ λ _ _ → refl)) - F-seq CompOpenDistLattice _ _ = LatticeHom≡f _ _ - (funExt λ _ → makeNatTransPath (funExt₂ λ _ _ → refl)) - - - module _ (X : ℤFunctor) where - open isIsoC - private instance _ = (CompOpenDistLattice .F-ob X) .snd - - compOpenTopNatIso : NatIso X ⟦ 1l ⟧ᶜᵒ - N-ob (trans compOpenTopNatIso) _ φ = φ , refl - N-hom (trans compOpenTopNatIso) _ = funExt λ _ → Σ≡Prop (λ _ → squash/ _ _) refl - inv (nIso compOpenTopNatIso B) = fst - sec (nIso compOpenTopNatIso B) = funExt λ _ → Σ≡Prop (λ _ → squash/ _ _) refl - ret (nIso compOpenTopNatIso B) = funExt λ _ → refl - - - module _ (X : ℤFunctor) where - open isIsoC - open Join (CompOpenDistLattice .F-ob X) - open JoinSemilattice (Lattice→JoinSemilattice (DistLattice→Lattice (CompOpenDistLattice .F-ob X))) - open PosetStr (IndPoset .snd) hiding (_≤_) - open LatticeTheory ⦃...⦄ - private instance _ = (CompOpenDistLattice .F-ob X) .snd - - compOpenGlobalIncl : (U : CompactOpen X) → ⟦ U ⟧ᶜᵒ ⇒ X - N-ob (compOpenGlobalIncl U) A = fst - N-hom (compOpenGlobalIncl U) φ = refl - - compOpenIncl : {U V : CompactOpen X} → V ≤ U → ⟦ V ⟧ᶜᵒ ⇒ ⟦ U ⟧ᶜᵒ - N-ob (compOpenIncl {U = U} {V = V} V≤U) A (x , Vx≡D1) = x , path - where - instance - _ = A .snd - _ = ZariskiLattice A .snd - _ = DistLattice→Lattice (ZariskiLattice A) - path : U .N-ob A x ≡ D A 1r - path = U .N-ob A x ≡⟨ funExt⁻ (funExt⁻ (cong N-ob (sym V≤U)) A) x ⟩ - V .N-ob A x ∨l U .N-ob A x ≡⟨ cong (_∨l U .N-ob A x) Vx≡D1 ⟩ - D A 1r ∨l U .N-ob A x ≡⟨ 1lLeftAnnihilates∨l _ ⟩ - D A 1r ∎ - N-hom (compOpenIncl V≤U) φ = funExt λ x → Σ≡Prop (λ _ → squash/ _ _) refl - - -- this is essentially U∧_ - compOpenDownHom : (U : CompactOpen X) - → DistLatticeHom (CompOpenDistLattice .F-ob X) - (CompOpenDistLattice .F-ob ⟦ U ⟧ᶜᵒ) - compOpenDownHom U = CompOpenDistLattice .F-hom (compOpenGlobalIncl U) - - module _ {U V : CompactOpen X} (V≤U : V ≤ U) where - -- We need this separate definition to avoid termination checker issues, - -- but we don't understand why. - private - compOpenDownHomFun : (A : CommRing ℓ) - → ⟦ V ⟧ᶜᵒ .F-ob A .fst - → ⟦ compOpenDownHom U .fst V ⟧ᶜᵒ .F-ob A .fst - compOpenDownHomFun A v = (compOpenIncl V≤U ⟦ A ⟧) v , snd v - - compOpenDownHomNatIso : NatIso ⟦ V ⟧ᶜᵒ ⟦ compOpenDownHom U .fst V ⟧ᶜᵒ - N-ob (trans compOpenDownHomNatIso) = compOpenDownHomFun - N-hom (trans compOpenDownHomNatIso) _ = - funExt λ _ → Σ≡Prop (λ _ → squash/ _ _) (Σ≡Prop (λ _ → squash/ _ _) refl) - inv (nIso compOpenDownHomNatIso A) ((x , Ux≡D1) , Vx≡D1) = x , Vx≡D1 - sec (nIso compOpenDownHomNatIso A) = - funExt λ _ → Σ≡Prop (λ _ → squash/ _ _) (Σ≡Prop (λ _ → squash/ _ _) refl) - ret (nIso compOpenDownHomNatIso A) = funExt λ _ → Σ≡Prop (λ _ → squash/ _ _) refl - - compOpenInclId : ∀ {U : CompactOpen X} → compOpenIncl (is-refl U) ≡ idTrans ⟦ U ⟧ᶜᵒ - compOpenInclId = makeNatTransPath (funExt₂ (λ _ _ → Σ≡Prop (λ _ → squash/ _ _) refl)) - - compOpenInclSeq : ∀ {U V W : CompactOpen X} (U≤V : U ≤ V) (V≤W : V ≤ W) - → compOpenIncl (is-trans _ _ _ U≤V V≤W) - ≡ compOpenIncl U≤V ●ᵛ compOpenIncl V≤W - compOpenInclSeq _ _ = makeNatTransPath - (funExt₂ (λ _ _ → Σ≡Prop (λ _ → squash/ _ _) refl)) - - - -- the structure sheaf - private COᵒᵖ = (DistLatticeCategory (CompOpenDistLattice .F-ob X)) ^op - - strDLSh : Functor COᵒᵖ (CommRingsCategory {ℓ = ℓ-suc ℓ}) - F-ob strDLSh U = 𝓞 .F-ob ⟦ U ⟧ᶜᵒ - F-hom strDLSh U≥V = 𝓞 .F-hom (compOpenIncl U≥V) - F-id strDLSh = cong (𝓞 .F-hom) compOpenInclId ∙ 𝓞 .F-id - F-seq strDLSh _ _ = cong (𝓞 .F-hom) (compOpenInclSeq _ _) ∙ 𝓞 .F-seq _ _ - - - -- def. affine cover and locality for definition of qcqs-scheme - module _ (X : ℤFunctor) where - open isIsoC - open Join (CompOpenDistLattice .F-ob X) - open JoinSemilattice (Lattice→JoinSemilattice (DistLattice→Lattice (CompOpenDistLattice .F-ob X))) - open PosetStr (IndPoset .snd) hiding (_≤_) - open LatticeTheory ⦃...⦄ - private instance _ = (CompOpenDistLattice .F-ob X) .snd - - record AffineCover : Type (ℓ-suc ℓ) where - field - n : ℕ - U : FinVec (CompactOpen X) n - covers : ⋁ U ≡ 1l -- TODO: equivalent to X ≡ ⟦ ⋁ U ⟧ᶜᵒ - isAffineU : ∀ i → isAffineCompactOpen (U i) - - hasAffineCover : Type (ℓ-suc ℓ) - hasAffineCover = ∥ AffineCover ∥₁ - - -- qcqs-schemes as Zariski sheaves (local ℤ-functors) with an affine cover in the sense above - isLocal : ℤFunctor → Type (ℓ-suc ℓ) - isLocal X = isSheaf zariskiCoverage X - - -- Compact opens of Zariski sheaves are sheaves - presLocalCompactOpen : (X : ℤFunctor) (U : CompactOpen X) → isLocal X → isLocal ⟦ U ⟧ᶜᵒ - presLocalCompactOpen X U isLocalX R um@(unimodvec _ f _) = isoToIsEquiv isoU - where - open Coverage zariskiCoverage - open InvertingElementsBase R - instance _ = R .snd - - fᵢCoverR = covers R .snd um - - isoX : Iso (X .F-ob R .fst) (CompatibleFamily X fᵢCoverR) - isoX = equivToIso (elementToCompatibleFamily _ _ , isLocalX R um) - - compatibleFamIncl : (CompatibleFamily ⟦ U ⟧ᶜᵒ fᵢCoverR) → (CompatibleFamily X fᵢCoverR) - compatibleFamIncl fam = (fst ∘ fst fam) - , λ i j B φ ψ φψComm → cong fst (fam .snd i j B φ ψ φψComm) - - compatibleFamIncl≡ : ∀ (y : Σ[ x ∈ X .F-ob R .fst ] U .N-ob R x ≡ D R 1r) - → compatibleFamIncl (elementToCompatibleFamily ⟦ U ⟧ᶜᵒ fᵢCoverR y) - ≡ elementToCompatibleFamily X fᵢCoverR (y .fst) - compatibleFamIncl≡ y = CompatibleFamily≡ _ _ _ _ λ _ → refl - - isoU : Iso (Σ[ x ∈ X .F-ob R .fst ] U .N-ob R x ≡ D R 1r) - (CompatibleFamily ⟦ U ⟧ᶜᵒ fᵢCoverR) - fun isoU = elementToCompatibleFamily _ _ - fst (inv isoU fam) = isoX .inv (compatibleFamIncl fam) - snd (inv isoU fam) = -- U (x) ≡ D(1) - -- knowing that U(x/1)¸≡ D(1) in R[1/fᵢ] - let x = isoX .inv (compatibleFamIncl fam) in - isSeparatedZarLatFun R um (U .N-ob R x) (D R 1r) - λ i → let open UniversalProp (f i) - instance _ = R[1/ (f i) ]AsCommRing .snd in - - inducedZarLatHom /1AsCommRingHom .fst (U .N-ob R x) - - ≡⟨ funExt⁻ (sym (U .N-hom /1AsCommRingHom)) x ⟩ - - U .N-ob R[1/ (f i) ]AsCommRing (X .F-hom /1AsCommRingHom x) - - ≡⟨ cong (U .N-ob R[1/ f i ]AsCommRing) - (funExt⁻ (cong fst (isoX .rightInv (compatibleFamIncl fam))) i) ⟩ - - U .N-ob R[1/ (f i) ]AsCommRing (fam .fst i .fst) - - ≡⟨ fam .fst i .snd ⟩ - - D R[1/ (f i) ]AsCommRing 1r - - ≡⟨ sym (inducedZarLatHom /1AsCommRingHom .snd .pres1) ⟩ - - inducedZarLatHom /1AsCommRingHom .fst (D R 1r) ∎ - - rightInv isoU fam = - Σ≡Prop (λ _ → isPropIsCompatibleFamily _ _ _) - (funExt λ i → Σ≡Prop (λ _ → squash/ _ _) - (funExt⁻ (cong fst - (isoX .rightInv (compatibleFamIncl fam))) i)) - leftInv isoU y = Σ≡Prop (λ _ → squash/ _ _) - (cong (isoX .inv) (compatibleFamIncl≡ y) - ∙ isoX .leftInv (y .fst)) - - - -- definition of quasi-compact, quasi-separated schemes - isQcQsScheme : ℤFunctor → Type (ℓ-suc ℓ) - isQcQsScheme X = isLocal X × hasAffineCover X - - - -- affine schemes are qcqs-schemes - module _ (A : CommRing ℓ) where - open AffineCover - private instance _ = (CompOpenDistLattice ⟅ Sp ⟅ A ⟆ ⟆) .snd - - -- the canonical one element affine cover of a representable - singlAffineCover : AffineCover (Sp .F-ob A) - n singlAffineCover = 1 - U singlAffineCover zero = 1l - covers singlAffineCover = ∨lRid _ - isAffineU singlAffineCover zero = ∣ A , compOpenTopNatIso (Sp ⟅ A ⟆) ∣₁ - - isQcQsSchemeAffine : isQcQsScheme (Sp .F-ob A) - fst isQcQsSchemeAffine = isSubcanonicalZariskiCoverage A - snd isQcQsSchemeAffine = ∣ singlAffineCover ∣₁ - - --- standard affine opens --- TODO: separate file? -module StandardOpens {ℓ : Level} (R : CommRing ℓ) (f : R .fst) where - - open Iso - open Functor - open NatTrans - open NatIso - open isIsoC - open DistLatticeStr ⦃...⦄ - open CommRingStr ⦃...⦄ - open IsRingHom - open RingHoms - open IsLatticeHom - open ZarLat - - open InvertingElementsBase R - open UniversalProp f - - private module ZL = ZarLatUniversalProp - - private - instance - _ = R .snd - - D : CompactOpen (Sp ⟅ R ⟆) - D = yonedaᴾ ZarLatFun R .inv (ZL.D R f) - - SpR[1/f]≅⟦Df⟧ : NatIso (Sp .F-ob R[1/ f ]AsCommRing) ⟦ D ⟧ᶜᵒ - N-ob (trans SpR[1/f]≅⟦Df⟧) B φ = (φ ∘r /1AsCommRingHom) , ∨lRid _ ∙ path - where - open CommRingHomTheory φ - open IsSupport (ZL.isSupportD B) - instance - _ = B .snd - _ = ZariskiLattice B .snd - - isUnitφ[f/1] : φ .fst (f /1) ∈ B ˣ - isUnitφ[f/1] = RingHomRespInv (f /1) ⦃ S/1⊆S⁻¹Rˣ f ∣ 1 , sym (·IdR f) ∣₁ ⦄ - - path : ZL.D B (φ .fst (f /1)) ≡ 1l - path = supportUnit _ isUnitφ[f/1] - - N-hom (trans SpR[1/f]≅⟦Df⟧) _ = funExt λ _ → Σ≡Prop (λ _ → squash/ _ _) (RingHom≡ refl) - - inv (nIso SpR[1/f]≅⟦Df⟧ B) (φ , Dφf≡D1) = invElemUniversalProp B φ isUnitφf .fst .fst - where - instance _ = ZariskiLattice B .snd - isUnitφf : φ .fst f ∈ B ˣ - isUnitφf = unitLemmaZarLat B (φ $r f) (sym (∨lRid _) ∙ Dφf≡D1) - - sec (nIso SpR[1/f]≅⟦Df⟧ B) = - funExt λ _ → Σ≡Prop (λ _ → squash/ _ _) (RingHom≡ (invElemUniversalProp _ _ _ .fst .snd)) - ret (nIso SpR[1/f]≅⟦Df⟧ B) = - funExt λ φ → cong fst (invElemUniversalProp B (φ ∘r /1AsCommRingHom) _ .snd (φ , refl)) - - isAffineD : isAffineCompactOpen D - isAffineD = ∣ R[1/ f ]AsCommRing , SpR[1/f]≅⟦Df⟧ ∣₁ - - --- compact opens of affine schemes are qcqs-schemes -module _ {ℓ : Level} (R : CommRing ℓ) (W : CompactOpen (Sp ⟅ R ⟆)) where - - open StandardOpens - - open Iso - open Functor - open NatTrans - open NatIso - open isIsoC - open DistLatticeStr ⦃...⦄ - open CommRingStr ⦃...⦄ - open PosetStr ⦃...⦄ - open IsRingHom - open RingHoms - open IsLatticeHom - open ZarLat - - open JoinSemilattice (Lattice→JoinSemilattice (DistLattice→Lattice (CompOpenDistLattice .F-ob (Sp .F-ob R)))) using (IndPoset; ind≤bigOp) - open InvertingElementsBase R - open Join - open JoinMap - open AffineCover - private module ZL = ZarLatUniversalProp - - private - instance - _ = R .snd - _ = ZariskiLattice R .snd - _ = CompOpenDistLattice .F-ob (Sp .F-ob R) .snd - _ = CompOpenDistLattice .F-ob ⟦ W ⟧ᶜᵒ .snd - _ = IndPoset .snd - - w : ZL R - w = yonedaᴾ ZarLatFun R .fun W - - -- yoneda is a lattice homomorphsim - isHomYoneda : IsLatticeHom (DistLattice→Lattice (ZariskiLattice R) .snd) - (yonedaᴾ ZarLatFun R .inv) - (DistLattice→Lattice (CompOpenDistLattice ⟅ Sp ⟅ R ⟆ ⟆) .snd) - pres0 isHomYoneda = makeNatTransPath (funExt₂ (λ _ _ → refl)) - pres1 isHomYoneda = - makeNatTransPath (funExt₂ (λ _ φ → inducedZarLatHom φ .snd .pres1)) - pres∨l isHomYoneda u v = - makeNatTransPath (funExt₂ (λ _ φ → inducedZarLatHom φ .snd .pres∨l u v)) - pres∧l isHomYoneda u v = - makeNatTransPath (funExt₂ (λ _ φ → inducedZarLatHom φ .snd .pres∧l u v)) - - module _ {n : ℕ} - (f : FinVec (fst R) n) - (⋁Df≡W : ⋁ (CompOpenDistLattice ⟅ Sp ⟅ R ⟆ ⟆) (D R ∘ f) ≡ W) where +{- - Df≤W : ∀ i → D R (f i) ≤ W - Df≤W i = subst (D R (f i) ≤_) ⋁Df≡W (ind≤bigOp (D R ∘ f) i) + The category of ℤ-functors is the category of functors from rings to sets. + It contains the category of schemes as a full subcategory and is thus of + special interest to algebraic geometers. The basic notions needed to + develop algebraic geometry using ℤ-functors can be found in: - toAffineCover : AffineCover ⟦ W ⟧ᶜᵒ - AffineCover.n toAffineCover = n - U toAffineCover i = compOpenDownHom (Sp ⟅ R ⟆) W .fst (D R (f i)) - covers toAffineCover = sym (pres⋁ (compOpenDownHom (Sp ⟅ R ⟆) W) (D R ∘ f)) - ∙ cong (compOpenDownHom (Sp ⟅ R ⟆) W .fst) ⋁Df≡W - ∙ makeNatTransPath (funExt₂ (λ _ → snd)) - isAffineU toAffineCover i = - ∣ _ , seqNatIso (SpR[1/f]≅⟦Df⟧ R (f i)) (compOpenDownHomNatIso _ (Df≤W i)) ∣₁ +-} - module _ {n : ℕ} - (f : FinVec (fst R) n) - (⋁Df≡w : ⋁ (ZariskiLattice R) (ZL.D R ∘ f) ≡ w) where +open import Cubical.AlgebraicGeometry.Functorial.ZFunctors.Base public - private - ⋁Df≡W : ⋁ (CompOpenDistLattice ⟅ Sp ⟅ R ⟆ ⟆) (D R ∘ f) ≡ W - ⋁Df≡W = sym (pres⋁ (_ , isHomYoneda) (ZL.D R ∘ f)) - ∙ cong (yonedaᴾ ZarLatFun R .inv) ⋁Df≡w - ∙ yonedaᴾ ZarLatFun R .leftInv W +{- - makeAffineCoverCompOpenOfAffine : AffineCover ⟦ W ⟧ᶜᵒ - makeAffineCoverCompOpenOfAffine = toAffineCover f ⋁Df≡W + In Cubical Agda we can define the full subcategory of qcqs-schemes. + This is done in: - hasAffineCoverCompOpenOfAffine : hasAffineCover ⟦ W ⟧ᶜᵒ - hasAffineCoverCompOpenOfAffine = PT.map truncHelper ([]surjective w) - where - truncHelper : Σ[ n,f ∈ Σ ℕ (FinVec (fst R)) ] [ n,f ] ≡ w → AffineCover ⟦ W ⟧ᶜᵒ - truncHelper ((n , f) , [n,f]≡w) = makeAffineCoverCompOpenOfAffine f (ZL.⋁D≡ R f ∙ [n,f]≡w) +-} - isQcQsSchemeCompOpenOfAffine : isQcQsScheme ⟦ W ⟧ᶜᵒ - fst isQcQsSchemeCompOpenOfAffine = presLocalCompactOpen _ _ (isSubcanonicalZariskiCoverage R) - snd isQcQsSchemeCompOpenOfAffine = hasAffineCoverCompOpenOfAffine +open import Cubical.AlgebraicGeometry.Functorial.ZFunctors.CompactOpen +open import Cubical.AlgebraicGeometry.Functorial.ZFunctors.QcQsScheme +open import Cubical.AlgebraicGeometry.Functorial.ZFunctors.OpenSubscheme diff --git a/Cubical/Papers/AffineSchemes.agda b/Cubical/Papers/AffineSchemes.agda index 2f63ba1f7..5d679863b 100644 --- a/Cubical/Papers/AffineSchemes.agda +++ b/Cubical/Papers/AffineSchemes.agda @@ -24,55 +24,55 @@ module Cubical.Papers.AffineSchemes where -- 2: Background -- 2.2: Cubical Agda -import Cubical.Foundations.Prelude as Prelude -import Cubical.Foundations.HLevels as HLevels -import Cubical.Foundations.Univalence as Univalence -import Cubical.Data.Sigma as Sigma -import Cubical.HITs.PropositionalTruncation as PT -import Cubical.Algebra.DistLattice.Basis as DistLatticeBasis -import Cubical.HITs.SetQuotients as SQ +import Cubical.Foundations.Prelude as Prelude +import Cubical.Foundations.HLevels as HLevels +import Cubical.Foundations.Univalence as Univalence +import Cubical.Data.Sigma as Sigma +import Cubical.HITs.PropositionalTruncation as PT +import Cubical.Algebra.DistLattice.Basis as DistLatticeBasis +import Cubical.HITs.SetQuotients as SQ -- 3: Commutative Algebra -- 3.1: Localization -import Cubical.Algebra.CommRing.Localisation.Base as L +import Cubical.Algebra.CommRing.Localisation.Base as L module Localization = L.Loc -import Cubical.Algebra.CommRing.Localisation.UniversalProperty as LocalizationUnivProp -import Cubical.Algebra.CommRing.Localisation.InvertingElements as LocalizationInvEl -import Cubical.Algebra.CommAlgebra as R-Algs -import Cubical.Algebra.CommAlgebra.Localisation as LocalizationR-Alg +import Cubical.Algebra.CommRing.Localisation.UniversalProperty as LocalizationUnivProp +import Cubical.Algebra.CommRing.Localisation.InvertingElements as LocalizationInvEl +import Cubical.Algebra.CommAlgebra as R-Algs +import Cubical.Algebra.CommAlgebra.Localisation as LocalizationR-Alg -- 3.2: The Zariski Lattice -import Cubical.Data.FinData.Base as FiniteTypes -import Cubical.Algebra.Matrix as Matrices -import Cubical.Algebra.CommRing.FGIdeal as FinGenIdeals +import Cubical.Data.FinData.Base as FiniteTypes +import Cubical.Algebra.Matrix as Matrices +import Cubical.Algebra.CommRing.FGIdeal as FinGenIdeals -import Cubical.Algebra.ZariskiLattice.Base as ZLB +import Cubical.AlgebraicGeometry.ZariskiLattice.Base as ZLB module ZariskiLatDef = ZLB.ZarLat -import Cubical.Algebra.ZariskiLattice.UniversalProperty as ZLUP +import Cubical.AlgebraicGeometry.ZariskiLattice.UniversalProperty as ZLUP module ZariskiLatUnivProp = ZLUP.ZarLatUniversalProp -- 4: Category Theory -- background theory not explicitly mentioned -import Cubical.Categories.Category.Base as CatTheory -import Cubical.Categories.Limits as GeneralLimits -import Cubical.Categories.Limits.RightKan as GeneralKanExtension +import Cubical.Categories.Category.Base as CatTheory +import Cubical.Categories.Limits as GeneralLimits +import Cubical.Categories.Limits.RightKan as GeneralKanExtension -import Cubical.Categories.DistLatticeSheaf.Diagram as SheafDiagShapes -import Cubical.Categories.DistLatticeSheaf.Base as Sheaves +import Cubical.Categories.DistLatticeSheaf.Diagram as SheafDiagShapes +import Cubical.Categories.DistLatticeSheaf.Base as Sheaves -import Cubical.Categories.DistLatticeSheaf.Extension as E +import Cubical.Categories.DistLatticeSheaf.Extension as E module SheafExtension = E.PreSheafExtension -- 5: The Structure Sheaf -import Cubical.Categories.Instances.CommAlgebras as R-AlgConstructions -import Cubical.Algebra.CommRing.Localisation.Limit as LocalizationLimit -import Cubical.Algebra.ZariskiLattice.StructureSheaf as StructureSheaf +import Cubical.Categories.Instances.CommAlgebras as R-AlgConstructions +import Cubical.Algebra.CommRing.Localisation.Limit as LocalizationLimit +import Cubical.AlgebraicGeometry.ZariskiLattice.StructureSheaf as StructureSheaf diff --git a/Cubical/Papers/FunctorialQcQsSchemes.agda b/Cubical/Papers/FunctorialQcQsSchemes.agda index 6abba9a03..86c727c96 100644 --- a/Cubical/Papers/FunctorialQcQsSchemes.agda +++ b/Cubical/Papers/FunctorialQcQsSchemes.agda @@ -21,47 +21,47 @@ module Cubical.Papers.FunctorialQcQsSchemes where -- 2: Background -- 2.1: Univalent type theory in Cubical Agda -import Cubical.Foundations.Prelude as Prelude -import Cubical.Foundations.HLevels as HLevels -import Cubical.Foundations.Univalence as Univalence -import Cubical.Data.Sigma as Sigma -import Cubical.HITs.PropositionalTruncation as PT -import Cubical.HITs.SetQuotients as SQ +import Cubical.Foundations.Prelude as Prelude +import Cubical.Foundations.HLevels as HLevels +import Cubical.Foundations.Univalence as Univalence +import Cubical.Data.Sigma as Sigma +import Cubical.HITs.PropositionalTruncation as PT +import Cubical.HITs.SetQuotients as SQ -- 2.2: Localizations and the Zariski lattice -import Cubical.Algebra.CommRing.Localisation.InvertingElements as LocalizationInvEl +import Cubical.Algebra.CommRing.Localisation.InvertingElements as LocalizationInvEl module LocalizationInvElBase = LocalizationInvEl.InvertingElementsBase module LocalizationInvElUniversalProp = LocalizationInvElBase.UniversalProp -import Cubical.Algebra.ZariskiLattice.Base as ZLB +import Cubical.AlgebraicGeometry.ZariskiLattice.Base as ZLB module ZariskiLatDef = ZLB.ZarLat -import Cubical.Algebra.ZariskiLattice.UniversalProperty as ZLUP +import Cubical.AlgebraicGeometry.ZariskiLattice.UniversalProperty as ZLUP module ZariskiLatUnivProp = ZLUP.ZarLatUniversalProp module Localization&Radicals = LocalizationInvEl.RadicalLemma -import Cubical.Algebra.ZariskiLattice.Properties as ZLP +import Cubical.AlgebraicGeometry.ZariskiLattice.Properties as ZLP -- 3: ℤ-functors -import Cubical.Categories.Instances.ZFunctors as ZFun +import Cubical.AlgebraicGeometry.Functorial.ZFunctors.Base as ZFun module RelativeAdjunction = ZFun.AdjBij -- 4: Local ℤ-functors -import Cubical.Categories.Site.Cover as Cover -import Cubical.Categories.Site.Coverage as Coverage -import Cubical.Categories.Site.Sheaf as Sheaf +import Cubical.Categories.Site.Cover as Cover +import Cubical.Categories.Site.Coverage as Coverage +import Cubical.Categories.Site.Sheaf as Sheaf -import Cubical.Categories.Site.Instances.ZariskiCommRing as ZariskiCoverage +import Cubical.Categories.Site.Instances.ZariskiCommRing as ZariskiCoverage module ZarCovSubcanonical = ZariskiCoverage.SubcanonicalLemmas -import Cubical.Algebra.CommRing.Localisation.Limit as LocalizationLimit +import Cubical.Algebra.CommRing.Localisation.Limit as LocalizationLimit --- !!! note: the ZFunctors file is supposed to be broken up into smaller files !!! -- 5: Compact opens and qcqs-schemes --- import Cubical.Categories.Instances.ZFunctors as ZFun +import Cubical.AlgebraicGeometry.Functorial.ZFunctors.CompactOpen as CO +import Cubical.AlgebraicGeometry.Functorial.ZFunctors.QcQsScheme as QcQsSchemes -- 6: Open subschemes --- import Cubical.Categories.Instances.ZFunctors as ZFun -module StandardOpen = ZFun.StandardOpens +import Cubical.AlgebraicGeometry.Functorial.ZFunctors.OpenSubscheme as OSubscheme +module StandardOpen = OSubscheme.StandardOpens @@ -160,32 +160,32 @@ open ZariskiCoverage using (isSubcanonicalZariskiCoverage) ---------- 4: Compact opens and qcqs-schemes ---------- -- Definition 13 -open ZFun renaming (ZarLatFun to 𝓛) +open CO renaming (ZarLatFun to 𝓛) -- Definition 14 -open ZFun using (CompactOpen ; ⟦_⟧ᶜᵒ) +open CO using (CompactOpen ; ⟦_⟧ᶜᵒ) -- Definition 15 -open ZFun using (CompOpenDistLattice) +open CO using (CompOpenDistLattice) -- Definition 16 -open ZFun using (isQcQsScheme) +open QcQsSchemes using (isQcQsScheme) -- Proposition 17 -open ZFun using (singlAffineCover ; isQcQsSchemeAffine) +open QcQsSchemes using (singlAffineCover ; isQcQsSchemeAffine) -- Remark 18 -open ZFun using (AffineCover ; hasAffineCover) +open QcQsSchemes using (AffineCover ; hasAffineCover) ----------- 5: Open subschemes ---------- -- Lemma 20 -open ZFun using (isSeparatedZarLatFun) +open CO using (isSeparatedZarLatFun) -- Lemma 21 -open ZFun using (presLocalCompactOpen) +open CO using (presLocalCompactOpen) -- Definition 22 open StandardOpen using (D) @@ -194,4 +194,4 @@ open StandardOpen using (D) open StandardOpen using (SpR[1/f]≅⟦Df⟧ ; isAffineD) -- Theorem 24 -open ZFun using (isQcQsSchemeCompOpenOfAffine) +open OSubscheme using (isQcQsSchemeCompOpenOfAffine) diff --git a/Cubical/README.agda b/Cubical/README.agda index ed23331c7..b707a2e03 100644 --- a/Cubical/README.agda +++ b/Cubical/README.agda @@ -68,6 +68,9 @@ import Cubical.ZCohomology.Everything -- Algebra library (in development) import Cubical.Algebra.Everything +-- Algebraic geometry +import Cubical.AlgebraicGeometry.Everything + -- Various talks import Cubical.Talks.Everything