From 7d4cdfa1f475faf2d592b5c5a65f2dce5962d526 Mon Sep 17 00:00:00 2001 From: mzeuner Date: Mon, 23 Aug 2021 19:44:28 +0200 Subject: [PATCH 01/18] 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/18] 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 8aef51b76891e16b6befd76f1f6031fd8b2885e2 Mon Sep 17 00:00:00 2001 From: mzeuner Date: Wed, 11 Oct 2023 00:04:35 +0200 Subject: [PATCH 03/18] get started --- .../Categories/Instances/FPAlgebrasSmall.agda | 103 ++++++++++++++++++ 1 file changed, 103 insertions(+) create mode 100644 Cubical/Categories/Instances/FPAlgebrasSmall.agda diff --git a/Cubical/Categories/Instances/FPAlgebrasSmall.agda b/Cubical/Categories/Instances/FPAlgebrasSmall.agda new file mode 100644 index 0000000000..bd37b01ab4 --- /dev/null +++ b/Cubical/Categories/Instances/FPAlgebrasSmall.agda @@ -0,0 +1,103 @@ +{-# OPTIONS --safe --lossy-unification #-} +module Cubical.Categories.Instances.FPAlgebrasSmall 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.Foundations.Structure + +open import Cubical.Data.Unit +open import Cubical.Data.Sigma +open import Cubical.Data.Nat +open import Cubical.Data.FinData + +open import Cubical.Algebra.Ring +open import Cubical.Algebra.CommRing +open import Cubical.Algebra.Algebra +open import Cubical.Algebra.CommAlgebra +open import Cubical.Algebra.CommAlgebra.FPAlgebra +open import Cubical.Algebra.CommAlgebra.FPAlgebra.Instances +open import Cubical.Algebra.CommAlgebra.Instances.Unit +open import Cubical.Algebra.ZariskiLattice.Base +open import Cubical.Algebra.ZariskiLattice.UniversalProperty + +open import Cubical.Categories.Category +open import Cubical.Categories.Functor +-- open import Cubical.Categories.Limits.Terminal +-- open import Cubical.Categories.Limits.Pullback +-- open import Cubical.Categories.Limits.Limits +open import Cubical.Categories.Instances.Sets +open import Cubical.Categories.Instances.CommRings +open import Cubical.Categories.Instances.CommAlgebras +open import Cubical.Categories.Instances.Functors +open import Cubical.Categories.NaturalTransformation +open import Cubical.Categories.Presheaf.Base +open import Cubical.Categories.Yoneda + + +open import Cubical.HITs.PropositionalTruncation as PT +open import Cubical.HITs.SetQuotients as SQ + +open Category hiding (_∘_) renaming (_⋆_ to _⋆c_) +open CommAlgebraHoms +-- open Cospan +-- open Pullback + +private + variable + ℓ ℓ' ℓ'' : Level + + +module _ (R : CommRing ℓ) where + open Category + + -- type living in the same universe as the base ring R + record SmallFPAlgebra : Type ℓ where + field + n : ℕ + m : ℕ + relations : FinVec ⟨ Polynomials {R = R} n ⟩ m + + open SmallFPAlgebra + private + indFPAlg : SmallFPAlgebra → CommAlgebra R ℓ + indFPAlg A = FPAlgebra (A .n) (A .relations) + + FPAlgebrasSmallCategory : Category ℓ ℓ + ob FPAlgebrasSmallCategory = SmallFPAlgebra + Hom[_,_] FPAlgebrasSmallCategory A B = + CommAlgebraHom (indFPAlg A) (indFPAlg B) + id FPAlgebrasSmallCategory = idCommAlgebraHom _ + _⋆_ FPAlgebrasSmallCategory = compCommAlgebraHom _ _ _ + ⋆IdL FPAlgebrasSmallCategory = compIdCommAlgebraHom + ⋆IdR FPAlgebrasSmallCategory = idCompCommAlgebraHom + ⋆Assoc FPAlgebrasSmallCategory = compAssocCommAlgebraHom + isSetHom FPAlgebrasSmallCategory = isSetAlgebraHom _ _ + + + -- yoneda in the notation of Demazure-Gabriel + -- uses η-equality of Categories + Sp : Functor (FPAlgebrasSmallCategory ^op) (FUNCTOR FPAlgebrasSmallCategory (SET ℓ)) + Sp = YO {C = (FPAlgebrasSmallCategory ^op)} + + open Functor + + -- special internal objects to talk about schemes + -- first the affine line + private + R[x]ᶠᵖ : SmallFPAlgebra + n R[x]ᶠᵖ = 1 + m R[x]ᶠᵖ = 0 + relations R[x]ᶠᵖ = λ () + + 𝔸¹ = Sp .F-ob R[x]ᶠᵖ + + -- the Zariski lattice (classifying compact open subobjects) + 𝓛 : Functor FPAlgebrasSmallCategory (SET ℓ) + F-ob 𝓛 A = ZarLat.ZL (CommAlgebra→CommRing (indFPAlg A)) , SQ.squash/ + F-hom 𝓛 φ = inducedZarLatHom (CommAlgebraHom→CommRingHom _ _ φ) .fst + F-id 𝓛 = {!!} + F-seq 𝓛 = {!!} From 8e4580f696835712ea9d44b0183466b393539dff Mon Sep 17 00:00:00 2001 From: mzeuner Date: Wed, 11 Oct 2023 00:05:14 +0200 Subject: [PATCH 04/18] functorial action --- .../ZariskiLattice/UniversalProperty.agda | 43 +++++++++++++++++++ 1 file changed, 43 insertions(+) diff --git a/Cubical/Algebra/ZariskiLattice/UniversalProperty.agda b/Cubical/Algebra/ZariskiLattice/UniversalProperty.agda index 2216c737b3..9b751c8f86 100644 --- a/Cubical/Algebra/ZariskiLattice/UniversalProperty.agda +++ b/Cubical/Algebra/ZariskiLattice/UniversalProperty.agda @@ -315,3 +315,46 @@ module ZarLatUniversalProp (R' : CommRing ℓ) where open Join ZariskiLattice ⋁D≡ : {n : ℕ} (α : FinVec R n) → ⋁ (D ∘ α) ≡ [ n , α ] ⋁D≡ _ = funExt⁻ (cong fst ZLUniversalPropCorollary) _ + +-- the lattice morphism induced by a ring morphism +module _ {A B : CommRing ℓ} (φ : CommRingHom A B) where + + open ZarLat + open ZarLatUniversalProp + open IsZarMap + open CommRingStr ⦃...⦄ + open DistLatticeStr ⦃...⦄ + open IsRingHom + private + instance + _ = A .snd + _ = B .snd + _ = (ZariskiLattice A) .snd + _ = (ZariskiLattice B) .snd + + Dcomp : A .fst → ZL B + Dcomp f = D B (φ .fst f) + + isZarMapDcomp : IsZarMap A (ZariskiLattice B) Dcomp + pres0 isZarMapDcomp = cong (D B) (φ .snd .pres0) ∙ isZarMapD B .pres0 + pres1 isZarMapDcomp = cong (D B) (φ .snd .pres1) ∙ isZarMapD B .pres1 + ·≡∧ isZarMapDcomp f g = cong (D B) (φ .snd .pres· f g) + ∙ isZarMapD B .·≡∧ (φ .fst f) (φ .fst g) + +≤∨ isZarMapDcomp f g = + let open JoinSemilattice + (Lattice→JoinSemilattice (DistLattice→Lattice (ZariskiLattice B))) + in subst (λ x → x ≤ (Dcomp f) ∨l (Dcomp g)) + (sym (cong (D B) (φ .snd .pres+ f g))) + (isZarMapD B .+≤∨ (φ .fst f) (φ .fst g)) + + inducedZarLatHom : DistLatticeHom (ZariskiLattice A) (ZariskiLattice B) + inducedZarLatHom = ZLHasUniversalProp A (ZariskiLattice B) Dcomp isZarMapDcomp .fst .fst + +-- functoriality +module _ (A : CommRing ℓ) where + open ZarLat + open ZarLatUniversalProp + + inducedZarLatHomId : inducedZarLatHom (idCommRingHom A) + ≡ idDistLatticeHom (ZariskiLattice A) + inducedZarLatHomId = {!!} From aa0a839f9bc4e458ef789a98e838f5de5fcd3f85 Mon Sep 17 00:00:00 2001 From: mzeuner Date: Wed, 11 Oct 2023 19:28:26 +0200 Subject: [PATCH 05/18] identity action --- .../Algebra/ZariskiLattice/UniversalProperty.agda | 14 +++++++++++++- 1 file changed, 13 insertions(+), 1 deletion(-) diff --git a/Cubical/Algebra/ZariskiLattice/UniversalProperty.agda b/Cubical/Algebra/ZariskiLattice/UniversalProperty.agda index 9b751c8f86..c0d78ee0b5 100644 --- a/Cubical/Algebra/ZariskiLattice/UniversalProperty.agda +++ b/Cubical/Algebra/ZariskiLattice/UniversalProperty.agda @@ -357,4 +357,16 @@ module _ (A : CommRing ℓ) where inducedZarLatHomId : inducedZarLatHom (idCommRingHom A) ≡ idDistLatticeHom (ZariskiLattice A) - inducedZarLatHomId = {!!} + inducedZarLatHomId = + cong fst + (ZLHasUniversalProp A (ZariskiLattice A) (Dcomp (idCommRingHom A)) + (isZarMapDcomp (idCommRingHom A)) .snd + (idDistLatticeHom (ZariskiLattice A) , refl)) + +module _ {A B C : CommRing ℓ} (φ : CommRingHom A B) (ψ : CommRingHom B C) where + open ZarLat + open ZarLatUniversalProp + + inducedZarLatHomSeq : inducedZarLatHom (ψ ∘cr φ) ≡ {!!} + -- ≡ inducedZarLatHom ψ ∘dl inducedZarLatHom φ + inducedZarLatHomSeq = {!!} From 862af1802b6d5bc4385f618e506186b305195999 Mon Sep 17 00:00:00 2001 From: mzeuner Date: Thu, 12 Oct 2023 16:18:27 +0200 Subject: [PATCH 06/18] Zar latt presheaf --- Cubical/Algebra/DistLattice.agda | 1 + Cubical/Algebra/DistLattice/Properties.agda | 55 ++++++++ Cubical/Algebra/Lattice/Properties.agda | 40 +++++- .../ZariskiLattice/UniversalProperty.agda | 14 +- .../Categories/Instances/FPAlgebrasSmall.agda | 2 +- Cubical/Categories/Instances/ZFunctors.agda | 122 ++++++++++++++++++ 6 files changed, 228 insertions(+), 6 deletions(-) create mode 100644 Cubical/Algebra/DistLattice/Properties.agda create mode 100644 Cubical/Categories/Instances/ZFunctors.agda diff --git a/Cubical/Algebra/DistLattice.agda b/Cubical/Algebra/DistLattice.agda index a0d6e821a5..d5e617f09a 100644 --- a/Cubical/Algebra/DistLattice.agda +++ b/Cubical/Algebra/DistLattice.agda @@ -2,3 +2,4 @@ module Cubical.Algebra.DistLattice where open import Cubical.Algebra.DistLattice.Base public +open import Cubical.Algebra.DistLattice.Properties public diff --git a/Cubical/Algebra/DistLattice/Properties.agda b/Cubical/Algebra/DistLattice/Properties.agda new file mode 100644 index 0000000000..eb5aa171b8 --- /dev/null +++ b/Cubical/Algebra/DistLattice/Properties.agda @@ -0,0 +1,55 @@ +{-# OPTIONS --safe --lossy-unification #-} +module Cubical.Algebra.DistLattice.Properties where + +open import Cubical.Foundations.Prelude +open import Cubical.Foundations.Function +open import Cubical.Foundations.Equiv +open import Cubical.Foundations.Equiv.HalfAdjoint +open import Cubical.Foundations.HLevels +open import Cubical.Foundations.Isomorphism +open import Cubical.Foundations.Univalence +open import Cubical.Foundations.Transport +open import Cubical.Foundations.SIP + +open import Cubical.Data.Sigma + +open import Cubical.Structures.Axioms +open import Cubical.Structures.Auto +open import Cubical.Structures.Macro +open import Cubical.Algebra.Semigroup +open import Cubical.Algebra.Monoid +open import Cubical.Algebra.CommMonoid +open import Cubical.Algebra.Semilattice +open import Cubical.Algebra.Lattice +open import Cubical.Algebra.DistLattice.Base + +open import Cubical.Relation.Binary.Order.Poset + +private + variable + ℓ ℓ' ℓ'' : Level + +module _ where + open LatticeHoms + + compDistLatticeHom : (L : DistLattice ℓ) (M : DistLattice ℓ') (N : DistLattice ℓ'') + → DistLatticeHom L M → DistLatticeHom M N → DistLatticeHom L N + compDistLatticeHom L M N = compLatticeHom {L = DistLattice→Lattice L} {DistLattice→Lattice M} {DistLattice→Lattice N} + + _∘dl_ : {L : DistLattice ℓ} {M : DistLattice ℓ'} {N : DistLattice ℓ''} + → DistLatticeHom M N → DistLatticeHom L M → DistLatticeHom L N + g ∘dl f = compDistLatticeHom _ _ _ f g + + compIdDistLatticeHom : {L M : DistLattice ℓ} (f : DistLatticeHom L M) + → compDistLatticeHom _ _ _ (idDistLatticeHom L) f ≡ f + compIdDistLatticeHom = compIdLatticeHom + + idCompDistLatticeHom : {L M : DistLattice ℓ} (f : DistLatticeHom L M) + → compDistLatticeHom _ _ _ f (idDistLatticeHom M) ≡ f + idCompDistLatticeHom = idCompLatticeHom + + compAssocDistLatticeHom : {L M N U : DistLattice ℓ} + (f : DistLatticeHom L M) (g : DistLatticeHom M N) (h : DistLatticeHom N U) + → compDistLatticeHom _ _ _ (compDistLatticeHom _ _ _ f g) h + ≡ compDistLatticeHom _ _ _ f (compDistLatticeHom _ _ _ g h) + compAssocDistLatticeHom = compAssocLatticeHom diff --git a/Cubical/Algebra/Lattice/Properties.agda b/Cubical/Algebra/Lattice/Properties.agda index bd5f3ae8bf..c1622d2fc7 100644 --- a/Cubical/Algebra/Lattice/Properties.agda +++ b/Cubical/Algebra/Lattice/Properties.agda @@ -2,6 +2,7 @@ module Cubical.Algebra.Lattice.Properties where open import Cubical.Foundations.Prelude +open import Cubical.Foundations.Function open import Cubical.Foundations.Equiv open import Cubical.Foundations.Equiv.HalfAdjoint open import Cubical.Foundations.HLevels @@ -25,7 +26,7 @@ open import Cubical.Relation.Binary.Order.Poset private variable - ℓ : Level + ℓ ℓ' ℓ'' ℓ''' : Level module LatticeTheory (L' : Lattice ℓ) where private L = fst L' @@ -81,7 +82,7 @@ module Order (L' : Lattice ℓ) where ∧≤LCancelJoin x y = ≤m→≤j _ _ (∧≤LCancel x y) -module _ {L M : Lattice ℓ} (φ ψ : LatticeHom L M) where +module _ {L : Lattice ℓ} {M : Lattice ℓ'} (φ ψ : LatticeHom L M) where open LatticeStr ⦃...⦄ open IsLatticeHom private @@ -93,3 +94,38 @@ module _ {L M : Lattice ℓ} (φ ψ : LatticeHom L M) where LatticeHom≡f : fst φ ≡ fst ψ → φ ≡ ψ LatticeHom≡f = Σ≡Prop λ f → isPropIsLatticeHom _ f _ + + + +module LatticeHoms where + open IsLatticeHom + + compIsLatticeHom : {A : Lattice ℓ} {B : Lattice ℓ'} {C : Lattice ℓ''} + {g : ⟨ B ⟩ → ⟨ C ⟩} {f : ⟨ A ⟩ → ⟨ B ⟩} + → IsLatticeHom (B .snd) g (C .snd) + → IsLatticeHom (A .snd) f (B .snd) + → IsLatticeHom (A .snd) (g ∘ f) (C .snd) + compIsLatticeHom {g = g} {f} gh fh .pres0 = cong g (fh .pres0) ∙ gh .pres0 + compIsLatticeHom {g = g} {f} gh fh .pres1 = cong g (fh .pres1) ∙ gh .pres1 + compIsLatticeHom {g = g} {f} gh fh .pres∨l x y = cong g (fh .pres∨l x y) ∙ gh .pres∨l (f x) (f y) + compIsLatticeHom {g = g} {f} gh fh .pres∧l x y = cong g (fh .pres∧l x y) ∙ gh .pres∧l (f x) (f y) + + + compLatticeHom : {L : Lattice ℓ} {M : Lattice ℓ'} {N : Lattice ℓ''} + → LatticeHom L M → LatticeHom M N → LatticeHom L N + fst (compLatticeHom f g) x = g .fst (f .fst x) + snd (compLatticeHom f g) = compIsLatticeHom (g .snd) (f .snd) + + _∘l_ : {L : Lattice ℓ} {M : Lattice ℓ'} {N : Lattice ℓ''} → LatticeHom M N → LatticeHom L M → LatticeHom L N + _∘l_ = flip compLatticeHom + + compIdLatticeHom : {L : Lattice ℓ} {M : Lattice ℓ'} (φ : LatticeHom L M) → compLatticeHom (idLatticeHom L) φ ≡ φ + compIdLatticeHom φ = LatticeHom≡f _ _ refl + + idCompLatticeHom : {L : Lattice ℓ} {M : Lattice ℓ'} (φ : LatticeHom L M) → compLatticeHom φ (idLatticeHom M) ≡ φ + idCompLatticeHom φ = LatticeHom≡f _ _ refl + + compAssocLatticeHom : {L : Lattice ℓ} {M : Lattice ℓ'} {N : Lattice ℓ''} {U : Lattice ℓ'''} + → (φ : LatticeHom L M) (ψ : LatticeHom M N) (χ : LatticeHom N U) + → compLatticeHom (compLatticeHom φ ψ) χ ≡ compLatticeHom φ (compLatticeHom ψ χ) + compAssocLatticeHom _ _ _ = LatticeHom≡f _ _ refl diff --git a/Cubical/Algebra/ZariskiLattice/UniversalProperty.agda b/Cubical/Algebra/ZariskiLattice/UniversalProperty.agda index c0d78ee0b5..0a5dd28e7d 100644 --- a/Cubical/Algebra/ZariskiLattice/UniversalProperty.agda +++ b/Cubical/Algebra/ZariskiLattice/UniversalProperty.agda @@ -367,6 +367,14 @@ module _ {A B C : CommRing ℓ} (φ : CommRingHom A B) (ψ : CommRingHom B C) wh open ZarLat open ZarLatUniversalProp - inducedZarLatHomSeq : inducedZarLatHom (ψ ∘cr φ) ≡ {!!} - -- ≡ inducedZarLatHom ψ ∘dl inducedZarLatHom φ - inducedZarLatHomSeq = {!!} + inducedZarLatHomSeq : inducedZarLatHom (ψ ∘cr φ) + ≡ inducedZarLatHom ψ ∘dl inducedZarLatHom φ + inducedZarLatHomSeq = + cong fst + (ZLHasUniversalProp A (ZariskiLattice C) (Dcomp (ψ ∘cr φ)) + (isZarMapDcomp (ψ ∘cr φ)) .snd + (inducedZarLatHom ψ ∘dl inducedZarLatHom φ , funExt path)) + where + path : ∀ f → fst (inducedZarLatHom ψ ∘dl inducedZarLatHom φ) (D A f) + ≡ Dcomp (ψ ∘cr φ) f + path f i = [ 1 , (++FinRid {n = 1} (λ _ → (ψ ∘cr φ) .fst f) λ ()) i ] diff --git a/Cubical/Categories/Instances/FPAlgebrasSmall.agda b/Cubical/Categories/Instances/FPAlgebrasSmall.agda index bd37b01ab4..06d430dd0b 100644 --- a/Cubical/Categories/Instances/FPAlgebrasSmall.agda +++ b/Cubical/Categories/Instances/FPAlgebrasSmall.agda @@ -99,5 +99,5 @@ module _ (R : CommRing ℓ) where 𝓛 : Functor FPAlgebrasSmallCategory (SET ℓ) F-ob 𝓛 A = ZarLat.ZL (CommAlgebra→CommRing (indFPAlg A)) , SQ.squash/ F-hom 𝓛 φ = inducedZarLatHom (CommAlgebraHom→CommRingHom _ _ φ) .fst - F-id 𝓛 = {!!} + F-id 𝓛 {A} = {!cong fst (inducedZarLatHomId (CommAlgebra→CommRing (indFPAlg A)))!} F-seq 𝓛 = {!!} diff --git a/Cubical/Categories/Instances/ZFunctors.agda b/Cubical/Categories/Instances/ZFunctors.agda new file mode 100644 index 0000000000..743d7fbd62 --- /dev/null +++ b/Cubical/Categories/Instances/ZFunctors.agda @@ -0,0 +1,122 @@ +{- + + The impredicative way to do the functor of points of qcqs-schemes + (over Spec(ℤ)) + +-} +{-# OPTIONS --safe --lossy-unification #-} +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.Foundations.Structure + +open import Cubical.Data.Unit +open import Cubical.Data.Sigma +open import Cubical.Data.Nat +open import Cubical.Data.FinData +open import Cubical.Data.Int as Int + renaming ( ℤ to ℤ ; _+_ to _+ℤ_; _·_ to _·ℤ_; -_ to -ℤ_) + + +open import Cubical.Algebra.Ring +open import Cubical.Algebra.CommRing +open import Cubical.Algebra.CommRing.Instances.Int +open import Cubical.Algebra.CommRing.Instances.Unit +open import Cubical.Algebra.Algebra +open import Cubical.Algebra.CommAlgebra +open import Cubical.Algebra.CommAlgebra.FreeCommAlgebra +open import Cubical.Algebra.CommAlgebra.Instances.Unit +open import Cubical.Algebra.ZariskiLattice.Base +open import Cubical.Algebra.ZariskiLattice.UniversalProperty + +open import Cubical.Categories.Category +open import Cubical.Categories.Functor +open import Cubical.Categories.Instances.Sets +open import Cubical.Categories.Instances.CommRings +open import Cubical.Categories.Instances.CommAlgebras +open import Cubical.Categories.Instances.Functors +open import Cubical.Categories.NaturalTransformation +open import Cubical.Categories.Presheaf.Base +open import Cubical.Categories.Yoneda + + +open import Cubical.HITs.PropositionalTruncation as PT +open import Cubical.HITs.SetQuotients as SQ hiding ([_]) + +open Category hiding (_∘_) renaming (_⋆_ to _⋆c_) +open CommAlgebraHoms +-- open Cospan +-- open Pullback + +private + variable + ℓ' ℓ'' : Level + +-- TODO generalize level +--module _ {ℓ : Level} where + +-- using the naming conventions of Nieper-Wisskirchen +ℤFunctor = Functor (CommRingsCategory {ℓ = ℓ-zero}) (SET ℓ-zero) +ℤFUNCTOR = FUNCTOR (CommRingsCategory {ℓ = ℓ-zero}) (SET ℓ-zero) + +-- Yoneda in the notation of Demazure-Gabriel +-- uses that double op is original category definitionally +Sp : Functor (CommRingsCategory {ℓ = ℓ-zero} ^op) ℤFUNCTOR +Sp = YO {C = (CommRingsCategory {ℓ = ℓ-zero} ^op)} + +-- special functors to talk about schemes +open Functor +open ZarLat + +-- 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 φ ψ) + +-- the forgetful functor +-- aka the representable of ℤ[x] +-- aka the affine line +open Construction ℤCommRing +private + ℤ[x] : CommRing ℓ-zero + ℤ[x] = CommAlgebra→CommRing (ℤCommRing [ Unit ]) + +𝔸¹ : ℤFunctor +𝔸¹ = Sp .F-ob ℤ[x] + + +-- the big lattice of compact opens +CompactOpen : ℤFunctor → Type₁ +CompactOpen X = X ⇒ 𝓛 + +open NatTrans +open ZarLatUniversalProp +open CommRingStr ⦃...⦄ +-- the induced subfunctor +coSubfun : {X : ℤFunctor} (U : CompactOpen X) + → ℤFunctor +F-ob (coSubfun {X = X} U) A = let instance _ = snd A in + (Σ[ x ∈ X .F-ob A .fst ] U .N-ob A x ≡ D A 1r) + , isSetΣSndProp (X .F-ob A .snd) λ _ → squash/ _ _ +F-hom (coSubfun {X = X} U) = {!!} +F-id (coSubfun {X = X} U) = {!!} +F-seq (coSubfun {X = X} U) = {!!} + +-- the global sections functor +Γ : Functor ℤFUNCTOR (CommRingsCategory {ℓ-suc ℓ-zero}) +fst (F-ob Γ X) = X ⇒ 𝔸¹ +snd (F-ob Γ X) = {!!} +F-hom Γ = {!!} +F-id Γ = {!!} +F-seq Γ = {!!} + + +-- we get an adjunction modulo size issues +-- ΓSpOb : (A : CommRing ℓ) From d8ae9cd73da9850e1356811c7306be5c3190051a Mon Sep 17 00:00:00 2001 From: mzeuner Date: Fri, 13 Oct 2023 16:47:33 +0200 Subject: [PATCH 07/18] ring structure on global section --- Cubical/Categories/Instances/ZFunctors.agda | 194 +++++++++++++------- 1 file changed, 130 insertions(+), 64 deletions(-) diff --git a/Cubical/Categories/Instances/ZFunctors.agda b/Cubical/Categories/Instances/ZFunctors.agda index 743d7fbd62..0c5f7e2aee 100644 --- a/Cubical/Categories/Instances/ZFunctors.agda +++ b/Cubical/Categories/Instances/ZFunctors.agda @@ -17,7 +17,11 @@ open import Cubical.Foundations.Structure open import Cubical.Data.Unit open import Cubical.Data.Sigma -open import Cubical.Data.Nat +open import Cubical.Data.Nat renaming ( _+_ to _+ℕ_ ; _·_ to _·ℕ_ ; _^_ to _^ℕ_ + ; +-comm to +ℕ-comm ; +-assoc to +ℕ-assoc + ; ·-assoc to ·ℕ-assoc ; ·-comm to ·ℕ-comm + ; ·-identityʳ to ·ℕ-rid) + open import Cubical.Data.FinData open import Cubical.Data.Int as Int renaming ( ℤ to ℤ ; _+_ to _+ℤ_; _·_ to _·ℤ_; -_ to -ℤ_) @@ -31,6 +35,7 @@ open import Cubical.Algebra.Algebra open import Cubical.Algebra.CommAlgebra open import Cubical.Algebra.CommAlgebra.FreeCommAlgebra open import Cubical.Algebra.CommAlgebra.Instances.Unit +open import Cubical.Algebra.Lattice open import Cubical.Algebra.ZariskiLattice.Base open import Cubical.Algebra.ZariskiLattice.UniversalProperty @@ -57,66 +62,127 @@ private variable ℓ' ℓ'' : Level --- TODO generalize level ---module _ {ℓ : Level} where - --- using the naming conventions of Nieper-Wisskirchen -ℤFunctor = Functor (CommRingsCategory {ℓ = ℓ-zero}) (SET ℓ-zero) -ℤFUNCTOR = FUNCTOR (CommRingsCategory {ℓ = ℓ-zero}) (SET ℓ-zero) - --- Yoneda in the notation of Demazure-Gabriel --- uses that double op is original category definitionally -Sp : Functor (CommRingsCategory {ℓ = ℓ-zero} ^op) ℤFUNCTOR -Sp = YO {C = (CommRingsCategory {ℓ = ℓ-zero} ^op)} - --- special functors to talk about schemes -open Functor -open ZarLat - --- 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 φ ψ) - --- the forgetful functor --- aka the representable of ℤ[x] --- aka the affine line -open Construction ℤCommRing -private - ℤ[x] : CommRing ℓ-zero - ℤ[x] = CommAlgebra→CommRing (ℤCommRing [ Unit ]) - -𝔸¹ : ℤFunctor -𝔸¹ = Sp .F-ob ℤ[x] - - --- the big lattice of compact opens -CompactOpen : ℤFunctor → Type₁ -CompactOpen X = X ⇒ 𝓛 - -open NatTrans -open ZarLatUniversalProp -open CommRingStr ⦃...⦄ --- the induced subfunctor -coSubfun : {X : ℤFunctor} (U : CompactOpen X) - → ℤFunctor -F-ob (coSubfun {X = X} U) A = let instance _ = snd A in - (Σ[ x ∈ X .F-ob A .fst ] U .N-ob A x ≡ D A 1r) - , isSetΣSndProp (X .F-ob A .snd) λ _ → squash/ _ _ -F-hom (coSubfun {X = X} U) = {!!} -F-id (coSubfun {X = X} U) = {!!} -F-seq (coSubfun {X = X} U) = {!!} - --- the global sections functor -Γ : Functor ℤFUNCTOR (CommRingsCategory {ℓ-suc ℓ-zero}) -fst (F-ob Γ X) = X ⇒ 𝔸¹ -snd (F-ob Γ X) = {!!} -F-hom Γ = {!!} -F-id Γ = {!!} -F-seq Γ = {!!} - - --- we get an adjunction modulo size issues --- ΓSpOb : (A : CommRing ℓ) + +module _ {ℓ : Level} where + open Functor + open NatTrans + open ZarLat + open ZarLatUniversalProp + open CommRingStr ⦃...⦄ + open IsRingHom + + -- using the naming conventions of Nieper-Wisskirchen + ℤ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)} + + -- special functors to talk about schemes + -- 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 φ ψ) + + -- the forgetful functor + -- aka the affine line + -- (aka the representable of ℤ[x]) + -- open Construction ℤCommRing + -- private + -- ℤ[x] : CommRing ℓ-zero + -- ℤ[x] = CommAlgebra→CommRing (ℤCommRing [ Unit ]) + + 𝔸¹ : ℤFunctor + 𝔸¹ = ForgetfulCommRing→Set --Sp .F-ob ℤ[x] + + + -- the big lattice of compact opens + CompactOpen : ℤFunctor → Type (ℓ-suc ℓ) + CompactOpen X = X ⇒ 𝓛 + + -- 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 ⟩ + 𝓛 .F-hom φ (U .N-ob A x) ≡⟨ cong (𝓛 .F-hom φ) Ux≡D1 ⟩ + 𝓛 .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))) + + + -- the global sections functor + Γ : Functor ℤFUNCTOR (CommRingsCategory {ℓ-suc ℓ}) + 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)) = {!!} + -- functoriality of Γ + F-hom Γ = {!!} + F-id Γ = {!!} + F-seq Γ = {!!} + + + -- we get an adjunction modulo size issues + -- ΓSpOb : (A : CommRing ℓ) From e89de4a3dc80841f64638ce9b519d67f0b7e7c09 Mon Sep 17 00:00:00 2001 From: mzeuner Date: Wed, 18 Oct 2023 18:49:47 +0200 Subject: [PATCH 08/18] unit and conunit of adjunction --- Cubical/Categories/Instances/ZFunctors.agda | 98 +++++++++++++++++++-- 1 file changed, 90 insertions(+), 8 deletions(-) diff --git a/Cubical/Categories/Instances/ZFunctors.agda b/Cubical/Categories/Instances/ZFunctors.agda index 0c5f7e2aee..f5b40e8dd1 100644 --- a/Cubical/Categories/Instances/ZFunctors.agda +++ b/Cubical/Categories/Instances/ZFunctors.agda @@ -15,6 +15,8 @@ open import Cubical.Foundations.Powerset open import Cubical.Foundations.HLevels open import Cubical.Foundations.Structure +open import Cubical.Functions.FunExtEquiv + open import Cubical.Data.Unit open import Cubical.Data.Sigma open import Cubical.Data.Nat renaming ( _+_ to _+ℕ_ ; _·_ to _·ℕ_ ; _^_ to _^ℕ_ @@ -60,7 +62,7 @@ open CommAlgebraHoms private variable - ℓ' ℓ'' : Level + ℓ ℓ' ℓ'' : Level module _ {ℓ : Level} where @@ -128,7 +130,7 @@ module _ {ℓ : Level} where -- the global sections functor - Γ : Functor ℤFUNCTOR (CommRingsCategory {ℓ-suc ℓ}) + Γ : 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 @@ -177,12 +179,92 @@ module _ {ℓ : Level} where - φ .fst (α .N-ob A x) ≡⟨ sym (φ .snd .pres- _) ⟩ φ .fst (- α .N-ob A x) ∎ - CommRingStr.isCommRing (snd (F-ob Γ 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-hom Γ = {!!} - F-id Γ = {!!} - F-seq Γ = {!!} + F-id Γ = RingHom≡ (funExt λ _ → makeNatTransPath (funExt₂ λ _ _ → refl)) + F-seq Γ _ _ = RingHom≡ (funExt λ _ → makeNatTransPath (funExt₂ λ _ _ → refl)) - -- we get an adjunction modulo size issues - -- ΓSpOb : (A : CommRing ℓ) +-- we get an adjunction Γ ⊣ Sp modulo size issues +-- note that we can't write unit and counit as +-- elements of type NatTrans because the type CommRingHom +-- ends up living in the next higher universe +open Functor +open NatTrans +open Iso +open IsRingHom + +private + -- hack, because Functor record doesn't have η-equality + ntSwap : {A : CommRing ℓ} → CommRingsCategory ^op [-, A ] ⇒ 𝔸¹ + → CommRingsCategory [ A ,-] ⇒ 𝔸¹ + N-ob (ntSwap α) B = α .N-ob B + N-hom (ntSwap α) φ = α .N-hom φ + +-- The counit is an equivalence +ΓSpOb : (A : CommRing ℓ) → CommRingHom ((Γ ∘F Sp) .F-ob A) A +fst (ΓSpOb A) α = yoneda 𝔸¹ A .fun (ntSwap α) +pres0 (snd (ΓSpOb A)) = refl +pres1 (snd (ΓSpOb A)) = refl +pres+ (snd (ΓSpOb A)) _ _ = refl +pres· (snd (ΓSpOb A)) _ _ = refl +pres- (snd (ΓSpOb A)) _ = refl + +ΓSpHom : {A B : CommRing ℓ} (φ : CommRingHom A B) + → φ ∘cr ΓSpOb A ≡ ΓSpOb B ∘cr ((Γ ∘F Sp) .F-hom φ) +ΓSpHom φ = {!!} + +-- The unit is an equivalence iff the ℤ-functor is affine +-- unfortunately, we can't give a natural transformation +-- X ⇒ Hom (Γ X , ·), because the latter ℤ-functor lives +-- in a higher universe. +-- we can however give terms that look just like +-- a natural transformation: +SpΓObOb : (X : ℤFunctor) (A : CommRing ℓ) + → X .F-ob A .fst → CommRingHom (Γ .F-ob X) A +fst (SpΓObOb X A x) α = yoneda 𝔸¹ A .fun ((yoneda X A .inv x) ●ᵛ α) +pres0 (snd (SpΓObOb X A x)) = refl +pres1 (snd (SpΓObOb X A x)) = refl +pres+ (snd (SpΓObOb X A x)) _ _ = refl +pres· (snd (SpΓObOb X A x)) _ _ = refl +pres- (snd (SpΓObOb X A x)) _ = refl + +-- the reason to prefer isAffine over isAffine' is that +-- it becomes small when replacing comm rings with fp-algebras +isAffine : (X : ℤFunctor {ℓ = ℓ}) → Type (ℓ-suc ℓ) +isAffine X = ∀ (A : CommRing _) → isEquiv (SpΓObOb X A) +-- TODO equivalence with naive def: +isAffine' : (ℓ : Level) (X : ℤFunctor {ℓ = ℓ}) → Type (ℓ-suc ℓ) +isAffine' ℓ X = ∃[ A ∈ CommRing ℓ ] CommRingEquiv A (Γ .F-ob X) + +-- the rest of the "quasi natural transoformation" +SpΓObHom : (X : ℤFunctor) {A B : CommRing ℓ} (φ : CommRingHom A B) + → SpΓObOb X B ∘ (X .F-hom φ) ≡ (φ ∘cr_) ∘ SpΓObOb X A +SpΓObHom X {A = A} {B = B} φ = funExt funExtHelper + where + funExtHelper : ∀ (x : X .F-ob A .fst) + → SpΓObOb X B (X .F-hom φ x) ≡ φ ∘cr (SpΓObOb X A x) + funExtHelper x = RingHom≡ (funExt funExtHelper2) + where + funExtHelper2 : ∀ (α : X ⇒ 𝔸¹) + → yoneda 𝔸¹ B .fun ((yoneda X B .inv (X .F-hom φ x)) ●ᵛ α) + ≡ φ .fst (yoneda 𝔸¹ A .fun ((yoneda X A .inv x) ●ᵛ α)) + funExtHelper2 α = {!!} From fd206556098dd298a0729a3408e1919804d8f1cf Mon Sep 17 00:00:00 2001 From: mzeuner Date: Fri, 20 Oct 2023 18:29:09 +0200 Subject: [PATCH 09/18] new approach --- Cubical/Categories/Instances/ZFunctors.agda | 127 ++++++++++++++++---- 1 file changed, 102 insertions(+), 25 deletions(-) diff --git a/Cubical/Categories/Instances/ZFunctors.agda b/Cubical/Categories/Instances/ZFunctors.agda index f5b40e8dd1..b2f316fbae 100644 --- a/Cubical/Categories/Instances/ZFunctors.agda +++ b/Cubical/Categories/Instances/ZFunctors.agda @@ -212,16 +212,9 @@ open NatTrans open Iso open IsRingHom -private - -- hack, because Functor record doesn't have η-equality - ntSwap : {A : CommRing ℓ} → CommRingsCategory ^op [-, A ] ⇒ 𝔸¹ - → CommRingsCategory [ A ,-] ⇒ 𝔸¹ - N-ob (ntSwap α) B = α .N-ob B - N-hom (ntSwap α) φ = α .N-hom φ --- The counit is an equivalence ΓSpOb : (A : CommRing ℓ) → CommRingHom ((Γ ∘F Sp) .F-ob A) A -fst (ΓSpOb A) α = yoneda 𝔸¹ A .fun (ntSwap α) +fst (ΓSpOb A) α = yonedaᴾ 𝔸¹ A .fun α pres0 (snd (ΓSpOb A)) = refl pres1 (snd (ΓSpOb A)) = refl pres+ (snd (ΓSpOb A)) _ _ = refl @@ -230,30 +223,28 @@ pres- (snd (ΓSpOb A)) _ = refl ΓSpHom : {A B : CommRing ℓ} (φ : CommRingHom A B) → φ ∘cr ΓSpOb A ≡ ΓSpOb B ∘cr ((Γ ∘F Sp) .F-hom φ) -ΓSpHom φ = {!!} +ΓSpHom {A = A} {B = B} φ = RingHom≡ (funExt funExtHelper) + where + funExtHelper : ∀ (α : Sp .F-ob A ⇒ 𝔸¹) + → φ .fst (yonedaᴾ 𝔸¹ A .fun α) ≡ yonedaᴾ 𝔸¹ B .fun (Sp .F-hom φ ●ᵛ α) + funExtHelper α = funExt⁻ (sym (yonedaIsNaturalInOb {F = 𝔸¹} A B φ)) + (record { N-ob = α .N-ob ; N-hom = α .N-hom }) + -- hack because Functor doesn't have η-equality + --- The unit is an equivalence iff the ℤ-functor is affine --- unfortunately, we can't give a natural transformation --- X ⇒ Hom (Γ X , ·), because the latter ℤ-functor lives --- in a higher universe. --- we can however give terms that look just like --- a natural transformation: SpΓObOb : (X : ℤFunctor) (A : CommRing ℓ) → X .F-ob A .fst → CommRingHom (Γ .F-ob X) A -fst (SpΓObOb X A x) α = yoneda 𝔸¹ A .fun ((yoneda X A .inv x) ●ᵛ α) +fst (SpΓObOb X A x) α = α .N-ob A x pres0 (snd (SpΓObOb X A x)) = refl pres1 (snd (SpΓObOb X A x)) = refl pres+ (snd (SpΓObOb X A x)) _ _ = refl pres· (snd (SpΓObOb X A x)) _ _ = refl pres- (snd (SpΓObOb X A x)) _ = refl --- the reason to prefer isAffine over isAffine' is that --- it becomes small when replacing comm rings with fp-algebras -isAffine : (X : ℤFunctor {ℓ = ℓ}) → Type (ℓ-suc ℓ) -isAffine X = ∀ (A : CommRing _) → isEquiv (SpΓObOb X A) + +-- isAffine : (X : ℤFunctor {ℓ = ℓ}) → Type (ℓ-suc ℓ) +-- isAffine X = ∀ (A : CommRing _) → isEquiv (SpΓObOb X A) -- TODO equivalence with naive def: -isAffine' : (ℓ : Level) (X : ℤFunctor {ℓ = ℓ}) → Type (ℓ-suc ℓ) -isAffine' ℓ X = ∃[ A ∈ CommRing ℓ ] CommRingEquiv A (Γ .F-ob X) -- the rest of the "quasi natural transoformation" SpΓObHom : (X : ℤFunctor) {A B : CommRing ℓ} (φ : CommRingHom A B) @@ -265,6 +256,92 @@ SpΓObHom X {A = A} {B = B} φ = funExt funExtHelper funExtHelper x = RingHom≡ (funExt funExtHelper2) where funExtHelper2 : ∀ (α : X ⇒ 𝔸¹) - → yoneda 𝔸¹ B .fun ((yoneda X B .inv (X .F-hom φ x)) ●ᵛ α) - ≡ φ .fst (yoneda 𝔸¹ A .fun ((yoneda X A .inv x) ●ᵛ α)) - funExtHelper2 α = {!!} + → α .N-ob B (X .F-hom φ x) ≡ φ .fst (α .N-ob A x) + funExtHelper2 α = funExt⁻ (α .N-hom φ) x + + +-- can only state equality on object part, but that would be enough +SpΓHom : {X Y : ℤFunctor} (α : X ⇒ Y) (A : CommRing ℓ) (x : X .F-ob A .fst) + → SpΓObOb Y A (α .N-ob A x) ≡ SpΓObOb X A x ∘cr Γ .F-hom α +SpΓHom _ _ _ = RingHom≡ refl + +-- TODO: can you state the triangle identities in a reasonable form? + +module AdjBij where + + 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)) + + Γ⊣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 + + +module _ {ℓ : Level} where + isAffine : (X : ℤFunctor {ℓ = ℓ}) → Type (ℓ-suc ℓ) + isAffine X = ∃[ A ∈ CommRing ℓ ] CommRingEquiv A (Γ .F-ob X) + +-- 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 +module AffineDefs {ℓ : Level} where From 66b0967cc92e46d2c8b88400b6d19e221d663086 Mon Sep 17 00:00:00 2001 From: mzeuner Date: Fri, 20 Oct 2023 18:47:55 +0200 Subject: [PATCH 10/18] reorganize and tidy up --- Cubical/Categories/Instances/ZFunctors.agda | 102 +++++++------------- 1 file changed, 36 insertions(+), 66 deletions(-) diff --git a/Cubical/Categories/Instances/ZFunctors.agda b/Cubical/Categories/Instances/ZFunctors.agda index b2f316fbae..1809403b51 100644 --- a/Cubical/Categories/Instances/ZFunctors.agda +++ b/Cubical/Categories/Instances/ZFunctors.agda @@ -93,11 +93,6 @@ module _ {ℓ : Level} where -- the forgetful functor -- aka the affine line -- (aka the representable of ℤ[x]) - -- open Construction ℤCommRing - -- private - -- ℤ[x] : CommRing ℓ-zero - -- ℤ[x] = CommAlgebra→CommRing (ℤCommRing [ Unit ]) - 𝔸¹ : ℤFunctor 𝔸¹ = ForgetfulCommRing→Set --Sp .F-ob ℤ[x] @@ -107,8 +102,7 @@ module _ {ℓ : Level} where CompactOpen X = X ⇒ 𝓛 -- the induced subfunctor - ⟦_⟧ᶜᵒ : {X : ℤFunctor} (U : CompactOpen X) - → ℤFunctor + ⟦_⟧ᶜᵒ : {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 @@ -132,6 +126,7 @@ module _ {ℓ : Level} where -- 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 @@ -204,69 +199,11 @@ module _ {ℓ : Level} where -- we get an adjunction Γ ⊣ Sp modulo size issues --- note that we can't write unit and counit as --- elements of type NatTrans because the type CommRingHom --- ends up living in the next higher universe open Functor open NatTrans open Iso open IsRingHom - -ΓSpOb : (A : CommRing ℓ) → CommRingHom ((Γ ∘F Sp) .F-ob A) A -fst (ΓSpOb A) α = yonedaᴾ 𝔸¹ A .fun α -pres0 (snd (ΓSpOb A)) = refl -pres1 (snd (ΓSpOb A)) = refl -pres+ (snd (ΓSpOb A)) _ _ = refl -pres· (snd (ΓSpOb A)) _ _ = refl -pres- (snd (ΓSpOb A)) _ = refl - -ΓSpHom : {A B : CommRing ℓ} (φ : CommRingHom A B) - → φ ∘cr ΓSpOb A ≡ ΓSpOb B ∘cr ((Γ ∘F Sp) .F-hom φ) -ΓSpHom {A = A} {B = B} φ = RingHom≡ (funExt funExtHelper) - where - funExtHelper : ∀ (α : Sp .F-ob A ⇒ 𝔸¹) - → φ .fst (yonedaᴾ 𝔸¹ A .fun α) ≡ yonedaᴾ 𝔸¹ B .fun (Sp .F-hom φ ●ᵛ α) - funExtHelper α = funExt⁻ (sym (yonedaIsNaturalInOb {F = 𝔸¹} A B φ)) - (record { N-ob = α .N-ob ; N-hom = α .N-hom }) - -- hack because Functor doesn't have η-equality - - -SpΓObOb : (X : ℤFunctor) (A : CommRing ℓ) - → X .F-ob A .fst → CommRingHom (Γ .F-ob X) A -fst (SpΓObOb X A x) α = α .N-ob A x -pres0 (snd (SpΓObOb X A x)) = refl -pres1 (snd (SpΓObOb X A x)) = refl -pres+ (snd (SpΓObOb X A x)) _ _ = refl -pres· (snd (SpΓObOb X A x)) _ _ = refl -pres- (snd (SpΓObOb X A x)) _ = refl - - --- isAffine : (X : ℤFunctor {ℓ = ℓ}) → Type (ℓ-suc ℓ) --- isAffine X = ∀ (A : CommRing _) → isEquiv (SpΓObOb X A) --- TODO equivalence with naive def: - --- the rest of the "quasi natural transoformation" -SpΓObHom : (X : ℤFunctor) {A B : CommRing ℓ} (φ : CommRingHom A B) - → SpΓObOb X B ∘ (X .F-hom φ) ≡ (φ ∘cr_) ∘ SpΓObOb X A -SpΓObHom X {A = A} {B = B} φ = funExt funExtHelper - where - funExtHelper : ∀ (x : X .F-ob A .fst) - → SpΓObOb X B (X .F-hom φ x) ≡ φ ∘cr (SpΓObOb X A x) - funExtHelper x = RingHom≡ (funExt funExtHelper2) - where - funExtHelper2 : ∀ (α : X ⇒ 𝔸¹) - → α .N-ob B (X .F-hom φ x) ≡ φ .fst (α .N-ob A x) - funExtHelper2 α = funExt⁻ (α .N-hom φ) x - - --- can only state equality on object part, but that would be enough -SpΓHom : {X Y : ℤFunctor} (α : X ⇒ Y) (A : CommRing ℓ) (x : X .F-ob A .fst) - → SpΓObOb Y A (α .N-ob A x) ≡ SpΓObOb X A x ∘cr Γ .F-hom α -SpΓHom _ _ _ = RingHom≡ refl - --- TODO: can you state the triangle identities in a reasonable form? - module AdjBij where private module _ {A : CommRing ℓ} {X : ℤFunctor {ℓ}} where @@ -335,9 +272,14 @@ module AdjBij where snd (Γ⊣SpCounitEquiv A) = ε A .snd +-- Affine schemes module _ {ℓ : Level} where isAffine : (X : ℤFunctor {ℓ = ℓ}) → Type (ℓ-suc ℓ) - isAffine X = ∃[ A ∈ CommRing ℓ ] CommRingEquiv A (Γ .F-ob X) + isAffine X = ∃[ A ∈ CommRing ℓ ] NatIso (Sp .F-ob A) X + + isAffineCompactOpen : {X : ℤFunctor {ℓ = ℓ}} (U : CompactOpen X) → Type (ℓ-suc ℓ) + isAffineCompactOpen U = isAffine ⟦ U ⟧ᶜᵒ + -- The unit is an equivalence iff the ℤ-functor is affine -- unfortunately, we can't give a natural transformation @@ -345,3 +287,31 @@ module _ {ℓ : Level} where -- we can however give terms that look just like the unit, -- giving us an alternative def. of affine ℤ-functors module AffineDefs {ℓ : Level} where + + η : (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 + + private -- the rest of the "quasi natural transoformation" + η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 + + isAffineSmall : (X : ℤFunctor) → Type (ℓ-suc ℓ) + isAffineSmall X = ∀ (A : CommRing ℓ) → isEquiv (η X A) + + -- isAffineBig : (X : ℤFunctor {ℓ = ℓ}) → Type (ℓ-suc (ℓ-suc ℓ)) + -- isAffineBig X = ∃[ A ∈ CommRing (ℓ-suc ℓ) ] NatIso A (Γ .F-ob X) + + -- TODO isAffine → isAffineSmall → isAffineBig or other way around??? + +-- TODO: lattice structure on compact opens and affine covers From c958982dc26e635bf7de53371d70efe5eb29d118 Mon Sep 17 00:00:00 2001 From: mzeuner Date: Mon, 23 Oct 2023 12:41:45 +0200 Subject: [PATCH 11/18] def affine cover --- Cubical/Categories/Instances/ZFunctors.agda | 129 +++++++++++++++++--- 1 file changed, 115 insertions(+), 14 deletions(-) diff --git a/Cubical/Categories/Instances/ZFunctors.agda b/Cubical/Categories/Instances/ZFunctors.agda index 1809403b51..698dd86047 100644 --- a/Cubical/Categories/Instances/ZFunctors.agda +++ b/Cubical/Categories/Instances/ZFunctors.agda @@ -38,6 +38,8 @@ open import Cubical.Algebra.CommAlgebra open import Cubical.Algebra.CommAlgebra.FreeCommAlgebra open import Cubical.Algebra.CommAlgebra.Instances.Unit 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 @@ -47,13 +49,14 @@ open import Cubical.Categories.Instances.Sets open import Cubical.Categories.Instances.CommRings open import Cubical.Categories.Instances.CommAlgebras open import Cubical.Categories.Instances.Functors +open import Cubical.Categories.Instances.DistLattice open import Cubical.Categories.NaturalTransformation open import Cubical.Categories.Presheaf.Base open import Cubical.Categories.Yoneda open import Cubical.HITs.PropositionalTruncation as PT -open import Cubical.HITs.SetQuotients as SQ hiding ([_]) +open import Cubical.HITs.SetQuotients as SQ open Category hiding (_∘_) renaming (_⋆_ to _⋆c_) open CommAlgebraHoms @@ -90,13 +93,6 @@ module _ {ℓ : Level} where F-id 𝓛 {A} = cong fst (inducedZarLatHomId A) F-seq 𝓛 φ ψ = cong fst (inducedZarLatHomSeq φ ψ) - -- the forgetful functor - -- aka the affine line - -- (aka the representable of ℤ[x]) - 𝔸¹ : ℤFunctor - 𝔸¹ = ForgetfulCommRing→Set --Sp .F-ob ℤ[x] - - -- the big lattice of compact opens CompactOpen : ℤFunctor → Type (ℓ-suc ℓ) CompactOpen X = X ⇒ 𝓛 @@ -123,6 +119,13 @@ module _ {ℓ : Level} where (funExt⁻ (X .F-seq φ ψ) (x .fst))) + + -- 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 ⇒ 𝔸¹ @@ -131,9 +134,11 @@ module _ {ℓ : Level} where 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 @@ -148,6 +153,7 @@ module _ {ℓ : Level} where φ .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 @@ -162,6 +168,7 @@ module _ {ℓ : Level} where φ .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 @@ -306,12 +313,106 @@ module AffineDefs {ℓ : Level} where → η Y A (α .N-ob A x) ≡ η X A x ∘cr Γ .F-hom α ηHom _ _ _ = RingHom≡ refl - isAffineSmall : (X : ℤFunctor) → Type (ℓ-suc ℓ) - isAffineSmall X = ∀ (A : CommRing ℓ) → isEquiv (η X A) + isAffine' : (X : ℤFunctor) → Type (ℓ-suc ℓ) + isAffine' X = ∀ (A : CommRing ℓ) → isEquiv (η X A) + -- TODO: is it possible to prove isAffine ↔ isAffine' , or just one direction? + + +-- The lattice structure on compact opens and affine covers +module _ {ℓ : Level} (X : ℤFunctor {ℓ}) where + + open DistLatticeStr ⦃...⦄ + open CommRingStr ⦃...⦄ + open IsLatticeHom + open ZarLat - -- isAffineBig : (X : ℤFunctor {ℓ = ℓ}) → Type (ℓ-suc (ℓ-suc ℓ)) - -- isAffineBig X = ∃[ A ∈ CommRing (ℓ-suc ℓ) ] NatIso A (Γ .F-ob X) + CompOpenDistLattice : DistLattice (ℓ-suc ℓ) + fst CompOpenDistLattice = CompactOpen X - -- TODO isAffine → isAffineSmall → isAffineBig or other way around??? + -- dist. lattice structure induced by internal lattice object 𝓛 + N-ob (DistLatticeStr.0l (snd CompOpenDistLattice)) A _ = 0l + where instance _ = ZariskiLattice A .snd + N-hom (DistLatticeStr.0l (snd CompOpenDistLattice)) _ = funExt λ _ → refl --- TODO: lattice structure on compact opens and affine covers + N-ob (DistLatticeStr.1l (snd CompOpenDistLattice)) A _ = 1l + where instance _ = ZariskiLattice A .snd + N-hom (DistLatticeStr.1l (snd CompOpenDistLattice)) {x = A} {y = B} φ = funExt λ _ → path + where + instance + _ = A .snd + _ = B .snd + path : [ 1 , replicateFinVec 1 1r ] ≡ [ 1 , (replicateFinVec 1 ( φ .fst 1r)) ++Fin (λ ()) ] + path = [ 1 , replicateFinVec 1 1r ] + ≡[ i ]⟨ [ 1 , replicateFinVec 1 (φ .snd .pres1 (~ i)) ] ⟩ + [ 1 , replicateFinVec 1 (φ .fst 1r) ] + ≡[ i ]⟨ [ 1 , (++FinRid {n = 1} (replicateFinVec 1 (φ .fst 1r)) λ ()) (~ i) ] ⟩ + [ 1 , (replicateFinVec 1 ( φ .fst 1r)) ++Fin (λ ()) ] ∎ + + N-ob ((snd CompOpenDistLattice 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 CompOpenDistLattice 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) + ≡ 𝓛 .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) + ≡⟨ sym (inducedZarLatHom φ .snd .pres∨l _ _) ⟩ + 𝓛 .F-hom φ (U .N-ob A x ∨l V .N-ob A x) ∎ + + N-ob ((snd CompOpenDistLattice 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 CompOpenDistLattice 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) + ≡ 𝓛 .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) + ≡⟨ sym (inducedZarLatHom φ .snd .pres∧l _ _) ⟩ + 𝓛 .F-hom φ (U .N-ob A x ∧l V .N-ob A x) ∎ + + DistLatticeStr.isDistLattice (snd CompOpenDistLattice) = 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))) + + + open Join CompOpenDistLattice + private instance _ = CompOpenDistLattice .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 ∥₁ + -- 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) ^op + + -- 𝓞 : Functor COᵒᵖ (CommRingsCategory {ℓ = ℓ-suc ℓ}) + -- F-ob 𝓞 U = Γ .F-ob ⟦ U ⟧ᶜᵒ + -- F-hom 𝓞 U≥V = {!!} + -- F-id 𝓞 = {!!} + -- F-seq 𝓞 = {!!} From 7cd669d5103f0e1aa9462b292983a72a8c4fd7d9 Mon Sep 17 00:00:00 2001 From: mzeuner Date: Mon, 23 Oct 2023 12:42:56 +0200 Subject: [PATCH 12/18] remove FP stuff --- .../Categories/Instances/FPAlgebrasSmall.agda | 103 ------------------ 1 file changed, 103 deletions(-) delete mode 100644 Cubical/Categories/Instances/FPAlgebrasSmall.agda diff --git a/Cubical/Categories/Instances/FPAlgebrasSmall.agda b/Cubical/Categories/Instances/FPAlgebrasSmall.agda deleted file mode 100644 index 06d430dd0b..0000000000 --- a/Cubical/Categories/Instances/FPAlgebrasSmall.agda +++ /dev/null @@ -1,103 +0,0 @@ -{-# OPTIONS --safe --lossy-unification #-} -module Cubical.Categories.Instances.FPAlgebrasSmall 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.Foundations.Structure - -open import Cubical.Data.Unit -open import Cubical.Data.Sigma -open import Cubical.Data.Nat -open import Cubical.Data.FinData - -open import Cubical.Algebra.Ring -open import Cubical.Algebra.CommRing -open import Cubical.Algebra.Algebra -open import Cubical.Algebra.CommAlgebra -open import Cubical.Algebra.CommAlgebra.FPAlgebra -open import Cubical.Algebra.CommAlgebra.FPAlgebra.Instances -open import Cubical.Algebra.CommAlgebra.Instances.Unit -open import Cubical.Algebra.ZariskiLattice.Base -open import Cubical.Algebra.ZariskiLattice.UniversalProperty - -open import Cubical.Categories.Category -open import Cubical.Categories.Functor --- open import Cubical.Categories.Limits.Terminal --- open import Cubical.Categories.Limits.Pullback --- open import Cubical.Categories.Limits.Limits -open import Cubical.Categories.Instances.Sets -open import Cubical.Categories.Instances.CommRings -open import Cubical.Categories.Instances.CommAlgebras -open import Cubical.Categories.Instances.Functors -open import Cubical.Categories.NaturalTransformation -open import Cubical.Categories.Presheaf.Base -open import Cubical.Categories.Yoneda - - -open import Cubical.HITs.PropositionalTruncation as PT -open import Cubical.HITs.SetQuotients as SQ - -open Category hiding (_∘_) renaming (_⋆_ to _⋆c_) -open CommAlgebraHoms --- open Cospan --- open Pullback - -private - variable - ℓ ℓ' ℓ'' : Level - - -module _ (R : CommRing ℓ) where - open Category - - -- type living in the same universe as the base ring R - record SmallFPAlgebra : Type ℓ where - field - n : ℕ - m : ℕ - relations : FinVec ⟨ Polynomials {R = R} n ⟩ m - - open SmallFPAlgebra - private - indFPAlg : SmallFPAlgebra → CommAlgebra R ℓ - indFPAlg A = FPAlgebra (A .n) (A .relations) - - FPAlgebrasSmallCategory : Category ℓ ℓ - ob FPAlgebrasSmallCategory = SmallFPAlgebra - Hom[_,_] FPAlgebrasSmallCategory A B = - CommAlgebraHom (indFPAlg A) (indFPAlg B) - id FPAlgebrasSmallCategory = idCommAlgebraHom _ - _⋆_ FPAlgebrasSmallCategory = compCommAlgebraHom _ _ _ - ⋆IdL FPAlgebrasSmallCategory = compIdCommAlgebraHom - ⋆IdR FPAlgebrasSmallCategory = idCompCommAlgebraHom - ⋆Assoc FPAlgebrasSmallCategory = compAssocCommAlgebraHom - isSetHom FPAlgebrasSmallCategory = isSetAlgebraHom _ _ - - - -- yoneda in the notation of Demazure-Gabriel - -- uses η-equality of Categories - Sp : Functor (FPAlgebrasSmallCategory ^op) (FUNCTOR FPAlgebrasSmallCategory (SET ℓ)) - Sp = YO {C = (FPAlgebrasSmallCategory ^op)} - - open Functor - - -- special internal objects to talk about schemes - -- first the affine line - private - R[x]ᶠᵖ : SmallFPAlgebra - n R[x]ᶠᵖ = 1 - m R[x]ᶠᵖ = 0 - relations R[x]ᶠᵖ = λ () - - 𝔸¹ = Sp .F-ob R[x]ᶠᵖ - - -- the Zariski lattice (classifying compact open subobjects) - 𝓛 : Functor FPAlgebrasSmallCategory (SET ℓ) - F-ob 𝓛 A = ZarLat.ZL (CommAlgebra→CommRing (indFPAlg A)) , SQ.squash/ - F-hom 𝓛 φ = inducedZarLatHom (CommAlgebraHom→CommRingHom _ _ φ) .fst - F-id 𝓛 {A} = {!cong fst (inducedZarLatHomId (CommAlgebra→CommRing (indFPAlg A)))!} - F-seq 𝓛 = {!!} From 9014c59c4f3ff123c0bdc2822c55fd6b870f67a5 Mon Sep 17 00:00:00 2001 From: mzeuner Date: Mon, 23 Oct 2023 17:57:18 +0200 Subject: [PATCH 13/18] collect TODOs --- Cubical/Categories/Instances/ZFunctors.agda | 55 +++++++-------------- 1 file changed, 18 insertions(+), 37 deletions(-) diff --git a/Cubical/Categories/Instances/ZFunctors.agda b/Cubical/Categories/Instances/ZFunctors.agda index 698dd86047..5d01566f69 100644 --- a/Cubical/Categories/Instances/ZFunctors.agda +++ b/Cubical/Categories/Instances/ZFunctors.agda @@ -13,30 +13,19 @@ open import Cubical.Foundations.Isomorphism open import Cubical.Foundations.Function open import Cubical.Foundations.Powerset open import Cubical.Foundations.HLevels -open import Cubical.Foundations.Structure + open import Cubical.Functions.FunExtEquiv -open import Cubical.Data.Unit open import Cubical.Data.Sigma -open import Cubical.Data.Nat renaming ( _+_ to _+ℕ_ ; _·_ to _·ℕ_ ; _^_ to _^ℕ_ - ; +-comm to +ℕ-comm ; +-assoc to +ℕ-assoc - ; ·-assoc to ·ℕ-assoc ; ·-comm to ·ℕ-comm - ; ·-identityʳ to ·ℕ-rid) +open import Cubical.Data.Nat using (ℕ) open import Cubical.Data.FinData -open import Cubical.Data.Int as Int - renaming ( ℤ to ℤ ; _+_ to _+ℤ_; _·_ to _·ℤ_; -_ to -ℤ_) - open import Cubical.Algebra.Ring open import Cubical.Algebra.CommRing -open import Cubical.Algebra.CommRing.Instances.Int -open import Cubical.Algebra.CommRing.Instances.Unit open import Cubical.Algebra.Algebra open import Cubical.Algebra.CommAlgebra -open import Cubical.Algebra.CommAlgebra.FreeCommAlgebra -open import Cubical.Algebra.CommAlgebra.Instances.Unit open import Cubical.Algebra.Lattice open import Cubical.Algebra.DistLattice open import Cubical.Algebra.DistLattice.BigOps @@ -47,21 +36,14 @@ open import Cubical.Categories.Category open import Cubical.Categories.Functor open import Cubical.Categories.Instances.Sets open import Cubical.Categories.Instances.CommRings -open import Cubical.Categories.Instances.CommAlgebras open import Cubical.Categories.Instances.Functors -open import Cubical.Categories.Instances.DistLattice open import Cubical.Categories.NaturalTransformation -open import Cubical.Categories.Presheaf.Base open import Cubical.Categories.Yoneda - open import Cubical.HITs.PropositionalTruncation as PT open import Cubical.HITs.SetQuotients as SQ open Category hiding (_∘_) renaming (_⋆_ to _⋆c_) -open CommAlgebraHoms --- open Cospan --- open Pullback private variable @@ -80,7 +62,7 @@ module _ {ℓ : Level} where ℤ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)} @@ -127,7 +109,7 @@ module _ {ℓ : Level} where 𝔸¹ = ForgetfulCommRing→Set -- the global sections functor - Γ : Functor ℤFUNCTOR (CommRingsCategory {ℓ-suc ℓ} ^op) + Γ : Functor ℤFUNCTOR (CommRingsCategory {ℓ = ℓ-suc ℓ} ^op) fst (F-ob Γ X) = X ⇒ 𝔸¹ -- ring struncture induced by internal ring object 𝔸¹ @@ -281,17 +263,22 @@ module AdjBij where -- Affine schemes module _ {ℓ : Level} where - isAffine : (X : ℤFunctor {ℓ = ℓ}) → Type (ℓ-suc ℓ) + isAffine : (X : ℤFunctor) → Type (ℓ-suc ℓ) isAffine X = ∃[ A ∈ CommRing ℓ ] NatIso (Sp .F-ob A) X - isAffineCompactOpen : {X : ℤFunctor {ℓ = ℓ}} (U : CompactOpen X) → Type (ℓ-suc ℓ) + -- TODO: 𝔸¹ is affine, namely Sp ℤ[x] + + isAffineCompactOpen : {X : ℤFunctor} (U : CompactOpen X) → Type (ℓ-suc ℓ) isAffineCompactOpen U = isAffine ⟦ U ⟧ᶜᵒ + -- TODO: define standard basic open D(f) ↪ Sp A and prove + -- D(f) ≅ Sp A[1/f], in particular isAffineCompactOpen D(f) + --- The unit is an equivalence iff the ℤ-functor is affine --- unfortunately, we can't give a natural transformation +-- 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, +-- We can however give terms that look just like the unit, -- giving us an alternative def. of affine ℤ-functors module AffineDefs {ℓ : Level} where @@ -315,11 +302,11 @@ module AffineDefs {ℓ : Level} where isAffine' : (X : ℤFunctor) → Type (ℓ-suc ℓ) isAffine' X = ∀ (A : CommRing ℓ) → isEquiv (η X A) - -- TODO: is it possible to prove isAffine ↔ isAffine' , or just one direction? + -- TODO: isAffine → isAffine' -- The lattice structure on compact opens and affine covers -module _ {ℓ : Level} (X : ℤFunctor {ℓ}) where +module _ {ℓ : Level} (X : ℤFunctor) where open DistLatticeStr ⦃...⦄ open CommRingStr ⦃...⦄ @@ -393,6 +380,7 @@ module _ {ℓ : Level} (X : ℤFunctor {ℓ}) where (λ _ _ _ → makeNatTransPath (funExt₂ -- same here (λ A _ → ZariskiLattice A .snd .DistLatticeStr.∧l-dist-∨l _ _ _ .fst))) + -- TODO: (contravariant) action on morphisms open Join CompOpenDistLattice private instance _ = CompOpenDistLattice .snd @@ -408,11 +396,4 @@ module _ {ℓ : Level} (X : ℤFunctor {ℓ}) where 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) ^op - - -- 𝓞 : Functor COᵒᵖ (CommRingsCategory {ℓ = ℓ-suc ℓ}) - -- F-ob 𝓞 U = Γ .F-ob ⟦ U ⟧ᶜᵒ - -- F-hom 𝓞 U≥V = {!!} - -- F-id 𝓞 = {!!} - -- F-seq 𝓞 = {!!} + -- TODO: Define the structure sheaf of X as 𝓞 U = Γ ⟦ U ⟧ᶜᵒ From 00ff326384451fef7549315a203bcd73d173d939 Mon Sep 17 00:00:00 2001 From: mzeuner Date: Mon, 23 Oct 2023 18:28:16 +0200 Subject: [PATCH 14/18] refacor --- Cubical/Categories/Instances/ZFunctors.agda | 161 +++++++++++--------- 1 file changed, 87 insertions(+), 74 deletions(-) diff --git a/Cubical/Categories/Instances/ZFunctors.agda b/Cubical/Categories/Instances/ZFunctors.agda index 5d01566f69..647bf2a3a8 100644 --- a/Cubical/Categories/Instances/ZFunctors.agda +++ b/Cubical/Categories/Instances/ZFunctors.agda @@ -51,10 +51,9 @@ private module _ {ℓ : Level} where + open Functor open NatTrans - open ZarLat - open ZarLatUniversalProp open CommRingStr ⦃...⦄ open IsRingHom @@ -67,41 +66,6 @@ module _ {ℓ : Level} where Sp : Functor (CommRingsCategory {ℓ = ℓ} ^op) ℤFUNCTOR Sp = YO {C = (CommRingsCategory {ℓ = ℓ} ^op)} - -- special functors to talk about schemes - -- 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 φ ψ) - - -- the big lattice of compact opens - CompactOpen : ℤFunctor → Type (ℓ-suc ℓ) - CompactOpen X = X ⇒ 𝓛 - - -- 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 ⟩ - 𝓛 .F-hom φ (U .N-ob A x) ≡⟨ cong (𝓛 .F-hom φ) Ux≡D1 ⟩ - 𝓛 .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))) - - - -- the forgetful functor -- aka the affine line -- (aka the representable of ℤ[x]) @@ -188,13 +152,13 @@ module _ {ℓ : Level} where -- we get an adjunction Γ ⊣ Sp modulo size issues -open Functor -open NatTrans -open Iso -open IsRingHom - 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 @@ -263,17 +227,13 @@ module AdjBij where -- Affine schemes module _ {ℓ : Level} where + open Functor + isAffine : (X : ℤFunctor) → Type (ℓ-suc ℓ) isAffine X = ∃[ A ∈ CommRing ℓ ] NatIso (Sp .F-ob A) X -- TODO: 𝔸¹ is affine, namely Sp ℤ[x] - isAffineCompactOpen : {X : ℤFunctor} (U : CompactOpen X) → Type (ℓ-suc ℓ) - isAffineCompactOpen U = isAffine ⟦ U ⟧ᶜᵒ - - -- TODO: define standard basic open D(f) ↪ Sp A and prove - -- D(f) ≅ Sp A[1/f], in particular isAffineCompactOpen D(f) - -- The unit is an equivalence iff the ℤ-functor is affine. -- Unfortunately, we can't give a natural transformation @@ -281,7 +241,10 @@ module _ {ℓ : Level} where -- We can however give terms that look just like the unit, -- giving us an alternative def. of affine ℤ-functors 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 @@ -305,25 +268,73 @@ module AffineDefs {ℓ : Level} where -- TODO: isAffine → isAffine' --- The lattice structure on compact opens and affine covers -module _ {ℓ : Level} (X : ℤFunctor) where +-- compact opens and affine covers +module _ {ℓ : Level} where + open Iso + open Functor + open NatTrans open DistLatticeStr ⦃...⦄ open CommRingStr ⦃...⦄ + open IsRingHom open IsLatticeHom open ZarLat + 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 φ ψ) - CompOpenDistLattice : DistLattice (ℓ-suc ℓ) - fst CompOpenDistLattice = CompactOpen X + -- the big lattice of compact opens + CompactOpen : ℤFunctor → Type (ℓ-suc ℓ) + CompactOpen X = X ⇒ 𝓛 + + -- 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 ⟩ + 𝓛 .F-hom φ (U .N-ob A x) ≡⟨ cong (𝓛 .F-hom φ) Ux≡D1 ⟩ + 𝓛 .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 ⟧ᶜᵒ + + -- basic opens + 𝔇 : (A : CommRing ℓ) (f : A .fst) → CompactOpen (Sp .F-ob A) + 𝔇 A f = yonedaᴾ 𝓛 A .inv (D A f) + -- TODO: 𝔇 A f ≅ Sp A[1/f], in particular isAffineCompactOpen (𝔇 A f) + + + -- the dist. lattice of compact opens + CompOpenDistLattice : ℤFunctor → DistLattice (ℓ-suc ℓ) + fst (CompOpenDistLattice X) = CompactOpen X -- dist. lattice structure induced by internal lattice object 𝓛 - N-ob (DistLatticeStr.0l (snd CompOpenDistLattice)) A _ = 0l + N-ob (DistLatticeStr.0l (snd (CompOpenDistLattice X))) A _ = 0l where instance _ = ZariskiLattice A .snd - N-hom (DistLatticeStr.0l (snd CompOpenDistLattice)) _ = funExt λ _ → refl + N-hom (DistLatticeStr.0l (snd (CompOpenDistLattice X))) _ = funExt λ _ → refl - N-ob (DistLatticeStr.1l (snd CompOpenDistLattice)) A _ = 1l + N-ob (DistLatticeStr.1l (snd (CompOpenDistLattice X))) A _ = 1l where instance _ = ZariskiLattice A .snd - N-hom (DistLatticeStr.1l (snd CompOpenDistLattice)) {x = A} {y = B} φ = funExt λ _ → path + N-hom (DistLatticeStr.1l (snd (CompOpenDistLattice X))) {x = A} {y = B} φ = funExt λ _ → path where instance _ = A .snd @@ -335,9 +346,9 @@ module _ {ℓ : Level} (X : ℤFunctor) where ≡[ i ]⟨ [ 1 , (++FinRid {n = 1} (replicateFinVec 1 (φ .fst 1r)) λ ()) (~ i) ] ⟩ [ 1 , (replicateFinVec 1 ( φ .fst 1r)) ++Fin (λ ()) ] ∎ - N-ob ((snd CompOpenDistLattice DistLatticeStr.∨l U) V) A x = U .N-ob A x ∨l V .N-ob A x + N-ob ((snd (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 CompOpenDistLattice DistLatticeStr.∨l U) V) {x = A} {y = B} φ = funExt path + N-hom ((snd (CompOpenDistLattice X) DistLatticeStr.∨l U) V) {x = A} {y = B} φ = funExt path where instance _ = ZariskiLattice A .snd @@ -350,9 +361,9 @@ module _ {ℓ : Level} (X : ℤFunctor) where ≡⟨ sym (inducedZarLatHom φ .snd .pres∨l _ _) ⟩ 𝓛 .F-hom φ (U .N-ob A x ∨l V .N-ob A x) ∎ - N-ob ((snd CompOpenDistLattice DistLatticeStr.∧l U) V) A x = U .N-ob A x ∧l V .N-ob A x + N-ob ((snd (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 CompOpenDistLattice DistLatticeStr.∧l U) V) {x = A} {y = B} φ = funExt path + N-hom ((snd (CompOpenDistLattice X) DistLatticeStr.∧l U) V) {x = A} {y = B} φ = funExt path where instance _ = ZariskiLattice A .snd @@ -365,7 +376,7 @@ module _ {ℓ : Level} (X : ℤFunctor) where ≡⟨ sym (inducedZarLatHom φ .snd .pres∧l _ _) ⟩ 𝓛 .F-hom φ (U .N-ob A x ∧l V .N-ob A x) ∎ - DistLatticeStr.isDistLattice (snd CompOpenDistLattice) = makeIsDistLattice∧lOver∨l + DistLatticeStr.isDistLattice (snd (CompOpenDistLattice X)) = makeIsDistLattice∧lOver∨l isSetNatTrans (λ _ _ _ → makeNatTransPath (funExt₂ (λ A _ → ZariskiLattice A .snd .DistLatticeStr.∨lAssoc _ _ _))) @@ -382,18 +393,20 @@ module _ {ℓ : Level} (X : ℤFunctor) where -- TODO: (contravariant) action on morphisms - open Join CompOpenDistLattice - private instance _ = CompOpenDistLattice .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) + module _ (X : ℤFunctor) where + open Join (CompOpenDistLattice X) + private instance _ = (CompOpenDistLattice 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 ∥₁ - -- TODO: A ℤ-functor is a qcqs-scheme if it is a Zariski sheaf and has an affine cover + hasAffineCover : Type (ℓ-suc ℓ) + hasAffineCover = ∥ AffineCover ∥₁ + -- TODO: A ℤ-functor is a qcqs-scheme if it is a Zariski sheaf and has an affine cover - -- TODO: Define the structure sheaf of X as 𝓞 U = Γ ⟦ U ⟧ᶜᵒ + -- TODO: Define the structure sheaf of X as 𝓞 U = Γ ⟦ U ⟧ᶜᵒ From adf19d4f3648554dd2de4a257cdf57301d692817 Mon Sep 17 00:00:00 2001 From: mzeuner Date: Wed, 25 Oct 2023 16:15:21 +0200 Subject: [PATCH 15/18] standard basic opens --- Cubical/Categories/Instances/ZFunctors.agda | 38 +++++++++++++-------- 1 file changed, 24 insertions(+), 14 deletions(-) diff --git a/Cubical/Categories/Instances/ZFunctors.agda b/Cubical/Categories/Instances/ZFunctors.agda index 647bf2a3a8..aff4d4f2ac 100644 --- a/Cubical/Categories/Instances/ZFunctors.agda +++ b/Cubical/Categories/Instances/ZFunctors.agda @@ -24,8 +24,7 @@ open import Cubical.Data.FinData open import Cubical.Algebra.Ring open import Cubical.Algebra.CommRing -open import Cubical.Algebra.Algebra -open import Cubical.Algebra.CommAlgebra +open import Cubical.Algebra.CommRing.Localisation open import Cubical.Algebra.Lattice open import Cubical.Algebra.DistLattice open import Cubical.Algebra.DistLattice.BigOps @@ -253,15 +252,15 @@ module AffineDefs {ℓ : Level} where pres· (snd (η X A x)) _ _ = refl pres- (snd (η X A x)) _ = refl - private -- the rest of the "quasi natural transoformation" - η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)) + -- 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 + -- 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) @@ -317,10 +316,21 @@ module _ {ℓ : Level} where isAffineCompactOpen : {X : ℤFunctor} (U : CompactOpen X) → Type (ℓ-suc ℓ) isAffineCompactOpen U = isAffine ⟦ U ⟧ᶜᵒ - -- basic opens - 𝔇 : (A : CommRing ℓ) (f : A .fst) → CompactOpen (Sp .F-ob A) - 𝔇 A f = yonedaᴾ 𝓛 A .inv (D A f) - -- TODO: 𝔇 A f ≅ Sp A[1/f], in particular isAffineCompactOpen (𝔇 A f) + -- -- basic opens + -- module BasicAffineCompactOpen (R : CommRing ℓ) (f : R .fst) where + -- open NatIso + -- open InvertingElementsBase R + + -- 𝔇 : CompactOpen (Sp .F-ob R) + -- 𝔇 = yonedaᴾ 𝓛 R .inv (D R f) + + -- 𝔇LocIso : NatIso ⟦ 𝔇 ⟧ᶜᵒ (Sp .F-ob R[1/ f ]AsCommRing) + -- N-ob (trans 𝔇LocIso) B (φ , 𝔇fφ≡D1) = {!𝔇fφ≡D1!} + -- N-hom (trans 𝔇LocIso) = {!!} + -- isIso.inv (nIso 𝔇LocIso x) = {!!} + -- isIso.sec (nIso 𝔇LocIso x) = {!!} + -- isIso.ret (nIso 𝔇LocIso x) = {!!} + -- -- TODO: 𝔇 A f ≅ Sp A[1/f], in particular isAffineCompactOpen (𝔇 A f) -- the dist. lattice of compact opens From 1dc9ab4f856ea424b585e80be3b5789e3543a896 Mon Sep 17 00:00:00 2001 From: mzeuner Date: Wed, 25 Oct 2023 16:31:39 +0200 Subject: [PATCH 16/18] more cleaning up --- .../ZariskiLattice/UniversalProperty.agda | 7 ++--- Cubical/Categories/Instances/ZFunctors.agda | 30 ++++--------------- 2 files changed, 7 insertions(+), 30 deletions(-) diff --git a/Cubical/Algebra/ZariskiLattice/UniversalProperty.agda b/Cubical/Algebra/ZariskiLattice/UniversalProperty.agda index 0a5dd28e7d..351562674d 100644 --- a/Cubical/Algebra/ZariskiLattice/UniversalProperty.agda +++ b/Cubical/Algebra/ZariskiLattice/UniversalProperty.agda @@ -373,8 +373,5 @@ module _ {A B C : CommRing ℓ} (φ : CommRingHom A B) (ψ : CommRingHom B C) wh cong fst (ZLHasUniversalProp A (ZariskiLattice C) (Dcomp (ψ ∘cr φ)) (isZarMapDcomp (ψ ∘cr φ)) .snd - (inducedZarLatHom ψ ∘dl inducedZarLatHom φ , funExt path)) - where - path : ∀ f → fst (inducedZarLatHom ψ ∘dl inducedZarLatHom φ) (D A f) - ≡ Dcomp (ψ ∘cr φ) f - path f i = [ 1 , (++FinRid {n = 1} (λ _ → (ψ ∘cr φ) .fst f) λ ()) i ] + (inducedZarLatHom ψ ∘dl inducedZarLatHom φ , funExt (λ _ → ∨lRid _))) + where open DistLatticeStr (ZariskiLattice C .snd) diff --git a/Cubical/Categories/Instances/ZFunctors.agda b/Cubical/Categories/Instances/ZFunctors.agda index aff4d4f2ac..a3e1eefaa5 100644 --- a/Cubical/Categories/Instances/ZFunctors.agda +++ b/Cubical/Categories/Instances/ZFunctors.agda @@ -24,7 +24,6 @@ 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.Lattice open import Cubical.Algebra.DistLattice open import Cubical.Algebra.DistLattice.BigOps @@ -287,7 +286,6 @@ module _ {ℓ : Level} where F-id 𝓛 {A} = cong fst (inducedZarLatHomId A) F-seq 𝓛 φ ψ = cong fst (inducedZarLatHomSeq φ ψ) - -- the big lattice of compact opens CompactOpen : ℤFunctor → Type (ℓ-suc ℓ) CompactOpen X = X ⇒ 𝓛 @@ -316,24 +314,9 @@ module _ {ℓ : Level} where isAffineCompactOpen : {X : ℤFunctor} (U : CompactOpen X) → Type (ℓ-suc ℓ) isAffineCompactOpen U = isAffine ⟦ U ⟧ᶜᵒ - -- -- basic opens - -- module BasicAffineCompactOpen (R : CommRing ℓ) (f : R .fst) where - -- open NatIso - -- open InvertingElementsBase R + -- TODO: define basic opens D(f) ↪ Sp A and prove D(f) ≅ Sp A[1/f] - -- 𝔇 : CompactOpen (Sp .F-ob R) - -- 𝔇 = yonedaᴾ 𝓛 R .inv (D R f) - - -- 𝔇LocIso : NatIso ⟦ 𝔇 ⟧ᶜᵒ (Sp .F-ob R[1/ f ]AsCommRing) - -- N-ob (trans 𝔇LocIso) B (φ , 𝔇fφ≡D1) = {!𝔇fφ≡D1!} - -- N-hom (trans 𝔇LocIso) = {!!} - -- isIso.inv (nIso 𝔇LocIso x) = {!!} - -- isIso.sec (nIso 𝔇LocIso x) = {!!} - -- isIso.ret (nIso 𝔇LocIso x) = {!!} - -- -- TODO: 𝔇 A f ≅ Sp A[1/f], in particular isAffineCompactOpen (𝔇 A f) - - - -- the dist. lattice of compact opens + -- the (big) dist. lattice of compact opens CompOpenDistLattice : ℤFunctor → DistLattice (ℓ-suc ℓ) fst (CompOpenDistLattice X) = CompactOpen X @@ -349,12 +332,9 @@ module _ {ℓ : Level} where instance _ = A .snd _ = B .snd - path : [ 1 , replicateFinVec 1 1r ] ≡ [ 1 , (replicateFinVec 1 ( φ .fst 1r)) ++Fin (λ ()) ] - path = [ 1 , replicateFinVec 1 1r ] - ≡[ i ]⟨ [ 1 , replicateFinVec 1 (φ .snd .pres1 (~ i)) ] ⟩ - [ 1 , replicateFinVec 1 (φ .fst 1r) ] - ≡[ i ]⟨ [ 1 , (++FinRid {n = 1} (replicateFinVec 1 (φ .fst 1r)) λ ()) (~ i) ] ⟩ - [ 1 , (replicateFinVec 1 ( φ .fst 1r)) ++Fin (λ ()) ] ∎ + _ = 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 (CompOpenDistLattice X) DistLatticeStr.∨l U) V) A x = U .N-ob A x ∨l V .N-ob A x where instance _ = ZariskiLattice A .snd From 29cf5ca9248d4be9c47904e412606f442756dcec Mon Sep 17 00:00:00 2001 From: mzeuner Date: Thu, 26 Oct 2023 23:15:41 +0200 Subject: [PATCH 17/18] Structure sheaf --- Cubical/Categories/Instances/ZFunctors.agda | 67 +++++++++++++++++++-- 1 file changed, 61 insertions(+), 6 deletions(-) diff --git a/Cubical/Categories/Instances/ZFunctors.agda b/Cubical/Categories/Instances/ZFunctors.agda index a3e1eefaa5..f3b00ac377 100644 --- a/Cubical/Categories/Instances/ZFunctors.agda +++ b/Cubical/Categories/Instances/ZFunctors.agda @@ -1,7 +1,6 @@ {- - The impredicative way to do the functor of points of qcqs-schemes - (over Spec(ℤ)) + The impredicative way to define functorial qcqs-schemes (over Spec(ℤ)) -} {-# OPTIONS --safe --lossy-unification #-} @@ -24,6 +23,7 @@ open import Cubical.Data.FinData open import Cubical.Algebra.Ring 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 @@ -34,6 +34,7 @@ open import Cubical.Categories.Category 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.Functors open import Cubical.Categories.NaturalTransformation open import Cubical.Categories.Yoneda @@ -41,6 +42,8 @@ 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 @@ -238,7 +241,7 @@ module _ {ℓ : Level} where -- 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 -module AffineDefs {ℓ : Level} where +private module AffineDefs {ℓ : Level} where open Functor open NatTrans open Iso @@ -314,7 +317,7 @@ module _ {ℓ : Level} where 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] + -- 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 → DistLattice (ℓ-suc ℓ) @@ -381,11 +384,33 @@ module _ {ℓ : Level} where (λ _ _ _ → makeNatTransPath (funExt₂ -- same here (λ A _ → ZariskiLattice A .snd .DistLatticeStr.∧l-dist-∨l _ _ _ .fst))) - -- TODO: (contravariant) action on morphisms + -- (contravariant) action on morphisms + CompOpenDistLatticeHom : {X Y : ℤFunctor} (α : X ⇒ Y) + → DistLatticeHom (CompOpenDistLattice Y) (CompOpenDistLattice X) + fst (CompOpenDistLatticeHom α) = α ●ᵛ_ + pres0 (snd (CompOpenDistLatticeHom α)) = makeNatTransPath (funExt₂ λ _ _ → refl) + pres1 (snd (CompOpenDistLatticeHom α)) = makeNatTransPath (funExt₂ λ _ _ → refl) + pres∨l (snd (CompOpenDistLatticeHom α)) _ _ = makeNatTransPath (funExt₂ λ _ _ → refl) + pres∧l (snd (CompOpenDistLatticeHom α)) _ _ = makeNatTransPath (funExt₂ λ _ _ → refl) + + -- functoriality of this construction + CompOpenDistLatticeId : {X : ℤFunctor} → CompOpenDistLatticeHom (idTrans X) + ≡ idDistLatticeHom (CompOpenDistLattice X) + CompOpenDistLatticeId = LatticeHom≡f _ _ + (funExt λ _ → makeNatTransPath (funExt₂ λ _ _ → refl)) + + CompOpenDistLatticeSeq : {X Y Z : ℤFunctor} (α : X ⇒ Y) (β : Y ⇒ Z) + → CompOpenDistLatticeHom (α ●ᵛ β) + ≡ CompOpenDistLatticeHom α ∘dl CompOpenDistLatticeHom β + CompOpenDistLatticeSeq _ _ = LatticeHom≡f _ _ + (funExt λ _ → makeNatTransPath (funExt₂ λ _ _ → refl)) module _ (X : ℤFunctor) where open Join (CompOpenDistLattice X) + open JoinSemilattice (Lattice→JoinSemilattice (DistLattice→Lattice (CompOpenDistLattice X))) + open PosetStr (IndPoset .snd) hiding (_≤_) + open LatticeTheory ⦃...⦄ -- ((DistLattice→Lattice (CompOpenDistLattice X))) private instance _ = (CompOpenDistLattice X) .snd record AffineCover : Type (ℓ-suc ℓ) where @@ -399,4 +424,34 @@ module _ {ℓ : Level} where hasAffineCover = ∥ AffineCover ∥₁ -- TODO: A ℤ-functor is a qcqs-scheme if it is a Zariski sheaf and has an affine cover - -- TODO: Define the structure sheaf of X as 𝓞 U = Γ ⟦ U ⟧ᶜᵒ + -- the structure sheaf + private COᵒᵖ = (DistLatticeCategory (CompOpenDistLattice X)) ^op + + 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 + + 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)) + + 𝓞 : 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 _ _ From 8348a41417602a5817d9bf3f8022fb695e46a8c7 Mon Sep 17 00:00:00 2001 From: mzeuner Date: Fri, 27 Oct 2023 16:03:34 +0200 Subject: [PATCH 18/18] requested changes --- Cubical/Algebra/Lattice/Base.agda | 13 ++++ .../Categories/Instances/DistLattices.agda | 23 +++++++ Cubical/Categories/Instances/Lattices.agda | 22 ++++++ Cubical/Categories/Instances/ZFunctors.agda | 67 +++++++++---------- 4 files changed, 88 insertions(+), 37 deletions(-) create mode 100644 Cubical/Categories/Instances/DistLattices.agda create mode 100644 Cubical/Categories/Instances/Lattices.agda diff --git a/Cubical/Algebra/Lattice/Base.agda b/Cubical/Algebra/Lattice/Base.agda index 55889dfa6e..7f411bb793 100644 --- a/Cubical/Algebra/Lattice/Base.agda +++ b/Cubical/Algebra/Lattice/Base.agda @@ -194,6 +194,19 @@ isPropIsLatticeHom R f S = isOfHLevelRetractFromIso 1 IsLatticeHomIsoΣ open LatticeStr S +isSetLatticeHom : (A : Lattice ℓ) (B : Lattice ℓ') → isSet (LatticeHom A B) +isSetLatticeHom A B = isSetΣSndProp (isSetΠ λ _ → is-set) (λ f → isPropIsLatticeHom (snd A) f (snd B)) + where + open LatticeStr (str B) using (is-set) + +isSetLatticeEquiv : (A : Lattice ℓ) (B : Lattice ℓ') → isSet (LatticeEquiv A B) +isSetLatticeEquiv A B = isSetΣSndProp (isOfHLevel≃ 2 A.is-set B.is-set) + (λ e → isPropIsLatticeHom (snd A) (fst e) (snd B)) + where + module A = LatticeStr (str A) + module B = LatticeStr (str B) + + 𝒮ᴰ-Lattice : DUARel (𝒮-Univ ℓ) LatticeStr ℓ 𝒮ᴰ-Lattice = 𝒮ᴰ-Record (𝒮-Univ _) IsLatticeEquiv diff --git a/Cubical/Categories/Instances/DistLattices.agda b/Cubical/Categories/Instances/DistLattices.agda new file mode 100644 index 0000000000..15420d3be4 --- /dev/null +++ b/Cubical/Categories/Instances/DistLattices.agda @@ -0,0 +1,23 @@ +{-# OPTIONS --safe #-} +module Cubical.Categories.Instances.DistLattices where + +open import Cubical.Foundations.Prelude +open import Cubical.Foundations.Function + +open import Cubical.Algebra.Lattice +open import Cubical.Algebra.DistLattice + +open import Cubical.Categories.Category + +open Category + + +DistLatticesCategory : ∀ {ℓ} → Category (ℓ-suc ℓ) ℓ +ob DistLatticesCategory = DistLattice _ +Hom[_,_] DistLatticesCategory = DistLatticeHom +id DistLatticesCategory {L} = idDistLatticeHom L +_⋆_ DistLatticesCategory {L} {M} {N} = compDistLatticeHom L M N +⋆IdL DistLatticesCategory {L} {M} = compIdDistLatticeHom {L = L} {M} +⋆IdR DistLatticesCategory {L} {M} = idCompDistLatticeHom {L = L} {M} +⋆Assoc DistLatticesCategory {L} {M} {N} {O} = compAssocDistLatticeHom {L = L} {M} {N} {O} +isSetHom DistLatticesCategory = isSetLatticeHom _ _ diff --git a/Cubical/Categories/Instances/Lattices.agda b/Cubical/Categories/Instances/Lattices.agda new file mode 100644 index 0000000000..1a8b91267a --- /dev/null +++ b/Cubical/Categories/Instances/Lattices.agda @@ -0,0 +1,22 @@ +{-# OPTIONS --safe #-} +module Cubical.Categories.Instances.Lattices where + +open import Cubical.Foundations.Prelude +open import Cubical.Foundations.Function + +open import Cubical.Algebra.Lattice + +open import Cubical.Categories.Category + +open Category +open LatticeHoms + +LatticesCategory : ∀ {ℓ} → Category (ℓ-suc ℓ) ℓ +ob LatticesCategory = Lattice _ +Hom[_,_] LatticesCategory = LatticeHom +id LatticesCategory {L} = idLatticeHom L +_⋆_ LatticesCategory = compLatticeHom +⋆IdL LatticesCategory = compIdLatticeHom +⋆IdR LatticesCategory = idCompLatticeHom +⋆Assoc LatticesCategory = compAssocLatticeHom +isSetHom LatticesCategory = isSetLatticeHom _ _ diff --git a/Cubical/Categories/Instances/ZFunctors.agda b/Cubical/Categories/Instances/ZFunctors.agda index f3b00ac377..701f7c4020 100644 --- a/Cubical/Categories/Instances/ZFunctors.agda +++ b/Cubical/Categories/Instances/ZFunctors.agda @@ -35,6 +35,7 @@ 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.NaturalTransformation open import Cubical.Categories.Yoneda @@ -233,7 +234,7 @@ module _ {ℓ : Level} where isAffine : (X : ℤFunctor) → Type (ℓ-suc ℓ) isAffine X = ∃[ A ∈ CommRing ℓ ] NatIso (Sp .F-ob A) X - -- TODO: 𝔸¹ is affine, namely Sp ℤ[x] + -- TODO: 𝔸¹ ≅ Sp ℤ[x] and 𝔾ₘ ≅ Sp ℤ[x,x⁻¹] as first examples of affine schemes -- The unit is an equivalence iff the ℤ-functor is affine. @@ -320,17 +321,17 @@ module _ {ℓ : Level} where -- 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 → DistLattice (ℓ-suc ℓ) - fst (CompOpenDistLattice X) = CompactOpen X + CompOpenDistLattice : Functor ℤFUNCTOR (DistLatticesCategory {ℓ = ℓ-suc ℓ} ^op) + fst (F-ob CompOpenDistLattice X) = CompactOpen X - -- dist. lattice structure induced by internal lattice object 𝓛 - N-ob (DistLatticeStr.0l (snd (CompOpenDistLattice X))) A _ = 0l + -- lattice structure induce by internal lattice object 𝓛 + N-ob (DistLatticeStr.0l (snd (F-ob CompOpenDistLattice X))) A _ = 0l where instance _ = ZariskiLattice A .snd - N-hom (DistLatticeStr.0l (snd (CompOpenDistLattice X))) _ = funExt λ _ → refl + N-hom (DistLatticeStr.0l (snd (F-ob CompOpenDistLattice X))) _ = funExt λ _ → refl - N-ob (DistLatticeStr.1l (snd (CompOpenDistLattice X))) A _ = 1l + N-ob (DistLatticeStr.1l (snd (F-ob CompOpenDistLattice X))) A _ = 1l where instance _ = ZariskiLattice A .snd - N-hom (DistLatticeStr.1l (snd (CompOpenDistLattice X))) {x = A} {y = B} φ = funExt λ _ → path + N-hom (DistLatticeStr.1l (snd (F-ob CompOpenDistLattice X))) {x = A} {y = B} φ = funExt λ _ → path where instance _ = A .snd @@ -339,9 +340,9 @@ module _ {ℓ : Level} where path : D B 1r ≡ D B (φ .fst 1r) ∨l 0l path = cong (D B) (sym (φ .snd .pres1)) ∙ sym (∨lRid _) - N-ob ((snd (CompOpenDistLattice X) DistLatticeStr.∨l U) V) A x = 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 (CompOpenDistLattice X) DistLatticeStr.∨l U) V) {x = A} {y = B} φ = funExt path + N-hom ((snd (F-ob CompOpenDistLattice X) DistLatticeStr.∨l U) V) {x = A} {y = B} φ = funExt path where instance _ = ZariskiLattice A .snd @@ -354,9 +355,9 @@ module _ {ℓ : Level} where ≡⟨ sym (inducedZarLatHom φ .snd .pres∨l _ _) ⟩ 𝓛 .F-hom φ (U .N-ob A x ∨l V .N-ob A x) ∎ - N-ob ((snd (CompOpenDistLattice X) DistLatticeStr.∧l U) V) A x = 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 (CompOpenDistLattice X) DistLatticeStr.∧l U) V) {x = A} {y = B} φ = funExt path + N-hom ((snd (F-ob CompOpenDistLattice X) DistLatticeStr.∧l U) V) {x = A} {y = B} φ = funExt path where instance _ = ZariskiLattice A .snd @@ -369,7 +370,7 @@ module _ {ℓ : Level} where ≡⟨ sym (inducedZarLatHom φ .snd .pres∧l _ _) ⟩ 𝓛 .F-hom φ (U .N-ob A x ∧l V .N-ob A x) ∎ - DistLatticeStr.isDistLattice (snd (CompOpenDistLattice X)) = makeIsDistLattice∧lOver∨l + DistLatticeStr.isDistLattice (snd (F-ob CompOpenDistLattice X)) = makeIsDistLattice∧lOver∨l isSetNatTrans (λ _ _ _ → makeNatTransPath (funExt₂ (λ A _ → ZariskiLattice A .snd .DistLatticeStr.∨lAssoc _ _ _))) @@ -385,33 +386,25 @@ module _ {ℓ : Level} where (λ A _ → ZariskiLattice A .snd .DistLatticeStr.∧l-dist-∨l _ _ _ .fst))) -- (contravariant) action on morphisms - CompOpenDistLatticeHom : {X Y : ℤFunctor} (α : X ⇒ Y) - → DistLatticeHom (CompOpenDistLattice Y) (CompOpenDistLattice X) - fst (CompOpenDistLatticeHom α) = α ●ᵛ_ - pres0 (snd (CompOpenDistLatticeHom α)) = makeNatTransPath (funExt₂ λ _ _ → refl) - pres1 (snd (CompOpenDistLatticeHom α)) = makeNatTransPath (funExt₂ λ _ _ → refl) - pres∨l (snd (CompOpenDistLatticeHom α)) _ _ = makeNatTransPath (funExt₂ λ _ _ → refl) - pres∧l (snd (CompOpenDistLatticeHom α)) _ _ = makeNatTransPath (funExt₂ λ _ _ → refl) - - -- functoriality of this construction - CompOpenDistLatticeId : {X : ℤFunctor} → CompOpenDistLatticeHom (idTrans X) - ≡ idDistLatticeHom (CompOpenDistLattice X) - CompOpenDistLatticeId = LatticeHom≡f _ _ - (funExt λ _ → makeNatTransPath (funExt₂ λ _ _ → refl)) - - CompOpenDistLatticeSeq : {X Y Z : ℤFunctor} (α : X ⇒ Y) (β : Y ⇒ Z) - → CompOpenDistLatticeHom (α ●ᵛ β) - ≡ CompOpenDistLatticeHom α ∘dl CompOpenDistLatticeHom β - CompOpenDistLatticeSeq _ _ = LatticeHom≡f _ _ - (funExt λ _ → makeNatTransPath (funExt₂ λ _ _ → refl)) + 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 Join (CompOpenDistLattice X) - open JoinSemilattice (Lattice→JoinSemilattice (DistLattice→Lattice (CompOpenDistLattice X))) + open Join (CompOpenDistLattice .F-ob X) + open JoinSemilattice (Lattice→JoinSemilattice (DistLattice→Lattice (CompOpenDistLattice .F-ob X))) open PosetStr (IndPoset .snd) hiding (_≤_) - open LatticeTheory ⦃...⦄ -- ((DistLattice→Lattice (CompOpenDistLattice X))) - private instance _ = (CompOpenDistLattice X) .snd + open LatticeTheory ⦃...⦄ -- ((DistLattice→Lattice (CompOpenDistLattice .F-ob X))) + private instance _ = (CompOpenDistLattice .F-ob X) .snd record AffineCover : Type (ℓ-suc ℓ) where field @@ -425,7 +418,7 @@ module _ {ℓ : Level} where -- 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 X)) ^op + private COᵒᵖ = (DistLatticeCategory (CompOpenDistLattice .F-ob X)) ^op compOpenIncl : {U V : CompactOpen X} → V ≤ U → ⟦ V ⟧ᶜᵒ ⇒ ⟦ U ⟧ᶜᵒ N-ob (compOpenIncl {U = U} {V = V} V≤U) A (x , Vx≡D1) = x , path