From 7d4cdfa1f475faf2d592b5c5a65f2dce5962d526 Mon Sep 17 00:00:00 2001 From: mzeuner Date: Mon, 23 Aug 2021 19:44:28 +0200 Subject: [PATCH 01/10] use improved ringsolver --- .../Algebra/CommRing/Localisation/Base.agda | 19 ++++++------------- 1 file changed, 6 insertions(+), 13 deletions(-) diff --git a/Cubical/Algebra/CommRing/Localisation/Base.agda b/Cubical/Algebra/CommRing/Localisation/Base.agda index 21e863804f..199c39baf6 100644 --- a/Cubical/Algebra/CommRing/Localisation/Base.agda +++ b/Cubical/Algebra/CommRing/Localisation/Base.agda @@ -161,14 +161,13 @@ module Loc (R' : CommRing ℓ) (S' : ℙ (fst R')) (SMultClosedSubset : isMultCl +ₗ-rid[] : (a : R × S) → [ a ] +ₗ 0ₗ ≡ [ a ] +ₗ-rid[] (r , s , s∈S) = path where - -- possible to automate with improved ring solver? - eq1 : r · 1r + 0r · s ≡ r - eq1 = cong (r · 1r +_) (0LeftAnnihilates _) ∙∙ +Rid _ ∙∙ ·Rid _ + eq1 : (r s : R) → r · 1r + 0r · s ≡ r + eq1 = solve R' path : [ r · 1r + 0r · s , s · 1r , SMultClosedSubset .multClosed s∈S (SMultClosedSubset .containsOne) ] ≡ [ r , s , s∈S ] - path = cong [_] (ΣPathP (eq1 , Σ≡Prop (λ x → ∈-isProp S' x) (·Rid _))) + path = cong [_] (ΣPathP (eq1 r s , Σ≡Prop (λ x → ∈-isProp S' x) (·Rid _))) -ₗ_ : S⁻¹R → S⁻¹R -ₗ_ = SQ.rec squash/ -ₗ[] -ₗWellDef @@ -192,17 +191,11 @@ module Loc (R' : CommRing ℓ) (S' : ℙ (fst R')) (SMultClosedSubset : isMultCl +ₗ-rinv = SQ.elimProp (λ _ → squash/ _ _) +ₗ-rinv[] where +ₗ-rinv[] : (a : R × S) → ([ a ] +ₗ (-ₗ [ a ])) ≡ 0ₗ - +ₗ-rinv[] (r , s , s∈S) = eq/ _ _ ((1r , SMultClosedSubset .containsOne) , path) + +ₗ-rinv[] (r , s , s∈S) = eq/ _ _ ((1r , SMultClosedSubset .containsOne) , path r s) where -- not yet possible with ring solver - path : 1r · (r · s + - r · s) · 1r ≡ 1r · 0r · (s · s) - path = 1r · (r · s + - r · s) · 1r ≡⟨ cong (λ x → 1r · (r · s + x) · 1r) (-DistL· _ _) ⟩ - 1r · (r · s + - (r · s)) · 1r ≡⟨ cong (λ x → 1r · x · 1r) (+Rinv _) ⟩ - 1r · 0r · 1r ≡⟨ ·Rid _ ⟩ - 1r · 0r ≡⟨ ·Lid _ ⟩ - 0r ≡⟨ sym (0LeftAnnihilates _) ⟩ - 0r · (s · s) ≡⟨ cong (_· (s · s)) (sym (·Lid _)) ⟩ - 1r · 0r · (s · s) ∎ + path : (r s : R) → 1r · (r · s + - r · s) · 1r ≡ 1r · 0r · (s · s) + path = solve R' +ₗ-comm : (x y : S⁻¹R) → x +ₗ y ≡ y +ₗ x +ₗ-comm = SQ.elimProp2 (λ _ _ → squash/ _ _) +ₗ-comm[] From e4d5d8dc4482eb121fe2af0b9dd852fdd95872bc Mon Sep 17 00:00:00 2001 From: mzeuner Date: Mon, 23 Aug 2021 19:52:23 +0200 Subject: [PATCH 02/10] delete one more line --- Cubical/Algebra/CommRing/Localisation/Base.agda | 1 - 1 file changed, 1 deletion(-) diff --git a/Cubical/Algebra/CommRing/Localisation/Base.agda b/Cubical/Algebra/CommRing/Localisation/Base.agda index 199c39baf6..59c8fc31d8 100644 --- a/Cubical/Algebra/CommRing/Localisation/Base.agda +++ b/Cubical/Algebra/CommRing/Localisation/Base.agda @@ -193,7 +193,6 @@ module Loc (R' : CommRing ℓ) (S' : ℙ (fst R')) (SMultClosedSubset : isMultCl +ₗ-rinv[] : (a : R × S) → ([ a ] +ₗ (-ₗ [ a ])) ≡ 0ₗ +ₗ-rinv[] (r , s , s∈S) = eq/ _ _ ((1r , SMultClosedSubset .containsOne) , path r s) where - -- not yet possible with ring solver path : (r s : R) → 1r · (r · s + - r · s) · 1r ≡ 1r · 0r · (s · s) path = solve R' From fac763bc94702d28c75fd4ed8ab055a513862343 Mon Sep 17 00:00:00 2001 From: Matthias Hutzler Date: Mon, 27 Nov 2023 16:45:51 +0100 Subject: [PATCH 03/10] (wip) for Zariski coverage on CommRing (with Max Zeuner) --- .../Localisation/InvertingElements.agda | 4 + .../Algebra/CommRing/Localisation/Limit.agda | 2 +- .../Site/Instances/ZariskiCommRing.agda | 103 ++++++++++++++++++ 3 files changed, 108 insertions(+), 1 deletion(-) create mode 100644 Cubical/Categories/Site/Instances/ZariskiCommRing.agda diff --git a/Cubical/Algebra/CommRing/Localisation/InvertingElements.agda b/Cubical/Algebra/CommRing/Localisation/InvertingElements.agda index be3dd9d176..a25e56358c 100644 --- a/Cubical/Algebra/CommRing/Localisation/InvertingElements.agda +++ b/Cubical/Algebra/CommRing/Localisation/InvertingElements.agda @@ -80,6 +80,10 @@ module InvertingElementsBase (R' : CommRing ℓ) where R[1/_] : R → Type ℓ R[1/ f ] = Loc.S⁻¹R R' [ f ⁿ|n≥0] (powersFormMultClosedSubset f) + -- TODO: Provide a more specialized universal property. + -- (Just ask f to become invertible, not all its powers.) + module UniversalProp (f : R) = S⁻¹RUniversalProp R' [ f ⁿ|n≥0] (powersFormMultClosedSubset f) + -- a quick fact isContrR[1/0] : isContr R[1/ 0r ] fst isContrR[1/0] = [ 1r , 0r , ∣ 1 , sym (·IdR 0r) ∣₁ ] -- everything is equal to 1/0 diff --git a/Cubical/Algebra/CommRing/Localisation/Limit.agda b/Cubical/Algebra/CommRing/Localisation/Limit.agda index 316c491e84..c8c755f512 100644 --- a/Cubical/Algebra/CommRing/Localisation/Limit.agda +++ b/Cubical/Algebra/CommRing/Localisation/Limit.agda @@ -64,7 +64,7 @@ module _ (R' : CommRing ℓ) {n : ℕ} (f : FinVec (fst R') (suc n)) where open CommRingTheory R' open RingTheory (CommRing→Ring R') open Sum (CommRing→Ring R') - open CommIdeal R' hiding (subst-∈) + open CommIdeal R' open InvertingElementsBase R' open Exponentiation R' open CommRingStr ⦃...⦄ diff --git a/Cubical/Categories/Site/Instances/ZariskiCommRing.agda b/Cubical/Categories/Site/Instances/ZariskiCommRing.agda new file mode 100644 index 0000000000..7f5158558c --- /dev/null +++ b/Cubical/Categories/Site/Instances/ZariskiCommRing.agda @@ -0,0 +1,103 @@ +{-# OPTIONS --safe #-} +module Cubical.Categories.Site.Instances.ZariskiCommRing where + +-- TODO: clean up imports +open import Cubical.Foundations.Prelude +open import Cubical.Foundations.Function +open import Cubical.Foundations.HLevels +open import Cubical.Foundations.Equiv +open import Cubical.Foundations.Structure +open import Cubical.Foundations.Isomorphism +-- open import Cubical.Foundations.Powerset + +open import Cubical.Data.Unit +open import Cubical.Data.Nat using (ℕ) +open import Cubical.Data.Sigma +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.Ideal +open import Cubical.Algebra.CommRing.FGIdeal + +open import Cubical.Categories.Category +open import Cubical.Categories.Instances.CommRings +open import Cubical.Categories.Site.Coverage +open import Cubical.Categories.Constructions.Slice + +open import Cubical.HITs.PropositionalTruncation + +open Category hiding (_∘_) +open isUnivalent +open isIso +open RingHoms +open IsRingHom + +private + variable + ℓ ℓ' ℓ'' : Level + +-- module _ (R' : CommRing ℓ) {n : ℕ} (f : FinVec (fst R') (suc n)) where +-- open isMultClosedSubset +-- open CommRingTheory R' +-- open RingTheory (CommRing→Ring R') +-- open Sum (CommRing→Ring R') +-- open CommIdeal R' +-- open InvertingElementsBase R' +-- open Exponentiation R' +-- open CommRingStr ⦃...⦄ +-- +-- private +-- R = fst R' +-- ⟨_⟩ : {n : ℕ} → FinVec R n → CommIdeal +-- ⟨ V ⟩ = ⟨ V ⟩[ R' ] +-- ⟨f₀,⋯,fₙ⟩ = ⟨ f ⟩[ R' ] + +open Coverage + +record UniModVec (R : CommRing ℓ) : Type ℓ where + open CommRingStr (str R) + open CommIdeal R using (_∈_) + + field + n : ℕ + f : FinVec ⟨ R ⟩ n + isUniMod : 1r ∈ ⟨ f ⟩[ R ] + +open SliceOb + +zariskiCoverage : Coverage (CommRingsCategory {ℓ = ℓ} ^op) ℓ ℓ-zero +fst (covers zariskiCoverage R) = UniModVec R +fst (snd (covers zariskiCoverage R) um) = Fin n + where + open UniModVec um +S-ob (snd (snd (covers zariskiCoverage R) um) i) = R[1/ f i ]AsCommRing + where + open UniModVec um + open InvertingElementsBase R +S-arr (snd (snd (covers zariskiCoverage R) um) i) = /1AsCommRingHom + where + open UniModVec um + open InvertingElementsBase.UniversalProp R (f i) +pullbackStability zariskiCoverage {c = R} um {d = R'} φ = + ∣ um' , + (λ i → + let + module R = InvertingElementsBase.UniversalProp R (um .f i) + module R' = InvertingElementsBase.UniversalProp R' (um' .f i) + open InvertingElementsBase R' renaming (R[1/_]AsCommRing to R'[1/_]AsCommRing) using () + (ψ , comm) , _ = + R.S⁻¹RHasUniversalProp + R'[1/ um' .f i ]AsCommRing + (R'./1AsCommRingHom ∘r φ) + {!!} + in + ∣ i , ψ , RingHom≡ {!sym comm!} ∣₁) + ∣₁ + where + open UniModVec + um' : UniModVec R' + um' .n = um .n + um' .f i = φ $r um .f i + um' .isUniMod = {!!} From bbd73369e23a6a7827ae47e7047d81561c16fc4a Mon Sep 17 00:00:00 2001 From: mzeuner Date: Thu, 30 Nov 2023 17:05:09 +0100 Subject: [PATCH 04/10] pullback stability --- .../Localisation/InvertingElements.agda | 38 ++++++++++-- Cubical/Algebra/CommRing/Properties.agda | 62 ++++++++++--------- .../Site/Instances/ZariskiCommRing.agda | 27 ++++---- 3 files changed, 80 insertions(+), 47 deletions(-) diff --git a/Cubical/Algebra/CommRing/Localisation/InvertingElements.agda b/Cubical/Algebra/CommRing/Localisation/InvertingElements.agda index a25e56358c..ef0432834a 100644 --- a/Cubical/Algebra/CommRing/Localisation/InvertingElements.agda +++ b/Cubical/Algebra/CommRing/Localisation/InvertingElements.agda @@ -80,10 +80,6 @@ module InvertingElementsBase (R' : CommRing ℓ) where R[1/_] : R → Type ℓ R[1/ f ] = Loc.S⁻¹R R' [ f ⁿ|n≥0] (powersFormMultClosedSubset f) - -- TODO: Provide a more specialized universal property. - -- (Just ask f to become invertible, not all its powers.) - module UniversalProp (f : R) = S⁻¹RUniversalProp R' [ f ⁿ|n≥0] (powersFormMultClosedSubset f) - -- a quick fact isContrR[1/0] : isContr R[1/ 0r ] fst isContrR[1/0] = [ 1r , 0r , ∣ 1 , sym (·IdR 0r) ∣₁ ] -- everything is equal to 1/0 @@ -283,6 +279,40 @@ module InvertingElementsBase (R' : CommRing ℓ) where PT.rec (PisProp s) λ (n , p) → subst P (sym p) (base n) + + -- A more specialized universal property. + -- (Just ask f to become invertible, not all its powers.) + module UniversalProp (f : R) where + open S⁻¹RUniversalProp R' [ f ⁿ|n≥0] (powersFormMultClosedSubset f) public + open CommRingHomTheory + + invElemUniversalProp : (A : CommRing ℓ) (φ : CommRingHom R' A) + → (φ .fst f ∈ A ˣ) + → ∃![ χ ∈ CommRingHom R[1/ f ]AsCommRing A ] + (fst χ) ∘ (fst /1AsCommRingHom) ≡ (fst φ) + invElemUniversalProp A φ φf∈Aˣ = + S⁻¹RHasUniversalProp A φ + (powersPropElim (λ _ → ∈-isProp _ _) + (λ n → subst-∈ (A ˣ) (sym (pres^ φ f n)) (Exponentiation.^-presUnit A _ n φf∈Aˣ))) + + +-- "functorial action" of localizing away from an element +module _ {A B : CommRing ℓ} (φ : CommRingHom A B) (f : fst A) where + module A = InvertingElementsBase A + module B = InvertingElementsBase B + module AU = S⁻¹RUniversalProp A A.[ f ⁿ|n≥0] (A.powersFormMultClosedSubset f) + module BU = S⁻¹RUniversalProp B B.[ φ $r f ⁿ|n≥0] (B.powersFormMultClosedSubset (φ $r f)) + open A.UniversalProp f + open CommRingStr (snd B) + + private φ/1 = BU./1AsCommRingHom ∘cr φ + + uniqInvElemHom : ∃![ χ ∈ CommRingHom A.R[1/ f ]AsCommRing B.R[1/ φ $r f ]AsCommRing ] + (fst χ) ∘ (fst AU./1AsCommRingHom) ≡ (fst φ/1) + uniqInvElemHom = invElemUniversalProp _ φ/1 (BU.S/1⊆S⁻¹Rˣ _ ∣ 1 , sym (·IdR _) ∣₁) + + + module _ (R : CommRing ℓ) (f : fst R) where open CommRingTheory R open RingTheory (CommRing→Ring R) diff --git a/Cubical/Algebra/CommRing/Properties.agda b/Cubical/Algebra/CommRing/Properties.agda index b8d2033797..726774187f 100644 --- a/Cubical/Algebra/CommRing/Properties.agda +++ b/Cubical/Algebra/CommRing/Properties.agda @@ -200,34 +200,6 @@ module CommRingEquivs where fst (idCommRingEquiv A) = idEquiv (fst A) snd (idCommRingEquiv A) = makeIsRingHom refl (λ _ _ → refl) (λ _ _ → refl) -module CommRingHomTheory {A' B' : CommRing ℓ} (φ : CommRingHom A' B') where - open Units A' renaming (Rˣ to Aˣ ; _⁻¹ to _⁻¹ᵃ ; ·-rinv to ·A-rinv ; ·-linv to ·A-linv) - private A = fst A' - open CommRingStr (snd A') renaming (_·_ to _·A_ ; 1r to 1a) - open Units B' renaming (Rˣ to Bˣ ; _⁻¹ to _⁻¹ᵇ ; ·-rinv to ·B-rinv) - open CommRingStr (snd B') renaming ( _·_ to _·B_ ; 1r to 1b - ; ·IdL to ·B-lid ; ·IdR to ·B-rid - ; ·Assoc to ·B-assoc) - - private - f = fst φ - open IsRingHom (φ .snd) - - RingHomRespInv : (r : A) ⦃ r∈Aˣ : r ∈ Aˣ ⦄ → f r ∈ Bˣ - RingHomRespInv r = f (r ⁻¹ᵃ) , (sym (pres· r (r ⁻¹ᵃ)) ∙∙ cong (f) (·A-rinv r) ∙∙ pres1) - - φ[x⁻¹]≡φ[x]⁻¹ : (r : A) ⦃ r∈Aˣ : r ∈ Aˣ ⦄ ⦃ φr∈Bˣ : f r ∈ Bˣ ⦄ - → f (r ⁻¹ᵃ) ≡ (f r) ⁻¹ᵇ - φ[x⁻¹]≡φ[x]⁻¹ r ⦃ r∈Aˣ ⦄ ⦃ φr∈Bˣ ⦄ = - f (r ⁻¹ᵃ) ≡⟨ sym (·B-rid _) ⟩ - f (r ⁻¹ᵃ) ·B 1b ≡⟨ congR _·B_ (sym (·B-rinv _)) ⟩ - f (r ⁻¹ᵃ) ·B ((f r) ·B (f r) ⁻¹ᵇ) ≡⟨ ·B-assoc _ _ _ ⟩ - f (r ⁻¹ᵃ) ·B (f r) ·B (f r) ⁻¹ᵇ ≡⟨ congL _·B_ (sym (pres· _ _)) ⟩ - f (r ⁻¹ᵃ ·A r) ·B (f r) ⁻¹ᵇ ≡⟨ cong (λ x → f x ·B (f r) ⁻¹ᵇ) (·A-linv _) ⟩ - f 1a ·B (f r) ⁻¹ᵇ ≡⟨ congL _·B_ pres1 ⟩ - 1b ·B (f r) ⁻¹ᵇ ≡⟨ ·B-lid _ ⟩ - (f r) ⁻¹ᵇ ∎ - module Exponentiation (R' : CommRing ℓ) where open CommRingStr (snd R') @@ -276,6 +248,40 @@ module Exponentiation (R' : CommRing ℓ) where ^-presUnit f (suc n) f∈Rˣ = RˣMultClosed f (f ^ n) ⦃ f∈Rˣ ⦄ ⦃ ^-presUnit f n f∈Rˣ ⦄ +module CommRingHomTheory {A' B' : CommRing ℓ} (φ : CommRingHom A' B') where + open Units A' renaming (Rˣ to Aˣ ; _⁻¹ to _⁻¹ᵃ ; ·-rinv to ·A-rinv ; ·-linv to ·A-linv) + open Units B' renaming (Rˣ to Bˣ ; _⁻¹ to _⁻¹ᵇ ; ·-rinv to ·B-rinv) + open Exponentiation A' renaming (_^_ to _^ᵃ_) + open Exponentiation B' renaming (_^_ to _^ᵇ_) + open CommRingStr ⦃...⦄ + private + A = fst A' + f = fst φ + instance + _ = A' .snd + _ = B' .snd + open IsRingHom (φ .snd) + + RingHomRespInv : (r : A) ⦃ r∈Aˣ : r ∈ Aˣ ⦄ → f r ∈ Bˣ + RingHomRespInv r = f (r ⁻¹ᵃ) , (sym (pres· r (r ⁻¹ᵃ)) ∙∙ cong (f) (·A-rinv r) ∙∙ pres1) + + φ[x⁻¹]≡φ[x]⁻¹ : (r : A) ⦃ r∈Aˣ : r ∈ Aˣ ⦄ ⦃ φr∈Bˣ : f r ∈ Bˣ ⦄ + → f (r ⁻¹ᵃ) ≡ (f r) ⁻¹ᵇ + φ[x⁻¹]≡φ[x]⁻¹ r ⦃ r∈Aˣ ⦄ ⦃ φr∈Bˣ ⦄ = + f (r ⁻¹ᵃ) ≡⟨ sym (·IdR _) ⟩ + f (r ⁻¹ᵃ) · 1r ≡⟨ congR _·_ (sym (·B-rinv _)) ⟩ + f (r ⁻¹ᵃ) · ((f r) · (f r) ⁻¹ᵇ) ≡⟨ ·Assoc _ _ _ ⟩ + f (r ⁻¹ᵃ) · (f r) · (f r) ⁻¹ᵇ ≡⟨ congL _·_ (sym (pres· _ _)) ⟩ + f (r ⁻¹ᵃ · r) · (f r) ⁻¹ᵇ ≡⟨ cong (λ x → f x · (f r) ⁻¹ᵇ) (·A-linv _) ⟩ + f 1r · (f r) ⁻¹ᵇ ≡⟨ congL _·_ pres1 ⟩ + 1r · (f r) ⁻¹ᵇ ≡⟨ ·IdL _ ⟩ + (f r) ⁻¹ᵇ ∎ + + pres^ : (x : A) (n : ℕ) → f (x ^ᵃ n) ≡ f x ^ᵇ n + pres^ x zero = pres1 + pres^ x (suc n) = pres· _ _ ∙ cong (f x ·_) (pres^ x n) + + -- like in Ring.Properties we provide helpful lemmas here module CommRingTheory (R' : CommRing ℓ) where open CommRingStr (snd R') diff --git a/Cubical/Categories/Site/Instances/ZariskiCommRing.agda b/Cubical/Categories/Site/Instances/ZariskiCommRing.agda index 7f5158558c..582192cd46 100644 --- a/Cubical/Categories/Site/Instances/ZariskiCommRing.agda +++ b/Cubical/Categories/Site/Instances/ZariskiCommRing.agda @@ -1,4 +1,4 @@ -{-# OPTIONS --safe #-} +{-# OPTIONS --safe --lossy-unification #-} module Cubical.Categories.Site.Instances.ZariskiCommRing where -- TODO: clean up imports @@ -81,23 +81,20 @@ S-arr (snd (snd (covers zariskiCoverage R) um) i) = /1AsCommRingHom open UniModVec um open InvertingElementsBase.UniversalProp R (f i) pullbackStability zariskiCoverage {c = R} um {d = R'} φ = - ∣ um' , - (λ i → - let - module R = InvertingElementsBase.UniversalProp R (um .f i) - module R' = InvertingElementsBase.UniversalProp R' (um' .f i) - open InvertingElementsBase R' renaming (R[1/_]AsCommRing to R'[1/_]AsCommRing) using () - (ψ , comm) , _ = - R.S⁻¹RHasUniversalProp - R'[1/ um' .f i ]AsCommRing - (R'./1AsCommRingHom ∘r φ) - {!!} - in - ∣ i , ψ , RingHom≡ {!sym comm!} ∣₁) - ∣₁ + ∣ um' , (λ i → ∣ i , ψ i , RingHom≡ (sym (ψComm i)) ∣₁) ∣₁ where open UniModVec um' : UniModVec R' um' .n = um .n um' .f i = φ $r um .f i um' .isUniMod = {!!} + + open InvertingElementsBase R + open InvertingElementsBase R' renaming (R[1/_]AsCommRing to R'[1/_]AsCommRing) using () + ψ : (i : Fin (um .n)) → CommRingHom R[1/ um .f i ]AsCommRing R'[1/ um' .f i ]AsCommRing + ψ i = uniqInvElemHom φ (um .f i) .fst .fst + + module R = UniversalProp + module R' = InvertingElementsBase.UniversalProp R' + ψComm : ∀ i → (ψ i .fst) ∘ (R._/1 (um .f i)) ≡ (R'._/1 (um' .f i)) ∘ φ .fst + ψComm i = uniqInvElemHom φ (um .f i) .fst .snd From 76b4e655a0d03d6ff06b98b7988f4a29d85d4cc5 Mon Sep 17 00:00:00 2001 From: mzeuner Date: Fri, 1 Dec 2023 15:49:12 +0100 Subject: [PATCH 05/10] 1 ideal lemma --- .../Localisation/InvertingElements.agda | 14 +-- Cubical/Algebra/Monoid/BigOp.agda | 14 +++ .../Site/Instances/ZariskiCommRing.agda | 93 ++++++++++--------- 3 files changed, 71 insertions(+), 50 deletions(-) diff --git a/Cubical/Algebra/CommRing/Localisation/InvertingElements.agda b/Cubical/Algebra/CommRing/Localisation/InvertingElements.agda index ef0432834a..37a56b2037 100644 --- a/Cubical/Algebra/CommRing/Localisation/InvertingElements.agda +++ b/Cubical/Algebra/CommRing/Localisation/InvertingElements.agda @@ -298,18 +298,18 @@ module InvertingElementsBase (R' : CommRing ℓ) where -- "functorial action" of localizing away from an element module _ {A B : CommRing ℓ} (φ : CommRingHom A B) (f : fst A) where - module A = InvertingElementsBase A - module B = InvertingElementsBase B - module AU = S⁻¹RUniversalProp A A.[ f ⁿ|n≥0] (A.powersFormMultClosedSubset f) - module BU = S⁻¹RUniversalProp B B.[ φ $r f ⁿ|n≥0] (B.powersFormMultClosedSubset (φ $r f)) - open A.UniversalProp f open CommRingStr (snd B) + private + module A = InvertingElementsBase A + module B = InvertingElementsBase B + module AU = A.UniversalProp f + module BU = B.UniversalProp (φ $r f) - private φ/1 = BU./1AsCommRingHom ∘cr φ + φ/1 = BU./1AsCommRingHom ∘cr φ uniqInvElemHom : ∃![ χ ∈ CommRingHom A.R[1/ f ]AsCommRing B.R[1/ φ $r f ]AsCommRing ] (fst χ) ∘ (fst AU./1AsCommRingHom) ≡ (fst φ/1) - uniqInvElemHom = invElemUniversalProp _ φ/1 (BU.S/1⊆S⁻¹Rˣ _ ∣ 1 , sym (·IdR _) ∣₁) + uniqInvElemHom = AU.invElemUniversalProp _ φ/1 (BU.S/1⊆S⁻¹Rˣ _ ∣ 1 , sym (·IdR _) ∣₁) diff --git a/Cubical/Algebra/Monoid/BigOp.agda b/Cubical/Algebra/Monoid/BigOp.agda index 803074aaf2..d2a74b41e7 100644 --- a/Cubical/Algebra/Monoid/BigOp.agda +++ b/Cubical/Algebra/Monoid/BigOp.agda @@ -57,3 +57,17 @@ module MonoidBigOp (M' : Monoid ℓ) where bigOpSplit++ {n = zero} V W = sym (·IdL _) bigOpSplit++ {n = suc n} V W = cong (V zero ·_) (bigOpSplit++ (V ∘ suc) W) ∙ ·Assoc _ _ _ + + +module _ {M : Monoid ℓ} {M' : Monoid ℓ'} (φ : MonoidHom M M') where + module M = MonoidBigOp M + module M' = MonoidBigOp M' + open IsMonoidHom (φ .snd) + open MonoidStr ⦃...⦄ + private instance + _ = M .snd + _ = M' .snd + + presBigOp : {n : ℕ} (U : FinVec ⟨ M ⟩ n) → φ .fst (M.bigOp U) ≡ M'.bigOp (φ .fst ∘ U) + presBigOp {n = zero} U = presε + presBigOp {n = suc n} U = pres· _ _ ∙ cong (φ .fst (U zero) ·_) (presBigOp (U ∘ suc)) diff --git a/Cubical/Categories/Site/Instances/ZariskiCommRing.agda b/Cubical/Categories/Site/Instances/ZariskiCommRing.agda index 582192cd46..3405f09c76 100644 --- a/Cubical/Categories/Site/Instances/ZariskiCommRing.agda +++ b/Cubical/Categories/Site/Instances/ZariskiCommRing.agda @@ -1,21 +1,17 @@ {-# OPTIONS --safe --lossy-unification #-} module Cubical.Categories.Site.Instances.ZariskiCommRing where --- TODO: clean up imports + open import Cubical.Foundations.Prelude open import Cubical.Foundations.Function -open import Cubical.Foundations.HLevels -open import Cubical.Foundations.Equiv open import Cubical.Foundations.Structure -open import Cubical.Foundations.Isomorphism --- open import Cubical.Foundations.Powerset -open import Cubical.Data.Unit open import Cubical.Data.Nat using (ℕ) open import Cubical.Data.Sigma open import Cubical.Data.FinData open import Cubical.Algebra.Ring +open import Cubical.Algebra.Ring.BigOps open import Cubical.Algebra.CommRing open import Cubical.Algebra.CommRing.Localisation open import Cubical.Algebra.CommRing.Ideal @@ -26,36 +22,16 @@ open import Cubical.Categories.Instances.CommRings open import Cubical.Categories.Site.Coverage open import Cubical.Categories.Constructions.Slice -open import Cubical.HITs.PropositionalTruncation - -open Category hiding (_∘_) -open isUnivalent -open isIso -open RingHoms -open IsRingHom +open import Cubical.HITs.PropositionalTruncation as PT private variable ℓ ℓ' ℓ'' : Level --- module _ (R' : CommRing ℓ) {n : ℕ} (f : FinVec (fst R') (suc n)) where --- open isMultClosedSubset --- open CommRingTheory R' --- open RingTheory (CommRing→Ring R') --- open Sum (CommRing→Ring R') --- open CommIdeal R' --- open InvertingElementsBase R' --- open Exponentiation R' --- open CommRingStr ⦃...⦄ --- --- private --- R = fst R' --- ⟨_⟩ : {n : ℕ} → FinVec R n → CommIdeal --- ⟨ V ⟩ = ⟨ V ⟩[ R' ] --- ⟨f₀,⋯,fₙ⟩ = ⟨ f ⟩[ R' ] - open Coverage +open SliceOb +-- the type of unimodular vectors, i.e. generators of the 1-ideal record UniModVec (R : CommRing ℓ) : Type ℓ where open CommRingStr (str R) open CommIdeal R using (_∈_) @@ -65,11 +41,46 @@ record UniModVec (R : CommRing ℓ) : Type ℓ where f : FinVec ⟨ R ⟩ n isUniMod : 1r ∈ ⟨ f ⟩[ R ] -open SliceOb +module _ {A : CommRing ℓ} {B : CommRing ℓ'} (φ : CommRingHom A B) where + open UniModVec + open IsRingHom ⦃...⦄ + open CommRingStr ⦃...⦄ + open Sum (CommRing→Ring B) + open SumMap _ _ φ + private + module A = CommIdeal A + module B = CommIdeal B + instance + _ = A .snd + _ = B .snd + _ = φ .snd + + pullbackUniModVec : UniModVec A → UniModVec B + n (pullbackUniModVec um) = um .n + f (pullbackUniModVec um) i = φ $r um .f i + isUniMod (pullbackUniModVec um) = B.subst-∈ -- 1 ∈ ⟨ f₁ ,..., fₙ ⟩ → 1 ∈ ⟨ φ(f₁) ,..., φ(fₙ) ⟩ + ⟨ φ .fst ∘ um .f ⟩[ B ] + pres1 (PT.map mapHelper (um .isUniMod)) + where + mapHelper : Σ[ α ∈ FinVec ⟨ A ⟩ _ ] 1r ≡ linearCombination A α (um .f) + → Σ[ β ∈ FinVec ⟨ B ⟩ _ ] φ $r 1r ≡ linearCombination B β (φ .fst ∘ um .f) + fst (mapHelper (α , 1≡∑αf)) = φ .fst ∘ α + snd (mapHelper (α , 1≡∑αf)) = + subst (λ x → φ $r x ≡ linearCombination B (φ .fst ∘ α) (φ .fst ∘ um .f)) + (sym 1≡∑αf) + (∑Map _ ∙ ∑Ext (λ _ → pres· _ _)) + + +{- + + For 1 ∈ ⟨ f₁ ,..., fₙ ⟩ we get a cover by arrows _/1 : R → R[1/fᵢ] for i=1,...,n + Pullback along φ : A → B is given by the induced arrows A[1/fᵢ] → B[1/φ(fᵢ)] + +-} zariskiCoverage : Coverage (CommRingsCategory {ℓ = ℓ} ^op) ℓ ℓ-zero fst (covers zariskiCoverage R) = UniModVec R -fst (snd (covers zariskiCoverage R) um) = Fin n +fst (snd (covers zariskiCoverage R) um) = Fin n --patches where open UniModVec um S-ob (snd (snd (covers zariskiCoverage R) um) i) = R[1/ f i ]AsCommRing @@ -80,21 +91,17 @@ S-arr (snd (snd (covers zariskiCoverage R) um) i) = /1AsCommRingHom where open UniModVec um open InvertingElementsBase.UniversalProp R (f i) -pullbackStability zariskiCoverage {c = R} um {d = R'} φ = - ∣ um' , (λ i → ∣ i , ψ i , RingHom≡ (sym (ψComm i)) ∣₁) ∣₁ +pullbackStability zariskiCoverage {c = A} um {d = B} φ = + ∣ pullbackUniModVec φ um , (λ i → ∣ i , ψ i , RingHom≡ (sym (ψComm i)) ∣₁) ∣₁ where open UniModVec - um' : UniModVec R' - um' .n = um .n - um' .f i = φ $r um .f i - um' .isUniMod = {!!} + module A = InvertingElementsBase A + module B = InvertingElementsBase B + module AU = A.UniversalProp + module BU = B.UniversalProp - open InvertingElementsBase R - open InvertingElementsBase R' renaming (R[1/_]AsCommRing to R'[1/_]AsCommRing) using () - ψ : (i : Fin (um .n)) → CommRingHom R[1/ um .f i ]AsCommRing R'[1/ um' .f i ]AsCommRing + ψ : (i : Fin (um .n)) → CommRingHom A.R[1/ um .f i ]AsCommRing B.R[1/ φ $r um .f i ]AsCommRing ψ i = uniqInvElemHom φ (um .f i) .fst .fst - module R = UniversalProp - module R' = InvertingElementsBase.UniversalProp R' - ψComm : ∀ i → (ψ i .fst) ∘ (R._/1 (um .f i)) ≡ (R'._/1 (um' .f i)) ∘ φ .fst + ψComm : ∀ i → (ψ i .fst) ∘ (AU._/1 (um .f i)) ≡ (BU._/1 (φ $r um .f i)) ∘ φ .fst ψComm i = uniqInvElemHom φ (um .f i) .fst .snd From c93f9ec73930e8a85310ca70a2fe2f3dff140efd Mon Sep 17 00:00:00 2001 From: mzeuner Date: Mon, 4 Dec 2023 16:50:51 +0100 Subject: [PATCH 06/10] only zero case left --- .../Site/Instances/ZariskiCommRing.agda | 103 +++++++++++++++++- Cubical/Categories/Site/Sheaf.agda | 19 ++++ 2 files changed, 121 insertions(+), 1 deletion(-) diff --git a/Cubical/Categories/Site/Instances/ZariskiCommRing.agda b/Cubical/Categories/Site/Instances/ZariskiCommRing.agda index 3405f09c76..7482fe0f9e 100644 --- a/Cubical/Categories/Site/Instances/ZariskiCommRing.agda +++ b/Cubical/Categories/Site/Instances/ZariskiCommRing.agda @@ -4,11 +4,13 @@ module Cubical.Categories.Site.Instances.ZariskiCommRing where open import Cubical.Foundations.Prelude open import Cubical.Foundations.Function +open import Cubical.Foundations.Isomorphism open import Cubical.Foundations.Structure -open import Cubical.Data.Nat using (ℕ) +open import Cubical.Data.Nat using (ℕ ; zero ; suc) open import Cubical.Data.Sigma open import Cubical.Data.FinData +open import Cubical.Data.FinData.Order renaming (_<'Fin_ to _<_) open import Cubical.Algebra.Ring open import Cubical.Algebra.Ring.BigOps @@ -20,7 +22,9 @@ open import Cubical.Algebra.CommRing.FGIdeal open import Cubical.Categories.Category open import Cubical.Categories.Instances.CommRings open import Cubical.Categories.Site.Coverage +open import Cubical.Categories.Site.Sheaf open import Cubical.Categories.Constructions.Slice +open import Cubical.Categories.Yoneda open import Cubical.HITs.PropositionalTruncation as PT @@ -33,6 +37,9 @@ open SliceOb -- the type of unimodular vectors, i.e. generators of the 1-ideal record UniModVec (R : CommRing ℓ) : Type ℓ where + constructor + unimodvec + open CommRingStr (str R) open CommIdeal R using (_∈_) @@ -105,3 +112,97 @@ pullbackStability zariskiCoverage {c = A} um {d = B} φ = ψComm : ∀ i → (ψ i .fst) ∘ (AU._/1 (um .f i)) ≡ (BU._/1 (φ $r um .f i)) ∘ φ .fst ψComm i = uniqInvElemHom φ (um .f i) .fst .snd + + +-- this defines a subcanonical coverage +-- the proof is analoguous to the case of lattice sheaves, +-- see "isLimConeLocCone" in Cubical.Algebra.CommRing.Localisation.Limit +-- first, a lemma +module SubcanonicalLemmas (A R : CommRing ℓ) where + open CommRingStr ⦃...⦄ + open CommIdeal R using (_∈_) + + private instance + _ = A .snd + _ = R .snd + + module _ + {n : ℕ} + (f : FinVec ⟨ R ⟩ (suc n)) -- have to treat case of empty vec separately + (isUniModF : 1r ∈ ⟨ f ⟩[ R ]) + (fam@(φ , isCompatibleφ) : CompatibleFamily (yo A) + (str (covers zariskiCoverage R) + (unimodvec (suc n) f isUniModF))) + where + open InvertingElementsBase R + open RingHoms + module U i = UniversalProp (f i) + module UP i j = UniversalProp (f i · f j) + + private + _/1ⁱ : ⟨ R ⟩ → {i : Fin (suc n)} → R[1/ (f i) ] + (r /1ⁱ) {i = i} = U._/1 i r + + + applyEqualizerLemma : ∀ a → ∃![ r ∈ ⟨ R ⟩ ] ∀ i → r /1ⁱ ≡ φ i .fst a + applyEqualizerLemma a = equalizerLemma R f isUniModF (λ i → φ i .fst a) path + where + pathHelper : ∀ i j → χˡ R f i j ∘r (U./1AsCommRingHom i) + ≡ χʳ R f i j ∘r (U./1AsCommRingHom j) + pathHelper i j = RingHom≡ + (χˡUnique R f i j .fst .snd ∙ sym (χʳUnique R f i j .fst .snd)) + + path : ∀ i j → χˡ R f i j .fst (φ i $r a) ≡ χʳ R f i j .fst (φ j $r a) + path i j = funExt⁻ (cong fst (isCompatibleφ i j _ _ _ (pathHelper i j))) a + + inducedHom : CommRingHom A R + fst inducedHom a = applyEqualizerLemma a .fst .fst + snd inducedHom = makeIsRingHom + (cong fst (applyEqualizerLemma 1r .snd (1r , 1Coh))) + (λ x y → cong fst (applyEqualizerLemma (x + y) .snd (_ , +Coh x y))) + (λ x y → cong fst (applyEqualizerLemma (x · y) .snd (_ , ·Coh x y))) + where + open IsRingHom + 1Coh : ∀ i → (1r /1ⁱ ≡ φ i .fst 1r) + 1Coh i = sym (φ i .snd .pres1) + + +Coh : ∀ x y i → ((fst inducedHom x + fst inducedHom y) /1ⁱ ≡ φ i .fst (x + y)) + +Coh x y i = let instance _ = snd R[1/ f i ]AsCommRing in + U./1AsCommRingHom i .snd .pres+ _ _ + ∙∙ cong₂ _+_ (applyEqualizerLemma x .fst .snd i) (applyEqualizerLemma y .fst .snd i) + ∙∙ sym (φ i .snd .pres+ x y) + + ·Coh : ∀ x y i → ((fst inducedHom x · fst inducedHom y) /1ⁱ ≡ φ i .fst (x · y)) + ·Coh x y i = let instance _ = snd R[1/ f i ]AsCommRing in + U./1AsCommRingHom i .snd .pres· _ _ + ∙∙ cong₂ _·_ (applyEqualizerLemma x .fst .snd i) (applyEqualizerLemma y .fst .snd i) + ∙∙ sym (φ i .snd .pres· x y) + + inducedHomUnique : ∀ (ψ : CommRingHom A R) + → (∀ a i → (ψ $r a) /1ⁱ ≡ φ i $r a) + → inducedHom ≡ ψ + inducedHomUnique ψ ψ/1≡φ = + RingHom≡ + (funExt + (λ a → cong fst (applyEqualizerLemma a .snd (ψ $r a , ψ/1≡φ a)))) + + +isSubcanonicalZariskiCoverage : isSubcanonical + (CommRingsCategory {ℓ = ℓ} ^op) + zariskiCoverage +isSubcanonicalZariskiCoverage A R (unimodvec zero f isUniModF) = {!!} + -- better way than pattern matching inside unimodvec??? +isSubcanonicalZariskiCoverage A R (unimodvec (suc n) f isUniModF) = isoToIsEquiv theIso + where + open Iso + open SubcanonicalLemmas A R + um = (unimodvec (suc n) f isUniModF) + + theIso : Iso (CommRingHom A R) + (CompatibleFamily (yo A) (str (covers zariskiCoverage R) um)) + fun theIso = elementToCompatibleFamily _ _ + inv theIso fam = inducedHom f isUniModF fam + rightInv theIso fam = CompatibleFamily≡ _ _ _ _ + λ i → RingHom≡ (funExt + λ a → applyEqualizerLemma f isUniModF fam a .fst .snd i) + leftInv theIso φ = inducedHomUnique _ _ _ _ λ _ _ → refl diff --git a/Cubical/Categories/Site/Sheaf.agda b/Cubical/Categories/Site/Sheaf.agda index c1fa5b53ac..12f0ea25af 100644 --- a/Cubical/Categories/Site/Sheaf.agda +++ b/Cubical/Categories/Site/Sheaf.agda @@ -20,6 +20,7 @@ open import Cubical.Categories.Site.Coverage open import Cubical.Categories.Presheaf open import Cubical.Categories.Functor open import Cubical.Categories.Constructions.FullSubcategory +open import Cubical.Categories.Yoneda module _ {ℓ ℓ' : Level} @@ -62,6 +63,11 @@ module _ (isSetΠ (λ i → str (P ⟅ patchObj cov i ⟆))) isPropIsCompatibleFamily + CompatibleFamily≡ : (fam fam' : CompatibleFamily) + → (∀ i → fam .fst i ≡ fam' .fst i) + → fam ≡ fam' + CompatibleFamily≡ fam fam' p = Σ≡Prop isPropIsCompatibleFamily (funExt p) + elementToCompatibleFamily : ⟨ P ⟅ c ⟆ ⟩ → CompatibleFamily elementToCompatibleFamily x = (λ i → (P ⟪ patchArr cov i ⟫) x) , @@ -136,3 +142,16 @@ module _ (ℓ-max (ℓ-max (ℓ-max (ℓ-max ℓ ℓ') ℓcov) ℓpat) (ℓ-suc ℓF)) (ℓ-max (ℓ-max ℓ ℓ') ℓF) SheafCategory = FullSubcategory (PresheafCategory C ℓF) (isSheaf J) + + +module _ + {ℓ ℓ' ℓcov ℓpat : Level} + (C : Category ℓ ℓ') + (J : Coverage C ℓcov ℓpat) + where + + isSubcanonical : Type (ℓ-max (ℓ-max (ℓ-max ℓ ℓ') ℓcov) ℓpat) + isSubcanonical = ∀ c → isSheaf J (yo c) + + isPropIsSubcanonical : isProp isSubcanonical + isPropIsSubcanonical = isPropΠ λ c → isPropIsSheaf J (yo c) From 095f7a15c7a844ced45bc8018d01bb9409c49c80 Mon Sep 17 00:00:00 2001 From: mzeuner Date: Mon, 4 Dec 2023 22:32:28 +0100 Subject: [PATCH 07/10] finish zero case --- Cubical/Categories/Instances/CommRings.agda | 20 +++++++++++++++- .../Site/Instances/ZariskiCommRing.agda | 23 ++++++++++++++++++- 2 files changed, 41 insertions(+), 2 deletions(-) diff --git a/Cubical/Categories/Instances/CommRings.agda b/Cubical/Categories/Instances/CommRings.agda index 4b9353cabe..326022b5ce 100644 --- a/Cubical/Categories/Instances/CommRings.agda +++ b/Cubical/Categories/Instances/CommRings.agda @@ -1,4 +1,4 @@ -{-# OPTIONS --safe #-} +{-# OPTIONS --safe --lossy-unification #-} module Cubical.Categories.Instances.CommRings where open import Cubical.Foundations.Prelude @@ -105,6 +105,24 @@ module _ {ℓ : Level} where snd (fst (snd TerminalCommRing y)) = makeIsRingHom refl (λ _ _ → refl) (λ _ _ → refl) snd (snd TerminalCommRing y) f = RingHom≡ (funExt (λ _ → refl)) + open RingTheory + trivialIsTerminalCommRing : ∀ (R : CommRing ℓ) + → R .snd .0r ≡ R .snd .1r + → isTerminal CommRingsCategory R + fst (fst (trivialIsTerminalCommRing R 0≡1 A)) _ = R .snd .0r + pres0 (snd (fst (trivialIsTerminalCommRing R 0≡1 A))) = refl + pres1 (snd (fst (trivialIsTerminalCommRing R 0≡1 A))) = 0≡1 + pres+ (snd (fst (trivialIsTerminalCommRing R 0≡1 A))) _ _ = sym (R .snd .+IdR _) + pres· (snd (fst (trivialIsTerminalCommRing R 0≡1 A))) _ _ = + sym (0RightAnnihilates (CommRing→Ring R) _) + pres- (snd (fst (trivialIsTerminalCommRing R 0≡1 A))) _ = + sym (0Selfinverse (CommRing→Ring R)) + snd (trivialIsTerminalCommRing R 0≡1 A) f = + RingHom≡ (funExt λ x → sym (0RightAnnihilates (CommRing→Ring R) _) + ∙∙ cong (R .snd ._·_ (f .fst x)) 0≡1 + ∙∙ R .snd .·IdR _) + + open Pullback {- diff --git a/Cubical/Categories/Site/Instances/ZariskiCommRing.agda b/Cubical/Categories/Site/Instances/ZariskiCommRing.agda index 7482fe0f9e..602d26e9d8 100644 --- a/Cubical/Categories/Site/Instances/ZariskiCommRing.agda +++ b/Cubical/Categories/Site/Instances/ZariskiCommRing.agda @@ -20,6 +20,7 @@ open import Cubical.Algebra.CommRing.Ideal open import Cubical.Algebra.CommRing.FGIdeal open import Cubical.Categories.Category +open import Cubical.Categories.Limits.Terminal open import Cubical.Categories.Instances.CommRings open import Cubical.Categories.Site.Coverage open import Cubical.Categories.Site.Sheaf @@ -190,8 +191,28 @@ module SubcanonicalLemmas (A R : CommRing ℓ) where isSubcanonicalZariskiCoverage : isSubcanonical (CommRingsCategory {ℓ = ℓ} ^op) zariskiCoverage -isSubcanonicalZariskiCoverage A R (unimodvec zero f isUniModF) = {!!} +isSubcanonicalZariskiCoverage A R (unimodvec zero f isUniModF) = + isoToIsEquiv (isContr→Iso' + (trivialIsTerminalCommRing R 0≡1 A) + isContrCompatibleFamily _) -- better way than pattern matching inside unimodvec??? + where + um = (unimodvec zero f isUniModF) + open CommRingStr (R .snd) + + 0≡1 : 0r ≡ 1r + 0≡1 = PT.rec (is-set _ _) Σhelper isUniModF + where + Σhelper : Σ[ α ∈ FinVec ⟨ R ⟩ zero ] 1r ≡ linearCombination R α f + → 0r ≡ 1r + Σhelper (_ , 1≡αf) = sym 1≡αf + + isContrCompatibleFamily : isContr (CompatibleFamily (yo A) + (str (covers zariskiCoverage R) um)) + fst (fst isContrCompatibleFamily) () + snd (fst isContrCompatibleFamily) () + snd isContrCompatibleFamily _ = CompatibleFamily≡ _ _ _ _ λ () + isSubcanonicalZariskiCoverage A R (unimodvec (suc n) f isUniModF) = isoToIsEquiv theIso where open Iso From 5aa14300e13148dba8c93a660f54aaf61e40e816 Mon Sep 17 00:00:00 2001 From: mzeuner Date: Tue, 5 Dec 2023 18:05:52 +0100 Subject: [PATCH 08/10] def of scheme --- Cubical/Categories/Instances/ZFunctors.agda | 53 ++++++++++++++++++++- 1 file changed, 52 insertions(+), 1 deletion(-) diff --git a/Cubical/Categories/Instances/ZFunctors.agda b/Cubical/Categories/Instances/ZFunctors.agda index 701f7c4020..5fca914ad2 100644 --- a/Cubical/Categories/Instances/ZFunctors.agda +++ b/Cubical/Categories/Instances/ZFunctors.agda @@ -37,9 +37,13 @@ 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.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 @@ -415,7 +419,6 @@ module _ {ℓ : Level} where hasAffineCover : Type (ℓ-suc ℓ) hasAffineCover = ∥ AffineCover ∥₁ - -- TODO: A ℤ-functor is a qcqs-scheme if it is a Zariski sheaf and has an affine cover -- the structure sheaf private COᵒᵖ = (DistLatticeCategory (CompOpenDistLattice .F-ob X)) ^op @@ -448,3 +451,51 @@ module _ {ℓ : Level} where F-hom 𝓞 U≥V = Γ .F-hom (compOpenIncl U≥V) F-id 𝓞 = cong (Γ .F-hom) compOpenInclId ∙ Γ .F-id F-seq 𝓞 _ _ = cong (Γ .F-hom) (compOpenInclSeq _ _) ∙ Γ .F-seq _ _ + + +-- qcqs-schemes as Zariski sheaves (local ℤ-functors) with an affine cover in the sense above +module _ {ℓ : Level} where + + open Iso + open Functor + open NatTrans + open NatIso + open DistLatticeStr ⦃...⦄ + open CommRingStr ⦃...⦄ + open IsRingHom + open IsLatticeHom + open ZarLat + open ZarLatUniversalProp + + isLocal : ℤFunctor → Type (ℓ-suc ℓ) + isLocal X = isSheaf zariskiCoverage X + + isQcQsScheme : ℤFunctor → Type (ℓ-suc ℓ) + isQcQsScheme X = isLocal X × hasAffineCover X + + isQcQsSchemeAffine : ∀ (A : CommRing ℓ) → isQcQsScheme (Sp .F-ob A) + fst (isQcQsSchemeAffine A) = isSubcanonicalZariskiCoverage A + snd (isQcQsSchemeAffine A) = ∣ singlCover ∣₁ -- separate lemma somewhere??? + where + open AffineCover + open isIso + + U₁ : CompactOpen (Sp .F-ob A) + N-ob U₁ B _ = let instance _ = B .snd in + D B 1r + N-hom U₁ {y = B} φ = let instance _ = ZariskiLattice B .snd in + funExt (λ _ → cong (D B) (sym (φ .snd .pres1)) ∙ sym (∨lRid _)) + + SpA≅U₁ : NatIso (Sp .F-ob A) ⟦ U₁ ⟧ᶜᵒ + N-ob (trans SpA≅U₁) _ φ = φ , refl + N-hom (trans SpA≅U₁) _ = funExt λ _ → Σ≡Prop (λ _ → squash/ _ _) refl + inv (nIso SpA≅U₁ B) = fst + sec (nIso SpA≅U₁ B) = funExt λ _ → Σ≡Prop (λ _ → squash/ _ _) refl + ret (nIso SpA≅U₁ B) = funExt λ _ → refl + + singlCover : AffineCover (Sp .F-ob A) + n singlCover = 1 + U singlCover zero = U₁ + covers singlCover = + makeNatTransPath (funExt₂ λ B _ → let instance _ = ZariskiLattice B .snd in ∨lRid _) + isAffineU singlCover zero = ∣ A , SpA≅U₁ ∣₁ From 9b40562ecb03c164432b528670d2a6350ea0ba1e Mon Sep 17 00:00:00 2001 From: mzeuner Date: Wed, 6 Dec 2023 14:51:49 +0100 Subject: [PATCH 09/10] renaming --- Cubical/Categories/Instances/ZFunctors.agda | 203 ++++++++++---------- 1 file changed, 98 insertions(+), 105 deletions(-) diff --git a/Cubical/Categories/Instances/ZFunctors.agda b/Cubical/Categories/Instances/ZFunctors.agda index 5fca914ad2..ed1abf7d22 100644 --- a/Cubical/Categories/Instances/ZFunctors.agda +++ b/Cubical/Categories/Instances/ZFunctors.agda @@ -63,11 +63,11 @@ module _ {ℓ : Level} where open CommRingStr ⦃...⦄ open IsRingHom - -- using the naming conventions of Nieper-Wisskirchen + -- using the naming conventions of Demazure & Gabriel ℤFunctor = Functor (CommRingsCategory {ℓ = ℓ}) (SET ℓ) ℤFUNCTOR = FUNCTOR (CommRingsCategory {ℓ = ℓ}) (SET ℓ) - -- Yoneda in the notation of Demazure-Gabriel, + -- 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)} @@ -79,21 +79,21 @@ module _ {ℓ : Level} where 𝔸¹ = ForgetfulCommRing→Set -- the global sections functor - Γ : Functor ℤFUNCTOR (CommRingsCategory {ℓ = ℓ-suc ℓ} ^op) - fst (F-ob Γ X) = X ⇒ 𝔸¹ + 𝓞 : 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 + 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-hom (CommRingStr.0r (snd (F-ob 𝓞 X))) φ = funExt λ _ → sym (φ .snd .pres0) - N-ob (CommRingStr.1r (snd (F-ob Γ X))) A _ = 1r + 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-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 + 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 + N-hom ((snd (F-ob 𝓞 X) CommRingStr.+ α) β) {x = A} {y = B} φ = funExt path where instance _ = A .snd @@ -106,9 +106,9 @@ module _ {ℓ : Level} where ≡⟨ 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 + 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 + N-hom ((snd (F-ob 𝓞 X) CommRingStr.· α) β) {x = A} {y = B} φ = funExt path where instance _ = A .snd @@ -121,9 +121,9 @@ module _ {ℓ : Level} where ≡⟨ 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 + 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 + N-hom ((CommRingStr.- snd (F-ob 𝓞 X)) α) {x = A} {y = B} φ = funExt path where instance _ = A .snd @@ -133,7 +133,7 @@ module _ {ℓ : Level} where - φ .fst (α .N-ob A x) ≡⟨ sym (φ .snd .pres- _) ⟩ φ .fst (- α .N-ob A x) ∎ - CommRingStr.isCommRing (snd (F-ob Γ X)) = makeIsCommRing + CommRingStr.isCommRing (snd (F-ob 𝓞 X)) = makeIsCommRing isSetNatTrans (λ _ _ _ → makeNatTransPath (funExt₂ λ A _ → A .snd .CommRingStr.+Assoc _ _ _)) (λ _ → makeNatTransPath (funExt₂ λ A _ → A .snd .CommRingStr.+IdR _)) @@ -145,19 +145,19 @@ module _ {ℓ : Level} where (λ _ _ → 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) + 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)) + -- functoriality of 𝓞 + F-id 𝓞 = RingHom≡ (funExt λ _ → makeNatTransPath (funExt₂ λ _ _ → refl)) + F-seq 𝓞 _ _ = RingHom≡ (funExt λ _ → makeNatTransPath (funExt₂ λ _ _ → refl)) --- we get an adjunction Γ ⊣ Sp modulo size issues +-- we get an adjunction 𝓞 ⊣ Sp modulo size issues module AdjBij where open Functor @@ -166,7 +166,7 @@ module AdjBij where open IsRingHom private module _ {A : CommRing ℓ} {X : ℤFunctor {ℓ}} where - _♭ : CommRingHom A (Γ .F-ob X) → X ⇒ Sp .F-ob A + _♭ : 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) @@ -179,7 +179,7 @@ module AdjBij where -- the other direction is just precomposition modulo Yoneda - _♯ : X ⇒ Sp .F-ob A → CommRingHom A (Γ .F-ob X) + _♯ : 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) @@ -193,34 +193,34 @@ module AdjBij where ♭♯Id : ∀ (α : X ⇒ Sp .F-ob A) → ((α ♯) ♭) ≡ α ♭♯Id _ = makeNatTransPath (funExt₂ λ _ _ → RingHom≡ (funExt (λ _ → refl))) - ♯♭Id : ∀ (φ : CommRingHom A (Γ .F-ob X)) → ((φ ♭) ♯) ≡ φ + ♯♭Id : ∀ (φ : CommRingHom A (𝓞 .F-ob X)) → ((φ ♭) ♯) ≡ φ ♯♭Id _ = RingHom≡ (funExt λ _ → makeNatTransPath (funExt₂ λ _ _ → refl)) - Γ⊣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 + 𝓞⊣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)))) + 𝓞⊣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) + 𝓞⊣SpNatCommRing : {X : ℤFunctor {ℓ}} {A B : CommRing ℓ} + (φ : CommRingHom A (𝓞 .F-ob X)) (ψ : CommRingHom B A) → (φ ∘cr ψ) ♭ ≡ (φ ♭) ●ᵛ Sp .F-hom ψ - Γ⊣SpNatCommRing _ _ = makeNatTransPath (funExt₂ λ _ _ → RingHom≡ (funExt (λ _ → refl))) + 𝓞⊣SpNatCommRing _ _ = makeNatTransPath (funExt₂ λ _ _ → RingHom≡ (funExt (λ _ → refl))) -- the counit is an equivalence private - ε : (A : CommRing ℓ) → CommRingHom A ((Γ ∘F Sp) .F-ob A) + ε : (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 + 𝓞⊣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) + 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 α @@ -228,7 +228,7 @@ module AdjBij where 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 @@ -243,7 +243,7 @@ module _ {ℓ : Level} where -- 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. +-- 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 @@ -251,7 +251,7 @@ private module AffineDefs {ℓ : Level} where open NatTrans open Iso open IsRingHom - η : (X : ℤFunctor) (A : CommRing ℓ) → X .F-ob A .fst → CommRingHom (Γ .F-ob X) A + η : (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 @@ -266,7 +266,7 @@ private module AffineDefs {ℓ : Level} where -- 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 α + → η Y A (α .N-ob A x) ≡ η X A x ∘cr 𝓞 .F-hom α ηHom _ _ _ = RingHom≡ refl isAffine' : (X : ℤFunctor) → Type (ℓ-suc ℓ) @@ -280,6 +280,7 @@ module _ {ℓ : Level} where open Iso open Functor open NatTrans + open NatIso open DistLatticeStr ⦃...⦄ open CommRingStr ⦃...⦄ open IsRingHom @@ -288,14 +289,14 @@ module _ {ℓ : Level} where open ZarLatUniversalProp -- the Zariski lattice classifying compact open subobjects - 𝓛 : ℤFunctor {ℓ = ℓ} - F-ob 𝓛 A = ZL A , SQ.squash/ - F-hom 𝓛 φ = inducedZarLatHom φ .fst - F-id 𝓛 {A} = cong fst (inducedZarLatHomId A) - F-seq 𝓛 φ ψ = cong fst (inducedZarLatHomSeq φ ψ) + 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 φ ψ) CompactOpen : ℤFunctor → Type (ℓ-suc ℓ) - CompactOpen X = X ⇒ 𝓛 + CompactOpen X = X ⇒ ZarLatFun -- the induced subfunctor ⟦_⟧ᶜᵒ : {X : ℤFunctor} (U : CompactOpen X) → ℤFunctor @@ -309,9 +310,9 @@ module _ {ℓ : Level} where _ = 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 ⟩ - 𝓛 .F-hom φ (U .N-ob A x) ≡⟨ cong (𝓛 .F-hom φ) Ux≡D1 ⟩ - 𝓛 .F-hom φ (D A 1r) ≡⟨ inducedZarLatHom φ .snd .pres1 ⟩ + 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))) @@ -328,7 +329,7 @@ module _ {ℓ : Level} where CompOpenDistLattice : Functor ℤFUNCTOR (DistLatticesCategory {ℓ = ℓ-suc ℓ} ^op) fst (F-ob CompOpenDistLattice X) = CompactOpen X - -- lattice structure induce by internal lattice object 𝓛 + -- 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 @@ -352,12 +353,12 @@ module _ {ℓ : Level} where _ = 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) - ≡ 𝓛 .F-hom φ (U .N-ob A x ∨l V .N-ob A 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) ⟩ - 𝓛 .F-hom φ (U .N-ob A x) ∨l 𝓛 .F-hom φ (V .N-ob A x) + ZarLatFun .F-hom φ (U .N-ob A x) ∨l ZarLatFun .F-hom φ (V .N-ob A x) ≡⟨ sym (inducedZarLatHom φ .snd .pres∨l _ _) ⟩ - 𝓛 .F-hom φ (U .N-ob A x ∨l V .N-ob A x) ∎ + 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 @@ -367,12 +368,12 @@ module _ {ℓ : Level} where _ = 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) - ≡ 𝓛 .F-hom φ (U .N-ob A x ∧l V .N-ob A 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) ⟩ - 𝓛 .F-hom φ (U .N-ob A x) ∧l 𝓛 .F-hom φ (V .N-ob A x) + ZarLatFun .F-hom φ (U .N-ob A x) ∧l ZarLatFun .F-hom φ (V .N-ob A x) ≡⟨ sym (inducedZarLatHom φ .snd .pres∧l _ _) ⟩ - 𝓛 .F-hom φ (U .N-ob A x ∧l V .N-ob A x) ∎ + 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 @@ -446,56 +447,48 @@ module _ {ℓ : Level} where compOpenInclSeq _ _ = makeNatTransPath (funExt₂ (λ _ _ → Σ≡Prop (λ _ → squash/ _ _) refl)) - 𝓞 : Functor COᵒᵖ (CommRingsCategory {ℓ = ℓ-suc ℓ}) - F-ob 𝓞 U = Γ .F-ob ⟦ U ⟧ᶜᵒ - F-hom 𝓞 U≥V = Γ .F-hom (compOpenIncl U≥V) - F-id 𝓞 = cong (Γ .F-hom) compOpenInclId ∙ Γ .F-id - F-seq 𝓞 _ _ = cong (Γ .F-hom) (compOpenInclSeq _ _) ∙ Γ .F-seq _ _ + 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 _ _ + -- the canonical one element affine cover of a representable + module _ (A : CommRing ℓ) where + open AffineCover + open isIso --- qcqs-schemes as Zariski sheaves (local ℤ-functors) with an affine cover in the sense above -module _ {ℓ : Level} where + private + U₁ : CompactOpen (Sp .F-ob A) + N-ob U₁ B _ = let instance _ = B .snd in + D B 1r + N-hom U₁ {y = B} φ = let instance _ = ZariskiLattice B .snd in + funExt (λ _ → cong (D B) (sym (φ .snd .pres1)) ∙ sym (∨lRid _)) + + SpA≅U₁ : NatIso (Sp .F-ob A) ⟦ U₁ ⟧ᶜᵒ + N-ob (trans SpA≅U₁) _ φ = φ , refl + N-hom (trans SpA≅U₁) _ = funExt λ _ → Σ≡Prop (λ _ → squash/ _ _) refl + inv (nIso SpA≅U₁ B) = fst + sec (nIso SpA≅U₁ B) = funExt λ _ → Σ≡Prop (λ _ → squash/ _ _) refl + ret (nIso SpA≅U₁ B) = funExt λ _ → refl + + singlAffineCover : AffineCover (Sp .F-ob A) + n singlAffineCover = 1 + U singlAffineCover zero = U₁ + covers singlAffineCover = + makeNatTransPath (funExt₂ λ B _ → let instance _ = ZariskiLattice B .snd in ∨lRid _) + isAffineU singlAffineCover zero = ∣ A , SpA≅U₁ ∣₁ - open Iso - open Functor - open NatTrans - open NatIso - open DistLatticeStr ⦃...⦄ - open CommRingStr ⦃...⦄ - open IsRingHom - open IsLatticeHom - open ZarLat - open ZarLatUniversalProp + -- qcqs-schemes as Zariski sheaves (local ℤ-functors) with an affine cover in the sense above + -- TODO: work in Zariski sheaves instead of ℤ-functors??? isLocal : ℤFunctor → Type (ℓ-suc ℓ) isLocal X = isSheaf zariskiCoverage X isQcQsScheme : ℤFunctor → Type (ℓ-suc ℓ) isQcQsScheme X = isLocal X × hasAffineCover X + -- affine schemes are qcqs-schemes isQcQsSchemeAffine : ∀ (A : CommRing ℓ) → isQcQsScheme (Sp .F-ob A) fst (isQcQsSchemeAffine A) = isSubcanonicalZariskiCoverage A - snd (isQcQsSchemeAffine A) = ∣ singlCover ∣₁ -- separate lemma somewhere??? - where - open AffineCover - open isIso - - U₁ : CompactOpen (Sp .F-ob A) - N-ob U₁ B _ = let instance _ = B .snd in - D B 1r - N-hom U₁ {y = B} φ = let instance _ = ZariskiLattice B .snd in - funExt (λ _ → cong (D B) (sym (φ .snd .pres1)) ∙ sym (∨lRid _)) - - SpA≅U₁ : NatIso (Sp .F-ob A) ⟦ U₁ ⟧ᶜᵒ - N-ob (trans SpA≅U₁) _ φ = φ , refl - N-hom (trans SpA≅U₁) _ = funExt λ _ → Σ≡Prop (λ _ → squash/ _ _) refl - inv (nIso SpA≅U₁ B) = fst - sec (nIso SpA≅U₁ B) = funExt λ _ → Σ≡Prop (λ _ → squash/ _ _) refl - ret (nIso SpA≅U₁ B) = funExt λ _ → refl - - singlCover : AffineCover (Sp .F-ob A) - n singlCover = 1 - U singlCover zero = U₁ - covers singlCover = - makeNatTransPath (funExt₂ λ B _ → let instance _ = ZariskiLattice B .snd in ∨lRid _) - isAffineU singlCover zero = ∣ A , SpA≅U₁ ∣₁ + snd (isQcQsSchemeAffine A) = ∣ singlAffineCover A ∣₁ From 947871f71283f7ee0c910a0eb486611d605e07c7 Mon Sep 17 00:00:00 2001 From: mzeuner Date: Wed, 17 Jan 2024 16:15:14 +0100 Subject: [PATCH 10/10] cleanup aff sch --- Cubical/Categories/Instances/ZFunctors.agda | 35 ++++++++++----------- 1 file changed, 16 insertions(+), 19 deletions(-) diff --git a/Cubical/Categories/Instances/ZFunctors.agda b/Cubical/Categories/Instances/ZFunctors.agda index ed1abf7d22..b738891af7 100644 --- a/Cubical/Categories/Instances/ZFunctors.agda +++ b/Cubical/Categories/Instances/ZFunctors.agda @@ -404,6 +404,18 @@ module _ {ℓ : Level} where (funExt λ _ → makeNatTransPath (funExt₂ λ _ _ → refl)) + module _ (X : ℤFunctor) where + open isIso + private instance _ = (CompOpenDistLattice .F-ob X) .snd + -- better name? + X≅⟦1⟧ : NatIso X ⟦ 1l ⟧ᶜᵒ + N-ob (trans X≅⟦1⟧) _ φ = φ , refl + N-hom (trans X≅⟦1⟧) _ = funExt λ _ → Σ≡Prop (λ _ → squash/ _ _) refl + inv (nIso X≅⟦1⟧ B) = fst + sec (nIso X≅⟦1⟧ B) = funExt λ _ → Σ≡Prop (λ _ → squash/ _ _) refl + ret (nIso X≅⟦1⟧ B) = funExt λ _ → refl + + module _ (X : ℤFunctor) where open Join (CompOpenDistLattice .F-ob X) open JoinSemilattice (Lattice→JoinSemilattice (DistLattice→Lattice (CompOpenDistLattice .F-ob X))) @@ -456,28 +468,13 @@ module _ {ℓ : Level} where -- the canonical one element affine cover of a representable module _ (A : CommRing ℓ) where open AffineCover - open isIso - - private - U₁ : CompactOpen (Sp .F-ob A) - N-ob U₁ B _ = let instance _ = B .snd in - D B 1r - N-hom U₁ {y = B} φ = let instance _ = ZariskiLattice B .snd in - funExt (λ _ → cong (D B) (sym (φ .snd .pres1)) ∙ sym (∨lRid _)) - - SpA≅U₁ : NatIso (Sp .F-ob A) ⟦ U₁ ⟧ᶜᵒ - N-ob (trans SpA≅U₁) _ φ = φ , refl - N-hom (trans SpA≅U₁) _ = funExt λ _ → Σ≡Prop (λ _ → squash/ _ _) refl - inv (nIso SpA≅U₁ B) = fst - sec (nIso SpA≅U₁ B) = funExt λ _ → Σ≡Prop (λ _ → squash/ _ _) refl - ret (nIso SpA≅U₁ B) = funExt λ _ → refl + private instance _ = (CompOpenDistLattice ⟅ Sp ⟅ A ⟆ ⟆) .snd singlAffineCover : AffineCover (Sp .F-ob A) n singlAffineCover = 1 - U singlAffineCover zero = U₁ - covers singlAffineCover = - makeNatTransPath (funExt₂ λ B _ → let instance _ = ZariskiLattice B .snd in ∨lRid _) - isAffineU singlAffineCover zero = ∣ A , SpA≅U₁ ∣₁ + U singlAffineCover zero = 1l + covers singlAffineCover = ∨lRid _ + isAffineU singlAffineCover zero = ∣ A , X≅⟦1⟧ (Sp ⟅ A ⟆) ∣₁ -- qcqs-schemes as Zariski sheaves (local ℤ-functors) with an affine cover in the sense above