From 7d4cdfa1f475faf2d592b5c5a65f2dce5962d526 Mon Sep 17 00:00:00 2001 From: mzeuner Date: Mon, 23 Aug 2021 19:44:28 +0200 Subject: [PATCH 1/6] 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 2/6] 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 c5b27fe21ec04ac6e4a4d08789b54f6cdd0869f5 Mon Sep 17 00:00:00 2001 From: mzeuner Date: Wed, 8 Nov 2023 16:03:27 +0100 Subject: [PATCH 3/6] copy old file --- .../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..06d430dd0b --- /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 𝓛 {A} = {!cong fst (inducedZarLatHomId (CommAlgebra→CommRing (indFPAlg A)))!} + F-seq 𝓛 = {!!} From 8ae6bf7fb5c5d5bcb67d6b8ca74f5b615ebfc763 Mon Sep 17 00:00:00 2001 From: mzeuner Date: Thu, 16 Nov 2023 16:31:56 +0100 Subject: [PATCH 4/6] everything small now --- Cubical/Categories/Instances/CommRings.agda | 2 +- .../Categories/Instances/FPAlgebrasSmall.agda | 188 ++++++++++++++++-- Cubical/Categories/Instances/ZFunctors.agda | 2 +- .../NaturalTransformation/Base.agda | 4 +- 4 files changed, 177 insertions(+), 19 deletions(-) diff --git a/Cubical/Categories/Instances/CommRings.agda b/Cubical/Categories/Instances/CommRings.agda index 4b9353cabe..b7802ea960 100644 --- a/Cubical/Categories/Instances/CommRings.agda +++ b/Cubical/Categories/Instances/CommRings.agda @@ -1,4 +1,4 @@ -{-# OPTIONS --safe #-} +{-# OPTIONS --safe --lossy-unification #-} module Cubical.Categories.Instances.CommRings where open import Cubical.Foundations.Prelude diff --git a/Cubical/Categories/Instances/FPAlgebrasSmall.agda b/Cubical/Categories/Instances/FPAlgebrasSmall.agda index 06d430dd0b..513df2846a 100644 --- a/Cubical/Categories/Instances/FPAlgebrasSmall.agda +++ b/Cubical/Categories/Instances/FPAlgebrasSmall.agda @@ -9,6 +9,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 @@ -21,6 +23,10 @@ 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.Semilattice +open import Cubical.Algebra.Lattice +open import Cubical.Algebra.DistLattice +open import Cubical.Algebra.DistLattice.BigOps open import Cubical.Algebra.ZariskiLattice.Base open import Cubical.Algebra.ZariskiLattice.UniversalProperty @@ -32,11 +38,13 @@ 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.DistLattices 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.Relation.Binary.Order.Poset open import Cubical.HITs.PropositionalTruncation as PT open import Cubical.HITs.SetQuotients as SQ @@ -78,26 +86,176 @@ module _ (R : CommRing ℓ) where isSetHom FPAlgebrasSmallCategory = isSetAlgebraHom _ _ + -- "parsimonious" presheaf categories + fpAlgFunctor = Functor FPAlgebrasSmallCategory (SET ℓ) + fpAlgFUNCTOR = FUNCTOR FPAlgebrasSmallCategory (SET ℓ) + -- yoneda in the notation of Demazure-Gabriel -- uses η-equality of Categories - Sp : Functor (FPAlgebrasSmallCategory ^op) (FUNCTOR FPAlgebrasSmallCategory (SET ℓ)) + Sp : Functor (FPAlgebrasSmallCategory ^op) fpAlgFUNCTOR Sp = YO {C = (FPAlgebrasSmallCategory ^op)} + open Iso open Functor + open NatTrans + open DistLatticeStr ⦃...⦄ + open CommRingStr ⦃...⦄ + open IsRingHom + open IsLatticeHom + open ZarLat + open ZarLatUniversalProp - -- 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 𝓛 = {!!} + private forget = ForgetfulCommAlgebra→CommRing R + open ZarLat + 𝓛 : fpAlgFunctor + F-ob 𝓛 A = ZL (forget .F-ob (indFPAlg A)) , SQ.squash/ + F-hom 𝓛 φ = inducedZarLatHom (forget .F-hom φ) .fst + F-id 𝓛 = cong (λ x → inducedZarLatHom x .fst) (forget .F-id) + ∙ cong fst (inducedZarLatHomId _) + F-seq 𝓛 _ _ = cong (λ x → inducedZarLatHom x .fst) (forget .F-seq _ _) + ∙ cong fst (inducedZarLatHomSeq _ _) + + CompactOpen : fpAlgFunctor → Type ℓ + CompactOpen X = X ⇒ 𝓛 + + isAffine : fpAlgFunctor → Type ℓ + isAffine X = ∃[ A ∈ SmallFPAlgebra ] (Sp .F-ob A) ≅ᶜ X + + -- the induced subfunctor + ⟦_⟧ᶜᵒ : {X : fpAlgFunctor} (U : CompactOpen X) → fpAlgFunctor + F-ob (⟦_⟧ᶜᵒ {X = X} U) A = (Σ[ x ∈ X .F-ob A .fst ] U .N-ob A x ≡ D _ 1r) + , isSetΣSndProp (X .F-ob A .snd) λ _ → squash/ _ _ + where instance _ = snd (forget .F-ob (indFPAlg A)) + F-hom (⟦_⟧ᶜᵒ {X = X} U) {x = A} {y = B} φ (x , Ux≡D1) = (X .F-hom φ x) , path + where + instance + _ = (forget .F-ob (indFPAlg A)) .snd + _ = (forget .F-ob (indFPAlg B)) .snd + open IsLatticeHom + path : U .N-ob B (X .F-hom φ x) ≡ D _ 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 _ 1r) ≡⟨ inducedZarLatHom (forget .F-hom φ) .snd .pres1 ⟩ + D _ 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 : fpAlgFunctor} (U : CompactOpen X) → Type ℓ + isAffineCompactOpen U = isAffine ⟦ U ⟧ᶜᵒ + + -- the dist. lattice of compact opens + CompOpenDistLattice : Functor fpAlgFUNCTOR (DistLatticesCategory {ℓ} ^op) + fst (F-ob CompOpenDistLattice X) = CompactOpen X + + -- lattice structure induce by internal lattice object 𝓛 + N-ob (DistLatticeStr.0l (snd (F-ob CompOpenDistLattice X))) A _ = 0l + where instance _ = ZariskiLattice (forget .F-ob (indFPAlg A)) .snd + N-hom (DistLatticeStr.0l (snd (F-ob CompOpenDistLattice X))) _ = funExt λ _ → refl + + N-ob (DistLatticeStr.1l (snd (F-ob CompOpenDistLattice X))) A _ = 1l + where instance _ = ZariskiLattice (forget .F-ob (indFPAlg A)) .snd + N-hom (DistLatticeStr.1l (snd (F-ob CompOpenDistLattice X))) {x = A} {y = B} φ = funExt λ _ → path + where + instance + _ = (forget .F-ob (indFPAlg A)) .snd + _ = (forget .F-ob (indFPAlg B)) .snd + _ = ZariskiLattice (forget .F-ob (indFPAlg B)) .snd + path : D _ 1r ≡ D _ (φ .fst 1r) ∨l 0l + path = cong (D (forget .F-ob (indFPAlg B))) (sym (forget .F-hom φ .snd .pres1)) + ∙ sym (∨lRid _) + + N-ob ((snd (F-ob CompOpenDistLattice X) DistLatticeStr.∨l U) V) A x = + U .N-ob A x ∨l V .N-ob A x + where instance _ = ZariskiLattice (forget .F-ob (indFPAlg A)) .snd + N-hom ((snd (F-ob CompOpenDistLattice X) DistLatticeStr.∨l U) V) {x = A} {y = B} φ = + funExt path + where + instance + _ = ZariskiLattice (forget .F-ob (indFPAlg A)) .snd + _ = ZariskiLattice (forget .F-ob (indFPAlg 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 (forget .F-hom φ) .snd .pres∨l _ _) ⟩ + 𝓛 .F-hom φ (U .N-ob A x ∨l V .N-ob A x) ∎ + + N-ob ((snd (F-ob CompOpenDistLattice X) DistLatticeStr.∧l U) V) A x = + U .N-ob A x ∧l V .N-ob A x + where instance _ = ZariskiLattice (forget .F-ob (indFPAlg A)) .snd + N-hom ((snd (F-ob CompOpenDistLattice X) DistLatticeStr.∧l U) V) {x = A} {y = B} φ = + funExt path + where + instance + _ = ZariskiLattice (forget .F-ob (indFPAlg A)) .snd + _ = ZariskiLattice (forget .F-ob (indFPAlg 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 (forget .F-hom φ) .snd .pres∧l _ _) ⟩ + 𝓛 .F-hom φ (U .N-ob A x ∧l V .N-ob A x) ∎ + + DistLatticeStr.isDistLattice (snd (F-ob CompOpenDistLattice X)) = + makeIsDistLattice∧lOver∨l + isSetNatTrans + (λ _ _ _ → makeNatTransPath (funExt₂ + (λ A _ → ZariskiLattice (forget .F-ob (indFPAlg A)) .snd + .DistLatticeStr.∨lAssoc _ _ _))) + (λ _ → makeNatTransPath (funExt₂ + (λ A _ → ZariskiLattice (forget .F-ob (indFPAlg A)) .snd + .DistLatticeStr.∨lRid _))) + (λ _ _ → makeNatTransPath (funExt₂ + (λ A _ → ZariskiLattice (forget .F-ob (indFPAlg A)) .snd + .DistLatticeStr.∨lComm _ _))) + (λ _ _ _ → makeNatTransPath (funExt₂ + (λ A _ → ZariskiLattice (forget .F-ob (indFPAlg A)) .snd + .DistLatticeStr.∧lAssoc _ _ _))) + (λ _ → makeNatTransPath (funExt₂ + (λ A _ → ZariskiLattice (forget .F-ob (indFPAlg A)) .snd + .DistLatticeStr.∧lRid _))) + (λ _ _ → makeNatTransPath (funExt₂ + (λ A _ → ZariskiLattice (forget .F-ob (indFPAlg A)) .snd + .DistLatticeStr.∧lComm _ _))) + (λ _ _ → makeNatTransPath (funExt₂ -- don't know why ∧lAbsorb∨l doesn't work + (λ A _ → ZariskiLattice (forget .F-ob (indFPAlg A)) .snd + .DistLatticeStr.absorb _ _ .snd))) + (λ _ _ _ → makeNatTransPath (funExt₂ -- same here + (λ A _ → ZariskiLattice (forget .F-ob (indFPAlg A)) .snd + .DistLatticeStr.∧l-dist-∨l _ _ _ .fst))) + + -- (contravariant) action on morphisms + fst (F-hom CompOpenDistLattice α) = α ●ᵛ_ + pres0 (snd (F-hom CompOpenDistLattice α)) = makeNatTransPath (funExt₂ λ _ _ → refl) + pres1 (snd (F-hom CompOpenDistLattice α)) = makeNatTransPath (funExt₂ λ _ _ → refl) + pres∨l (snd (F-hom CompOpenDistLattice α)) _ _ = makeNatTransPath (funExt₂ λ _ _ → refl) + pres∧l (snd (F-hom CompOpenDistLattice α)) _ _ = makeNatTransPath (funExt₂ λ _ _ → refl) + + -- functoriality + F-id CompOpenDistLattice = LatticeHom≡f _ _ + (funExt λ _ → makeNatTransPath (funExt₂ λ _ _ → refl)) + F-seq CompOpenDistLattice _ _ = LatticeHom≡f _ _ + (funExt λ _ → makeNatTransPath (funExt₂ λ _ _ → refl)) + + + module _ (X : fpAlgFunctor) where + open Join (CompOpenDistLattice .F-ob X) + private instance _ = (CompOpenDistLattice .F-ob X) .snd + + record AffineCover : Type ℓ where + field + n : ℕ + U : FinVec (CompactOpen X) n + covers : ⋁ U ≡ 1l -- TODO: equivalent to X ≡ ⟦ ⋁ U ⟧ᶜᵒ + isAffineU : ∀ i → isAffineCompactOpen (U i) + + hasAffineCover : Type ℓ + hasAffineCover = ∥ AffineCover ∥₁ + -- TODO: A fp-alg-functor is a scheme of finite presentation (over R) + -- if it is a Zariski sheaf and has an affine cover diff --git a/Cubical/Categories/Instances/ZFunctors.agda b/Cubical/Categories/Instances/ZFunctors.agda index 701f7c4020..28703572d9 100644 --- a/Cubical/Categories/Instances/ZFunctors.agda +++ b/Cubical/Categories/Instances/ZFunctors.agda @@ -403,7 +403,7 @@ module _ {ℓ : Level} where 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 .F-ob X))) + open LatticeTheory ⦃...⦄ private instance _ = (CompOpenDistLattice .F-ob X) .snd record AffineCover : Type (ℓ-suc ℓ) where diff --git a/Cubical/Categories/NaturalTransformation/Base.agda b/Cubical/Categories/NaturalTransformation/Base.agda index 93b9fb2bd8..7e44493e35 100644 --- a/Cubical/Categories/NaturalTransformation/Base.agda +++ b/Cubical/Categories/NaturalTransformation/Base.agda @@ -42,7 +42,7 @@ module _ {C : Category ℓC ℓC'} {D : Category ℓD ℓD'} where -- naturality condition N-hom : N-hom-Type F G N-ob - record NatIso (F G : Functor C D): Type (ℓ-max (ℓ-max ℓC ℓC') (ℓ-max ℓD ℓD')) where + record NatIso (F G : Functor C D): Type (ℓ-max (ℓ-max ℓC ℓC') ℓD') where field trans : NatTrans F G open NatTrans trans @@ -77,7 +77,7 @@ module _ {C : Category ℓC ℓC'} {D : Category ℓD ℓD'} where infix 9 _≅ᶜ_ -- c superscript to indicate that this is in the context of categories - _≅ᶜ_ : Functor C D → Functor C D → Type (ℓ-max (ℓ-max ℓC ℓC') (ℓ-max ℓD ℓD')) + _≅ᶜ_ : Functor C D → Functor C D → Type (ℓ-max (ℓ-max ℓC ℓC') ℓD') _≅ᶜ_ = NatIso -- component of a natural transformation From 3a9ecc9bb7882299f4f7e5ec40b4849f0e766142 Mon Sep 17 00:00:00 2001 From: mzeuner Date: Fri, 17 Nov 2023 17:32:43 +0100 Subject: [PATCH 5/6] functor over base ring --- .../Categories/Instances/FPAlgebrasSmall.agda | 439 ++++++++++-------- 1 file changed, 256 insertions(+), 183 deletions(-) diff --git a/Cubical/Categories/Instances/FPAlgebrasSmall.agda b/Cubical/Categories/Instances/FPAlgebrasSmall.agda index 513df2846a..3c32cdb17b 100644 --- a/Cubical/Categories/Instances/FPAlgebrasSmall.agda +++ b/Cubical/Categories/Instances/FPAlgebrasSmall.agda @@ -13,7 +13,7 @@ open import Cubical.Functions.FunExtEquiv open import Cubical.Data.Unit open import Cubical.Data.Sigma -open import Cubical.Data.Nat +open import Cubical.Data.Nat using (ℕ) open import Cubical.Data.FinData open import Cubical.Algebra.Ring @@ -32,9 +32,6 @@ 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 @@ -49,10 +46,6 @@ open import Cubical.Relation.Binary.Order.Poset 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 @@ -60,7 +53,19 @@ private module _ (R : CommRing ℓ) where - open Category + + open Iso + open Category hiding (_∘_) renaming (_⋆_ to _⋆c_) + open Functor + open NatTrans + open DistLatticeStr ⦃...⦄ + open CommRingStr ⦃...⦄ + open IsRingHom + open CommAlgebraHoms + open IsLatticeHom + open ZarLat + open ZarLatUniversalProp + -- type living in the same universe as the base ring R record SmallFPAlgebra : Type ℓ where @@ -79,183 +84,251 @@ module _ (R : CommRing ℓ) where Hom[_,_] FPAlgebrasSmallCategory A B = CommAlgebraHom (indFPAlg A) (indFPAlg B) id FPAlgebrasSmallCategory = idCommAlgebraHom _ - _⋆_ FPAlgebrasSmallCategory = compCommAlgebraHom _ _ _ + _⋆c_ FPAlgebrasSmallCategory = compCommAlgebraHom _ _ _ ⋆IdL FPAlgebrasSmallCategory = compIdCommAlgebraHom ⋆IdR FPAlgebrasSmallCategory = idCompCommAlgebraHom ⋆Assoc FPAlgebrasSmallCategory = compAssocCommAlgebraHom isSetHom FPAlgebrasSmallCategory = isSetAlgebraHom _ _ - -- "parsimonious" presheaf categories - fpAlgFunctor = Functor FPAlgebrasSmallCategory (SET ℓ) - fpAlgFUNCTOR = FUNCTOR FPAlgebrasSmallCategory (SET ℓ) - - -- yoneda in the notation of Demazure-Gabriel - -- uses η-equality of Categories - Sp : Functor (FPAlgebrasSmallCategory ^op) fpAlgFUNCTOR - Sp = YO {C = (FPAlgebrasSmallCategory ^op)} - - 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) - private forget = ForgetfulCommAlgebra→CommRing R - open ZarLat - 𝓛 : fpAlgFunctor - F-ob 𝓛 A = ZL (forget .F-ob (indFPAlg A)) , SQ.squash/ - F-hom 𝓛 φ = inducedZarLatHom (forget .F-hom φ) .fst - F-id 𝓛 = cong (λ x → inducedZarLatHom x .fst) (forget .F-id) - ∙ cong fst (inducedZarLatHomId _) - F-seq 𝓛 _ _ = cong (λ x → inducedZarLatHom x .fst) (forget .F-seq _ _) - ∙ cong fst (inducedZarLatHomSeq _ _) - - CompactOpen : fpAlgFunctor → Type ℓ - CompactOpen X = X ⇒ 𝓛 - - isAffine : fpAlgFunctor → Type ℓ - isAffine X = ∃[ A ∈ SmallFPAlgebra ] (Sp .F-ob A) ≅ᶜ X - - -- the induced subfunctor - ⟦_⟧ᶜᵒ : {X : fpAlgFunctor} (U : CompactOpen X) → fpAlgFunctor - F-ob (⟦_⟧ᶜᵒ {X = X} U) A = (Σ[ x ∈ X .F-ob A .fst ] U .N-ob A x ≡ D _ 1r) - , isSetΣSndProp (X .F-ob A .snd) λ _ → squash/ _ _ - where instance _ = snd (forget .F-ob (indFPAlg A)) - F-hom (⟦_⟧ᶜᵒ {X = X} U) {x = A} {y = B} φ (x , Ux≡D1) = (X .F-hom φ x) , path - where - instance - _ = (forget .F-ob (indFPAlg A)) .snd - _ = (forget .F-ob (indFPAlg B)) .snd - open IsLatticeHom - path : U .N-ob B (X .F-hom φ x) ≡ D _ 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 _ 1r) ≡⟨ inducedZarLatHom (forget .F-hom φ) .snd .pres1 ⟩ - D _ 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 : fpAlgFunctor} (U : CompactOpen X) → Type ℓ - isAffineCompactOpen U = isAffine ⟦ U ⟧ᶜᵒ - - -- the dist. lattice of compact opens - CompOpenDistLattice : Functor fpAlgFUNCTOR (DistLatticesCategory {ℓ} ^op) - fst (F-ob CompOpenDistLattice X) = CompactOpen X - - -- lattice structure induce by internal lattice object 𝓛 - N-ob (DistLatticeStr.0l (snd (F-ob CompOpenDistLattice X))) A _ = 0l - where instance _ = ZariskiLattice (forget .F-ob (indFPAlg A)) .snd - N-hom (DistLatticeStr.0l (snd (F-ob CompOpenDistLattice X))) _ = funExt λ _ → refl - - N-ob (DistLatticeStr.1l (snd (F-ob CompOpenDistLattice X))) A _ = 1l - where instance _ = ZariskiLattice (forget .F-ob (indFPAlg A)) .snd - N-hom (DistLatticeStr.1l (snd (F-ob CompOpenDistLattice X))) {x = A} {y = B} φ = funExt λ _ → path - where - instance - _ = (forget .F-ob (indFPAlg A)) .snd - _ = (forget .F-ob (indFPAlg B)) .snd - _ = ZariskiLattice (forget .F-ob (indFPAlg B)) .snd - path : D _ 1r ≡ D _ (φ .fst 1r) ∨l 0l - path = cong (D (forget .F-ob (indFPAlg B))) (sym (forget .F-hom φ .snd .pres1)) - ∙ sym (∨lRid _) - - N-ob ((snd (F-ob CompOpenDistLattice X) DistLatticeStr.∨l U) V) A x = - U .N-ob A x ∨l V .N-ob A x - where instance _ = ZariskiLattice (forget .F-ob (indFPAlg A)) .snd - N-hom ((snd (F-ob CompOpenDistLattice X) DistLatticeStr.∨l U) V) {x = A} {y = B} φ = - funExt path - where - instance - _ = ZariskiLattice (forget .F-ob (indFPAlg A)) .snd - _ = ZariskiLattice (forget .F-ob (indFPAlg 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 (forget .F-hom φ) .snd .pres∨l _ _) ⟩ - 𝓛 .F-hom φ (U .N-ob A x ∨l V .N-ob A x) ∎ - - N-ob ((snd (F-ob CompOpenDistLattice X) DistLatticeStr.∧l U) V) A x = - U .N-ob A x ∧l V .N-ob A x - where instance _ = ZariskiLattice (forget .F-ob (indFPAlg A)) .snd - N-hom ((snd (F-ob CompOpenDistLattice X) DistLatticeStr.∧l U) V) {x = A} {y = B} φ = - funExt path - where - instance - _ = ZariskiLattice (forget .F-ob (indFPAlg A)) .snd - _ = ZariskiLattice (forget .F-ob (indFPAlg 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 (forget .F-hom φ) .snd .pres∧l _ _) ⟩ - 𝓛 .F-hom φ (U .N-ob A x ∧l V .N-ob A x) ∎ - - DistLatticeStr.isDistLattice (snd (F-ob CompOpenDistLattice X)) = - makeIsDistLattice∧lOver∨l - isSetNatTrans - (λ _ _ _ → makeNatTransPath (funExt₂ - (λ A _ → ZariskiLattice (forget .F-ob (indFPAlg A)) .snd - .DistLatticeStr.∨lAssoc _ _ _))) - (λ _ → makeNatTransPath (funExt₂ - (λ A _ → ZariskiLattice (forget .F-ob (indFPAlg A)) .snd - .DistLatticeStr.∨lRid _))) - (λ _ _ → makeNatTransPath (funExt₂ - (λ A _ → ZariskiLattice (forget .F-ob (indFPAlg A)) .snd - .DistLatticeStr.∨lComm _ _))) - (λ _ _ _ → makeNatTransPath (funExt₂ - (λ A _ → ZariskiLattice (forget .F-ob (indFPAlg A)) .snd - .DistLatticeStr.∧lAssoc _ _ _))) - (λ _ → makeNatTransPath (funExt₂ - (λ A _ → ZariskiLattice (forget .F-ob (indFPAlg A)) .snd - .DistLatticeStr.∧lRid _))) - (λ _ _ → makeNatTransPath (funExt₂ - (λ A _ → ZariskiLattice (forget .F-ob (indFPAlg A)) .snd - .DistLatticeStr.∧lComm _ _))) - (λ _ _ → makeNatTransPath (funExt₂ -- don't know why ∧lAbsorb∨l doesn't work - (λ A _ → ZariskiLattice (forget .F-ob (indFPAlg A)) .snd - .DistLatticeStr.absorb _ _ .snd))) - (λ _ _ _ → makeNatTransPath (funExt₂ -- same here - (λ A _ → ZariskiLattice (forget .F-ob (indFPAlg A)) .snd - .DistLatticeStr.∧l-dist-∨l _ _ _ .fst))) - - -- (contravariant) action on morphisms - fst (F-hom CompOpenDistLattice α) = α ●ᵛ_ - pres0 (snd (F-hom CompOpenDistLattice α)) = makeNatTransPath (funExt₂ λ _ _ → refl) - pres1 (snd (F-hom CompOpenDistLattice α)) = makeNatTransPath (funExt₂ λ _ _ → refl) - pres∨l (snd (F-hom CompOpenDistLattice α)) _ _ = makeNatTransPath (funExt₂ λ _ _ → refl) - pres∧l (snd (F-hom CompOpenDistLattice α)) _ _ = makeNatTransPath (funExt₂ λ _ _ → refl) - - -- functoriality - F-id CompOpenDistLattice = LatticeHom≡f _ _ - (funExt λ _ → makeNatTransPath (funExt₂ λ _ _ → refl)) - F-seq CompOpenDistLattice _ _ = LatticeHom≡f _ _ - (funExt λ _ → makeNatTransPath (funExt₂ λ _ _ → refl)) - - - module _ (X : fpAlgFunctor) where - open Join (CompOpenDistLattice .F-ob X) - private instance _ = (CompOpenDistLattice .F-ob X) .snd - - record AffineCover : Type ℓ where - field - n : ℕ - U : FinVec (CompactOpen X) n - covers : ⋁ U ≡ 1l -- TODO: equivalent to X ≡ ⟦ ⋁ U ⟧ᶜᵒ - isAffineU : ∀ i → isAffineCompactOpen (U i) - - hasAffineCover : Type ℓ - hasAffineCover = ∥ AffineCover ∥₁ - -- TODO: A fp-alg-functor is a scheme of finite presentation (over R) - -- if it is a Zariski sheaf and has an affine cover + -- the name of this module will be justified once we have defined + -- Zariski sheaves on small f.p. algebras + module SchemesOfFinitePresentation where + + -- "parsimonious" presheaf categories + fpAlgFunctor = Functor FPAlgebrasSmallCategory (SET ℓ) + fpAlgFUNCTOR = FUNCTOR FPAlgebrasSmallCategory (SET ℓ) + + -- yoneda in the notation of Demazure-Gabriel + -- uses η-equality of Categories + Sp : Functor (FPAlgebrasSmallCategory ^op) fpAlgFUNCTOR + Sp = YO {C = (FPAlgebrasSmallCategory ^op)} + + -- the Zariski lattice (classifying compact open subobjects) + private forget = ForgetfulCommAlgebra→CommRing R + + 𝓛 : fpAlgFunctor + F-ob 𝓛 A = ZL (forget .F-ob (indFPAlg A)) , SQ.squash/ + F-hom 𝓛 φ = inducedZarLatHom (forget .F-hom φ) .fst + F-id 𝓛 = cong (λ x → inducedZarLatHom x .fst) (forget .F-id) + ∙ cong fst (inducedZarLatHomId _) + F-seq 𝓛 _ _ = cong (λ x → inducedZarLatHom x .fst) (forget .F-seq _ _) + ∙ cong fst (inducedZarLatHomSeq _ _) + + CompactOpen : fpAlgFunctor → Type ℓ + CompactOpen X = X ⇒ 𝓛 + + isAffine : fpAlgFunctor → Type ℓ + isAffine X = ∃[ A ∈ SmallFPAlgebra ] (Sp .F-ob A) ≅ᶜ X + + -- the induced subfunctor + ⟦_⟧ᶜᵒ : {X : fpAlgFunctor} (U : CompactOpen X) → fpAlgFunctor + F-ob (⟦_⟧ᶜᵒ {X = X} U) A = (Σ[ x ∈ X .F-ob A .fst ] U .N-ob A x ≡ D _ 1r) + , isSetΣSndProp (X .F-ob A .snd) λ _ → squash/ _ _ + where instance _ = snd (forget .F-ob (indFPAlg A)) + F-hom (⟦_⟧ᶜᵒ {X = X} U) {x = A} {y = B} φ (x , Ux≡D1) = (X .F-hom φ x) , path + where + instance + _ = (forget .F-ob (indFPAlg A)) .snd + _ = (forget .F-ob (indFPAlg B)) .snd + open IsLatticeHom + path : U .N-ob B (X .F-hom φ x) ≡ D _ 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 _ 1r) ≡⟨ inducedZarLatHom (forget .F-hom φ) .snd .pres1 ⟩ + D _ 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 : fpAlgFunctor} (U : CompactOpen X) → Type ℓ + isAffineCompactOpen U = isAffine ⟦ U ⟧ᶜᵒ + + -- the dist. lattice of compact opens + CompOpenDistLattice : Functor fpAlgFUNCTOR (DistLatticesCategory {ℓ} ^op) + fst (F-ob CompOpenDistLattice X) = CompactOpen X + + -- lattice structure induce by internal lattice object 𝓛 + N-ob (DistLatticeStr.0l (snd (F-ob CompOpenDistLattice X))) A _ = 0l + where instance _ = ZariskiLattice (forget .F-ob (indFPAlg A)) .snd + N-hom (DistLatticeStr.0l (snd (F-ob CompOpenDistLattice X))) _ = funExt λ _ → refl + + N-ob (DistLatticeStr.1l (snd (F-ob CompOpenDistLattice X))) A _ = 1l + where instance _ = ZariskiLattice (forget .F-ob (indFPAlg A)) .snd + N-hom (DistLatticeStr.1l (snd (F-ob CompOpenDistLattice X))) {x = A} {y = B} φ = funExt λ _ → path + where + instance + _ = (forget .F-ob (indFPAlg A)) .snd + _ = (forget .F-ob (indFPAlg B)) .snd + _ = ZariskiLattice (forget .F-ob (indFPAlg B)) .snd + path : D _ 1r ≡ D _ (φ .fst 1r) ∨l 0l + path = cong (D (forget .F-ob (indFPAlg B))) (sym (forget .F-hom φ .snd .pres1)) + ∙ sym (∨lRid _) + + N-ob ((snd (F-ob CompOpenDistLattice X) DistLatticeStr.∨l U) V) A x = + U .N-ob A x ∨l V .N-ob A x + where instance _ = ZariskiLattice (forget .F-ob (indFPAlg A)) .snd + N-hom ((snd (F-ob CompOpenDistLattice X) DistLatticeStr.∨l U) V) {x = A} {y = B} φ = + funExt path + where + instance + _ = ZariskiLattice (forget .F-ob (indFPAlg A)) .snd + _ = ZariskiLattice (forget .F-ob (indFPAlg 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 (forget .F-hom φ) .snd .pres∨l _ _) ⟩ + 𝓛 .F-hom φ (U .N-ob A x ∨l V .N-ob A x) ∎ + + N-ob ((snd (F-ob CompOpenDistLattice X) DistLatticeStr.∧l U) V) A x = + U .N-ob A x ∧l V .N-ob A x + where instance _ = ZariskiLattice (forget .F-ob (indFPAlg A)) .snd + N-hom ((snd (F-ob CompOpenDistLattice X) DistLatticeStr.∧l U) V) {x = A} {y = B} φ = + funExt path + where + instance + _ = ZariskiLattice (forget .F-ob (indFPAlg A)) .snd + _ = ZariskiLattice (forget .F-ob (indFPAlg 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 (forget .F-hom φ) .snd .pres∧l _ _) ⟩ + 𝓛 .F-hom φ (U .N-ob A x ∧l V .N-ob A x) ∎ + + DistLatticeStr.isDistLattice (snd (F-ob CompOpenDistLattice X)) = + makeIsDistLattice∧lOver∨l + isSetNatTrans + (λ _ _ _ → makeNatTransPath (funExt₂ + (λ A _ → ZariskiLattice (forget .F-ob (indFPAlg A)) .snd + .DistLatticeStr.∨lAssoc _ _ _))) + (λ _ → makeNatTransPath (funExt₂ + (λ A _ → ZariskiLattice (forget .F-ob (indFPAlg A)) .snd + .DistLatticeStr.∨lRid _))) + (λ _ _ → makeNatTransPath (funExt₂ + (λ A _ → ZariskiLattice (forget .F-ob (indFPAlg A)) .snd + .DistLatticeStr.∨lComm _ _))) + (λ _ _ _ → makeNatTransPath (funExt₂ + (λ A _ → ZariskiLattice (forget .F-ob (indFPAlg A)) .snd + .DistLatticeStr.∧lAssoc _ _ _))) + (λ _ → makeNatTransPath (funExt₂ + (λ A _ → ZariskiLattice (forget .F-ob (indFPAlg A)) .snd + .DistLatticeStr.∧lRid _))) + (λ _ _ → makeNatTransPath (funExt₂ + (λ A _ → ZariskiLattice (forget .F-ob (indFPAlg A)) .snd + .DistLatticeStr.∧lComm _ _))) + (λ _ _ → makeNatTransPath (funExt₂ -- don't know why ∧lAbsorb∨l doesn't work + (λ A _ → ZariskiLattice (forget .F-ob (indFPAlg A)) .snd + .DistLatticeStr.absorb _ _ .snd))) + (λ _ _ _ → makeNatTransPath (funExt₂ -- same here + (λ A _ → ZariskiLattice (forget .F-ob (indFPAlg A)) .snd + .DistLatticeStr.∧l-dist-∨l _ _ _ .fst))) + + -- (contravariant) action on morphisms + fst (F-hom CompOpenDistLattice α) = α ●ᵛ_ + pres0 (snd (F-hom CompOpenDistLattice α)) = makeNatTransPath (funExt₂ λ _ _ → refl) + pres1 (snd (F-hom CompOpenDistLattice α)) = makeNatTransPath (funExt₂ λ _ _ → refl) + pres∨l (snd (F-hom CompOpenDistLattice α)) _ _ = makeNatTransPath (funExt₂ λ _ _ → refl) + pres∧l (snd (F-hom CompOpenDistLattice α)) _ _ = makeNatTransPath (funExt₂ λ _ _ → refl) + + -- functoriality + F-id CompOpenDistLattice = LatticeHom≡f _ _ + (funExt λ _ → makeNatTransPath (funExt₂ λ _ _ → refl)) + F-seq CompOpenDistLattice _ _ = LatticeHom≡f _ _ + (funExt λ _ → makeNatTransPath (funExt₂ λ _ _ → refl)) + + -- the above is actually a functor into dist. lattices over 𝓛 R + open import Cubical.Categories.Constructions.Slice + (DistLatticesCategory {ℓ} ^op) (ZariskiLattice R) + renaming (SliceCat to DistLatticeᵒᵖ/𝓛R) + open SliceOb + open SliceHom + open IsZarMap + private + d : (X : fpAlgFunctor) → fst R → CompactOpen X + N-ob (d X r) A _ = D _ (r ⋆ 1a) + where open CommAlgebraStr (indFPAlg A .snd) + N-hom (d X r) {A} {B} φ = funExt (λ _ → sym path) + where + open IsAlgebraHom + open CommAlgebraStr ⦃...⦄ using (_⋆_ ; 1a) + instance + _ = indFPAlg A .snd + _ = indFPAlg B .snd + _ = ZariskiLattice (forget .F-ob (indFPAlg B)) .snd + path : D _ (φ .fst (r ⋆ 1a)) ∨l 0l ≡ D _ (r ⋆ 1a) + path = D _ (φ .fst (r ⋆ 1a)) ∨l 0l ≡⟨ ∨lRid _ ⟩ + D _ (φ .fst (r ⋆ 1a)) ≡⟨ cong (D _) (φ .snd .pres⋆ _ _) ⟩ + D _ (r ⋆ φ .fst 1a) ≡⟨ cong (λ x → D _ (r ⋆ x)) (φ .snd .pres1) ⟩ + D _ (r ⋆ 1a) ∎ + + dIsZarMap : ∀ (X : fpAlgFunctor) → IsZarMap R (F-ob CompOpenDistLattice X) (d X) + pres0 (dIsZarMap X) = makeNatTransPath (funExt₂ (λ A _ → + let open AlgebraTheory (CommRing→Ring R) (CommAlgebra→Algebra (indFPAlg A)) + in cong (D _) (⋆AnnihilL _) ∙ isZarMapD _ .pres0)) + pres1 (dIsZarMap X) = makeNatTransPath (funExt₂ (λ A _ → + cong (D _) (CommAlgebraStr.⋆IdL (indFPAlg A .snd) _) ∙ isZarMapD _ .pres1)) + ·≡∧ (dIsZarMap X) r s = makeNatTransPath (funExt₂ (λ A _ → + let open AlgebraTheory (CommRing→Ring R) (CommAlgebra→Algebra (indFPAlg A)) + open CommAlgebraStr ⦃...⦄ using (_⋆_ ; 1a) renaming (_·_ to _·a_ ; ·IdL to ·aIdL) + instance _ = indFPAlg A .snd + _ = R .snd + _ = ZariskiLattice (forget .F-ob (indFPAlg A)) .snd + in D _((r · s) ⋆ 1a) ≡⟨ cong (λ x → D _ ((r · s) ⋆ x)) (sym (·aIdL 1a)) ⟩ + D _((r · s) ⋆ (1a ·a 1a)) ≡⟨ cong (D _) (⋆Dist· _ _ _ _) ⟩ + D _((r ⋆ 1a) ·a (s ⋆ 1a)) ≡⟨ isZarMapD _ .·≡∧ _ _ ⟩ + D _(r ⋆ 1a) ∧l D _ (s ⋆ 1a) ∎)) + +≤∨ (dIsZarMap X) r s = makeNatTransPath (funExt₂ (λ A _ → + let open CommAlgebraStr ⦃...⦄ using (_⋆_ ; 1a ; ⋆DistL+) + open JoinSemilattice (Lattice→JoinSemilattice (DistLattice→Lattice + (ZariskiLattice (forget .F-ob (indFPAlg A))))) + instance _ = indFPAlg A .snd + _ = ZariskiLattice (forget .F-ob (indFPAlg A)) .snd + in subst (_≤ D _(r ⋆ 1a) ∨l D _ (s ⋆ 1a)) (cong (D _) (sym (⋆DistL+ _ _ _))) + (isZarMapD _ .+≤∨ _ _))) + + + uniqueHom𝓛R→CompOpen : (X : fpAlgFunctor) + → ∃![ χ ∈ DistLatticeHom (ZariskiLattice R) + (F-ob CompOpenDistLattice X) ] + χ .fst ∘ D R ≡ d X + uniqueHom𝓛R→CompOpen X = ZLHasUniversalProp R (F-ob CompOpenDistLattice X) + (d X) (dIsZarMap X) + + CompOpenDistLatticeOver : Functor fpAlgFUNCTOR DistLatticeᵒᵖ/𝓛R + S-ob (F-ob CompOpenDistLatticeOver X) = CompOpenDistLattice .F-ob X + + -- the induced morphism 𝓛 R → CompactOpen X + S-arr (F-ob CompOpenDistLatticeOver X) = uniqueHom𝓛R→CompOpen X .fst .fst + S-hom (F-hom CompOpenDistLatticeOver α) = CompOpenDistLattice .F-hom α + S-comm (F-hom CompOpenDistLatticeOver {X} {Y} α) = + sym (cong fst (uniqueHom𝓛R→CompOpen X .snd (χ' , χ'Path))) + where + χ' = CompOpenDistLattice .F-hom α ∘dl uniqueHom𝓛R→CompOpen Y .fst .fst + χ'Path : χ' .fst ∘ D R ≡ d X + χ'Path = cong (CompOpenDistLattice .F-hom α .fst ∘_) + (uniqueHom𝓛R→CompOpen Y .fst .snd) + ∙ funExt (λ r → makeNatTransPath (funExt₂ (λ _ _ → refl))) + F-id CompOpenDistLatticeOver = SliceHom-≡-intro' (CompOpenDistLattice .F-id) + F-seq CompOpenDistLatticeOver _ _ = SliceHom-≡-intro' (CompOpenDistLattice .F-seq _ _) + + + module _ (X : fpAlgFunctor) where + open Join (CompOpenDistLattice .F-ob X) + private instance _ = (CompOpenDistLattice .F-ob X) .snd + + record AffineCover : Type ℓ where + field + n : ℕ + U : FinVec (CompactOpen X) n + covers : ⋁ U ≡ 1l -- TODO: equivalent to X ≡ ⟦ ⋁ U ⟧ᶜᵒ + isAffineU : ∀ i → isAffineCompactOpen (U i) + + hasAffineCover : Type ℓ + hasAffineCover = ∥ AffineCover ∥₁ + -- TODO: A fp-alg-functor is a scheme of finite presentation (over R) + -- if it is a Zariski sheaf and has an affine cover From 517526139bb5717730a87fe1fd74d6f9b5f4ccca Mon Sep 17 00:00:00 2001 From: mzeuner Date: Mon, 20 Nov 2023 14:29:23 +0100 Subject: [PATCH 6/6] fix levels --- Cubical/Categories/Presheaf/Representable.agda | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Cubical/Categories/Presheaf/Representable.agda b/Cubical/Categories/Presheaf/Representable.agda index 42aa2fdb7c..582dfe2bb8 100644 --- a/Cubical/Categories/Presheaf/Representable.agda +++ b/Cubical/Categories/Presheaf/Representable.agda @@ -56,11 +56,11 @@ open isIsoC -- | Lifts don't appear in practice because we usually use universal -- | elements instead module _ {ℓo}{ℓh}{ℓp} (C : Category ℓo ℓh) (P : Presheaf C ℓp) where - Representation : Type (ℓ-max (ℓ-max ℓo (ℓ-suc ℓh)) (ℓ-suc ℓp)) + Representation : Type (ℓ-max (ℓ-max ℓo ℓh) ℓp) Representation = Σ[ A ∈ C .ob ] PshIso C (C [-, A ]) P - Representable : Type (ℓ-max (ℓ-max ℓo (ℓ-suc ℓh)) (ℓ-suc ℓp)) + Representable : Type (ℓ-max (ℓ-max ℓo ℓh) ℓp) Representable = ∥ Representation ∥₁ Elements = ∫ᴾ_ {C = C} P