From 9dd7c6ad2ebf8744e927c0c51e8017438f4de635 Mon Sep 17 00:00:00 2001
From: Matthias Hutzler <matthias-hutzler@posteo.net>
Date: Mon, 27 Nov 2023 16:45:51 +0100
Subject: [PATCH 01/37] (wip) for Zariski coverage on CommRing
(with Max Zeuner)
---
Cubical/Algebra/CommRing/Localisation/InvertingElements.agda | 4 ++++
1 file changed, 4 insertions(+)
diff --git a/Cubical/Algebra/CommRing/Localisation/InvertingElements.agda b/Cubical/Algebra/CommRing/Localisation/InvertingElements.agda
index 1a10d2e56b..bf04d7a1c1 100644
--- a/Cubical/Algebra/CommRing/Localisation/InvertingElements.agda
+++ b/Cubical/Algebra/CommRing/Localisation/InvertingElements.agda
@@ -80,6 +80,10 @@ module InvertingElementsBase (R' : CommRing ℓ) where
R[1/_] : R → Type ℓ
R[1/ f ] = Loc.S⁻¹R R' [ f ⁿ|n≥0] (powersFormMultClosedSubset f)
+ -- TODO: Provide a more specialized universal property.
+ -- (Just ask f to become invertible, not all its powers.)
+ module UniversalProp (f : R) = S⁻¹RUniversalProp R' [ f ⁿ|n≥0] (powersFormMultClosedSubset f)
+
-- a quick fact
isContrR[1/0] : isContr R[1/ 0r ]
fst isContrR[1/0] = [ 1r , 0r , ∣ 1 , sym (·IdR 0r) ∣₁ ] -- everything is equal to 1/0
From 5aa46d8f14a11d396d4379c4c3dff9b41b7f0ed8 Mon Sep 17 00:00:00 2001
From: mzeuner <max@zeuner.net>
Date: Thu, 30 Nov 2023 17:05:09 +0100
Subject: [PATCH 02/37] pullback stability
---
Cubical/Algebra/CommRing/Localisation/InvertingElements.agda | 4 ----
1 file changed, 4 deletions(-)
diff --git a/Cubical/Algebra/CommRing/Localisation/InvertingElements.agda b/Cubical/Algebra/CommRing/Localisation/InvertingElements.agda
index bf04d7a1c1..1a10d2e56b 100644
--- a/Cubical/Algebra/CommRing/Localisation/InvertingElements.agda
+++ b/Cubical/Algebra/CommRing/Localisation/InvertingElements.agda
@@ -80,10 +80,6 @@ module InvertingElementsBase (R' : CommRing ℓ) where
R[1/_] : R → Type ℓ
R[1/ f ] = Loc.S⁻¹R R' [ f ⁿ|n≥0] (powersFormMultClosedSubset f)
- -- TODO: Provide a more specialized universal property.
- -- (Just ask f to become invertible, not all its powers.)
- module UniversalProp (f : R) = S⁻¹RUniversalProp R' [ f ⁿ|n≥0] (powersFormMultClosedSubset f)
-
-- a quick fact
isContrR[1/0] : isContr R[1/ 0r ]
fst isContrR[1/0] = [ 1r , 0r , ∣ 1 , sym (·IdR 0r) ∣₁ ] -- everything is equal to 1/0
From 5e0cb3519408d8441f6fb2c310cf4d404065dcef Mon Sep 17 00:00:00 2001
From: mzeuner <max@zeuner.net>
Date: Mon, 4 Dec 2023 16:50:51 +0100
Subject: [PATCH 03/37] only zero case left
---
Cubical/Categories/Site/Instances/ZariskiCommRing.agda | 3 ++-
1 file changed, 2 insertions(+), 1 deletion(-)
diff --git a/Cubical/Categories/Site/Instances/ZariskiCommRing.agda b/Cubical/Categories/Site/Instances/ZariskiCommRing.agda
index 9d86d30c23..84aab79823 100644
--- a/Cubical/Categories/Site/Instances/ZariskiCommRing.agda
+++ b/Cubical/Categories/Site/Instances/ZariskiCommRing.agda
@@ -8,9 +8,10 @@ open import Cubical.Foundations.Function
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Structure
-open import Cubical.Data.Nat using (ℕ)
+open import Cubical.Data.Nat using (ℕ ; zero ; suc)
open import Cubical.Data.Sigma
open import Cubical.Data.FinData
+open import Cubical.Data.FinData.Order renaming (_<'Fin_ to _<_)
open import Cubical.Algebra.Ring
open import Cubical.Algebra.Ring.BigOps
From 131c4578ede63ad93b3bd6d8612e6e13a28dc4c7 Mon Sep 17 00:00:00 2001
From: mzeuner <max@zeuner.net>
Date: Mon, 4 Dec 2023 22:32:28 +0100
Subject: [PATCH 04/37] finish zero case
---
Cubical/Categories/Site/Instances/ZariskiCommRing.agda | 1 +
1 file changed, 1 insertion(+)
diff --git a/Cubical/Categories/Site/Instances/ZariskiCommRing.agda b/Cubical/Categories/Site/Instances/ZariskiCommRing.agda
index 84aab79823..ecdce68dce 100644
--- a/Cubical/Categories/Site/Instances/ZariskiCommRing.agda
+++ b/Cubical/Categories/Site/Instances/ZariskiCommRing.agda
@@ -21,6 +21,7 @@ open import Cubical.Algebra.CommRing.Ideal
open import Cubical.Algebra.CommRing.FGIdeal
open import Cubical.Categories.Category
+open import Cubical.Categories.Limits.Terminal
open import Cubical.Categories.Instances.CommRings
open import Cubical.Categories.Site.Coverage
open import Cubical.Categories.Site.Sheaf
From 036a3238f950c6d0e02f58c4236c41c215ff2dd3 Mon Sep 17 00:00:00 2001
From: mzeuner <max@zeuner.net>
Date: Thu, 18 Jan 2024 09:51:44 +0100
Subject: [PATCH 05/37] def standard affine open
---
Cubical/Algebra/Lattice/Properties.agda | 3 ++
.../ZariskiLattice/UniversalProperty.agda | 10 ++++-
Cubical/Categories/Instances/ZFunctors.agda | 43 +++++++++++++++++++
3 files changed, 55 insertions(+), 1 deletion(-)
diff --git a/Cubical/Algebra/Lattice/Properties.agda b/Cubical/Algebra/Lattice/Properties.agda
index c1622d2fc7..1a7b4ab901 100644
--- a/Cubical/Algebra/Lattice/Properties.agda
+++ b/Cubical/Algebra/Lattice/Properties.agda
@@ -81,6 +81,9 @@ module Order (L' : Lattice ℓ) where
∧≤LCancelJoin : ∀ x y → x ∧l y ≤j y
∧≤LCancelJoin x y = ≤m→≤j _ _ (∧≤LCancel x y)
+ ∧≤RCancelJoin : ∀ x y → x ∧l y ≤j x
+ ∧≤RCancelJoin x y = ≤m→≤j _ _ (∧≤RCancel x y)
+
module _ {L : Lattice ℓ} {M : Lattice ℓ'} (φ ψ : LatticeHom L M) where
open LatticeStr ⦃...⦄
diff --git a/Cubical/Algebra/ZariskiLattice/UniversalProperty.agda b/Cubical/Algebra/ZariskiLattice/UniversalProperty.agda
index 3983ab834e..1ba6f964b7 100644
--- a/Cubical/Algebra/ZariskiLattice/UniversalProperty.agda
+++ b/Cubical/Algebra/ZariskiLattice/UniversalProperty.agda
@@ -9,7 +9,7 @@ open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Univalence
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Transport
-open import Cubical.Foundations.Powerset using (ℙ ; ⊆-refl-consequence)
+open import Cubical.Foundations.Powerset using (ℙ ; ⊆-refl-consequence) renaming (_∈_ to _∈ₚ_)
import Cubical.Data.Empty as ⊥
open import Cubical.Data.Bool hiding (_≤_)
@@ -57,6 +57,7 @@ module _ (R' : CommRing ℓ) (L' : DistLattice ℓ') where
open Sum (CommRing→Ring R')
open CommRingTheory R'
open Exponentiation R'
+ open Units R'
open DistLatticeStr (L' .snd) renaming (is-set to isSetL)
open Join L'
@@ -89,11 +90,18 @@ module _ (R' : CommRing ℓ) (L' : DistLattice ℓ') where
d·LCancel : ∀ x y → d (x · y) ≤ d y
d·LCancel x y = subst (λ a → a ≤ d y) (sym (·≡∧ x y)) (∧≤LCancelJoin _ _)
+ d·RCancel : ∀ x y → d (x · y) ≤ d x
+ d·RCancel x y = subst (λ a → a ≤ d x) (sym (·≡∧ x y)) (∧≤RCancelJoin _ _)
+
linearCombination≤LCancel : {n : ℕ} (α β : FinVec R n)
→ d (linearCombination R' α β) ≤ ⋁ (d ∘ β)
linearCombination≤LCancel α β = is-trans _ _ _ (∑≤⋁ (λ i → α i · β i))
(≤-⋁Ext _ _ λ i → d·LCancel (α i) (β i))
+ ZarMapUnit : ∀ x → x ∈ₚ Rˣ → d x ≡ 1l
+ ZarMapUnit x (x⁻¹ , xx⁻¹≡1) = is-antisym _ _ (1lRightAnnihilates∨l _)
+ (subst (_≤ d x) (cong d xx⁻¹≡1 ∙ pres1) (d·RCancel _ _))
+
ZarMapIdem : ∀ (n : ℕ) (x : R) → d (x ^ (suc n)) ≡ d x
ZarMapIdem zero x = ·≡∧ _ _ ∙∙ cong (d x ∧l_) pres1 ∙∙ ∧lRid _
ZarMapIdem (suc n) x = ·≡∧ _ _ ∙∙ cong (d x ∧l_) (ZarMapIdem n x) ∙∙ ∧lIdem _
diff --git a/Cubical/Categories/Instances/ZFunctors.agda b/Cubical/Categories/Instances/ZFunctors.agda
index a1a669082e..e8ca3ed2bd 100644
--- a/Cubical/Categories/Instances/ZFunctors.agda
+++ b/Cubical/Categories/Instances/ZFunctors.agda
@@ -23,6 +23,7 @@ open import Cubical.Data.FinData
open import Cubical.Algebra.Ring
open import Cubical.Algebra.CommRing
+open import Cubical.Algebra.CommRing.Localisation
open import Cubical.Algebra.Semilattice
open import Cubical.Algebra.Lattice
open import Cubical.Algebra.DistLattice
@@ -496,3 +497,45 @@ module _ {ℓ : Level} where
isQcQsSchemeAffine : ∀ (A : CommRing ℓ) → isQcQsScheme (Sp .F-ob A)
fst (isQcQsSchemeAffine A) = isSubcanonicalZariskiCoverage A
snd (isQcQsSchemeAffine A) = ∣ singlAffineCover A ∣₁
+
+-- standard affine opens
+-- TODO: separate file?
+module _ {ℓ : Level} (R : CommRing ℓ) (f : R .fst) where
+
+ open Iso
+ open Functor
+ open NatTrans
+ open NatIso
+ open DistLatticeStr ⦃...⦄
+ open CommRingStr ⦃...⦄
+ open IsRingHom
+ open RingHoms
+ open IsLatticeHom
+ open ZarLat
+
+ open InvertingElementsBase R
+ open UniversalProp f
+
+ module ZL = ZarLatUniversalProp
+
+ D : CompactOpen (Sp ⟅ R ⟆)
+ D = yonedaᴾ ZarLatFun R .inv (ZL.D R f)
+
+ SpR[1/f]≅⟦Df⟧ : NatIso (Sp .F-ob R[1/ f ]AsCommRing) ⟦ D ⟧ᶜᵒ
+ N-ob (trans SpR[1/f]≅⟦Df⟧) B φ = (φ ∘r /1AsCommRingHom) , ∨lRid _ ∙ path
+ where
+ instance
+ _ = B .snd
+ _ = ZariskiLattice B .snd
+
+ φ[f/1]Unit : φ .fst (f /1) ∈ B ˣ
+ φ[f/1]Unit = {!!}
+
+ path : ZL.D B (φ .fst (f /1)) ≡ 1l
+ path = IsZarMap.ZarMapUnit (ZL.isZarMapD B) _ φ[f/1]Unit
+
+ N-hom (trans SpR[1/f]≅⟦Df⟧) = {!!}
+ nIso SpR[1/f]≅⟦Df⟧ = {!!}
+
+ isAffineD : isAffineCompactOpen D
+ isAffineD = ∣ R[1/ f ]AsCommRing , SpR[1/f]≅⟦Df⟧ ∣₁
From 484231b049926a7e81c2e52c8c6681432c7293c6 Mon Sep 17 00:00:00 2001
From: mzeuner <max@zeuner.net>
Date: Fri, 19 Jan 2024 16:54:19 +0100
Subject: [PATCH 06/37] finish standard affine opens
---
.../Algebra/ZariskiLattice/Properties.agda | 109 ++++++++++++++++++
Cubical/Categories/Instances/ZFunctors.agda | 28 ++++-
2 files changed, 132 insertions(+), 5 deletions(-)
create mode 100644 Cubical/Algebra/ZariskiLattice/Properties.agda
diff --git a/Cubical/Algebra/ZariskiLattice/Properties.agda b/Cubical/Algebra/ZariskiLattice/Properties.agda
new file mode 100644
index 0000000000..1ad613d427
--- /dev/null
+++ b/Cubical/Algebra/ZariskiLattice/Properties.agda
@@ -0,0 +1,109 @@
+{-# OPTIONS --safe #-}
+module Cubical.Algebra.ZariskiLattice.Properties where
+
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Function
+open import Cubical.Foundations.Equiv
+open import Cubical.Foundations.Isomorphism
+open import Cubical.Foundations.Univalence
+open import Cubical.Foundations.HLevels
+open import Cubical.Foundations.Transport
+open import Cubical.Foundations.Powerset using (ℙ ; ⊆-refl-consequence)
+ renaming (_∈_ to _∈ₚ_ ; ∈-isProp to ∈ₚ-isProp)
+
+import Cubical.Data.Empty as ⊥
+open import Cubical.Data.Bool hiding (_≤_)
+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.Sigma.Base
+open import Cubical.Data.Sigma.Properties
+open import Cubical.Data.FinData
+open import Cubical.Data.Unit
+open import Cubical.Relation.Nullary
+open import Cubical.Relation.Binary
+open import Cubical.Relation.Binary.Order.Poset
+
+open import Cubical.Algebra.Ring
+open import Cubical.Algebra.Ring.Properties
+open import Cubical.Algebra.Ring.BigOps
+open import Cubical.Algebra.CommRing
+open import Cubical.Algebra.CommRing.BinomialThm
+open import Cubical.Algebra.CommRing.Ideal
+open import Cubical.Algebra.CommRing.FGIdeal
+open import Cubical.Algebra.CommRing.RadicalIdeal
+open import Cubical.Tactics.CommRingSolver.Reflection
+open import Cubical.Algebra.Semilattice
+open import Cubical.Algebra.Lattice
+open import Cubical.Algebra.DistLattice
+open import Cubical.Algebra.DistLattice.Basis
+open import Cubical.Algebra.DistLattice.BigOps
+open import Cubical.Algebra.Matrix
+
+open import Cubical.Algebra.ZariskiLattice.Base
+open import Cubical.Algebra.ZariskiLattice.UniversalProperty
+
+open import Cubical.HITs.SetQuotients as SQ
+open import Cubical.HITs.PropositionalTruncation as PT
+
+
+private variable ℓ : Level
+
+module _ (R : CommRing ℓ) where
+ open Iso
+ open CommRingStr ⦃...⦄
+ open DistLatticeStr ⦃...⦄
+ open PosetStr ⦃...⦄
+
+ open RingTheory (CommRing→Ring R)
+ open Sum (CommRing→Ring R)
+ open CommRingTheory R
+ open Exponentiation R
+ open BinomialThm R
+ open CommIdeal R
+ open RadicalIdeal R
+ open isCommIdeal
+ open ProdFin R
+
+ open ZarLat R
+ open ZarLatUniversalProp R
+ open IsZarMap isZarMapD
+
+ open JoinSemilattice (Lattice→JoinSemilattice (DistLattice→Lattice ZariskiLattice))
+ using (IndPoset)
+
+ private
+ instance
+ _ = R .snd
+ _ = ZariskiLattice .snd
+ _ = IndPoset .snd
+
+ ⟨_⟩ : {n : ℕ} → FinVec (fst R) n → CommIdeal
+ ⟨ V ⟩ = ⟨ V ⟩[ R ]
+
+ unitLemmaZarLat : ∀ f → D f ≡ D 1r → f ∈ₚ R ˣ
+ unitLemmaZarLat f Df≡D1 = PT.rec (∈ₚ-isProp (R ˣ) f) radicalHelper 1∈√⟨f⟩
+ where
+ D1≤Df : D 1r ≤ D f
+ D1≤Df = subst (_≤ D f) Df≡D1 (is-refl _)
+
+ 1∈√⟨f⟩ : 1r ∈ √ ⟨ replicateFinVec 1 f ⟩
+ 1∈√⟨f⟩ = isEquivRel→effectiveIso ∼PropValued ∼EquivRel _ _ .fun D1≤Df .fst zero
+
+ radicalHelper : Σ[ n ∈ ℕ ] 1r ^ n ∈ ⟨ replicateFinVec 1 f ⟩ → f ∈ₚ R ˣ
+ radicalHelper (n , 1ⁿ∈⟨f⟩) = PT.rec (∈ₚ-isProp (R ˣ) f) fgHelper 1ⁿ∈⟨f⟩
+ where
+ fgHelper : Σ[ α ∈ FinVec (fst R) 1 ] 1r ^ n ≡ linearCombination R α (replicateFinVec 1 f)
+ → f ∈ₚ R ˣ
+ fgHelper (α , 1ⁿ≡α₀f+0) = α zero , path
+ where
+ useSolver : ∀ f α₀ → f · α₀ ≡ α₀ · f + 0r
+ useSolver = solve R
+
+ path : f · α zero ≡ 1r
+ path = f · α zero ≡⟨ useSolver _ _ ⟩
+ α zero · f + 0r ≡⟨ sym 1ⁿ≡α₀f+0 ⟩
+ 1r ^ n ≡⟨ 1ⁿ≡1 n ⟩
+ 1r ∎
diff --git a/Cubical/Categories/Instances/ZFunctors.agda b/Cubical/Categories/Instances/ZFunctors.agda
index e8ca3ed2bd..cff41e75c8 100644
--- a/Cubical/Categories/Instances/ZFunctors.agda
+++ b/Cubical/Categories/Instances/ZFunctors.agda
@@ -30,6 +30,7 @@ open import Cubical.Algebra.DistLattice
open import Cubical.Algebra.DistLattice.BigOps
open import Cubical.Algebra.ZariskiLattice.Base
open import Cubical.Algebra.ZariskiLattice.UniversalProperty
+open import Cubical.Algebra.ZariskiLattice.Properties
open import Cubical.Categories.Category
open import Cubical.Categories.Functor
@@ -506,6 +507,7 @@ module _ {ℓ : Level} (R : CommRing ℓ) (f : R .fst) where
open Functor
open NatTrans
open NatIso
+ open isIso
open DistLatticeStr ⦃...⦄
open CommRingStr ⦃...⦄
open IsRingHom
@@ -518,24 +520,40 @@ module _ {ℓ : Level} (R : CommRing ℓ) (f : R .fst) where
module ZL = ZarLatUniversalProp
+ private
+ instance
+ _ = R .snd
+
D : CompactOpen (Sp ⟅ R ⟆)
D = yonedaᴾ ZarLatFun R .inv (ZL.D R f)
SpR[1/f]≅⟦Df⟧ : NatIso (Sp .F-ob R[1/ f ]AsCommRing) ⟦ D ⟧ᶜᵒ
N-ob (trans SpR[1/f]≅⟦Df⟧) B φ = (φ ∘r /1AsCommRingHom) , ∨lRid _ ∙ path
where
+ open CommRingHomTheory φ
+ open IsZarMap (ZL.isZarMapD B)
instance
_ = B .snd
_ = ZariskiLattice B .snd
- φ[f/1]Unit : φ .fst (f /1) ∈ B ˣ
- φ[f/1]Unit = {!!}
+ isUnitφ[f/1] : φ .fst (f /1) ∈ B ˣ
+ isUnitφ[f/1] = RingHomRespInv (f /1) ⦃ S/1⊆S⁻¹Rˣ f ∣ 1 , sym (·IdR f) ∣₁ ⦄
path : ZL.D B (φ .fst (f /1)) ≡ 1l
- path = IsZarMap.ZarMapUnit (ZL.isZarMapD B) _ φ[f/1]Unit
+ path = ZarMapUnit _ isUnitφ[f/1]
- N-hom (trans SpR[1/f]≅⟦Df⟧) = {!!}
- nIso SpR[1/f]≅⟦Df⟧ = {!!}
+ N-hom (trans SpR[1/f]≅⟦Df⟧) _ = funExt λ _ → Σ≡Prop (λ _ → squash/ _ _) (RingHom≡ refl)
+
+ inv (nIso SpR[1/f]≅⟦Df⟧ B) (φ , Dφf≡D1) = invElemUniversalProp B φ isUnitφf .fst .fst
+ where
+ instance _ = ZariskiLattice B .snd
+ isUnitφf : φ .fst f ∈ B ˣ
+ isUnitφf = unitLemmaZarLat B (φ $r f) (sym (∨lRid _) ∙ Dφf≡D1)
+
+ sec (nIso SpR[1/f]≅⟦Df⟧ B) =
+ funExt λ _ → Σ≡Prop (λ _ → squash/ _ _) (RingHom≡ (invElemUniversalProp _ _ _ .fst .snd))
+ ret (nIso SpR[1/f]≅⟦Df⟧ B) =
+ funExt λ φ → cong fst (invElemUniversalProp B (φ ∘r /1AsCommRingHom) _ .snd (φ , refl))
isAffineD : isAffineCompactOpen D
isAffineD = ∣ R[1/ f ]AsCommRing , SpR[1/f]≅⟦Df⟧ ∣₁
From e8fc66ddac320c741e808648f37e4df18a6b850a Mon Sep 17 00:00:00 2001
From: mzeuner <max@zeuner.net>
Date: Mon, 22 Jan 2024 16:50:54 +0100
Subject: [PATCH 07/37] towards opens of affines
---
Cubical/Categories/Instances/ZFunctors.agda | 54 ++++++++++++++++++++-
1 file changed, 53 insertions(+), 1 deletion(-)
diff --git a/Cubical/Categories/Instances/ZFunctors.agda b/Cubical/Categories/Instances/ZFunctors.agda
index cff41e75c8..40faa843d2 100644
--- a/Cubical/Categories/Instances/ZFunctors.agda
+++ b/Cubical/Categories/Instances/ZFunctors.agda
@@ -475,6 +475,10 @@ module _ {ℓ : Level} where
F-id strDLSh = cong (𝓞 .F-hom) compOpenInclId ∙ 𝓞 .F-id
F-seq strDLSh _ _ = cong (𝓞 .F-hom) (compOpenInclSeq _ _) ∙ 𝓞 .F-seq _ _
+ compOpenRest : {U V : CompactOpen X} → V ≤ U → CompactOpen ⟦ U ⟧ᶜᵒ
+ N-ob (compOpenRest {V = V} V≤U) A (x , Ux≡D1) = V .N-ob A x
+ N-hom (compOpenRest V≤U) φ = funExt (λ x → {!!})
+
-- the canonical one element affine cover of a representable
module _ (A : CommRing ℓ) where
open AffineCover
@@ -518,7 +522,7 @@ module _ {ℓ : Level} (R : CommRing ℓ) (f : R .fst) where
open InvertingElementsBase R
open UniversalProp f
- module ZL = ZarLatUniversalProp
+ private module ZL = ZarLatUniversalProp
private
instance
@@ -557,3 +561,51 @@ module _ {ℓ : Level} (R : CommRing ℓ) (f : R .fst) where
isAffineD : isAffineCompactOpen D
isAffineD = ∣ R[1/ f ]AsCommRing , SpR[1/f]≅⟦Df⟧ ∣₁
+
+
+module _ {ℓ : Level} (R : CommRing ℓ) (W : CompactOpen (Sp ⟅ R ⟆)) where
+
+
+ open Iso
+ open Functor
+ open NatTrans
+ open NatIso
+ open isIso
+ open DistLatticeStr ⦃...⦄
+ open CommRingStr ⦃...⦄
+ open PosetStr ⦃...⦄
+ open IsRingHom
+ open RingHoms
+ open IsLatticeHom
+ open ZarLat
+
+
+ open JoinSemilattice (Lattice→JoinSemilattice (DistLattice→Lattice (CompOpenDistLattice .F-ob (Sp .F-ob R)))) using (IndPoset)
+ open InvertingElementsBase R
+ open Join (ZariskiLattice R)
+ open AffineCover
+ module ZL = ZarLatUniversalProp
+
+ private
+ instance
+ _ = R .snd
+ _ = ZariskiLattice R .snd
+ _ = CompOpenDistLattice .F-ob (Sp .F-ob R) .snd
+ _ = IndPoset .snd
+
+ private
+ w : ZL R
+ w = yonedaᴾ ZarLatFun R .fun W
+
+ module _ {n : ℕ} (α : FinVec (fst R) n) (⋁Dα≡w : ⋁ (ZL.D R ∘ α) ≡ w) where
+
+ Dα≤W : ∀ i → D R (α i) ≤ W
+ Dα≤W i = {!!}
+
+ toAffineCover : AffineCover ⟦ W ⟧ᶜᵒ
+ AffineCover.n toAffineCover = n
+ U toAffineCover i = compOpenRest (Sp .F-ob R) (Dα≤W i)
+ covers toAffineCover = {!!}
+ isAffineU toAffineCover = {!!}
+
+ -- then use ⋁D≡
From bd1223afda63d00d97853cd15e96e88e0b58b4a8 Mon Sep 17 00:00:00 2001
From: mzeuner <max@zeuner.net>
Date: Tue, 23 Jan 2024 16:25:13 +0100
Subject: [PATCH 08/37] discussion
---
Cubical/Categories/Instances/ZFunctors.agda | 39 +++++++++++++++++++--
1 file changed, 36 insertions(+), 3 deletions(-)
diff --git a/Cubical/Categories/Instances/ZFunctors.agda b/Cubical/Categories/Instances/ZFunctors.agda
index 40faa843d2..5fc35aa876 100644
--- a/Cubical/Categories/Instances/ZFunctors.agda
+++ b/Cubical/Categories/Instances/ZFunctors.agda
@@ -475,6 +475,7 @@ module _ {ℓ : Level} where
F-id strDLSh = cong (𝓞 .F-hom) compOpenInclId ∙ 𝓞 .F-id
F-seq strDLSh _ _ = cong (𝓞 .F-hom) (compOpenInclSeq _ _) ∙ 𝓞 .F-seq _ _
+ -- ⟦ U ⟧ → X → 𝓛 via V
compOpenRest : {U V : CompactOpen X} → V ≤ U → CompactOpen ⟦ U ⟧ᶜᵒ
N-ob (compOpenRest {V = V} V≤U) A (x , Ux≡D1) = V .N-ob A x
N-hom (compOpenRest V≤U) φ = funExt (λ x → {!!})
@@ -601,11 +602,43 @@ module _ {ℓ : Level} (R : CommRing ℓ) (W : CompactOpen (Sp ⟅ R ⟆)) where
Dα≤W : ∀ i → D R (α i) ≤ W
Dα≤W i = {!!}
+ -- ⋁ (D αᵢ) ≡ W in SpR → 𝓛
toAffineCover : AffineCover ⟦ W ⟧ᶜᵒ
AffineCover.n toAffineCover = n
- U toAffineCover i = compOpenRest (Sp .F-ob R) (Dα≤W i)
+ U toAffineCover i = {!!} -- W → Sp R → 𝓛 via Dαᵢ --compOpenRest (Sp .F-ob R) (Dα≤W i)
covers toAffineCover = {!!}
isAffineU toAffineCover = {!!}
-
- -- then use ⋁D≡
+ -- ⟦ Dαᵢ ∘ W→SpR ⟧ ≅ ⟦ Dαᵢ ⟧ ≅ Sp R[1/αᵢ]
+
+ -- then use ⋁D≡ (merely covered by standard opens) → hasAffineCover ⟦W⟧
+ -- then isLocal ⟦W⟧
+
+ -- 𝓛 separated presheaf:
+ -- For u w : 𝓛 A and ⟨f₀,...,fₙ⟩=A s.t. ∀ i → uᵢ=wᵢ in 𝓛 A[1/fᵢ] then u = w
+ -- where u ↦ uᵢ for 𝓛 A → 𝓛 A[1/fᵢ]
+ -- Min: u : 𝓛 A and ⟨f₀,...,fₙ⟩=A s.t. ∀ i → uᵢ=D1 in 𝓛 A[1/fᵢ] then u = D1 in 𝓛 A
+ -- base case: u = Dg → have ∀ i → g/1 ∈ A[1/fᵢ]ˣ, need 1 ∈ √⟨g⟩ (g ∈ Aˣ)
+ -- g/1 ∈ A[1/fᵢ]ˣ → fᵢ ∈ √ ⟨g⟩ → 1=∑aᵢfᵢ ∈ √⟨g⟩
+ -- i.e. fᵢᵐ=aᵢg
+ -- choose m big enough s.t. it becomes independent of i
+ -- lemma ⟨f₀ᵐ,...,fₙᵐ⟩=A:
+ -- 1 = ∑ bᵢfᵢᵐ = ∑ bᵢaᵢg = (∑ aᵢbᵢ)g
+
+ -- u = D(g₁,...,gₖ) → ⟨g₁/1 ,..., gₖ/1 ⟩ = A[1/fᵢ]
+ -- 0 = A[1/fᵢ]/⟨g₁/1,...,gₖ/1⟩ =???= A/⟨g₁,...,gₙ⟩[1/[fᵢ]] → fᵢⁿ=0 mod ⟨g₁,...,gₙ⟩
+ -- 1/1 = ∑ aⱼ/fᵢⁿ gⱼ/1 → fᵢᵐ = ∑ aⱼgⱼ
+ -- → fᵢ ∈ √ ⟨ g₁ ,..., gₖ ⟩ → 1 = ∑ bᵢfᵢ ∈ √ ⟨ g₁ ,..., gₖ ⟩
+
+ -- 𝓛 sheaf: ⟨f₀,...,fₙ⟩=A → 𝓛 A = lim (↓ Dfᵢ) = lim (𝓛 A[1/fᵢ])
+ -- ⋁uᵢ=⊤ in L → L = lim (↓ uᵢ) = Σ[ vᵢ ≤ uᵢ ] vᵢ ∧ uⱼ = vⱼ ∧ uᵢ
+ -- (↓ Dfᵢ) = 𝓛 A[1/fᵢ]: Dg ≤ Dfᵢ ⇔ g ∈ √ ⟨fᵢ⟩ ⇔ fᵢ ∈ A[1/g]ˣ
+ -- ↓ Dfᵢ → 𝓛 A[1/fᵢ]: Dg ≤ Dfᵢ ↦ D(g/1)
+
+ -- 𝓛 A[1/fᵢ] → ↓ Dfᵢ: D(g/fᵢⁿ) ↦ Dg ∧ Dfᵢ = D(gfᵢ)
+ -- support A[1/fᵢ] → ↓ Dfᵢ given by g/fᵢⁿ ↦ Dg ∧ Dfᵢ = D(gfᵢ)
+ -- support A → A[1/fᵢ] → L gives (↓ Dfᵢ) ↪ 𝓛 A → L lattice hom!
+ -- have _∧Dfᵢ : 𝓛 A → ↓ Dfᵢ
+
+ -- U : CompactOpen X , isQcQsScheme X → isQcQsScheme ⟦U⟧
+ -- X=⋁Uᵢ affine covering → isQcQsScheme U∧Uᵢ →(lemma)→ isQcQsScheme U=⋁(U∧Uᵢ)
From a59b3416772857b202289d4f02a60b2fdaa33392 Mon Sep 17 00:00:00 2001
From: mzeuner <max@zeuner.net>
Date: Wed, 24 Jan 2024 17:15:14 +0100
Subject: [PATCH 09/37] little progress
---
Cubical/Categories/Instances/ZFunctors.agda | 28 +++++++++++++++------
1 file changed, 21 insertions(+), 7 deletions(-)
diff --git a/Cubical/Categories/Instances/ZFunctors.agda b/Cubical/Categories/Instances/ZFunctors.agda
index 5fc35aa876..64517e9598 100644
--- a/Cubical/Categories/Instances/ZFunctors.agda
+++ b/Cubical/Categories/Instances/ZFunctors.agda
@@ -446,6 +446,10 @@ module _ {ℓ : Level} where
-- the structure sheaf
private COᵒᵖ = (DistLatticeCategory (CompOpenDistLattice .F-ob X)) ^op
+ compOpenGlobalIncl : (U : CompactOpen X) → ⟦ U ⟧ᶜᵒ ⇒ X
+ N-ob (compOpenGlobalIncl U) A = fst
+ N-hom (compOpenGlobalIncl U) φ = refl
+
compOpenIncl : {U V : CompactOpen X} → V ≤ U → ⟦ V ⟧ᶜᵒ ⇒ ⟦ U ⟧ᶜᵒ
N-ob (compOpenIncl {U = U} {V = V} V≤U) A (x , Vx≡D1) = x , path
where
@@ -476,9 +480,9 @@ module _ {ℓ : Level} where
F-seq strDLSh _ _ = cong (𝓞 .F-hom) (compOpenInclSeq _ _) ∙ 𝓞 .F-seq _ _
-- ⟦ U ⟧ → X → 𝓛 via V
- compOpenRest : {U V : CompactOpen X} → V ≤ U → CompactOpen ⟦ U ⟧ᶜᵒ
- N-ob (compOpenRest {V = V} V≤U) A (x , Ux≡D1) = V .N-ob A x
- N-hom (compOpenRest V≤U) φ = funExt (λ x → {!!})
+ -- compOpenRest : {U V : CompactOpen X} → V ≤ U → CompactOpen ⟦ U ⟧ᶜᵒ
+ -- N-ob (compOpenRest {V = V} V≤U) A (x , Ux≡D1) = V .N-ob A x
+ -- N-hom (compOpenRest V≤U) φ = funExt (λ x → {!!})
-- the canonical one element affine cover of a representable
module _ (A : CommRing ℓ) where
@@ -583,7 +587,7 @@ module _ {ℓ : Level} (R : CommRing ℓ) (W : CompactOpen (Sp ⟅ R ⟆)) where
open JoinSemilattice (Lattice→JoinSemilattice (DistLattice→Lattice (CompOpenDistLattice .F-ob (Sp .F-ob R)))) using (IndPoset)
open InvertingElementsBase R
- open Join (ZariskiLattice R)
+ open Join
open AffineCover
module ZL = ZarLatUniversalProp
@@ -592,13 +596,22 @@ module _ {ℓ : Level} (R : CommRing ℓ) (W : CompactOpen (Sp ⟅ R ⟆)) where
_ = R .snd
_ = ZariskiLattice R .snd
_ = CompOpenDistLattice .F-ob (Sp .F-ob R) .snd
+ _ = CompOpenDistLattice .F-ob ⟦ W ⟧ᶜᵒ .snd
_ = IndPoset .snd
private
w : ZL R
w = yonedaᴾ ZarLatFun R .fun W
- module _ {n : ℕ} (α : FinVec (fst R) n) (⋁Dα≡w : ⋁ (ZL.D R ∘ α) ≡ w) where
+ module _ {n : ℕ}
+ (α : FinVec (fst R) n)
+ (⋁Dα≡w : ⋁ (ZariskiLattice R) (ZL.D R ∘ α) ≡ w) where
+
+ ⋁Dα≡W : ⋁ (CompOpenDistLattice ⟅ Sp ⟅ R ⟆ ⟆) (D R ∘ α) ≡ W
+ ⋁Dα≡W = makeNatTransPath (funExt₂ (λ A φ → {!!}))
+ where
+ foo : (A : CommRing ℓ) (φ : CommRingHom R A) → inducedZarLatHom φ .fst w ≡ W .N-ob A φ
+ foo A φ i = cong N-ob (yonedaᴾ ZarLatFun R .leftInv W) i A φ
Dα≤W : ∀ i → D R (α i) ≤ W
Dα≤W i = {!!}
@@ -606,8 +619,8 @@ module _ {ℓ : Level} (R : CommRing ℓ) (W : CompactOpen (Sp ⟅ R ⟆)) where
toAffineCover : AffineCover ⟦ W ⟧ᶜᵒ
AffineCover.n toAffineCover = n
- U toAffineCover i = {!!} -- W → Sp R → 𝓛 via Dαᵢ --compOpenRest (Sp .F-ob R) (Dα≤W i)
- covers toAffineCover = {!!}
+ U toAffineCover i = compOpenGlobalIncl (Sp ⟅ R ⟆) W ●ᵛ D R (α i) -- W → Sp R → 𝓛 via Dαᵢ
+ covers toAffineCover = makeNatTransPath (funExt₂ (λ A y → ({!!} ∙ funExt⁻ (funExt⁻ (cong N-ob ⋁Dα≡W) A) (fst y)) ∙ y .snd))
isAffineU toAffineCover = {!!}
-- ⟦ Dαᵢ ∘ W→SpR ⟧ ≅ ⟦ Dαᵢ ⟧ ≅ Sp R[1/αᵢ]
@@ -628,6 +641,7 @@ module _ {ℓ : Level} (R : CommRing ℓ) (W : CompactOpen (Sp ⟅ R ⟆)) where
-- u = D(g₁,...,gₖ) → ⟨g₁/1 ,..., gₖ/1 ⟩ = A[1/fᵢ]
-- 0 = A[1/fᵢ]/⟨g₁/1,...,gₖ/1⟩ =???= A/⟨g₁,...,gₙ⟩[1/[fᵢ]] → fᵢⁿ=0 mod ⟨g₁,...,gₙ⟩
-- 1/1 = ∑ aⱼ/fᵢⁿ gⱼ/1 → fᵢᵐ = ∑ aⱼgⱼ
+ -- use InvertingElementsBase.invElPropElimN to get uniform exponent
-- → fᵢ ∈ √ ⟨ g₁ ,..., gₖ ⟩ → 1 = ∑ bᵢfᵢ ∈ √ ⟨ g₁ ,..., gₖ ⟩
-- 𝓛 sheaf: ⟨f₀,...,fₙ⟩=A → 𝓛 A = lim (↓ Dfᵢ) = lim (𝓛 A[1/fᵢ])
From 911c9ac620de6868666017b2b398448ca35e9751 Mon Sep 17 00:00:00 2001
From: mzeuner <max@zeuner.net>
Date: Fri, 26 Jan 2024 17:45:13 +0100
Subject: [PATCH 10/37] towards separatedness
---
Cubical/Algebra/DistLattice/Downset.agda | 70 ++++++++
Cubical/Algebra/Lattice/Properties.agda | 45 ++++--
.../Algebra/ZariskiLattice/Properties.agda | 150 +++++++++++++++++-
.../ZariskiLattice/StructureSheaf.agda | 6 +-
.../StructureSheafPullback.agda | 8 +-
.../ZariskiLattice/UniversalProperty.agda | 119 ++++++++------
Cubical/Categories/Instances/ZFunctors.agda | 118 +++++++-------
Cubical/Papers/AffineSchemes.agda | 2 +-
.../Binary/Order/Poset/Properties.agda | 22 +++
9 files changed, 412 insertions(+), 128 deletions(-)
create mode 100644 Cubical/Algebra/DistLattice/Downset.agda
diff --git a/Cubical/Algebra/DistLattice/Downset.agda b/Cubical/Algebra/DistLattice/Downset.agda
new file mode 100644
index 0000000000..907c419732
--- /dev/null
+++ b/Cubical/Algebra/DistLattice/Downset.agda
@@ -0,0 +1,70 @@
+{-# OPTIONS --safe #-}
+module Cubical.Algebra.DistLattice.Downset where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.HLevels
+open import Cubical.Foundations.Isomorphism
+open import Cubical.Foundations.Powerset
+
+open import Cubical.Data.Sigma
+
+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
+
+open Iso
+
+private
+ variable
+ ℓ ℓ' : Level
+
+module DistLatticeDownset (L' : DistLattice ℓ) where
+
+ open DistLatticeStr ⦃...⦄
+ open PosetStr ⦃...⦄ hiding (is-set)
+ open JoinSemilattice (Lattice→JoinSemilattice (DistLattice→Lattice L'))
+ open MeetSemilattice (Lattice→MeetSemilattice (DistLattice→Lattice L')) hiding (_≤_ ; IndPoset)
+ open LatticeTheory (DistLattice→Lattice L')
+ open Order (DistLattice→Lattice L')
+ open IsLatticeHom
+
+ -- importing other downset related stuff
+ open PosetDownset IndPoset public
+
+ private
+ L = L' .fst
+ LPoset = IndPoset
+ instance
+ _ = L' .snd
+ _ = LPoset .snd
+
+ ↓ᴰᴸ : L → DistLattice ℓ
+ fst (↓ᴰᴸ u) = ↓ u
+ DistLatticeStr.0l (snd (↓ᴰᴸ u)) = 0l , ∨lLid u
+ DistLatticeStr.1l (snd (↓ᴰᴸ u)) = u , is-refl u
+ DistLatticeStr._∨l_ (snd (↓ᴰᴸ u)) (v , v≤u) (w , w≤u) =
+ v ∨l w , ∨lIsMax _ _ _ v≤u w≤u
+ DistLatticeStr._∧l_ (snd (↓ᴰᴸ u)) (v , v≤u) (w , _) =
+ v ∧l w , is-trans _ _ _ (≤m→≤j _ _ (∧≤RCancel _ _)) v≤u
+ DistLatticeStr.isDistLattice (snd (↓ᴰᴸ u)) = makeIsDistLattice∧lOver∨l
+ (isSetΣSndProp is-set λ _ → is-prop-valued _ _)
+ (λ _ _ _ → Σ≡Prop (λ _ → is-prop-valued _ _) (∨lAssoc _ _ _))
+ (λ _ → Σ≡Prop (λ _ → is-prop-valued _ _) (∨lRid _))
+ (λ _ _ → Σ≡Prop (λ _ → is-prop-valued _ _) (∨lComm _ _))
+ (λ _ _ _ → Σ≡Prop (λ _ → is-prop-valued _ _) (∧lAssoc _ _ _))
+ (λ (_ , v≤u) → Σ≡Prop (λ _ → is-prop-valued _ _) (≤j→≤m _ _ v≤u))
+ (λ _ _ → Σ≡Prop (λ _ → is-prop-valued _ _) (∧lComm _ _))
+ (λ _ _ → Σ≡Prop (λ _ → is-prop-valued _ _) (∧lAbsorb∨l _ _))
+ (λ _ _ _ → Σ≡Prop (λ _ → is-prop-valued _ _) (∧lLdist∨l _ _ _))
+
+ toDownHom : (u : L) → DistLatticeHom L' (↓ᴰᴸ u)
+ fst (toDownHom u) w = (u ∧l w) , ≤m→≤j _ _ (∧≤RCancel _ _)
+ pres0 (snd (toDownHom u)) = Σ≡Prop (λ _ → is-prop-valued _ _) (0lRightAnnihilates∧l _)
+ pres1 (snd (toDownHom u)) = Σ≡Prop (λ _ → is-prop-valued _ _) (∧lRid _)
+ pres∨l (snd (toDownHom u)) v w = Σ≡Prop (λ _ → is-prop-valued _ _) (∧lLdist∨l _ _ _)
+ pres∧l (snd (toDownHom u)) v w = Σ≡Prop (λ _ → is-prop-valued _ _) (∧lLdist∧l u v w)
diff --git a/Cubical/Algebra/Lattice/Properties.agda b/Cubical/Algebra/Lattice/Properties.agda
index 1a7b4ab901..4b28da2f88 100644
--- a/Cubical/Algebra/Lattice/Properties.agda
+++ b/Cubical/Algebra/Lattice/Properties.agda
@@ -29,24 +29,41 @@ private
ℓ ℓ' ℓ'' ℓ''' : Level
module LatticeTheory (L' : Lattice ℓ) where
- private L = fst L'
- open LatticeStr (snd L')
+ private L = fst L'
+ open LatticeStr (snd L')
+
+ 0lLeftAnnihilates∧l : ∀ (x : L) → 0l ∧l x ≡ 0l
+ 0lLeftAnnihilates∧l x = 0l ∧l x ≡⟨ cong (0l ∧l_) (sym (∨lLid _)) ⟩
+ 0l ∧l (0l ∨l x) ≡⟨ ∧lAbsorb∨l _ _ ⟩
+ 0l ∎
+
+ 0lRightAnnihilates∧l : ∀ (x : L) → x ∧l 0l ≡ 0l
+ 0lRightAnnihilates∧l _ = ∧lComm _ _ ∙ 0lLeftAnnihilates∧l _
+
+ 1lLeftAnnihilates∨l : ∀ (x : L) → 1l ∨l x ≡ 1l
+ 1lLeftAnnihilates∨l x = 1l ∨l x ≡⟨ cong (1l ∨l_) (sym (∧lLid _)) ⟩
+ 1l ∨l (1l ∧l x) ≡⟨ ∨lAbsorb∧l _ _ ⟩
+ 1l ∎
+
+ 1lRightAnnihilates∨l : ∀ (x : L) → x ∨l 1l ≡ 1l
+ 1lRightAnnihilates∨l _ = ∨lComm _ _ ∙ 1lLeftAnnihilates∨l _
+
+
+ ∧lCommAssocl : ∀ x y z → x ∧l (y ∧l z) ≡ y ∧l (x ∧l z)
+ ∧lCommAssocl x y z = ∧lAssoc x y z ∙∙ congL _∧l_ (∧lComm x y) ∙∙ sym (∧lAssoc y x z)
- 0lLeftAnnihilates∧l : ∀ (x : L) → 0l ∧l x ≡ 0l
- 0lLeftAnnihilates∧l x = 0l ∧l x ≡⟨ cong (0l ∧l_) (sym (∨lLid _)) ⟩
- 0l ∧l (0l ∨l x) ≡⟨ ∧lAbsorb∨l _ _ ⟩
- 0l ∎
+ ∧lCommAssocr : ∀ x y z → (x ∧l y) ∧l z ≡ (x ∧l z) ∧l y
+ ∧lCommAssocr x y z = sym (∧lAssoc x y z) ∙∙ congR _∧l_ (∧lComm y z) ∙∙ ∧lAssoc x z y
- 0lRightAnnihilates∧l : ∀ (x : L) → x ∧l 0l ≡ 0l
- 0lRightAnnihilates∧l _ = ∧lComm _ _ ∙ 0lLeftAnnihilates∧l _
+ ∧lCommAssocr2 : ∀ x y z → (x ∧l y) ∧l z ≡ (z ∧l y) ∧l x
+ ∧lCommAssocr2 x y z = ∧lCommAssocr _ _ _ ∙∙ congL _∧l_ (∧lComm _ _) ∙∙ ∧lCommAssocr _ _ _
- 1lLeftAnnihilates∨l : ∀ (x : L) → 1l ∨l x ≡ 1l
- 1lLeftAnnihilates∨l x = 1l ∨l x ≡⟨ cong (1l ∨l_) (sym (∧lLid _)) ⟩
- 1l ∨l (1l ∧l x) ≡⟨ ∨lAbsorb∧l _ _ ⟩
- 1l ∎
+ ∧lCommAssocSwap : ∀ x y z w → (x ∧l y) ∧l (z ∧l w) ≡ (x ∧l z) ∧l (y ∧l w)
+ ∧lCommAssocSwap x y z w =
+ ∧lAssoc (x ∧l y) z w ∙∙ congL _∧l_ (∧lCommAssocr x y z) ∙∙ sym (∧lAssoc (x ∧l z) y w)
- 1lRightAnnihilates∨l : ∀ (x : L) → x ∨l 1l ≡ 1l
- 1lRightAnnihilates∨l _ = ∨lComm _ _ ∙ 1lLeftAnnihilates∨l _
+ ∧lLdist∧l : ∀ x y z → x ∧l (y ∧l z) ≡ (x ∧l y) ∧l (x ∧l z)
+ ∧lLdist∧l x y z = congL _∧l_ (sym (∧lIdem _)) ∙ ∧lCommAssocSwap x x y z
diff --git a/Cubical/Algebra/ZariskiLattice/Properties.agda b/Cubical/Algebra/ZariskiLattice/Properties.agda
index 1ad613d427..e95011a5eb 100644
--- a/Cubical/Algebra/ZariskiLattice/Properties.agda
+++ b/Cubical/Algebra/ZariskiLattice/Properties.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe #-}
+{-# OPTIONS --safe --lossy-unification #-}
module Cubical.Algebra.ZariskiLattice.Properties where
@@ -30,6 +30,7 @@ open import Cubical.Algebra.Ring
open import Cubical.Algebra.Ring.Properties
open import Cubical.Algebra.Ring.BigOps
open import Cubical.Algebra.CommRing
+open import Cubical.Algebra.CommRing.Localisation
open import Cubical.Algebra.CommRing.BinomialThm
open import Cubical.Algebra.CommRing.Ideal
open import Cubical.Algebra.CommRing.FGIdeal
@@ -40,6 +41,7 @@ open import Cubical.Algebra.Lattice
open import Cubical.Algebra.DistLattice
open import Cubical.Algebra.DistLattice.Basis
open import Cubical.Algebra.DistLattice.BigOps
+open import Cubical.Algebra.DistLattice.Downset
open import Cubical.Algebra.Matrix
open import Cubical.Algebra.ZariskiLattice.Base
@@ -69,7 +71,7 @@ module _ (R : CommRing ℓ) where
open ZarLat R
open ZarLatUniversalProp R
- open IsZarMap isZarMapD
+ open IsSupport isSupportD
open JoinSemilattice (Lattice→JoinSemilattice (DistLattice→Lattice ZariskiLattice))
using (IndPoset)
@@ -107,3 +109,147 @@ module _ (R : CommRing ℓ) where
α zero · f + 0r ≡⟨ sym 1ⁿ≡α₀f+0 ⟩
1r ^ n ≡⟨ 1ⁿ≡1 n ⟩
1r ∎
+
+
+
+module LocDownSetIso (R : CommRing ℓ) (f : R .fst) where
+ open Iso
+ open CommRingStr ⦃...⦄
+ open DistLatticeStr ⦃...⦄
+ open PosetStr ⦃...⦄
+
+ open Exponentiation R
+ open InvertingElementsBase R
+ open UniversalProp f
+
+ open ZarLat
+ open ZarLatUniversalProp
+ open IsSupport
+
+ open DistLatticeDownset (ZariskiLattice R)
+ open Order (DistLattice→Lattice (ZariskiLattice R))
+ open LatticeTheory (DistLattice→Lattice (ZariskiLattice R))
+ open JoinSemilattice (Lattice→JoinSemilattice (DistLattice→Lattice (ZariskiLattice R)))
+ using () renaming (IndPoset to ZLRPoset)
+
+ open MeetSemilattice (Lattice→MeetSemilattice (DistLattice→Lattice (ZariskiLattice R)))
+ using (≤-∧LPres ; ∧≤RCancel)
+
+ private
+ instance
+ _ = R .snd
+ _ = R[1/ f ]AsCommRing .snd
+ _ = ZariskiLattice R .snd
+ _ = ZLRPoset .snd
+
+ powerLemma : ∀ fⁿ → fⁿ ∈ₚ [ f ⁿ|n≥0] → D R f ∧l D R fⁿ ≡ D R f
+ powerLemma fⁿ = PT.rec (squash/ _ _)
+ λ (n , fⁿ≡f^n) → cong (λ x → D R f ∧l D R x) fⁿ≡f^n
+ ∙ ≤j→≤m _ _ (supportExpIneq (isSupportD R) n f)
+
+ locEqPowerLemma : ∀ r fⁿ → fⁿ ∈ₚ [ f ⁿ|n≥0]
+ → D R f ∧l D R (r · fⁿ) ≡ D R f ∧l D R r
+ locEqPowerLemma r fⁿ fⁿIsPow =
+ D R f ∧l D R (r · fⁿ) ≡⟨ cong (D R f ∧l_) (isSupportD R .·≡∧ _ _) ⟩
+ D R f ∧l (D R r ∧l D R fⁿ) ≡⟨ ∧lAssoc (D R f) (D R r) (D R fⁿ) ⟩
+ (D R f ∧l D R r) ∧l D R fⁿ ≡⟨ ∧lCommAssocr (D R f) (D R r) (D R fⁿ) ⟩
+ (D R f ∧l D R fⁿ) ∧l D R r ≡⟨ cong (_∧l D R r) (powerLemma _ fⁿIsPow) ⟩
+ D R f ∧l D R r ∎
+
+ locEqPowerLemma2 : ∀ r fᵐ fⁿ → fᵐ ∈ₚ [ f ⁿ|n≥0] → fⁿ ∈ₚ [ f ⁿ|n≥0]
+ → D R f ∧l D R (fᵐ · r · fⁿ) ≡ D R f ∧l D R r
+ locEqPowerLemma2 r fᵐ fⁿ fᵐIsPow fⁿIsPow =
+ D R f ∧l D R (fᵐ · r · fⁿ) ≡⟨ locEqPowerLemma (fᵐ · r) fⁿ fⁿIsPow ⟩
+ D R f ∧l D R (fᵐ · r) ≡⟨ cong (D R f ∧l_) (isSupportD R .·≡∧ _ _) ⟩
+ D R f ∧l (D R fᵐ ∧l D R r) ≡⟨ ∧lAssoc (D R f) (D R fᵐ) (D R r) ⟩
+ (D R f ∧l D R fᵐ) ∧l D R r ≡⟨ cong (_∧l D R r) (powerLemma _ fᵐIsPow) ⟩
+ D R f ∧l D R r ∎
+
+
+ locDownSupp : R[1/ f ] → ↓ (D R f)
+ locDownSupp =
+ SQ.rec
+ (isSetΣSndProp squash/ λ x → is-prop-valued x _)
+ -- the actual map: r/fⁿ ↦ Dr∧Df
+ (λ (r , _) → (D R f ∧l D R r) , ≤m→≤j _ _ (∧≤RCancel (D R f) (D R r)))
+ -- coherence
+ λ (r , fⁿ , fⁿIsPow) (r' , fᵐ , fᵐIsPow) ((fᵏ , fᵏIsPow) , fᵏrfᵐ≡fᵏr'fⁿ)
+ → Σ≡Prop (λ x → is-prop-valued x _)
+ (sym (locEqPowerLemma2 r fᵏ fᵐ fᵏIsPow fᵐIsPow)
+ ∙∙ cong (λ x → D R f ∧l D R x) fᵏrfᵐ≡fᵏr'fⁿ
+ ∙∙ locEqPowerLemma2 r' fᵏ fⁿ fᵏIsPow fⁿIsPow)
+
+ isSupportLocDownSupp : IsSupport R[1/ f ]AsCommRing (↓ᴰᴸ (D R f)) locDownSupp
+ pres0 isSupportLocDownSupp =
+ Σ≡Prop (λ x → is-prop-valued x _)
+ (cong (D R f ∧l_) (isSupportD R .pres0) ∙ 0lRightAnnihilates∧l (D R f))
+ pres1 isSupportLocDownSupp = Σ≡Prop (λ x → is-prop-valued x _) (∧lRid (D R f))
+ ·≡∧ isSupportLocDownSupp =
+ SQ.elimProp2
+ (λ _ _ → DistLatticeStr.is-set (↓ᴰᴸ (D R f) .snd) _ _)
+ λ (r , _) (r' , _) → Σ≡Prop (λ x → is-prop-valued x _)
+ (cong (D R f ∧l_) (isSupportD R .·≡∧ r r')
+ ∙ ∧lLdist∧l (D R f) (D R r) (D R r'))
+ +≤∨ isSupportLocDownSupp =
+ SQ.elimProp2
+ (λ _ _ → DistLatticeStr.is-set (↓ᴰᴸ (D R f) .snd) _ _)
+ λ (r , fⁿ , fⁿIsPow) (r' , fᵐ , fᵐIsPow)
+ → Σ≡Prop (λ x → is-prop-valued x _)
+ (subst ((D R f ∧l D R ((r · fᵐ) + (r' · fⁿ))) ≤_)
+ (path r r' fⁿ fᵐ fⁿIsPow fᵐIsPow)
+ (ineq r r' fⁿ fᵐ))
+ where
+ ineq : ∀ r r' fⁿ fᵐ
+ → (D R f ∧l D R (r · fᵐ + r' · fⁿ)) ≤ (D R f ∧l (D R (r · fᵐ) ∨l D R (r' · fⁿ)))
+ ineq r r' fⁿ fᵐ = ≤m→≤j _ _ (≤-∧LPres (D R (r · fᵐ + r' · fⁿ))
+ (D R (r · fᵐ) ∨l D R (r' · fⁿ))
+ (D R f)
+ (≤j→≤m _ _ (isSupportD R .+≤∨ (r · fᵐ) (r' · fⁿ))))
+
+ path : ∀ r r' fⁿ fᵐ → fⁿ ∈ₚ [ f ⁿ|n≥0] → fᵐ ∈ₚ [ f ⁿ|n≥0]
+ → D R f ∧l (D R (r · fᵐ) ∨l D R (r' · fⁿ))
+ ≡ (D R f ∧l D R r) ∨l (D R f ∧l D R r')
+ path r r' fⁿ fᵐ fⁿIsPow fᵐIsPow =
+ ∧lLdist∨l (D R f) (D R (r · fᵐ)) (D R (r' · fⁿ))
+ ∙ cong₂ (_∨l_) (locEqPowerLemma r fᵐ fᵐIsPow) (locEqPowerLemma r' fⁿ fⁿIsPow)
+
+
+ -- one direction of the equivalence
+ locToDownHom : DistLatticeHom (ZariskiLattice R[1/ f ]AsCommRing) (↓ᴰᴸ (D R f))
+ locToDownHom = ZLHasUniversalProp _ _ _ isSupportLocDownSupp .fst .fst
+
+ toDownSupp : R .fst → ↓ (D R f)
+ toDownSupp = locDownSupp ∘ _/1
+
+ isSupportToDownSupp : IsSupport R (↓ᴰᴸ (D R f)) toDownSupp
+ isSupportToDownSupp = presSupportPrecomp /1AsCommRingHom _ _ isSupportLocDownSupp
+
+ -- the map ZL R → ZL R[1/f] → ↓Df is just Df∧_
+ -- does not type check without lossy unification!!!
+ toLocToDown≡ToDown : locToDownHom ∘dl inducedZarLatHom /1AsCommRingHom
+ ≡ toDownHom (D R f)
+ toLocToDown≡ToDown =
+ cong fst (isContr→isProp
+ (ZLHasUniversalProp R (↓ᴰᴸ (D R f)) toDownSupp isSupportToDownSupp)
+ (locToDownHom ∘dl (inducedZarLatHom /1AsCommRingHom) , toLocToDownComm)
+ (toDownHom (D R f) , toDownComm))
+ where
+ toDownComm : toDownHom (D R f) .fst ∘ (D R) ≡ toDownSupp
+ toDownComm = funExt λ r → Σ≡Prop (λ x → is-prop-valued x _) refl
+
+ toLocToDownComm : locToDownHom .fst ∘ inducedZarLatHom /1AsCommRingHom .fst ∘ D R
+ ≡ toDownSupp
+ toLocToDownComm =
+ locToDownHom .fst ∘ (inducedZarLatHom /1AsCommRingHom) .fst ∘ D R
+
+ ≡⟨ cong (locToDownHom .fst ∘_) (inducedZarLatHomComm /1AsCommRingHom) ⟩
+
+ locToDownHom .fst ∘ D R[1/ f ]AsCommRing ∘ _/1
+
+ ≡⟨ ∘-assoc (locToDownHom .fst) (D R[1/ f ]AsCommRing) _/1 ⟩
+
+ (locToDownHom .fst ∘ D R[1/ f ]AsCommRing) ∘ _/1
+
+ ≡⟨ cong (_∘ _/1) (ZLHasUniversalProp _ _ _ isSupportLocDownSupp .fst .snd) ⟩
+
+ locDownSupp ∘ _/1 ∎
diff --git a/Cubical/Algebra/ZariskiLattice/StructureSheaf.agda b/Cubical/Algebra/ZariskiLattice/StructureSheaf.agda
index ac8798946b..b70970886c 100644
--- a/Cubical/Algebra/ZariskiLattice/StructureSheaf.agda
+++ b/Cubical/Algebra/ZariskiLattice/StructureSheaf.agda
@@ -91,7 +91,7 @@ module _ {ℓ : Level} (R' : CommRing ℓ) where
open ZarLat R'
open ZarLatUniversalProp R'
- open IsZarMap
+ open IsSupport
open Join ZariskiLattice
open JoinSemilattice (Lattice→JoinSemilattice (DistLattice→Lattice ZariskiLattice))
@@ -111,9 +111,9 @@ module _ {ℓ : Level} (R' : CommRing ℓ) where
BO = Σ[ 𝔞 ∈ ZL ] (𝔞 ∈ₚ BasicOpens)
basicOpensAreBasis : IsBasis ZariskiLattice BasicOpens
- contains1 basicOpensAreBasis = ∣ 1r , isZarMapD .pres1 ∣₁
+ contains1 basicOpensAreBasis = ∣ 1r , isSupportD .pres1 ∣₁
∧lClosed basicOpensAreBasis 𝔞 𝔟 = map2
- λ (f , Df≡𝔞) (g , Dg≡𝔟) → (f · g) , isZarMapD .·≡∧ f g ∙ cong₂ (_∧z_) Df≡𝔞 Dg≡𝔟
+ λ (f , Df≡𝔞) (g , Dg≡𝔟) → (f · g) , isSupportD .·≡∧ f g ∙ cong₂ (_∧z_) Df≡𝔞 Dg≡𝔟
⋁Basis basicOpensAreBasis = elimProp (λ _ → isPropPropTrunc) Σhelper
where
Σhelper : (a : Σ[ n ∈ ℕ ] FinVec R n)
diff --git a/Cubical/Algebra/ZariskiLattice/StructureSheafPullback.agda b/Cubical/Algebra/ZariskiLattice/StructureSheafPullback.agda
index a01e5d6971..61bc82976c 100644
--- a/Cubical/Algebra/ZariskiLattice/StructureSheafPullback.agda
+++ b/Cubical/Algebra/ZariskiLattice/StructureSheafPullback.agda
@@ -92,7 +92,7 @@ module _ (R' : CommRing ℓ) where
open ZarLat R'
open ZarLatUniversalProp R'
- open IsZarMap
+ open IsSupport
open Join ZariskiLattice
open JoinSemilattice (Lattice→JoinSemilattice (DistLattice→Lattice ZariskiLattice))
@@ -115,9 +115,9 @@ module _ (R' : CommRing ℓ) where
BO = Σ[ 𝔞 ∈ ZL ] (𝔞 ∈ₚ BasicOpens)
basicOpensAreBasis : IsBasis ZariskiLattice BasicOpens
- contains1 basicOpensAreBasis = ∣ 1r , isZarMapD .pres1 ∣₁
+ contains1 basicOpensAreBasis = ∣ 1r , isSupportD .pres1 ∣₁
∧lClosed basicOpensAreBasis 𝔞 𝔟 = map2
- λ (f , Df≡𝔞) (g , Dg≡𝔟) → (f · g) , isZarMapD .·≡∧ f g ∙ cong₂ (_∧z_) Df≡𝔞 Dg≡𝔟
+ λ (f , Df≡𝔞) (g , Dg≡𝔟) → (f · g) , isSupportD .·≡∧ f g ∙ cong₂ (_∧z_) Df≡𝔞 Dg≡𝔟
⋁Basis basicOpensAreBasis = elimProp (λ _ → isPropPropTrunc) Σhelper
where
Σhelper : (a : Σ[ n ∈ ℕ ] FinVec R n)
@@ -189,7 +189,7 @@ module _ (R' : CommRing ℓ) where
_ = BasisStructurePShf
canonical0∈BO : 0z ∈ₚ BasicOpens
- canonical0∈BO = ∣ 0r , isZarMapD .pres0 ∣₁
+ canonical0∈BO = ∣ 0r , isSupportD .pres0 ∣₁
canonical0∈BO≡0∈BO : canonical0∈BO ≡ 0∈BO
canonical0∈BO≡0∈BO = BasicOpens 0z .snd _ _
diff --git a/Cubical/Algebra/ZariskiLattice/UniversalProperty.agda b/Cubical/Algebra/ZariskiLattice/UniversalProperty.agda
index 1ba6f964b7..cfd480deab 100644
--- a/Cubical/Algebra/ZariskiLattice/UniversalProperty.agda
+++ b/Cubical/Algebra/ZariskiLattice/UniversalProperty.agda
@@ -70,7 +70,7 @@ module _ (R' : CommRing ℓ) (L' : DistLattice ℓ') where
R = fst R'
L = fst L'
- record IsZarMap (d : R → L) : Type (ℓ-max ℓ ℓ') where
+ record IsSupport (d : R → L) : Type (ℓ-max ℓ ℓ') where
constructor iszarmap
field
@@ -98,17 +98,17 @@ module _ (R' : CommRing ℓ) (L' : DistLattice ℓ') where
linearCombination≤LCancel α β = is-trans _ _ _ (∑≤⋁ (λ i → α i · β i))
(≤-⋁Ext _ _ λ i → d·LCancel (α i) (β i))
- ZarMapUnit : ∀ x → x ∈ₚ Rˣ → d x ≡ 1l
- ZarMapUnit x (x⁻¹ , xx⁻¹≡1) = is-antisym _ _ (1lRightAnnihilates∨l _)
+ supportUnit : ∀ x → x ∈ₚ Rˣ → d x ≡ 1l
+ supportUnit x (x⁻¹ , xx⁻¹≡1) = is-antisym _ _ (1lRightAnnihilates∨l _)
(subst (_≤ d x) (cong d xx⁻¹≡1 ∙ pres1) (d·RCancel _ _))
- ZarMapIdem : ∀ (n : ℕ) (x : R) → d (x ^ (suc n)) ≡ d x
- ZarMapIdem zero x = ·≡∧ _ _ ∙∙ cong (d x ∧l_) pres1 ∙∙ ∧lRid _
- ZarMapIdem (suc n) x = ·≡∧ _ _ ∙∙ cong (d x ∧l_) (ZarMapIdem n x) ∙∙ ∧lIdem _
+ supportIdem : ∀ (n : ℕ) (x : R) → d (x ^ (suc n)) ≡ d x
+ supportIdem zero x = ·≡∧ _ _ ∙∙ cong (d x ∧l_) pres1 ∙∙ ∧lRid _
+ supportIdem (suc n) x = ·≡∧ _ _ ∙∙ cong (d x ∧l_) (supportIdem n x) ∙∙ ∧lIdem _
- ZarMapExpIneq : ∀ (n : ℕ) (x : R) → d x ≤ d (x ^ n)
- ZarMapExpIneq zero x = cong (d x ∨l_) pres1 ∙∙ 1lRightAnnihilates∨l _ ∙∙ sym pres1
- ZarMapExpIneq (suc n) x = subst (λ y → d x ≤ y) (sym (ZarMapIdem _ x)) (∨lIdem _)
+ supportExpIneq : ∀ (n : ℕ) (x : R) → d x ≤ d (x ^ n)
+ supportExpIneq zero x = cong (d x ∨l_) pres1 ∙∙ 1lRightAnnihilates∨l _ ∙∙ sym pres1
+ supportExpIneq (suc n) x = subst (λ y → d x ≤ y) (sym (supportIdem _ x)) (∨lIdem _)
-- the crucial lemma about "Zariski maps"
open CommIdeal R'
@@ -118,18 +118,45 @@ module _ (R' : CommRing ℓ) (L' : DistLattice ℓ') where
⟨_⟩ : {n : ℕ} → FinVec R n → CommIdeal
⟨ V ⟩ = ⟨ V ⟩[ R' ]
- ZarMapRadicalIneq : ∀ {n : ℕ} (α : FinVec R n) (x : R)
+ supportRadicalIneq : ∀ {n : ℕ} (α : FinVec R n) (x : R)
→ x ∈ √ ⟨ α ⟩ → d x ≤ ⋁ (d ∘ α)
- ZarMapRadicalIneq α x = PT.elim (λ _ → isSetL _ _)
+ supportRadicalIneq α x = PT.elim (λ _ → isSetL _ _)
(uncurry (λ n → (PT.elim (λ _ → isSetL _ _) (uncurry (curriedHelper n)))))
where
curriedHelper : (n : ℕ) (β : FinVec R _)
→ x ^ n ≡ linearCombination R' β α → d x ≤ ⋁ (d ∘ α)
- curriedHelper n β xⁿ≡∑βα = d x ≤⟨ ZarMapExpIneq n x ⟩
+ curriedHelper n β xⁿ≡∑βα = d x ≤⟨ supportExpIneq n x ⟩
d (x ^ n)
≤⟨ subst (λ y → y ≤ ⋁ (d ∘ α)) (sym (cong d xⁿ≡∑βα)) (linearCombination≤LCancel β α) ⟩
⋁ (d ∘ α) ◾
+-- precomposition with a ring hom
+module _ {A B : CommRing ℓ} (φ : CommRingHom A B)
+ (L : DistLattice ℓ) (d : B .fst → L .fst) where
+ open IsSupport
+ open CommRingStr ⦃...⦄
+ open DistLatticeStr ⦃...⦄
+ open IsRingHom
+ private
+ instance
+ _ = L .snd
+ _ = A .snd
+ _ = B .snd
+
+ presSupportPrecomp : IsSupport B L d → IsSupport A L (d ∘ fst φ)
+ pres0 (presSupportPrecomp dIsSupport) = cong d (φ .snd .pres0) ∙ dIsSupport .pres0
+ pres1 (presSupportPrecomp dIsSupport) = cong d (φ .snd .pres1) ∙ dIsSupport .pres1
+ ·≡∧ (presSupportPrecomp dIsSupport) x y = cong d (φ .snd .pres· x y)
+ ∙ dIsSupport .·≡∧ (φ .fst x) (φ .fst y)
+ +≤∨ (presSupportPrecomp dIsSupport) x y =
+ let open JoinSemilattice
+ (Lattice→JoinSemilattice (DistLattice→Lattice L))
+ in subst (λ z → z ≤ (d (φ .fst x)) ∨l (d (φ .fst y)))
+ (sym (cong d (φ .snd .pres+ x y)))
+ (dIsSupport .+≤∨ (φ .fst x) (φ .fst y))
+
+
+
module ZarLatUniversalProp (R' : CommRing ℓ) where
open CommRingStr (snd R')
open RingTheory (CommRing→Ring R')
@@ -143,7 +170,7 @@ module ZarLatUniversalProp (R' : CommRing ℓ) where
open ProdFin R'
open ZarLat R'
- open IsZarMap
+ open IsSupport
private
R = fst R'
@@ -154,11 +181,11 @@ module ZarLatUniversalProp (R' : CommRing ℓ) where
D : R → ZL
D x = [ 1 , replicateFinVec 1 x ] -- λ x → √⟨x⟩
- isZarMapD : IsZarMap R' ZariskiLattice D
- pres0 isZarMapD = eq/ _ _ (≡→∼ (cong √ (0FGIdeal _ ∙ sym (emptyFGIdeal _ _))))
- pres1 isZarMapD = refl
- ·≡∧ isZarMapD x y = cong {B = λ _ → ZL} (λ U → [ 1 , U ]) (Length1··Fin x y)
- +≤∨ isZarMapD x y = eq/ _ _ (≡→∼ (cong √ (CommIdeal≡Char
+ isSupportD : IsSupport R' ZariskiLattice D
+ pres0 isSupportD = eq/ _ _ (≡→∼ (cong √ (0FGIdeal _ ∙ sym (emptyFGIdeal _ _))))
+ pres1 isSupportD = refl
+ ·≡∧ isSupportD x y = cong {B = λ _ → ZL} (λ U → [ 1 , U ]) (Length1··Fin x y)
+ +≤∨ isSupportD x y = eq/ _ _ (≡→∼ (cong √ (CommIdeal≡Char
(inclOfFGIdeal _ 3Vec ⟨ 2Vec ⟩ 3Vec⊆2Vec)
(inclOfFGIdeal _ 2Vec ⟨ 3Vec ⟩ 2Vec⊆3Vec))))
where
@@ -177,18 +204,18 @@ module ZarLatUniversalProp (R' : CommRing ℓ) where
-- defintion of the universal property
hasZarLatUniversalProp : (L : DistLattice ℓ') (D : R → fst L)
- → IsZarMap R' L D
+ → IsSupport R' L D
→ Type _
hasZarLatUniversalProp {ℓ' = ℓ'} L D _ = ∀ (L' : DistLattice ℓ') (d : R → fst L')
- → IsZarMap R' L' d
+ → IsSupport R' L' d
→ ∃![ χ ∈ DistLatticeHom L L' ] (fst χ) ∘ D ≡ d
- isPropZarLatUniversalProp : (L : DistLattice ℓ') (D : R → fst L) (isZarMapD : IsZarMap R' L D)
- → isProp (hasZarLatUniversalProp L D isZarMapD)
- isPropZarLatUniversalProp L D isZarMapD = isPropΠ3 (λ _ _ _ → isPropIsContr)
+ isPropZarLatUniversalProp : (L : DistLattice ℓ') (D : R → fst L) (isSupportD : IsSupport R' L D)
+ → isProp (hasZarLatUniversalProp L D isSupportD)
+ isPropZarLatUniversalProp L D isSupportD = isPropΠ3 (λ _ _ _ → isPropIsContr)
- ZLHasUniversalProp : hasZarLatUniversalProp ZariskiLattice D isZarMapD
- ZLHasUniversalProp L' d isZarMapd = (χ , funExt χcomp) , χunique
+ ZLHasUniversalProp : hasZarLatUniversalProp ZariskiLattice D isSupportD
+ ZLHasUniversalProp L' d isSupportd = (χ , funExt χcomp) , χunique
where
open DistLatticeStr (snd L') renaming (is-set to isSetL)
open LatticeTheory (DistLattice→Lattice L')
@@ -214,18 +241,18 @@ module ZarLatUniversalProp (R' : CommRing ℓ) where
ineq1 : ⋁ (d ∘ α) ≤ ⋁ (d ∘ β)
ineq1 = ⋁IsMax (d ∘ α) (⋁ (d ∘ β))
- λ i → ZarMapRadicalIneq isZarMapd β (α i) (√FGIdealCharLImpl α ⟨ β ⟩ incl1 i)
+ λ i → supportRadicalIneq isSupportd β (α i) (√FGIdealCharLImpl α ⟨ β ⟩ incl1 i)
incl2 : √ ⟨ β ⟩ ⊆ √ ⟨ α ⟩
incl2 = ⊆-refl-consequence _ _ (cong fst (∼→≡ α∼β)) .snd
ineq2 : ⋁ (d ∘ β) ≤ ⋁ (d ∘ α)
ineq2 = ⋁IsMax (d ∘ β) (⋁ (d ∘ α))
- λ i → ZarMapRadicalIneq isZarMapd α (β i) (√FGIdealCharLImpl β ⟨ α ⟩ incl2 i)
+ λ i → supportRadicalIneq isSupportd α (β i) (√FGIdealCharLImpl β ⟨ α ⟩ incl2 i)
pres0 (snd χ) = refl
- pres1 (snd χ) = ∨lRid _ ∙ isZarMapd .pres1
+ pres1 (snd χ) = ∨lRid _ ∙ isSupportd .pres1
pres∨l (snd χ) = elimProp2 (λ _ _ → isSetL _ _) (uncurry (λ n α → uncurry (curriedHelper n α)))
where
curriedHelper : (n : ℕ) (α : FinVec R n) (m : ℕ) (β : FinVec R m)
@@ -261,7 +288,7 @@ module ZarLatUniversalProp (R' : CommRing ℓ) where
⋁ (d ∘ (λ j → α zero · β j)) ∨l ⋁ (d ∘ ((α ∘ suc) ··Fin β))
- ≡⟨ cong (_∨l ⋁ (d ∘ ((α ∘ suc) ··Fin β))) (⋁Ext (λ j → isZarMapd .·≡∧ (α zero) (β j))) ⟩
+ ≡⟨ cong (_∨l ⋁ (d ∘ ((α ∘ suc) ··Fin β))) (⋁Ext (λ j → isSupportd .·≡∧ (α zero) (β j))) ⟩
⋁ (λ j → d (α zero) ∧l d (β j)) ∨l ⋁ (d ∘ ((α ∘ suc) ··Fin β))
@@ -311,10 +338,10 @@ module ZarLatUniversalProp (R' : CommRing ℓ) where
-- the map induced by applying the universal property to the Zariski lattice
-- itself is the identity hom
- ZLUniversalPropCorollary : ZLHasUniversalProp ZariskiLattice D isZarMapD .fst .fst
+ ZLUniversalPropCorollary : ZLHasUniversalProp ZariskiLattice D isSupportD .fst .fst
≡ idDistLatticeHom ZariskiLattice
ZLUniversalPropCorollary = cong fst
- (ZLHasUniversalProp ZariskiLattice D isZarMapD .snd
+ (ZLHasUniversalProp ZariskiLattice D isSupportD .snd
(idDistLatticeHom ZariskiLattice , refl))
-- and another corollary
@@ -328,7 +355,7 @@ module _ {A B : CommRing ℓ} (φ : CommRingHom A B) where
open ZarLat
open ZarLatUniversalProp
- open IsZarMap
+ open IsSupport
open CommRingStr ⦃...⦄
open DistLatticeStr ⦃...⦄
open IsRingHom
@@ -340,22 +367,18 @@ module _ {A B : CommRing ℓ} (φ : CommRingHom A B) where
_ = (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))
+ Dcomp = D B ∘ fst φ
+
+ isSupportDcomp : IsSupport A (ZariskiLattice B) Dcomp
+ isSupportDcomp = presSupportPrecomp φ (ZariskiLattice B) (D B) (isSupportD B)
inducedZarLatHom : DistLatticeHom (ZariskiLattice A) (ZariskiLattice B)
- inducedZarLatHom = ZLHasUniversalProp A (ZariskiLattice B) Dcomp isZarMapDcomp .fst .fst
+ inducedZarLatHom =
+ ZLHasUniversalProp A (ZariskiLattice B) Dcomp isSupportDcomp .fst .fst
+
+ inducedZarLatHomComm : inducedZarLatHom .fst ∘ D A ≡ Dcomp
+ inducedZarLatHomComm =
+ ZLHasUniversalProp A (ZariskiLattice B) Dcomp isSupportDcomp .fst .snd
-- functoriality
module _ (A : CommRing ℓ) where
@@ -367,7 +390,7 @@ module _ (A : CommRing ℓ) where
inducedZarLatHomId =
cong fst
(ZLHasUniversalProp A (ZariskiLattice A) (Dcomp (idCommRingHom A))
- (isZarMapDcomp (idCommRingHom A)) .snd
+ (isSupportDcomp (idCommRingHom A)) .snd
(idDistLatticeHom (ZariskiLattice A) , refl))
module _ {A B C : CommRing ℓ} (φ : CommRingHom A B) (ψ : CommRingHom B C) where
@@ -379,6 +402,6 @@ module _ {A B C : CommRing ℓ} (φ : CommRingHom A B) (ψ : CommRingHom B C) wh
inducedZarLatHomSeq =
cong fst
(ZLHasUniversalProp A (ZariskiLattice C) (Dcomp (ψ ∘cr φ))
- (isZarMapDcomp (ψ ∘cr φ)) .snd
+ (isSupportDcomp (ψ ∘cr φ)) .snd
(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 64517e9598..53517578c4 100644
--- a/Cubical/Categories/Instances/ZFunctors.agda
+++ b/Cubical/Categories/Instances/ZFunctors.agda
@@ -305,6 +305,13 @@ module _ {ℓ : Level} where
F-id ZarLatFun {A} = cong fst (inducedZarLatHomId A)
F-seq ZarLatFun φ ψ = cong fst (inducedZarLatHomSeq φ ψ)
+ -- this is a separated presheaf
+ -- (TODO: prove this a sheaf)
+ isSeparatedZarLatFun : isSeparated zariskiCoverage ZarLatFun
+ isSeparatedZarLatFun A (unimodvec n f 1∈⟨f₁,⋯,fₙ⟩) u w uRest≡wRest = {!!}
+ where
+ instance _ = A .snd
+
CompactOpen : ℤFunctor → Type (ℓ-suc ℓ)
CompactOpen X = X ⇒ ZarLatFun
@@ -540,7 +547,7 @@ module _ {ℓ : Level} (R : CommRing ℓ) (f : R .fst) where
N-ob (trans SpR[1/f]≅⟦Df⟧) B φ = (φ ∘r /1AsCommRingHom) , ∨lRid _ ∙ path
where
open CommRingHomTheory φ
- open IsZarMap (ZL.isZarMapD B)
+ open IsSupport (ZL.isSupportD B)
instance
_ = B .snd
_ = ZariskiLattice B .snd
@@ -549,7 +556,7 @@ module _ {ℓ : Level} (R : CommRing ℓ) (f : R .fst) where
isUnitφ[f/1] = RingHomRespInv (f /1) ⦃ S/1⊆S⁻¹Rˣ f ∣ 1 , sym (·IdR f) ∣₁ ⦄
path : ZL.D B (φ .fst (f /1)) ≡ 1l
- path = ZarMapUnit _ isUnitφ[f/1]
+ path = supportUnit _ isUnitφ[f/1]
N-hom (trans SpR[1/f]≅⟦Df⟧) _ = funExt λ _ → Σ≡Prop (λ _ → squash/ _ _) (RingHom≡ refl)
@@ -568,60 +575,59 @@ module _ {ℓ : Level} (R : CommRing ℓ) (f : R .fst) where
isAffineD = ∣ R[1/ f ]AsCommRing , SpR[1/f]≅⟦Df⟧ ∣₁
-module _ {ℓ : Level} (R : CommRing ℓ) (W : CompactOpen (Sp ⟅ R ⟆)) where
-
-
- open Iso
- open Functor
- open NatTrans
- open NatIso
- open isIso
- open DistLatticeStr ⦃...⦄
- open CommRingStr ⦃...⦄
- open PosetStr ⦃...⦄
- open IsRingHom
- open RingHoms
- open IsLatticeHom
- open ZarLat
-
-
- open JoinSemilattice (Lattice→JoinSemilattice (DistLattice→Lattice (CompOpenDistLattice .F-ob (Sp .F-ob R)))) using (IndPoset)
- open InvertingElementsBase R
- open Join
- open AffineCover
- module ZL = ZarLatUniversalProp
-
- private
- instance
- _ = R .snd
- _ = ZariskiLattice R .snd
- _ = CompOpenDistLattice .F-ob (Sp .F-ob R) .snd
- _ = CompOpenDistLattice .F-ob ⟦ W ⟧ᶜᵒ .snd
- _ = IndPoset .snd
-
- private
- w : ZL R
- w = yonedaᴾ ZarLatFun R .fun W
-
- module _ {n : ℕ}
- (α : FinVec (fst R) n)
- (⋁Dα≡w : ⋁ (ZariskiLattice R) (ZL.D R ∘ α) ≡ w) where
-
- ⋁Dα≡W : ⋁ (CompOpenDistLattice ⟅ Sp ⟅ R ⟆ ⟆) (D R ∘ α) ≡ W
- ⋁Dα≡W = makeNatTransPath (funExt₂ (λ A φ → {!!}))
- where
- foo : (A : CommRing ℓ) (φ : CommRingHom R A) → inducedZarLatHom φ .fst w ≡ W .N-ob A φ
- foo A φ i = cong N-ob (yonedaᴾ ZarLatFun R .leftInv W) i A φ
-
- Dα≤W : ∀ i → D R (α i) ≤ W
- Dα≤W i = {!!}
- -- ⋁ (D αᵢ) ≡ W in SpR → 𝓛
-
- toAffineCover : AffineCover ⟦ W ⟧ᶜᵒ
- AffineCover.n toAffineCover = n
- U toAffineCover i = compOpenGlobalIncl (Sp ⟅ R ⟆) W ●ᵛ D R (α i) -- W → Sp R → 𝓛 via Dαᵢ
- covers toAffineCover = makeNatTransPath (funExt₂ (λ A y → ({!!} ∙ funExt⁻ (funExt⁻ (cong N-ob ⋁Dα≡W) A) (fst y)) ∙ y .snd))
- isAffineU toAffineCover = {!!}
+-- module _ {ℓ : Level} (R : CommRing ℓ) (W : CompactOpen (Sp ⟅ R ⟆)) where
+
+-- open Iso
+-- open Functor
+-- open NatTrans
+-- open NatIso
+-- open isIso
+-- open DistLatticeStr ⦃...⦄
+-- open CommRingStr ⦃...⦄
+-- open PosetStr ⦃...⦄
+-- open IsRingHom
+-- open RingHoms
+-- open IsLatticeHom
+-- open ZarLat
+
+
+-- open JoinSemilattice (Lattice→JoinSemilattice (DistLattice→Lattice (CompOpenDistLattice .F-ob (Sp .F-ob R)))) using (IndPoset)
+-- open InvertingElementsBase R
+-- open Join
+-- open AffineCover
+-- module ZL = ZarLatUniversalProp
+
+-- private
+-- instance
+-- _ = R .snd
+-- _ = ZariskiLattice R .snd
+-- _ = CompOpenDistLattice .F-ob (Sp .F-ob R) .snd
+-- _ = CompOpenDistLattice .F-ob ⟦ W ⟧ᶜᵒ .snd
+-- _ = IndPoset .snd
+
+-- private
+-- w : ZL R
+-- w = yonedaᴾ ZarLatFun R .fun W
+
+-- module _ {n : ℕ}
+-- (α : FinVec (fst R) n)
+-- (⋁Dα≡w : ⋁ (ZariskiLattice R) (ZL.D R ∘ α) ≡ w) where
+
+-- ⋁Dα≡W : ⋁ (CompOpenDistLattice ⟅ Sp ⟅ R ⟆ ⟆) (D R ∘ α) ≡ W
+-- ⋁Dα≡W = makeNatTransPath (funExt₂ (λ A φ → {!!}))
+-- where
+-- foo : (A : CommRing ℓ) (φ : CommRingHom R A) → inducedZarLatHom φ .fst w ≡ W .N-ob A φ
+-- foo A φ i = cong N-ob (yonedaᴾ ZarLatFun R .leftInv W) i A φ
+
+-- Dα≤W : ∀ i → D R (α i) ≤ W
+-- Dα≤W i = {!!}
+-- -- ⋁ (D αᵢ) ≡ W in SpR → 𝓛
+
+-- toAffineCover : AffineCover ⟦ W ⟧ᶜᵒ
+-- AffineCover.n toAffineCover = n
+-- U toAffineCover i = compOpenGlobalIncl (Sp ⟅ R ⟆) W ●ᵛ D R (α i) -- W → Sp R → 𝓛 via Dαᵢ
+-- covers toAffineCover = makeNatTransPath (funExt₂ (λ A y → ({!!} ∙ funExt⁻ (funExt⁻ (cong N-ob ⋁Dα≡W) A) (fst y)) ∙ y .snd))
+-- isAffineU toAffineCover = {!!}
-- ⟦ Dαᵢ ∘ W→SpR ⟧ ≅ ⟦ Dαᵢ ⟧ ≅ Sp R[1/αᵢ]
-- then use ⋁D≡ (merely covered by standard opens) → hasAffineCover ⟦W⟧
diff --git a/Cubical/Papers/AffineSchemes.agda b/Cubical/Papers/AffineSchemes.agda
index beb6a5859d..fc3d95bf73 100644
--- a/Cubical/Papers/AffineSchemes.agda
+++ b/Cubical/Papers/AffineSchemes.agda
@@ -164,7 +164,7 @@ open FinGenIdeals using (FGIdealMultLemma)
open ZariskiLatDef using (ZariskiLattice)
-- support map D and universal property
-open ZariskiLatUnivProp using (D ; isZarMapD)
+open ZariskiLatUnivProp using (D ; isSupportD)
open ZariskiLatUnivProp using (ZLHasUniversalProp)
-- D(g) ≤ D(f) ⇔ isContr (R-Hom R[1/f] R[1/g])
diff --git a/Cubical/Relation/Binary/Order/Poset/Properties.agda b/Cubical/Relation/Binary/Order/Poset/Properties.agda
index 4e56fc7d47..50d6f9b6ab 100644
--- a/Cubical/Relation/Binary/Order/Poset/Properties.agda
+++ b/Cubical/Relation/Binary/Order/Poset/Properties.agda
@@ -8,6 +8,8 @@ open import Cubical.Functions.Embedding
open import Cubical.HITs.PropositionalTruncation as ∥₁
+open import Cubical.Data.Sigma
+
open import Cubical.Relation.Binary.Base
open import Cubical.Relation.Binary.Order.Poset.Base
open import Cubical.Relation.Binary.Order.Preorder.Base
@@ -69,3 +71,23 @@ Poset→StrictPoset : Poset ℓ ℓ' → StrictPoset ℓ (ℓ-max ℓ ℓ')
Poset→StrictPoset (_ , pos)
= _ , strictposetstr (BinaryRelation.IrreflKernel (PosetStr._≤_ pos))
(isPoset→isStrictPosetIrreflKernel (PosetStr.isPoset pos))
+
+
+
+module PosetDownset (P' : Poset ℓ ℓ') where
+ private P = fst P'
+ open PosetStr (snd P')
+
+ ↓ : P → Type (ℓ-max ℓ ℓ')
+ ↓ u = Σ[ v ∈ P ] v ≤ u
+
+ ↓ᴾ : P → Poset (ℓ-max ℓ ℓ') ℓ'
+ fst (↓ᴾ u) = ↓ u
+ PosetStr._≤_ (snd (↓ᴾ u)) v w = v .fst ≤ w .fst
+ IsPoset.is-set (PosetStr.isPoset (snd (↓ᴾ u))) =
+ isSetΣSndProp is-set λ _ → is-prop-valued _ _
+ IsPoset.is-prop-valued (PosetStr.isPoset (snd (↓ᴾ u))) _ _ = is-prop-valued _ _
+ IsPoset.is-refl (PosetStr.isPoset (snd (↓ᴾ u))) _ = is-refl _
+ IsPoset.is-trans (PosetStr.isPoset (snd (↓ᴾ u))) _ _ _ = is-trans _ _ _
+ IsPoset.is-antisym (PosetStr.isPoset (snd (↓ᴾ u))) _ _ v≤w w≤v =
+ Σ≡Prop (λ _ → is-prop-valued _ _) (is-antisym _ _ v≤w w≤v)
From 2e3ed1b76313305fc489cf62d3058146a8eb0e0c Mon Sep 17 00:00:00 2001
From: mzeuner <max@zeuner.net>
Date: Mon, 29 Jan 2024 12:23:55 +0100
Subject: [PATCH 11/37] separatedness
---
Cubical/Categories/Instances/ZFunctors.agda | 40 +++++++++++++++++++--
1 file changed, 38 insertions(+), 2 deletions(-)
diff --git a/Cubical/Categories/Instances/ZFunctors.agda b/Cubical/Categories/Instances/ZFunctors.agda
index 53517578c4..64141002aa 100644
--- a/Cubical/Categories/Instances/ZFunctors.agda
+++ b/Cubical/Categories/Instances/ZFunctors.agda
@@ -24,6 +24,7 @@ open import Cubical.Data.FinData
open import Cubical.Algebra.Ring
open import Cubical.Algebra.CommRing
open import Cubical.Algebra.CommRing.Localisation
+open import Cubical.Algebra.CommRing.RadicalIdeal
open import Cubical.Algebra.Semilattice
open import Cubical.Algebra.Lattice
open import Cubical.Algebra.DistLattice
@@ -308,9 +309,44 @@ module _ {ℓ : Level} where
-- this is a separated presheaf
-- (TODO: prove this a sheaf)
isSeparatedZarLatFun : isSeparated zariskiCoverage ZarLatFun
- isSeparatedZarLatFun A (unimodvec n f 1∈⟨f₁,⋯,fₙ⟩) u w uRest≡wRest = {!!}
+ isSeparatedZarLatFun A (unimodvec n f 1∈⟨f₁,⋯,fₙ⟩) u w uRest≡wRest =
+ u ≡⟨ sym (∧lLid _) ⟩
+ 1l ∧l u ≡⟨ congL _∧l_ D1≡⋁Dfᵢ ⟩
+ (⋁ (D A ∘ f)) ∧l u ≡⟨ ⋁Meetldist _ _ ⟩
+ ⋁ (λ i → D A (f i) ∧l u) ≡⟨ ⋁Ext Dfᵢ∧u≡Dfᵢ∧w ⟩
+ ⋁ (λ i → D A (f i) ∧l w) ≡⟨ sym (⋁Meetldist _ _) ⟩
+ (⋁ (D A ∘ f)) ∧l w ≡⟨ congL _∧l_ (sym D1≡⋁Dfᵢ) ⟩
+ 1l ∧l w ≡⟨ ∧lLid _ ⟩
+ w ∎
where
- instance _ = A .snd
+ open Join (ZariskiLattice A)
+ open JoinSemilattice (Lattice→JoinSemilattice (DistLattice→Lattice (ZariskiLattice A)))
+ using (IndPoset)
+ open LatticeTheory (DistLattice→Lattice (ZariskiLattice A))
+ open PosetStr (IndPoset .snd)
+ open IsSupport (isSupportD A)
+ open RadicalIdeal A
+ instance
+ _ = A .snd
+ _ = ZariskiLattice A .snd
+
+ D1≡⋁Dfᵢ : 1l ≡ ⋁ (D A ∘ f)
+ D1≡⋁Dfᵢ = is-antisym _ _
+ (supportRadicalIneq f 1r (∈→∈√ _ _ 1∈⟨f₁,⋯,fₙ⟩))
+ (1lRightAnnihilates∨l _)
+
+ Dfᵢ∧u≡Dfᵢ∧w : ∀ i → D A (f i) ∧l u ≡ D A (f i) ∧l w
+ Dfᵢ∧u≡Dfᵢ∧w i =
+ D A (f i) ∧l u
+ ≡⟨ sym (cong fst (funExt⁻ (cong fst toLocToDown≡ToDown) u)) ⟩
+ locToDownHom .fst (inducedZarLatHom /1AsCommRingHom .fst u) .fst
+ ≡⟨ cong (λ x → locToDownHom .fst x .fst) (uRest≡wRest i) ⟩
+ locToDownHom .fst (inducedZarLatHom /1AsCommRingHom .fst w) .fst
+ ≡⟨ cong fst (funExt⁻ (cong fst toLocToDown≡ToDown) w) ⟩
+ D A (f i) ∧l w ∎
+ where
+ open InvertingElementsBase.UniversalProp A (f i)
+ open LocDownSetIso A (f i)
CompactOpen : ℤFunctor → Type (ℓ-suc ℓ)
CompactOpen X = X ⇒ ZarLatFun
From 06bec0786dec040f160d46023c3b174d059260e3 Mon Sep 17 00:00:00 2001
From: mzeuner <max@zeuner.net>
Date: Mon, 29 Jan 2024 17:10:47 +0100
Subject: [PATCH 12/37] locality
---
Cubical/Categories/Instances/ZFunctors.agda | 66 ++++++++++++++++++++-
1 file changed, 65 insertions(+), 1 deletion(-)
diff --git a/Cubical/Categories/Instances/ZFunctors.agda b/Cubical/Categories/Instances/ZFunctors.agda
index 64141002aa..402f18d914 100644
--- a/Cubical/Categories/Instances/ZFunctors.agda
+++ b/Cubical/Categories/Instances/ZFunctors.agda
@@ -40,6 +40,7 @@ open import Cubical.Categories.Instances.CommRings
open import Cubical.Categories.Instances.DistLattice
open import Cubical.Categories.Instances.DistLattices
open import Cubical.Categories.Instances.Functors
+open import Cubical.Categories.Site.Cover
open import Cubical.Categories.Site.Coverage
open import Cubical.Categories.Site.Sheaf
open import Cubical.Categories.Site.Instances.ZariskiCommRing
@@ -249,7 +250,7 @@ module _ {ℓ : Level} where
isAffine : (X : ℤFunctor) → Type (ℓ-suc ℓ)
isAffine X = ∃[ A ∈ CommRing ℓ ] NatIso (Sp .F-ob A) X
- -- TODO: 𝔸¹ ≅ Sp ℤ[x] and 𝔾ₘ ≅ Sp ℤ[x,x⁻¹] as first examples of affine schemes
+ -- TODO: 𝔸¹ ≅ Sp ℤ[x] and 𝔾ₘ ≅ Sp ℤ[x,x⁻¹] ≅ D(x) ↪ 𝔸¹ as first examples of affine schemes
-- The unit is an equivalence iff the ℤ-functor is affine.
@@ -543,6 +544,69 @@ module _ {ℓ : Level} where
isLocal : ℤFunctor → Type (ℓ-suc ℓ)
isLocal X = isSheaf zariskiCoverage X
+ -- Compact opens of Zariski sheaves are sheaves
+ presLocalCompactOpen : (X : ℤFunctor) (U : CompactOpen X) → isLocal X → isLocal ⟦ U ⟧ᶜᵒ
+ presLocalCompactOpen X U isLocalX R um@(unimodvec _ f _) = isoToIsEquiv isoU
+ where
+ open Coverage zariskiCoverage
+ open InvertingElementsBase R
+ instance _ = R .snd
+
+ fᵢCoverR = covers R .snd um
+
+ isoX : Iso (X .F-ob R .fst) (CompatibleFamily X fᵢCoverR)
+ isoX = equivToIso (elementToCompatibleFamily _ _ , isLocalX R um)
+
+ compatibleFamIncl : (CompatibleFamily ⟦ U ⟧ᶜᵒ fᵢCoverR) → (CompatibleFamily X fᵢCoverR)
+ compatibleFamIncl fam = (fst ∘ fst fam)
+ , λ i j B φ ψ φψComm → cong fst (fam .snd i j B φ ψ φψComm)
+
+ compatibleFamIncl≡ : ∀ (y : Σ[ x ∈ X .F-ob R .fst ] U .N-ob R x ≡ D R 1r)
+ → compatibleFamIncl (elementToCompatibleFamily ⟦ U ⟧ᶜᵒ fᵢCoverR y)
+ ≡ elementToCompatibleFamily X fᵢCoverR (y .fst)
+ compatibleFamIncl≡ y = CompatibleFamily≡ _ _ _ _ λ _ → refl
+
+ isoU : Iso (Σ[ x ∈ X .F-ob R .fst ] U .N-ob R x ≡ D R 1r)
+ (CompatibleFamily ⟦ U ⟧ᶜᵒ fᵢCoverR)
+ fun isoU = elementToCompatibleFamily _ _
+ fst (inv isoU fam) = isoX .inv (compatibleFamIncl fam)
+ snd (inv isoU fam) = -- U (x) ≡ D(1)
+ -- knowing that U(x/1)¸≡ D(1) in R[1/fᵢ]
+ let x = isoX .inv (compatibleFamIncl fam) in
+ isSeparatedZarLatFun R um (U .N-ob R x) (D R 1r)
+ λ i → let open UniversalProp (f i)
+ instance _ = R[1/ (f i) ]AsCommRing .snd in
+
+ inducedZarLatHom /1AsCommRingHom .fst (U .N-ob R x)
+
+ ≡⟨ funExt⁻ (sym (U .N-hom /1AsCommRingHom)) x ⟩
+
+ U .N-ob R[1/ (f i) ]AsCommRing (X .F-hom /1AsCommRingHom x)
+
+ ≡⟨ cong (U .N-ob R[1/ f i ]AsCommRing)
+ (funExt⁻ (cong fst (isoX .rightInv (compatibleFamIncl fam))) i) ⟩
+
+ U .N-ob R[1/ (f i) ]AsCommRing (fam .fst i .fst)
+
+ ≡⟨ fam .fst i .snd ⟩
+
+ D R[1/ (f i) ]AsCommRing 1r
+
+ ≡⟨ sym (inducedZarLatHom /1AsCommRingHom .snd .pres1) ⟩
+
+ inducedZarLatHom /1AsCommRingHom .fst (D R 1r) ∎
+
+ rightInv isoU fam =
+ Σ≡Prop (λ _ → isPropIsCompatibleFamily _ _ _)
+ (funExt λ i → Σ≡Prop (λ _ → squash/ _ _)
+ (funExt⁻ (cong fst
+ (isoX .rightInv (compatibleFamIncl fam))) i))
+ leftInv isoU y = Σ≡Prop (λ _ → squash/ _ _)
+ (cong (isoX .inv) (compatibleFamIncl≡ y)
+ ∙ isoX .leftInv (y .fst))
+
+
+ -- definition of quasi-compact, quasi-separated schemes
isQcQsScheme : ℤFunctor → Type (ℓ-suc ℓ)
isQcQsScheme X = isLocal X × hasAffineCover X
From fb225ce4bade6d9c7cc5752af7dce1054e0bc98b Mon Sep 17 00:00:00 2001
From: mzeuner <max@zeuner.net>
Date: Wed, 31 Jan 2024 14:41:19 +0100
Subject: [PATCH 13/37] towards aff cover
---
Cubical/Algebra/DistLattice/BigOps.agda | 16 +-
Cubical/Algebra/Lattice/Base.agda | 14 ++
Cubical/Categories/Instances/ZFunctors.agda | 241 ++++++++++++--------
3 files changed, 171 insertions(+), 100 deletions(-)
diff --git a/Cubical/Algebra/DistLattice/BigOps.agda b/Cubical/Algebra/DistLattice/BigOps.agda
index a812d64641..1d5dfca316 100644
--- a/Cubical/Algebra/DistLattice/BigOps.agda
+++ b/Cubical/Algebra/DistLattice/BigOps.agda
@@ -34,7 +34,7 @@ open import Cubical.Relation.Binary.Order.Poset
private
variable
- ℓ : Level
+ ℓ ℓ' : Level
module KroneckerDelta (L' : DistLattice ℓ) where
private
@@ -107,6 +107,20 @@ module Join (L' : DistLattice ℓ) where
≤-⋁Ext = ≤-bigOpExt
+module JoinMap {L : DistLattice ℓ} {L' : DistLattice ℓ'} (φ : DistLatticeHom L L') where
+ private module L = Join L
+ private module L' = Join L'
+ open IsLatticeHom (φ .snd)
+ open DistLatticeStr ⦃...⦄
+ open Join
+ open BigOpMap (LatticeHom→JoinSemilatticeHom φ)
+ private instance
+ _ = L .snd
+ _ = L' .snd
+
+ pres⋁ : {n : ℕ} (U : FinVec ⟨ L ⟩ n) → φ .fst (L.⋁ U) ≡ L'.⋁ (φ .fst ∘ U)
+ pres⋁ = presBigOp
+
module Meet (L' : DistLattice ℓ) where
private
L = fst L'
diff --git a/Cubical/Algebra/Lattice/Base.agda b/Cubical/Algebra/Lattice/Base.agda
index 7f411bb793..b96cf6c62e 100644
--- a/Cubical/Algebra/Lattice/Base.agda
+++ b/Cubical/Algebra/Lattice/Base.agda
@@ -231,5 +231,19 @@ LatticePath = ∫ 𝒮ᴰ-Lattice .UARel.ua
Lattice→JoinSemilattice : Lattice ℓ → Semilattice ℓ
Lattice→JoinSemilattice (A , latticestr _ _ _ _ L) = semilattice _ _ _ (L .IsLattice.joinSemilattice )
+LatticeHom→JoinSemilatticeHom : {L : Lattice ℓ} {L' : Lattice ℓ'}
+ → LatticeHom L L'
+ → SemilatticeHom (Lattice→JoinSemilattice L) (Lattice→JoinSemilattice L')
+fst (LatticeHom→JoinSemilatticeHom φ) = fst φ
+IsMonoidHom.presε (snd (LatticeHom→JoinSemilatticeHom φ)) = φ .snd .IsLatticeHom.pres0
+IsMonoidHom.pres· (snd (LatticeHom→JoinSemilatticeHom φ)) = φ .snd .IsLatticeHom.pres∨l
+
Lattice→MeetSemilattice : Lattice ℓ → Semilattice ℓ
Lattice→MeetSemilattice (A , latticestr _ _ _ _ L) = semilattice _ _ _ (L .IsLattice.meetSemilattice )
+
+LatticeHom→MeetSemilatticeHom : {L : Lattice ℓ} {L' : Lattice ℓ'}
+ → LatticeHom L L'
+ → SemilatticeHom (Lattice→MeetSemilattice L) (Lattice→MeetSemilattice L')
+fst (LatticeHom→MeetSemilatticeHom φ) = fst φ
+IsMonoidHom.presε (snd (LatticeHom→MeetSemilatticeHom φ)) = φ .snd .IsLatticeHom.pres1
+IsMonoidHom.pres· (snd (LatticeHom→MeetSemilatticeHom φ)) = φ .snd .IsLatticeHom.pres∧l
diff --git a/Cubical/Categories/Instances/ZFunctors.agda b/Cubical/Categories/Instances/ZFunctors.agda
index 402f18d914..04f582b7c5 100644
--- a/Cubical/Categories/Instances/ZFunctors.agda
+++ b/Cubical/Categories/Instances/ZFunctors.agda
@@ -494,6 +494,17 @@ module _ {ℓ : Level} where
N-ob (compOpenGlobalIncl U) A = fst
N-hom (compOpenGlobalIncl U) φ = refl
+ -- this is essentially U∧_
+ compOpenDownHom : (U : CompactOpen X)
+ → DistLatticeHom (CompOpenDistLattice .F-ob X)
+ (CompOpenDistLattice .F-ob ⟦ U ⟧ᶜᵒ)
+ compOpenDownHom U = CompOpenDistLattice .F-hom (compOpenGlobalIncl U)
+
+ compOpenDownHomNatIso : {U V : CompactOpen X}
+ → V ≤ U
+ → NatIso ⟦ V ⟧ᶜᵒ ⟦ compOpenDownHom U .fst V ⟧ᶜᵒ
+ compOpenDownHomNatIso {U = U} {V = V} V≤U = {!!}
+
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
@@ -545,65 +556,65 @@ module _ {ℓ : Level} where
isLocal X = isSheaf zariskiCoverage X
-- Compact opens of Zariski sheaves are sheaves
- presLocalCompactOpen : (X : ℤFunctor) (U : CompactOpen X) → isLocal X → isLocal ⟦ U ⟧ᶜᵒ
- presLocalCompactOpen X U isLocalX R um@(unimodvec _ f _) = isoToIsEquiv isoU
- where
- open Coverage zariskiCoverage
- open InvertingElementsBase R
- instance _ = R .snd
+ -- presLocalCompactOpen : (X : ℤFunctor) (U : CompactOpen X) → isLocal X → isLocal ⟦ U ⟧ᶜᵒ
+ -- presLocalCompactOpen X U isLocalX R um@(unimodvec _ f _) = isoToIsEquiv isoU
+ -- where
+ -- open Coverage zariskiCoverage
+ -- open InvertingElementsBase R
+ -- instance _ = R .snd
- fᵢCoverR = covers R .snd um
+ -- fᵢCoverR = covers R .snd um
- isoX : Iso (X .F-ob R .fst) (CompatibleFamily X fᵢCoverR)
- isoX = equivToIso (elementToCompatibleFamily _ _ , isLocalX R um)
+ -- isoX : Iso (X .F-ob R .fst) (CompatibleFamily X fᵢCoverR)
+ -- isoX = equivToIso (elementToCompatibleFamily _ _ , isLocalX R um)
- compatibleFamIncl : (CompatibleFamily ⟦ U ⟧ᶜᵒ fᵢCoverR) → (CompatibleFamily X fᵢCoverR)
- compatibleFamIncl fam = (fst ∘ fst fam)
- , λ i j B φ ψ φψComm → cong fst (fam .snd i j B φ ψ φψComm)
+ -- compatibleFamIncl : (CompatibleFamily ⟦ U ⟧ᶜᵒ fᵢCoverR) → (CompatibleFamily X fᵢCoverR)
+ -- compatibleFamIncl fam = (fst ∘ fst fam)
+ -- , λ i j B φ ψ φψComm → cong fst (fam .snd i j B φ ψ φψComm)
- compatibleFamIncl≡ : ∀ (y : Σ[ x ∈ X .F-ob R .fst ] U .N-ob R x ≡ D R 1r)
- → compatibleFamIncl (elementToCompatibleFamily ⟦ U ⟧ᶜᵒ fᵢCoverR y)
- ≡ elementToCompatibleFamily X fᵢCoverR (y .fst)
- compatibleFamIncl≡ y = CompatibleFamily≡ _ _ _ _ λ _ → refl
+ -- compatibleFamIncl≡ : ∀ (y : Σ[ x ∈ X .F-ob R .fst ] U .N-ob R x ≡ D R 1r)
+ -- → compatibleFamIncl (elementToCompatibleFamily ⟦ U ⟧ᶜᵒ fᵢCoverR y)
+ -- ≡ elementToCompatibleFamily X fᵢCoverR (y .fst)
+ -- compatibleFamIncl≡ y = CompatibleFamily≡ _ _ _ _ λ _ → refl
- isoU : Iso (Σ[ x ∈ X .F-ob R .fst ] U .N-ob R x ≡ D R 1r)
- (CompatibleFamily ⟦ U ⟧ᶜᵒ fᵢCoverR)
- fun isoU = elementToCompatibleFamily _ _
- fst (inv isoU fam) = isoX .inv (compatibleFamIncl fam)
- snd (inv isoU fam) = -- U (x) ≡ D(1)
- -- knowing that U(x/1)¸≡ D(1) in R[1/fᵢ]
- let x = isoX .inv (compatibleFamIncl fam) in
- isSeparatedZarLatFun R um (U .N-ob R x) (D R 1r)
- λ i → let open UniversalProp (f i)
- instance _ = R[1/ (f i) ]AsCommRing .snd in
+ -- isoU : Iso (Σ[ x ∈ X .F-ob R .fst ] U .N-ob R x ≡ D R 1r)
+ -- (CompatibleFamily ⟦ U ⟧ᶜᵒ fᵢCoverR)
+ -- fun isoU = elementToCompatibleFamily _ _
+ -- fst (inv isoU fam) = isoX .inv (compatibleFamIncl fam)
+ -- snd (inv isoU fam) = -- U (x) ≡ D(1)
+ -- -- knowing that U(x/1)¸≡ D(1) in R[1/fᵢ]
+ -- let x = isoX .inv (compatibleFamIncl fam) in
+ -- isSeparatedZarLatFun R um (U .N-ob R x) (D R 1r)
+ -- λ i → let open UniversalProp (f i)
+ -- instance _ = R[1/ (f i) ]AsCommRing .snd in
- inducedZarLatHom /1AsCommRingHom .fst (U .N-ob R x)
+ -- inducedZarLatHom /1AsCommRingHom .fst (U .N-ob R x)
- ≡⟨ funExt⁻ (sym (U .N-hom /1AsCommRingHom)) x ⟩
+ -- ≡⟨ funExt⁻ (sym (U .N-hom /1AsCommRingHom)) x ⟩
- U .N-ob R[1/ (f i) ]AsCommRing (X .F-hom /1AsCommRingHom x)
+ -- U .N-ob R[1/ (f i) ]AsCommRing (X .F-hom /1AsCommRingHom x)
- ≡⟨ cong (U .N-ob R[1/ f i ]AsCommRing)
- (funExt⁻ (cong fst (isoX .rightInv (compatibleFamIncl fam))) i) ⟩
+ -- ≡⟨ cong (U .N-ob R[1/ f i ]AsCommRing)
+ -- (funExt⁻ (cong fst (isoX .rightInv (compatibleFamIncl fam))) i) ⟩
- U .N-ob R[1/ (f i) ]AsCommRing (fam .fst i .fst)
+ -- U .N-ob R[1/ (f i) ]AsCommRing (fam .fst i .fst)
- ≡⟨ fam .fst i .snd ⟩
+ -- ≡⟨ fam .fst i .snd ⟩
- D R[1/ (f i) ]AsCommRing 1r
+ -- D R[1/ (f i) ]AsCommRing 1r
- ≡⟨ sym (inducedZarLatHom /1AsCommRingHom .snd .pres1) ⟩
+ -- ≡⟨ sym (inducedZarLatHom /1AsCommRingHom .snd .pres1) ⟩
- inducedZarLatHom /1AsCommRingHom .fst (D R 1r) ∎
+ -- inducedZarLatHom /1AsCommRingHom .fst (D R 1r) ∎
- rightInv isoU fam =
- Σ≡Prop (λ _ → isPropIsCompatibleFamily _ _ _)
- (funExt λ i → Σ≡Prop (λ _ → squash/ _ _)
- (funExt⁻ (cong fst
- (isoX .rightInv (compatibleFamIncl fam))) i))
- leftInv isoU y = Σ≡Prop (λ _ → squash/ _ _)
- (cong (isoX .inv) (compatibleFamIncl≡ y)
- ∙ isoX .leftInv (y .fst))
+ -- rightInv isoU fam =
+ -- Σ≡Prop (λ _ → isPropIsCompatibleFamily _ _ _)
+ -- (funExt λ i → Σ≡Prop (λ _ → squash/ _ _)
+ -- (funExt⁻ (cong fst
+ -- (isoX .rightInv (compatibleFamIncl fam))) i))
+ -- leftInv isoU y = Σ≡Prop (λ _ → squash/ _ _)
+ -- (cong (isoX .inv) (compatibleFamIncl≡ y)
+ -- ∙ isoX .leftInv (y .fst))
-- definition of quasi-compact, quasi-separated schemes
@@ -675,63 +686,95 @@ module _ {ℓ : Level} (R : CommRing ℓ) (f : R .fst) where
isAffineD = ∣ R[1/ f ]AsCommRing , SpR[1/f]≅⟦Df⟧ ∣₁
--- module _ {ℓ : Level} (R : CommRing ℓ) (W : CompactOpen (Sp ⟅ R ⟆)) where
-
--- open Iso
--- open Functor
--- open NatTrans
--- open NatIso
--- open isIso
--- open DistLatticeStr ⦃...⦄
--- open CommRingStr ⦃...⦄
--- open PosetStr ⦃...⦄
--- open IsRingHom
--- open RingHoms
--- open IsLatticeHom
--- open ZarLat
-
-
--- open JoinSemilattice (Lattice→JoinSemilattice (DistLattice→Lattice (CompOpenDistLattice .F-ob (Sp .F-ob R)))) using (IndPoset)
--- open InvertingElementsBase R
--- open Join
--- open AffineCover
--- module ZL = ZarLatUniversalProp
-
--- private
--- instance
--- _ = R .snd
--- _ = ZariskiLattice R .snd
--- _ = CompOpenDistLattice .F-ob (Sp .F-ob R) .snd
--- _ = CompOpenDistLattice .F-ob ⟦ W ⟧ᶜᵒ .snd
--- _ = IndPoset .snd
-
--- private
--- w : ZL R
--- w = yonedaᴾ ZarLatFun R .fun W
-
--- module _ {n : ℕ}
--- (α : FinVec (fst R) n)
--- (⋁Dα≡w : ⋁ (ZariskiLattice R) (ZL.D R ∘ α) ≡ w) where
-
--- ⋁Dα≡W : ⋁ (CompOpenDistLattice ⟅ Sp ⟅ R ⟆ ⟆) (D R ∘ α) ≡ W
--- ⋁Dα≡W = makeNatTransPath (funExt₂ (λ A φ → {!!}))
--- where
--- foo : (A : CommRing ℓ) (φ : CommRingHom R A) → inducedZarLatHom φ .fst w ≡ W .N-ob A φ
--- foo A φ i = cong N-ob (yonedaᴾ ZarLatFun R .leftInv W) i A φ
-
--- Dα≤W : ∀ i → D R (α i) ≤ W
--- Dα≤W i = {!!}
--- -- ⋁ (D αᵢ) ≡ W in SpR → 𝓛
-
--- toAffineCover : AffineCover ⟦ W ⟧ᶜᵒ
--- AffineCover.n toAffineCover = n
--- U toAffineCover i = compOpenGlobalIncl (Sp ⟅ R ⟆) W ●ᵛ D R (α i) -- W → Sp R → 𝓛 via Dαᵢ
--- covers toAffineCover = makeNatTransPath (funExt₂ (λ A y → ({!!} ∙ funExt⁻ (funExt⁻ (cong N-ob ⋁Dα≡W) A) (fst y)) ∙ y .snd))
--- isAffineU toAffineCover = {!!}
- -- ⟦ Dαᵢ ∘ W→SpR ⟧ ≅ ⟦ Dαᵢ ⟧ ≅ Sp R[1/αᵢ]
+module _ {ℓ : Level} (R : CommRing ℓ) (W : CompactOpen (Sp ⟅ R ⟆)) where
+
+ open Iso
+ open Functor
+ open NatTrans
+ open NatIso
+ open isIso
+ open DistLatticeStr ⦃...⦄
+ open CommRingStr ⦃...⦄
+ open PosetStr ⦃...⦄
+ open IsRingHom
+ open RingHoms
+ open IsLatticeHom
+ open ZarLat
+
+
+ open JoinSemilattice (Lattice→JoinSemilattice (DistLattice→Lattice (CompOpenDistLattice .F-ob (Sp .F-ob R)))) using (IndPoset; ind≤bigOp)
+ open InvertingElementsBase R
+ open Join
+ open JoinMap
+ open AffineCover
+ module ZL = ZarLatUniversalProp
+
+ private
+ instance
+ _ = R .snd
+ _ = ZariskiLattice R .snd
+ _ = CompOpenDistLattice .F-ob (Sp .F-ob R) .snd
+ _ = CompOpenDistLattice .F-ob ⟦ W ⟧ᶜᵒ .snd
+ _ = IndPoset .snd
+
+ w : ZL R
+ w = yonedaᴾ ZarLatFun R .fun W
+
+ -- yoneda is a lattice homomorphsim
+ isHomYoneda : IsLatticeHom (DistLattice→Lattice (ZariskiLattice R) .snd)
+ (yonedaᴾ ZarLatFun R .inv)
+ (DistLattice→Lattice (CompOpenDistLattice ⟅ Sp ⟅ R ⟆ ⟆) .snd)
+ isHomYoneda = {!!}
+
+ module _ {n : ℕ}
+ (f : FinVec (fst R) n)
+ (⋁Df≡W : ⋁ (CompOpenDistLattice ⟅ Sp ⟅ R ⟆ ⟆) (D R ∘ f) ≡ W) where
+
+ Df≤W : ∀ i → D R (f i) ≤ W
+ Df≤W i = subst (D R (f i) ≤_) ⋁Df≡W (ind≤bigOp (D R ∘ f) i)
+
+ toAffineCover : AffineCover ⟦ W ⟧ᶜᵒ
+ AffineCover.n toAffineCover = n
+ U toAffineCover i = compOpenDownHom (Sp ⟅ R ⟆) W .fst (D R (f i))
+ covers toAffineCover = sym (pres⋁ (compOpenDownHom (Sp ⟅ R ⟆) W) (D R ∘ f))
+ ∙ cong (compOpenDownHom (Sp ⟅ R ⟆) W .fst) ⋁Df≡W
+ ∙ makeNatTransPath (funExt₂ (λ _ → snd))
+ isAffineU toAffineCover i =
+ ∣ _ , seqNatIso (SpR[1/f]≅⟦Df⟧ R (f i)) (compOpenDownHomNatIso _ (Df≤W i)) ∣₁
+
+ module _ {n : ℕ}
+ (f : FinVec (fst R) n)
+ (⋁Df≡w : ⋁ (ZariskiLattice R) (ZL.D R ∘ f) ≡ w) where
+
+ ⋁Df≡W : ⋁ (CompOpenDistLattice ⟅ Sp ⟅ R ⟆ ⟆) (D R ∘ f) ≡ W
+ ⋁Df≡W = sym (pres⋁ (_ , isHomYoneda) (ZL.D R ∘ f))
+ ∙ cong (yonedaᴾ ZarLatFun R .inv) ⋁Df≡w
+ ∙ yonedaᴾ ZarLatFun R .leftInv W
+
+ makeAffineCover : AffineCover ⟦ W ⟧ᶜᵒ
+ makeAffineCover = toAffineCover f ⋁Df≡W
+
+ hasAffineCoverCompOpenOfAffine : hasAffineCover ⟦ W ⟧ᶜᵒ
+ hasAffineCoverCompOpenOfAffine = {!!}
-- then use ⋁D≡ (merely covered by standard opens) → hasAffineCover ⟦W⟧
- -- then isLocal ⟦W⟧
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
-- 𝓛 separated presheaf:
-- For u w : 𝓛 A and ⟨f₀,...,fₙ⟩=A s.t. ∀ i → uᵢ=wᵢ in 𝓛 A[1/fᵢ] then u = w
From 96b601628e43d8de4df4904ef64f4f837a2f0b39 Mon Sep 17 00:00:00 2001
From: mzeuner <max@zeuner.net>
Date: Wed, 31 Jan 2024 22:08:21 +0100
Subject: [PATCH 14/37] give up
---
Cubical/Categories/Instances/ZFunctors.agda | 143 ++++++++++++--------
1 file changed, 89 insertions(+), 54 deletions(-)
diff --git a/Cubical/Categories/Instances/ZFunctors.agda b/Cubical/Categories/Instances/ZFunctors.agda
index 04f582b7c5..98c5b3e5d7 100644
--- a/Cubical/Categories/Instances/ZFunctors.agda
+++ b/Cubical/Categories/Instances/ZFunctors.agda
@@ -33,7 +33,7 @@ open import Cubical.Algebra.ZariskiLattice.Base
open import Cubical.Algebra.ZariskiLattice.UniversalProperty
open import Cubical.Algebra.ZariskiLattice.Properties
-open import Cubical.Categories.Category
+open import Cubical.Categories.Category renaming (isIso to isIsoC)
open import Cubical.Categories.Functor
open import Cubical.Categories.Instances.Sets
open import Cubical.Categories.Instances.CommRings
@@ -459,7 +459,7 @@ module _ {ℓ : Level} where
module _ (X : ℤFunctor) where
- open isIso
+ open isIsoC
private instance _ = (CompOpenDistLattice .F-ob X) .snd
compOpenTopNatIso : NatIso X ⟦ 1l ⟧ᶜᵒ
@@ -471,10 +471,11 @@ module _ {ℓ : Level} where
module _ (X : ℤFunctor) where
+ open isIsoC
open Join (CompOpenDistLattice .F-ob X)
open JoinSemilattice (Lattice→JoinSemilattice (DistLattice→Lattice (CompOpenDistLattice .F-ob X)))
open PosetStr (IndPoset .snd) hiding (_≤_)
- open LatticeTheory ⦃...⦄ -- ((DistLattice→Lattice (CompOpenDistLattice .F-ob X)))
+ open LatticeTheory ⦃...⦄
private instance _ = (CompOpenDistLattice .F-ob X) .snd
record AffineCover : Type (ℓ-suc ℓ) where
@@ -500,10 +501,37 @@ module _ {ℓ : Level} where
(CompOpenDistLattice .F-ob ⟦ U ⟧ᶜᵒ)
compOpenDownHom U = CompOpenDistLattice .F-hom (compOpenGlobalIncl U)
+ -- termination issues
compOpenDownHomNatIso : {U V : CompactOpen X}
→ V ≤ U
→ NatIso ⟦ V ⟧ᶜᵒ ⟦ compOpenDownHom U .fst V ⟧ᶜᵒ
- compOpenDownHomNatIso {U = U} {V = V} V≤U = {!!}
+ compOpenDownHomNatIso = {!!}
+
+ compOpenDownHomIncl : {U V : CompactOpen X}
+ → V ≤ U
+ → ⟦ V ⟧ᶜᵒ ⇒ ⟦ compOpenDownHom U .fst V ⟧ᶜᵒ
+ N-ob (compOpenDownHomIncl {U = U} {V = V} V≤U) A (x , Vx≡D1) =
+ (x , path) , Vx≡D1
+ 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 (compOpenDownHomIncl V≤U) φ =
+ funExt (λ x → Σ≡Prop (λ _ → squash/ _ _) (Σ≡Prop (λ _ → squash/ _ _) refl))
+
+ isIsoCompOpenDownHomIncl : {U V : CompactOpen X} (V≤U : V ≤ U)
+ (A : CommRing ℓ) → isIsoC (SET ℓ) (compOpenDownHomIncl V≤U .N-ob A)
+ inv (isIsoCompOpenDownHomIncl V≤U A) ((x , Ux≡D1) , Vx≡D1) = x , Vx≡D1
+ sec (isIsoCompOpenDownHomIncl V≤U A) = funExt λ _ → Σ≡Prop (λ _ → squash/ _ _) (Σ≡Prop (λ _ → squash/ _ _) refl)
+ ret (isIsoCompOpenDownHomIncl V≤U A) = funExt λ _ → Σ≡Prop (λ _ → squash/ _ _) refl
+
+
compOpenIncl : {U V : CompactOpen X} → V ≤ U → ⟦ V ⟧ᶜᵒ ⇒ ⟦ U ⟧ᶜᵒ
N-ob (compOpenIncl {U = U} {V = V} V≤U) A (x , Vx≡D1) = x , path
@@ -556,65 +584,65 @@ module _ {ℓ : Level} where
isLocal X = isSheaf zariskiCoverage X
-- Compact opens of Zariski sheaves are sheaves
- -- presLocalCompactOpen : (X : ℤFunctor) (U : CompactOpen X) → isLocal X → isLocal ⟦ U ⟧ᶜᵒ
- -- presLocalCompactOpen X U isLocalX R um@(unimodvec _ f _) = isoToIsEquiv isoU
- -- where
- -- open Coverage zariskiCoverage
- -- open InvertingElementsBase R
- -- instance _ = R .snd
+ presLocalCompactOpen : (X : ℤFunctor) (U : CompactOpen X) → isLocal X → isLocal ⟦ U ⟧ᶜᵒ
+ presLocalCompactOpen X U isLocalX R um@(unimodvec _ f _) = isoToIsEquiv isoU
+ where
+ open Coverage zariskiCoverage
+ open InvertingElementsBase R
+ instance _ = R .snd
- -- fᵢCoverR = covers R .snd um
+ fᵢCoverR = covers R .snd um
- -- isoX : Iso (X .F-ob R .fst) (CompatibleFamily X fᵢCoverR)
- -- isoX = equivToIso (elementToCompatibleFamily _ _ , isLocalX R um)
+ isoX : Iso (X .F-ob R .fst) (CompatibleFamily X fᵢCoverR)
+ isoX = equivToIso (elementToCompatibleFamily _ _ , isLocalX R um)
- -- compatibleFamIncl : (CompatibleFamily ⟦ U ⟧ᶜᵒ fᵢCoverR) → (CompatibleFamily X fᵢCoverR)
- -- compatibleFamIncl fam = (fst ∘ fst fam)
- -- , λ i j B φ ψ φψComm → cong fst (fam .snd i j B φ ψ φψComm)
+ compatibleFamIncl : (CompatibleFamily ⟦ U ⟧ᶜᵒ fᵢCoverR) → (CompatibleFamily X fᵢCoverR)
+ compatibleFamIncl fam = (fst ∘ fst fam)
+ , λ i j B φ ψ φψComm → cong fst (fam .snd i j B φ ψ φψComm)
- -- compatibleFamIncl≡ : ∀ (y : Σ[ x ∈ X .F-ob R .fst ] U .N-ob R x ≡ D R 1r)
- -- → compatibleFamIncl (elementToCompatibleFamily ⟦ U ⟧ᶜᵒ fᵢCoverR y)
- -- ≡ elementToCompatibleFamily X fᵢCoverR (y .fst)
- -- compatibleFamIncl≡ y = CompatibleFamily≡ _ _ _ _ λ _ → refl
+ compatibleFamIncl≡ : ∀ (y : Σ[ x ∈ X .F-ob R .fst ] U .N-ob R x ≡ D R 1r)
+ → compatibleFamIncl (elementToCompatibleFamily ⟦ U ⟧ᶜᵒ fᵢCoverR y)
+ ≡ elementToCompatibleFamily X fᵢCoverR (y .fst)
+ compatibleFamIncl≡ y = CompatibleFamily≡ _ _ _ _ λ _ → refl
- -- isoU : Iso (Σ[ x ∈ X .F-ob R .fst ] U .N-ob R x ≡ D R 1r)
- -- (CompatibleFamily ⟦ U ⟧ᶜᵒ fᵢCoverR)
- -- fun isoU = elementToCompatibleFamily _ _
- -- fst (inv isoU fam) = isoX .inv (compatibleFamIncl fam)
- -- snd (inv isoU fam) = -- U (x) ≡ D(1)
- -- -- knowing that U(x/1)¸≡ D(1) in R[1/fᵢ]
- -- let x = isoX .inv (compatibleFamIncl fam) in
- -- isSeparatedZarLatFun R um (U .N-ob R x) (D R 1r)
- -- λ i → let open UniversalProp (f i)
- -- instance _ = R[1/ (f i) ]AsCommRing .snd in
+ isoU : Iso (Σ[ x ∈ X .F-ob R .fst ] U .N-ob R x ≡ D R 1r)
+ (CompatibleFamily ⟦ U ⟧ᶜᵒ fᵢCoverR)
+ fun isoU = elementToCompatibleFamily _ _
+ fst (inv isoU fam) = isoX .inv (compatibleFamIncl fam)
+ snd (inv isoU fam) = -- U (x) ≡ D(1)
+ -- knowing that U(x/1)¸≡ D(1) in R[1/fᵢ]
+ let x = isoX .inv (compatibleFamIncl fam) in
+ isSeparatedZarLatFun R um (U .N-ob R x) (D R 1r)
+ λ i → let open UniversalProp (f i)
+ instance _ = R[1/ (f i) ]AsCommRing .snd in
- -- inducedZarLatHom /1AsCommRingHom .fst (U .N-ob R x)
+ inducedZarLatHom /1AsCommRingHom .fst (U .N-ob R x)
- -- ≡⟨ funExt⁻ (sym (U .N-hom /1AsCommRingHom)) x ⟩
+ ≡⟨ funExt⁻ (sym (U .N-hom /1AsCommRingHom)) x ⟩
- -- U .N-ob R[1/ (f i) ]AsCommRing (X .F-hom /1AsCommRingHom x)
+ U .N-ob R[1/ (f i) ]AsCommRing (X .F-hom /1AsCommRingHom x)
- -- ≡⟨ cong (U .N-ob R[1/ f i ]AsCommRing)
- -- (funExt⁻ (cong fst (isoX .rightInv (compatibleFamIncl fam))) i) ⟩
+ ≡⟨ cong (U .N-ob R[1/ f i ]AsCommRing)
+ (funExt⁻ (cong fst (isoX .rightInv (compatibleFamIncl fam))) i) ⟩
- -- U .N-ob R[1/ (f i) ]AsCommRing (fam .fst i .fst)
+ U .N-ob R[1/ (f i) ]AsCommRing (fam .fst i .fst)
- -- ≡⟨ fam .fst i .snd ⟩
+ ≡⟨ fam .fst i .snd ⟩
- -- D R[1/ (f i) ]AsCommRing 1r
+ D R[1/ (f i) ]AsCommRing 1r
- -- ≡⟨ sym (inducedZarLatHom /1AsCommRingHom .snd .pres1) ⟩
+ ≡⟨ sym (inducedZarLatHom /1AsCommRingHom .snd .pres1) ⟩
- -- inducedZarLatHom /1AsCommRingHom .fst (D R 1r) ∎
+ inducedZarLatHom /1AsCommRingHom .fst (D R 1r) ∎
- -- rightInv isoU fam =
- -- Σ≡Prop (λ _ → isPropIsCompatibleFamily _ _ _)
- -- (funExt λ i → Σ≡Prop (λ _ → squash/ _ _)
- -- (funExt⁻ (cong fst
- -- (isoX .rightInv (compatibleFamIncl fam))) i))
- -- leftInv isoU y = Σ≡Prop (λ _ → squash/ _ _)
- -- (cong (isoX .inv) (compatibleFamIncl≡ y)
- -- ∙ isoX .leftInv (y .fst))
+ rightInv isoU fam =
+ Σ≡Prop (λ _ → isPropIsCompatibleFamily _ _ _)
+ (funExt λ i → Σ≡Prop (λ _ → squash/ _ _)
+ (funExt⁻ (cong fst
+ (isoX .rightInv (compatibleFamIncl fam))) i))
+ leftInv isoU y = Σ≡Prop (λ _ → squash/ _ _)
+ (cong (isoX .inv) (compatibleFamIncl≡ y)
+ ∙ isoX .leftInv (y .fst))
-- definition of quasi-compact, quasi-separated schemes
@@ -634,7 +662,7 @@ module _ {ℓ : Level} (R : CommRing ℓ) (f : R .fst) where
open Functor
open NatTrans
open NatIso
- open isIso
+ open isIsoC
open DistLatticeStr ⦃...⦄
open CommRingStr ⦃...⦄
open IsRingHom
@@ -692,7 +720,7 @@ module _ {ℓ : Level} (R : CommRing ℓ) (W : CompactOpen (Sp ⟅ R ⟆)) where
open Functor
open NatTrans
open NatIso
- open isIso
+ open isIsoC
open DistLatticeStr ⦃...⦄
open CommRingStr ⦃...⦄
open PosetStr ⦃...⦄
@@ -724,7 +752,13 @@ module _ {ℓ : Level} (R : CommRing ℓ) (W : CompactOpen (Sp ⟅ R ⟆)) where
isHomYoneda : IsLatticeHom (DistLattice→Lattice (ZariskiLattice R) .snd)
(yonedaᴾ ZarLatFun R .inv)
(DistLattice→Lattice (CompOpenDistLattice ⟅ Sp ⟅ R ⟆ ⟆) .snd)
- isHomYoneda = {!!}
+ pres0 isHomYoneda = makeNatTransPath (funExt₂ (λ _ _ → refl))
+ pres1 isHomYoneda =
+ makeNatTransPath (funExt₂ (λ _ φ → inducedZarLatHom φ .snd .pres1))
+ pres∨l isHomYoneda u v =
+ makeNatTransPath (funExt₂ (λ _ φ → inducedZarLatHom φ .snd .pres∨l u v))
+ pres∧l isHomYoneda u v =
+ makeNatTransPath (funExt₂ (λ _ φ → inducedZarLatHom φ .snd .pres∧l u v))
module _ {n : ℕ}
(f : FinVec (fst R) n)
@@ -755,9 +789,10 @@ module _ {ℓ : Level} (R : CommRing ℓ) (W : CompactOpen (Sp ⟅ R ⟆)) where
makeAffineCover = toAffineCover f ⋁Df≡W
hasAffineCoverCompOpenOfAffine : hasAffineCover ⟦ W ⟧ᶜᵒ
- hasAffineCoverCompOpenOfAffine = {!!}
-
- -- then use ⋁D≡ (merely covered by standard opens) → hasAffineCover ⟦W⟧
+ hasAffineCoverCompOpenOfAffine = PT.map truncHelper ([]surjective w)
+ where
+ truncHelper : Σ[ n,f ∈ Σ ℕ (FinVec (fst R)) ] [ n,f ] ≡ w → AffineCover ⟦ W ⟧ᶜᵒ
+ truncHelper ((n , f) , [n,f]≡w) = makeAffineCover f (ZL.⋁D≡ R f ∙ [n,f]≡w)
From 2e19a725f719491d499b803f94dfb4459921e4dd Mon Sep 17 00:00:00 2001
From: mzeuner <max@zeuner.net>
Date: Thu, 1 Feb 2024 14:13:10 +0100
Subject: [PATCH 15/37] finish
---
Cubical/Categories/Instances/ZFunctors.agda | 83 ++++++++++-----------
1 file changed, 39 insertions(+), 44 deletions(-)
diff --git a/Cubical/Categories/Instances/ZFunctors.agda b/Cubical/Categories/Instances/ZFunctors.agda
index 98c5b3e5d7..4c25b0d058 100644
--- a/Cubical/Categories/Instances/ZFunctors.agda
+++ b/Cubical/Categories/Instances/ZFunctors.agda
@@ -501,38 +501,35 @@ module _ {ℓ : Level} where
(CompOpenDistLattice .F-ob ⟦ U ⟧ᶜᵒ)
compOpenDownHom U = CompOpenDistLattice .F-hom (compOpenGlobalIncl U)
- -- termination issues
- compOpenDownHomNatIso : {U V : CompactOpen X}
- → V ≤ U
- → NatIso ⟦ V ⟧ᶜᵒ ⟦ compOpenDownHom U .fst V ⟧ᶜᵒ
- compOpenDownHomNatIso = {!!}
-
- compOpenDownHomIncl : {U V : CompactOpen X}
- → V ≤ U
- → ⟦ V ⟧ᶜᵒ ⇒ ⟦ compOpenDownHom U .fst V ⟧ᶜᵒ
- N-ob (compOpenDownHomIncl {U = U} {V = V} V≤U) A (x , Vx≡D1) =
- (x , path) , Vx≡D1
- 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 (compOpenDownHomIncl V≤U) φ =
- funExt (λ x → Σ≡Prop (λ _ → squash/ _ _) (Σ≡Prop (λ _ → squash/ _ _) refl))
-
- isIsoCompOpenDownHomIncl : {U V : CompactOpen X} (V≤U : V ≤ U)
- (A : CommRing ℓ) → isIsoC (SET ℓ) (compOpenDownHomIncl V≤U .N-ob A)
- inv (isIsoCompOpenDownHomIncl V≤U A) ((x , Ux≡D1) , Vx≡D1) = x , Vx≡D1
- sec (isIsoCompOpenDownHomIncl V≤U A) = funExt λ _ → Σ≡Prop (λ _ → squash/ _ _) (Σ≡Prop (λ _ → squash/ _ _) refl)
- ret (isIsoCompOpenDownHomIncl V≤U A) = funExt λ _ → Σ≡Prop (λ _ → squash/ _ _) refl
-
-
-
+ -- termination issues!!!
+ -- I don't understand what's going on???
+ module _ {U V : CompactOpen X} (V≤U : V ≤ U) where
+ private
+ compOpenDownHomFun : (A : CommRing ℓ)
+ → ⟦ V ⟧ᶜᵒ .F-ob A .fst
+ → ⟦ compOpenDownHom U .fst V ⟧ᶜᵒ .F-ob A .fst
+ compOpenDownHomFun A (x , Vx≡D1) = (x , path) , Vx≡D1
+ 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 ∎
+
+ compOpenDownHomNatIso : NatIso ⟦ V ⟧ᶜᵒ ⟦ compOpenDownHom U .fst V ⟧ᶜᵒ
+ N-ob (trans compOpenDownHomNatIso) = compOpenDownHomFun
+ N-hom (trans compOpenDownHomNatIso) _ =
+ funExt λ _ → Σ≡Prop (λ _ → squash/ _ _) (Σ≡Prop (λ _ → squash/ _ _) refl)
+ inv (nIso compOpenDownHomNatIso A) ((x , Ux≡D1) , Vx≡D1) = x , Vx≡D1
+ sec (nIso compOpenDownHomNatIso A) =
+ funExt λ _ → Σ≡Prop (λ _ → squash/ _ _) (Σ≡Prop (λ _ → squash/ _ _) refl)
+ ret (nIso compOpenDownHomNatIso A) = funExt λ _ → Σ≡Prop (λ _ → squash/ _ _) refl
+
+ -- code duplication!
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
@@ -562,11 +559,6 @@ module _ {ℓ : Level} where
F-id strDLSh = cong (𝓞 .F-hom) compOpenInclId ∙ 𝓞 .F-id
F-seq strDLSh _ _ = cong (𝓞 .F-hom) (compOpenInclSeq _ _) ∙ 𝓞 .F-seq _ _
- -- ⟦ U ⟧ → X → 𝓛 via V
- -- compOpenRest : {U V : CompactOpen X} → V ≤ U → CompactOpen ⟦ U ⟧ᶜᵒ
- -- N-ob (compOpenRest {V = V} V≤U) A (x , Ux≡D1) = V .N-ob A x
- -- N-hom (compOpenRest V≤U) φ = funExt (λ x → {!!})
-
-- the canonical one element affine cover of a representable
module _ (A : CommRing ℓ) where
open AffineCover
@@ -776,25 +768,28 @@ module _ {ℓ : Level} (R : CommRing ℓ) (W : CompactOpen (Sp ⟅ R ⟆)) where
isAffineU toAffineCover i =
∣ _ , seqNatIso (SpR[1/f]≅⟦Df⟧ R (f i)) (compOpenDownHomNatIso _ (Df≤W i)) ∣₁
- module _ {n : ℕ}
- (f : FinVec (fst R) n)
- (⋁Df≡w : ⋁ (ZariskiLattice R) (ZL.D R ∘ f) ≡ w) where
+ module _ {n : ℕ}
+ (f : FinVec (fst R) n)
+ (⋁Df≡w : ⋁ (ZariskiLattice R) (ZL.D R ∘ f) ≡ w) where
+ private
⋁Df≡W : ⋁ (CompOpenDistLattice ⟅ Sp ⟅ R ⟆ ⟆) (D R ∘ f) ≡ W
⋁Df≡W = sym (pres⋁ (_ , isHomYoneda) (ZL.D R ∘ f))
∙ cong (yonedaᴾ ZarLatFun R .inv) ⋁Df≡w
∙ yonedaᴾ ZarLatFun R .leftInv W
- makeAffineCover : AffineCover ⟦ W ⟧ᶜᵒ
- makeAffineCover = toAffineCover f ⋁Df≡W
+ makeAffineCoverCompOpenOfAffine : AffineCover ⟦ W ⟧ᶜᵒ
+ makeAffineCoverCompOpenOfAffine = toAffineCover f ⋁Df≡W
hasAffineCoverCompOpenOfAffine : hasAffineCover ⟦ W ⟧ᶜᵒ
hasAffineCoverCompOpenOfAffine = PT.map truncHelper ([]surjective w)
where
truncHelper : Σ[ n,f ∈ Σ ℕ (FinVec (fst R)) ] [ n,f ] ≡ w → AffineCover ⟦ W ⟧ᶜᵒ
- truncHelper ((n , f) , [n,f]≡w) = makeAffineCover f (ZL.⋁D≡ R f ∙ [n,f]≡w)
-
+ truncHelper ((n , f) , [n,f]≡w) = makeAffineCoverCompOpenOfAffine f (ZL.⋁D≡ R f ∙ [n,f]≡w)
+ isQcQsSchemeCompOpenOfAffine : isQcQsScheme ⟦ W ⟧ᶜᵒ
+ fst isQcQsSchemeCompOpenOfAffine = presLocalCompactOpen _ _ (isSubcanonicalZariskiCoverage R)
+ snd isQcQsSchemeCompOpenOfAffine = hasAffineCoverCompOpenOfAffine
From 9f024343409f9551bdead9a186bc38c59cc6f7f9 Mon Sep 17 00:00:00 2001
From: mzeuner <max@zeuner.net>
Date: Thu, 1 Feb 2024 14:21:59 +0100
Subject: [PATCH 16/37] cleanup
---
Cubical/Categories/Instances/ZFunctors.agda | 108 +++++++-------------
1 file changed, 38 insertions(+), 70 deletions(-)
diff --git a/Cubical/Categories/Instances/ZFunctors.agda b/Cubical/Categories/Instances/ZFunctors.agda
index 4c25b0d058..cb230b7504 100644
--- a/Cubical/Categories/Instances/ZFunctors.agda
+++ b/Cubical/Categories/Instances/ZFunctors.agda
@@ -478,19 +478,6 @@ module _ {ℓ : Level} where
open LatticeTheory ⦃...⦄
private instance _ = (CompOpenDistLattice .F-ob X) .snd
- record AffineCover : Type (ℓ-suc ℓ) where
- field
- n : ℕ
- U : FinVec (CompactOpen X) n
- covers : ⋁ U ≡ 1l -- TODO: equivalent to X ≡ ⟦ ⋁ U ⟧ᶜᵒ
- isAffineU : ∀ i → isAffineCompactOpen (U i)
-
- hasAffineCover : Type (ℓ-suc ℓ)
- hasAffineCover = ∥ AffineCover ∥₁
-
- -- the structure sheaf
- private COᵒᵖ = (DistLatticeCategory (CompOpenDistLattice .F-ob X)) ^op
-
compOpenGlobalIncl : (U : CompactOpen X) → ⟦ U ⟧ᶜᵒ ⇒ X
N-ob (compOpenGlobalIncl U) A = fst
N-hom (compOpenGlobalIncl U) φ = refl
@@ -553,23 +540,35 @@ module _ {ℓ : Level} where
compOpenInclSeq _ _ = makeNatTransPath
(funExt₂ (λ _ _ → Σ≡Prop (λ _ → squash/ _ _) refl))
+
+ -- the structure sheaf
+ private COᵒᵖ = (DistLatticeCategory (CompOpenDistLattice .F-ob X)) ^op
+
strDLSh : Functor COᵒᵖ (CommRingsCategory {ℓ = ℓ-suc ℓ})
F-ob strDLSh U = 𝓞 .F-ob ⟦ U ⟧ᶜᵒ
F-hom strDLSh U≥V = 𝓞 .F-hom (compOpenIncl U≥V)
F-id strDLSh = cong (𝓞 .F-hom) compOpenInclId ∙ 𝓞 .F-id
F-seq strDLSh _ _ = cong (𝓞 .F-hom) (compOpenInclSeq _ _) ∙ 𝓞 .F-seq _ _
- -- the canonical one element affine cover of a representable
- module _ (A : CommRing ℓ) where
- open AffineCover
- private instance _ = (CompOpenDistLattice ⟅ Sp ⟅ A ⟆ ⟆) .snd
- singlAffineCover : AffineCover (Sp .F-ob A)
- n singlAffineCover = 1
- U singlAffineCover zero = 1l
- covers singlAffineCover = ∨lRid _
- isAffineU singlAffineCover zero = ∣ A , compOpenTopNatIso (Sp ⟅ A ⟆) ∣₁
+ -- def. affine cover and locality for definition of qcqs-scheme
+ module _ (X : ℤFunctor) where
+ open isIsoC
+ open Join (CompOpenDistLattice .F-ob X)
+ open JoinSemilattice (Lattice→JoinSemilattice (DistLattice→Lattice (CompOpenDistLattice .F-ob X)))
+ open PosetStr (IndPoset .snd) hiding (_≤_)
+ open LatticeTheory ⦃...⦄
+ private instance _ = (CompOpenDistLattice .F-ob X) .snd
+ record AffineCover : Type (ℓ-suc ℓ) where
+ field
+ n : ℕ
+ U : FinVec (CompactOpen X) n
+ covers : ⋁ U ≡ 1l -- TODO: equivalent to X ≡ ⟦ ⋁ U ⟧ᶜᵒ
+ isAffineU : ∀ i → isAffineCompactOpen (U i)
+
+ hasAffineCover : Type (ℓ-suc ℓ)
+ hasAffineCover = ∥ AffineCover ∥₁
-- qcqs-schemes as Zariski sheaves (local ℤ-functors) with an affine cover in the sense above
isLocal : ℤFunctor → Type (ℓ-suc ℓ)
@@ -641,10 +640,23 @@ module _ {ℓ : Level} where
isQcQsScheme : ℤFunctor → Type (ℓ-suc ℓ)
isQcQsScheme X = isLocal X × hasAffineCover X
+
-- affine schemes are qcqs-schemes
- isQcQsSchemeAffine : ∀ (A : CommRing ℓ) → isQcQsScheme (Sp .F-ob A)
- fst (isQcQsSchemeAffine A) = isSubcanonicalZariskiCoverage A
- snd (isQcQsSchemeAffine A) = ∣ singlAffineCover A ∣₁
+ module _ (A : CommRing ℓ) where
+ open AffineCover
+ private instance _ = (CompOpenDistLattice ⟅ Sp ⟅ A ⟆ ⟆) .snd
+
+ -- the canonical one element affine cover of a representable
+ singlAffineCover : AffineCover (Sp .F-ob A)
+ n singlAffineCover = 1
+ U singlAffineCover zero = 1l
+ covers singlAffineCover = ∨lRid _
+ isAffineU singlAffineCover zero = ∣ A , X≅⟦1⟧ (Sp ⟅ A ⟆) ∣₁
+
+ isQcQsSchemeAffine : isQcQsScheme (Sp .F-ob A)
+ fst isQcQsSchemeAffine = isSubcanonicalZariskiCoverage A
+ snd isQcQsSchemeAffine = ∣ singlAffineCover ∣₁
+
-- standard affine opens
-- TODO: separate file?
@@ -706,6 +718,7 @@ module _ {ℓ : Level} (R : CommRing ℓ) (f : R .fst) where
isAffineD = ∣ R[1/ f ]AsCommRing , SpR[1/f]≅⟦Df⟧ ∣₁
+-- compact opens of affine schemes are qcqs-schemes
module _ {ℓ : Level} (R : CommRing ℓ) (W : CompactOpen (Sp ⟅ R ⟆)) where
open Iso
@@ -790,48 +803,3 @@ module _ {ℓ : Level} (R : CommRing ℓ) (W : CompactOpen (Sp ⟅ R ⟆)) where
isQcQsSchemeCompOpenOfAffine : isQcQsScheme ⟦ W ⟧ᶜᵒ
fst isQcQsSchemeCompOpenOfAffine = presLocalCompactOpen _ _ (isSubcanonicalZariskiCoverage R)
snd isQcQsSchemeCompOpenOfAffine = hasAffineCoverCompOpenOfAffine
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
- -- 𝓛 separated presheaf:
- -- For u w : 𝓛 A and ⟨f₀,...,fₙ⟩=A s.t. ∀ i → uᵢ=wᵢ in 𝓛 A[1/fᵢ] then u = w
- -- where u ↦ uᵢ for 𝓛 A → 𝓛 A[1/fᵢ]
- -- Min: u : 𝓛 A and ⟨f₀,...,fₙ⟩=A s.t. ∀ i → uᵢ=D1 in 𝓛 A[1/fᵢ] then u = D1 in 𝓛 A
- -- base case: u = Dg → have ∀ i → g/1 ∈ A[1/fᵢ]ˣ, need 1 ∈ √⟨g⟩ (g ∈ Aˣ)
- -- g/1 ∈ A[1/fᵢ]ˣ → fᵢ ∈ √ ⟨g⟩ → 1=∑aᵢfᵢ ∈ √⟨g⟩
- -- i.e. fᵢᵐ=aᵢg
- -- choose m big enough s.t. it becomes independent of i
- -- lemma ⟨f₀ᵐ,...,fₙᵐ⟩=A:
- -- 1 = ∑ bᵢfᵢᵐ = ∑ bᵢaᵢg = (∑ aᵢbᵢ)g
-
- -- u = D(g₁,...,gₖ) → ⟨g₁/1 ,..., gₖ/1 ⟩ = A[1/fᵢ]
- -- 0 = A[1/fᵢ]/⟨g₁/1,...,gₖ/1⟩ =???= A/⟨g₁,...,gₙ⟩[1/[fᵢ]] → fᵢⁿ=0 mod ⟨g₁,...,gₙ⟩
- -- 1/1 = ∑ aⱼ/fᵢⁿ gⱼ/1 → fᵢᵐ = ∑ aⱼgⱼ
- -- use InvertingElementsBase.invElPropElimN to get uniform exponent
- -- → fᵢ ∈ √ ⟨ g₁ ,..., gₖ ⟩ → 1 = ∑ bᵢfᵢ ∈ √ ⟨ g₁ ,..., gₖ ⟩
-
- -- 𝓛 sheaf: ⟨f₀,...,fₙ⟩=A → 𝓛 A = lim (↓ Dfᵢ) = lim (𝓛 A[1/fᵢ])
- -- ⋁uᵢ=⊤ in L → L = lim (↓ uᵢ) = Σ[ vᵢ ≤ uᵢ ] vᵢ ∧ uⱼ = vⱼ ∧ uᵢ
- -- (↓ Dfᵢ) = 𝓛 A[1/fᵢ]: Dg ≤ Dfᵢ ⇔ g ∈ √ ⟨fᵢ⟩ ⇔ fᵢ ∈ A[1/g]ˣ
- -- ↓ Dfᵢ → 𝓛 A[1/fᵢ]: Dg ≤ Dfᵢ ↦ D(g/1)
-
- -- 𝓛 A[1/fᵢ] → ↓ Dfᵢ: D(g/fᵢⁿ) ↦ Dg ∧ Dfᵢ = D(gfᵢ)
- -- support A[1/fᵢ] → ↓ Dfᵢ given by g/fᵢⁿ ↦ Dg ∧ Dfᵢ = D(gfᵢ)
- -- support A → A[1/fᵢ] → L gives (↓ Dfᵢ) ↪ 𝓛 A → L lattice hom!
- -- have _∧Dfᵢ : 𝓛 A → ↓ Dfᵢ
-
- -- U : CompactOpen X , isQcQsScheme X → isQcQsScheme ⟦U⟧
- -- X=⋁Uᵢ affine covering → isQcQsScheme U∧Uᵢ →(lemma)→ isQcQsScheme U=⋁(U∧Uᵢ)
From e582d077b787fd1f761ce969305c3839b2ac9f63 Mon Sep 17 00:00:00 2001
From: mzeuner <max@zeuner.net>
Date: Mon, 26 Feb 2024 17:16:15 +0100
Subject: [PATCH 17/37] use inline ring solver
---
Cubical/Algebra/ZariskiLattice/Properties.agda | 5 +----
1 file changed, 1 insertion(+), 4 deletions(-)
diff --git a/Cubical/Algebra/ZariskiLattice/Properties.agda b/Cubical/Algebra/ZariskiLattice/Properties.agda
index e95011a5eb..4de676d2b3 100644
--- a/Cubical/Algebra/ZariskiLattice/Properties.agda
+++ b/Cubical/Algebra/ZariskiLattice/Properties.agda
@@ -101,11 +101,8 @@ module _ (R : CommRing ℓ) where
→ f ∈ₚ R ˣ
fgHelper (α , 1ⁿ≡α₀f+0) = α zero , path
where
- useSolver : ∀ f α₀ → f · α₀ ≡ α₀ · f + 0r
- useSolver = solve R
-
path : f · α zero ≡ 1r
- path = f · α zero ≡⟨ useSolver _ _ ⟩
+ path = f · α zero ≡⟨ solve! R ⟩
α zero · f + 0r ≡⟨ sym 1ⁿ≡α₀f+0 ⟩
1r ^ n ≡⟨ 1ⁿ≡1 n ⟩
1r ∎
From a340591c60bad3617c6a5a1ee881c87f8bd10376 Mon Sep 17 00:00:00 2001
From: mzeuner <max@zeuner.net>
Date: Mon, 26 Feb 2024 17:29:46 +0100
Subject: [PATCH 18/37] fix
---
Cubical/Categories/Instances/ZFunctors.agda | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/Cubical/Categories/Instances/ZFunctors.agda b/Cubical/Categories/Instances/ZFunctors.agda
index cb230b7504..e675ba9007 100644
--- a/Cubical/Categories/Instances/ZFunctors.agda
+++ b/Cubical/Categories/Instances/ZFunctors.agda
@@ -651,7 +651,7 @@ module _ {ℓ : Level} where
n singlAffineCover = 1
U singlAffineCover zero = 1l
covers singlAffineCover = ∨lRid _
- isAffineU singlAffineCover zero = ∣ A , X≅⟦1⟧ (Sp ⟅ A ⟆) ∣₁
+ isAffineU singlAffineCover zero = ∣ A , compOpenTopNatIso (Sp ⟅ A ⟆) ∣₁
isQcQsSchemeAffine : isQcQsScheme (Sp .F-ob A)
fst isQcQsSchemeAffine = isSubcanonicalZariskiCoverage A
From e286103bc686a66980e8e0d3bf35af0fb106e163 Mon Sep 17 00:00:00 2001
From: mzeuner <max@zeuner.net>
Date: Mon, 26 Feb 2024 17:34:11 +0100
Subject: [PATCH 19/37] more fixes
---
Cubical/Categories/Site/Instances/ZariskiCommRing.agda | 4 +---
1 file changed, 1 insertion(+), 3 deletions(-)
diff --git a/Cubical/Categories/Site/Instances/ZariskiCommRing.agda b/Cubical/Categories/Site/Instances/ZariskiCommRing.agda
index ecdce68dce..9d86d30c23 100644
--- a/Cubical/Categories/Site/Instances/ZariskiCommRing.agda
+++ b/Cubical/Categories/Site/Instances/ZariskiCommRing.agda
@@ -8,10 +8,9 @@ open import Cubical.Foundations.Function
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Structure
-open import Cubical.Data.Nat using (ℕ ; zero ; suc)
+open import Cubical.Data.Nat using (ℕ)
open import Cubical.Data.Sigma
open import Cubical.Data.FinData
-open import Cubical.Data.FinData.Order renaming (_<'Fin_ to _<_)
open import Cubical.Algebra.Ring
open import Cubical.Algebra.Ring.BigOps
@@ -21,7 +20,6 @@ open import Cubical.Algebra.CommRing.Ideal
open import Cubical.Algebra.CommRing.FGIdeal
open import Cubical.Categories.Category
-open import Cubical.Categories.Limits.Terminal
open import Cubical.Categories.Instances.CommRings
open import Cubical.Categories.Site.Coverage
open import Cubical.Categories.Site.Sheaf
From b43c46409c2a959049aab1dcf8d56a9ab30a5cf5 Mon Sep 17 00:00:00 2001
From: Matthias Hutzler <matthias-hutzler@posteo.net>
Date: Tue, 27 Feb 2024 12:04:39 +0100
Subject: [PATCH 20/37] fix accidentally public module
manually cherry-picked from 93d52b57c6356b209b086fc9752445c05670b59e
---
Cubical/Categories/Instances/ZFunctors.agda | 3 +--
1 file changed, 1 insertion(+), 2 deletions(-)
diff --git a/Cubical/Categories/Instances/ZFunctors.agda b/Cubical/Categories/Instances/ZFunctors.agda
index e675ba9007..2bd90300fb 100644
--- a/Cubical/Categories/Instances/ZFunctors.agda
+++ b/Cubical/Categories/Instances/ZFunctors.agda
@@ -734,13 +734,12 @@ module _ {ℓ : Level} (R : CommRing ℓ) (W : CompactOpen (Sp ⟅ R ⟆)) where
open IsLatticeHom
open ZarLat
-
open JoinSemilattice (Lattice→JoinSemilattice (DistLattice→Lattice (CompOpenDistLattice .F-ob (Sp .F-ob R)))) using (IndPoset; ind≤bigOp)
open InvertingElementsBase R
open Join
open JoinMap
open AffineCover
- module ZL = ZarLatUniversalProp
+ private module ZL = ZarLatUniversalProp
private
instance
From 13cc5e80b1421a65a64d6729fece658128c5a461 Mon Sep 17 00:00:00 2001
From: Matthias Hutzler <matthias-hutzler@posteo.net>
Date: Tue, 27 Feb 2024 12:12:16 +0100
Subject: [PATCH 21/37] avoid code duplication
manually cherry-picked from 73cc74aba2c0968c987e25d3a5d1855a7e1ec037
---
Cubical/Categories/Instances/ZFunctors.agda | 41 ++++++++-------------
1 file changed, 15 insertions(+), 26 deletions(-)
diff --git a/Cubical/Categories/Instances/ZFunctors.agda b/Cubical/Categories/Instances/ZFunctors.agda
index 2bd90300fb..37d56666e3 100644
--- a/Cubical/Categories/Instances/ZFunctors.agda
+++ b/Cubical/Categories/Instances/ZFunctors.agda
@@ -482,6 +482,20 @@ module _ {ℓ : Level} where
N-ob (compOpenGlobalIncl U) A = fst
N-hom (compOpenGlobalIncl U) φ = refl
+ compOpenIncl : {U V : CompactOpen X} → V ≤ U → ⟦ V ⟧ᶜᵒ ⇒ ⟦ U ⟧ᶜᵒ
+ N-ob (compOpenIncl {U = U} {V = V} V≤U) A (x , Vx≡D1) = x , path
+ where
+ instance
+ _ = A .snd
+ _ = ZariskiLattice A .snd
+ _ = DistLattice→Lattice (ZariskiLattice A)
+ path : U .N-ob A x ≡ D A 1r
+ path = U .N-ob A x ≡⟨ funExt⁻ (funExt⁻ (cong N-ob (sym V≤U)) A) x ⟩
+ V .N-ob A x ∨l U .N-ob A x ≡⟨ cong (_∨l U .N-ob A x) Vx≡D1 ⟩
+ D A 1r ∨l U .N-ob A x ≡⟨ 1lLeftAnnihilates∨l _ ⟩
+ D A 1r ∎
+ N-hom (compOpenIncl V≤U) φ = funExt λ x → Σ≡Prop (λ _ → squash/ _ _) refl
+
-- this is essentially U∧_
compOpenDownHom : (U : CompactOpen X)
→ DistLatticeHom (CompOpenDistLattice .F-ob X)
@@ -495,17 +509,7 @@ module _ {ℓ : Level} where
compOpenDownHomFun : (A : CommRing ℓ)
→ ⟦ V ⟧ᶜᵒ .F-ob A .fst
→ ⟦ compOpenDownHom U .fst V ⟧ᶜᵒ .F-ob A .fst
- compOpenDownHomFun A (x , Vx≡D1) = (x , path) , Vx≡D1
- 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 ∎
+ compOpenDownHomFun A v = (compOpenIncl V≤U ⟦ A ⟧) v , snd v
compOpenDownHomNatIso : NatIso ⟦ V ⟧ᶜᵒ ⟦ compOpenDownHom U .fst V ⟧ᶜᵒ
N-ob (trans compOpenDownHomNatIso) = compOpenDownHomFun
@@ -516,21 +520,6 @@ module _ {ℓ : Level} where
funExt λ _ → Σ≡Prop (λ _ → squash/ _ _) (Σ≡Prop (λ _ → squash/ _ _) refl)
ret (nIso compOpenDownHomNatIso A) = funExt λ _ → Σ≡Prop (λ _ → squash/ _ _) refl
- -- code duplication!
- 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))
From 05bec8785e77fcd348defab8f745ac4e4ec51919 Mon Sep 17 00:00:00 2001
From: Matthias Hutzler <matthias-hutzler@posteo.net>
Date: Tue, 27 Feb 2024 12:16:34 +0100
Subject: [PATCH 22/37] improve comment
manually cherry-picked from 2c4d6d13f1d60ab2cf334cd6a5255b4df418216c
---
Cubical/Categories/Instances/ZFunctors.agda | 4 ++--
1 file changed, 2 insertions(+), 2 deletions(-)
diff --git a/Cubical/Categories/Instances/ZFunctors.agda b/Cubical/Categories/Instances/ZFunctors.agda
index 37d56666e3..1c0e7b7174 100644
--- a/Cubical/Categories/Instances/ZFunctors.agda
+++ b/Cubical/Categories/Instances/ZFunctors.agda
@@ -502,9 +502,9 @@ module _ {ℓ : Level} where
(CompOpenDistLattice .F-ob ⟦ U ⟧ᶜᵒ)
compOpenDownHom U = CompOpenDistLattice .F-hom (compOpenGlobalIncl U)
- -- termination issues!!!
- -- I don't understand what's going on???
module _ {U V : CompactOpen X} (V≤U : V ≤ U) where
+ -- We need this separate definition to avoid termination checker issues,
+ -- but we don't understand why.
private
compOpenDownHomFun : (A : CommRing ℓ)
→ ⟦ V ⟧ᶜᵒ .F-ob A .fst
From 78b463c331ff1f26ebee1165ba1f888c2f75b1ea Mon Sep 17 00:00:00 2001
From: Matthias Hutzler <matthias-hutzler@posteo.net>
Date: Tue, 27 Feb 2024 12:18:18 +0100
Subject: [PATCH 23/37] slightly improve comment
---
Cubical/Categories/Instances/ZFunctors.agda | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/Cubical/Categories/Instances/ZFunctors.agda b/Cubical/Categories/Instances/ZFunctors.agda
index 1c0e7b7174..da875ca8e4 100644
--- a/Cubical/Categories/Instances/ZFunctors.agda
+++ b/Cubical/Categories/Instances/ZFunctors.agda
@@ -300,7 +300,7 @@ module _ {ℓ : Level} where
open ZarLat
open ZarLatUniversalProp
- -- the Zariski lattice classifying compact open subobjects
+ -- the Zariski lattice functor classifying compact open subobjects
ZarLatFun : ℤFunctor {ℓ = ℓ}
F-ob ZarLatFun A = ZL A , SQ.squash/
F-hom ZarLatFun φ = inducedZarLatHom φ .fst
From 855146be343536de1fe6fcb489538ba6d9cb6e65 Mon Sep 17 00:00:00 2001
From: Matthias Hutzler <matthias-hutzler@posteo.net>
Date: Tue, 27 Feb 2024 12:20:55 +0100
Subject: [PATCH 24/37] named module StandardOpens
manually cherry-picked from d41b1781fcc273fe3445bf10be23e895c29f3939
---
Cubical/Categories/Instances/ZFunctors.agda | 4 +++-
1 file changed, 3 insertions(+), 1 deletion(-)
diff --git a/Cubical/Categories/Instances/ZFunctors.agda b/Cubical/Categories/Instances/ZFunctors.agda
index da875ca8e4..faec14ebef 100644
--- a/Cubical/Categories/Instances/ZFunctors.agda
+++ b/Cubical/Categories/Instances/ZFunctors.agda
@@ -649,7 +649,7 @@ module _ {ℓ : Level} where
-- standard affine opens
-- TODO: separate file?
-module _ {ℓ : Level} (R : CommRing ℓ) (f : R .fst) where
+module StandardOpens {ℓ : Level} (R : CommRing ℓ) (f : R .fst) where
open Iso
open Functor
@@ -710,6 +710,8 @@ module _ {ℓ : Level} (R : CommRing ℓ) (f : R .fst) where
-- compact opens of affine schemes are qcqs-schemes
module _ {ℓ : Level} (R : CommRing ℓ) (W : CompactOpen (Sp ⟅ R ⟆)) where
+ open StandardOpens
+
open Iso
open Functor
open NatTrans
From 0e100d78a5951004101530fbd968410f05db20e8 Mon Sep 17 00:00:00 2001
From: Matthias Hutzler <matthias-hutzler@posteo.net>
Date: Tue, 27 Feb 2024 13:09:07 +0100
Subject: [PATCH 25/37] indent by two spaces
---
.../Binary/Order/Poset/Properties.agda | 32 +++++++++----------
1 file changed, 16 insertions(+), 16 deletions(-)
diff --git a/Cubical/Relation/Binary/Order/Poset/Properties.agda b/Cubical/Relation/Binary/Order/Poset/Properties.agda
index 50d6f9b6ab..8687e58706 100644
--- a/Cubical/Relation/Binary/Order/Poset/Properties.agda
+++ b/Cubical/Relation/Binary/Order/Poset/Properties.agda
@@ -75,19 +75,19 @@ Poset→StrictPoset (_ , pos)
module PosetDownset (P' : Poset ℓ ℓ') where
- private P = fst P'
- open PosetStr (snd P')
-
- ↓ : P → Type (ℓ-max ℓ ℓ')
- ↓ u = Σ[ v ∈ P ] v ≤ u
-
- ↓ᴾ : P → Poset (ℓ-max ℓ ℓ') ℓ'
- fst (↓ᴾ u) = ↓ u
- PosetStr._≤_ (snd (↓ᴾ u)) v w = v .fst ≤ w .fst
- IsPoset.is-set (PosetStr.isPoset (snd (↓ᴾ u))) =
- isSetΣSndProp is-set λ _ → is-prop-valued _ _
- IsPoset.is-prop-valued (PosetStr.isPoset (snd (↓ᴾ u))) _ _ = is-prop-valued _ _
- IsPoset.is-refl (PosetStr.isPoset (snd (↓ᴾ u))) _ = is-refl _
- IsPoset.is-trans (PosetStr.isPoset (snd (↓ᴾ u))) _ _ _ = is-trans _ _ _
- IsPoset.is-antisym (PosetStr.isPoset (snd (↓ᴾ u))) _ _ v≤w w≤v =
- Σ≡Prop (λ _ → is-prop-valued _ _) (is-antisym _ _ v≤w w≤v)
+ private P = fst P'
+ open PosetStr (snd P')
+
+ ↓ : P → Type (ℓ-max ℓ ℓ')
+ ↓ u = Σ[ v ∈ P ] v ≤ u
+
+ ↓ᴾ : P → Poset (ℓ-max ℓ ℓ') ℓ'
+ fst (↓ᴾ u) = ↓ u
+ PosetStr._≤_ (snd (↓ᴾ u)) v w = v .fst ≤ w .fst
+ IsPoset.is-set (PosetStr.isPoset (snd (↓ᴾ u))) =
+ isSetΣSndProp is-set λ _ → is-prop-valued _ _
+ IsPoset.is-prop-valued (PosetStr.isPoset (snd (↓ᴾ u))) _ _ = is-prop-valued _ _
+ IsPoset.is-refl (PosetStr.isPoset (snd (↓ᴾ u))) _ = is-refl _
+ IsPoset.is-trans (PosetStr.isPoset (snd (↓ᴾ u))) _ _ _ = is-trans _ _ _
+ IsPoset.is-antisym (PosetStr.isPoset (snd (↓ᴾ u))) _ _ v≤w w≤v =
+ Σ≡Prop (λ _ → is-prop-valued _ _) (is-antisym _ _ v≤w w≤v)
From 87db220f5e30150031347793dc123117b1f58684 Mon Sep 17 00:00:00 2001
From: Matthias Hutzler <matthias-hutzler@posteo.net>
Date: Tue, 27 Feb 2024 13:35:44 +0100
Subject: [PATCH 26/37] less whitespace
---
Cubical/Relation/Binary/Order/Poset/Properties.agda | 1 -
1 file changed, 1 deletion(-)
diff --git a/Cubical/Relation/Binary/Order/Poset/Properties.agda b/Cubical/Relation/Binary/Order/Poset/Properties.agda
index 8687e58706..d99bae864b 100644
--- a/Cubical/Relation/Binary/Order/Poset/Properties.agda
+++ b/Cubical/Relation/Binary/Order/Poset/Properties.agda
@@ -73,7 +73,6 @@ Poset→StrictPoset (_ , pos)
(isPoset→isStrictPosetIrreflKernel (PosetStr.isPoset pos))
-
module PosetDownset (P' : Poset ℓ ℓ') where
private P = fst P'
open PosetStr (snd P')
From 76d4035876bd07bb2dc6825b95c3738168a0722c Mon Sep 17 00:00:00 2001
From: Matthias Hutzler <matthias-hutzler@posteo.net>
Date: Tue, 27 Feb 2024 15:09:05 +0100
Subject: [PATCH 27/37] avoid duplication in PosetDownset
---
Cubical/Relation/Binary/Order/Poset/Properties.agda | 12 +++++-------
1 file changed, 5 insertions(+), 7 deletions(-)
diff --git a/Cubical/Relation/Binary/Order/Poset/Properties.agda b/Cubical/Relation/Binary/Order/Poset/Properties.agda
index d99bae864b..a3122fb1ca 100644
--- a/Cubical/Relation/Binary/Order/Poset/Properties.agda
+++ b/Cubical/Relation/Binary/Order/Poset/Properties.agda
@@ -83,10 +83,8 @@ module PosetDownset (P' : Poset ℓ ℓ') where
↓ᴾ : P → Poset (ℓ-max ℓ ℓ') ℓ'
fst (↓ᴾ u) = ↓ u
PosetStr._≤_ (snd (↓ᴾ u)) v w = v .fst ≤ w .fst
- IsPoset.is-set (PosetStr.isPoset (snd (↓ᴾ u))) =
- isSetΣSndProp is-set λ _ → is-prop-valued _ _
- IsPoset.is-prop-valued (PosetStr.isPoset (snd (↓ᴾ u))) _ _ = is-prop-valued _ _
- IsPoset.is-refl (PosetStr.isPoset (snd (↓ᴾ u))) _ = is-refl _
- IsPoset.is-trans (PosetStr.isPoset (snd (↓ᴾ u))) _ _ _ = is-trans _ _ _
- IsPoset.is-antisym (PosetStr.isPoset (snd (↓ᴾ u))) _ _ v≤w w≤v =
- Σ≡Prop (λ _ → is-prop-valued _ _) (is-antisym _ _ v≤w w≤v)
+ PosetStr.isPoset (snd (↓ᴾ u)) =
+ isPosetInduced
+ (PosetStr.isPoset (snd P'))
+ _
+ (EmbeddingΣProp (λ a → is-prop-valued _ _))
From 56e25824c40f8a98d49cc19157f7922053fe7e9f Mon Sep 17 00:00:00 2001
From: Matthias Hutzler <matthias-hutzler@posteo.net>
Date: Thu, 29 Feb 2024 12:37:35 +0100
Subject: [PATCH 28/37] fix copy-paste errors in comment
---
Cubical/Algebra/DistLattice/BigOps.agda | 4 ++--
1 file changed, 2 insertions(+), 2 deletions(-)
diff --git a/Cubical/Algebra/DistLattice/BigOps.agda b/Cubical/Algebra/DistLattice/BigOps.agda
index 1d5dfca316..7b68a1a81b 100644
--- a/Cubical/Algebra/DistLattice/BigOps.agda
+++ b/Cubical/Algebra/DistLattice/BigOps.agda
@@ -1,5 +1,5 @@
--- define ⋁ and ⋀ as the bigOps of a Ring when interpreted
--- as an additive/multiplicative monoid
+-- define ⋁ and ⋀ as the bigOps of a DistLattice when interpreted
+-- as a join/meet semilattice
{-# OPTIONS --safe #-}
module Cubical.Algebra.DistLattice.BigOps where
From fbe4f93938d399750e0b9d45d9f344553eda8921 Mon Sep 17 00:00:00 2001
From: Matthias Hutzler <matthias-hutzler@posteo.net>
Date: Thu, 29 Feb 2024 12:55:39 +0100
Subject: [PATCH 29/37] cleanup JoinMap
---
Cubical/Algebra/DistLattice/BigOps.agda | 7 +------
1 file changed, 1 insertion(+), 6 deletions(-)
diff --git a/Cubical/Algebra/DistLattice/BigOps.agda b/Cubical/Algebra/DistLattice/BigOps.agda
index 7b68a1a81b..1586f3b7f0 100644
--- a/Cubical/Algebra/DistLattice/BigOps.agda
+++ b/Cubical/Algebra/DistLattice/BigOps.agda
@@ -110,17 +110,12 @@ module Join (L' : DistLattice ℓ) where
module JoinMap {L : DistLattice ℓ} {L' : DistLattice ℓ'} (φ : DistLatticeHom L L') where
private module L = Join L
private module L' = Join L'
- open IsLatticeHom (φ .snd)
- open DistLatticeStr ⦃...⦄
- open Join
open BigOpMap (LatticeHom→JoinSemilatticeHom φ)
- private instance
- _ = L .snd
- _ = L' .snd
pres⋁ : {n : ℕ} (U : FinVec ⟨ L ⟩ n) → φ .fst (L.⋁ U) ≡ L'.⋁ (φ .fst ∘ U)
pres⋁ = presBigOp
+
module Meet (L' : DistLattice ℓ) where
private
L = fst L'
From c051569762058dc5961b6a7cb4e4b7455486fafe Mon Sep 17 00:00:00 2001
From: Matthias Hutzler <matthias-hutzler@posteo.net>
Date: Thu, 29 Feb 2024 13:36:31 +0100
Subject: [PATCH 30/37] don't re-prove monoid lemmas
---
Cubical/Algebra/Lattice/Properties.agda | 18 +++---------------
Cubical/Algebra/ZariskiLattice/Properties.agda | 2 +-
2 files changed, 4 insertions(+), 16 deletions(-)
diff --git a/Cubical/Algebra/Lattice/Properties.agda b/Cubical/Algebra/Lattice/Properties.agda
index 4b28da2f88..e1c812c59c 100644
--- a/Cubical/Algebra/Lattice/Properties.agda
+++ b/Cubical/Algebra/Lattice/Properties.agda
@@ -48,23 +48,11 @@ module LatticeTheory (L' : Lattice ℓ) where
1lRightAnnihilates∨l : ∀ (x : L) → x ∨l 1l ≡ 1l
1lRightAnnihilates∨l _ = ∨lComm _ _ ∙ 1lLeftAnnihilates∨l _
-
- ∧lCommAssocl : ∀ x y z → x ∧l (y ∧l z) ≡ y ∧l (x ∧l z)
- ∧lCommAssocl x y z = ∧lAssoc x y z ∙∙ congL _∧l_ (∧lComm x y) ∙∙ sym (∧lAssoc y x z)
-
- ∧lCommAssocr : ∀ x y z → (x ∧l y) ∧l z ≡ (x ∧l z) ∧l y
- ∧lCommAssocr x y z = sym (∧lAssoc x y z) ∙∙ congR _∧l_ (∧lComm y z) ∙∙ ∧lAssoc x z y
-
- ∧lCommAssocr2 : ∀ x y z → (x ∧l y) ∧l z ≡ (z ∧l y) ∧l x
- ∧lCommAssocr2 x y z = ∧lCommAssocr _ _ _ ∙∙ congL _∧l_ (∧lComm _ _) ∙∙ ∧lCommAssocr _ _ _
-
- ∧lCommAssocSwap : ∀ x y z w → (x ∧l y) ∧l (z ∧l w) ≡ (x ∧l z) ∧l (y ∧l w)
- ∧lCommAssocSwap x y z w =
- ∧lAssoc (x ∧l y) z w ∙∙ congL _∧l_ (∧lCommAssocr x y z) ∙∙ sym (∧lAssoc (x ∧l z) y w)
+ module ∧l where
+ open CommMonoidTheory (Semilattice→CommMonoid (Lattice→MeetSemilattice L')) public
∧lLdist∧l : ∀ x y z → x ∧l (y ∧l z) ≡ (x ∧l y) ∧l (x ∧l z)
- ∧lLdist∧l x y z = congL _∧l_ (sym (∧lIdem _)) ∙ ∧lCommAssocSwap x x y z
-
+ ∧lLdist∧l x y z = congL _∧l_ (sym (∧lIdem _)) ∙ ∧l.commAssocSwap x x y z
module Order (L' : Lattice ℓ) where
diff --git a/Cubical/Algebra/ZariskiLattice/Properties.agda b/Cubical/Algebra/ZariskiLattice/Properties.agda
index 4de676d2b3..7214241ffb 100644
--- a/Cubical/Algebra/ZariskiLattice/Properties.agda
+++ b/Cubical/Algebra/ZariskiLattice/Properties.agda
@@ -149,7 +149,7 @@ module LocDownSetIso (R : CommRing ℓ) (f : R .fst) where
locEqPowerLemma r fⁿ fⁿIsPow =
D R f ∧l D R (r · fⁿ) ≡⟨ cong (D R f ∧l_) (isSupportD R .·≡∧ _ _) ⟩
D R f ∧l (D R r ∧l D R fⁿ) ≡⟨ ∧lAssoc (D R f) (D R r) (D R fⁿ) ⟩
- (D R f ∧l D R r) ∧l D R fⁿ ≡⟨ ∧lCommAssocr (D R f) (D R r) (D R fⁿ) ⟩
+ (D R f ∧l D R r) ∧l D R fⁿ ≡⟨ ∧l.commAssocr (D R f) (D R r) (D R fⁿ) ⟩
(D R f ∧l D R fⁿ) ∧l D R r ≡⟨ cong (_∧l D R r) (powerLemma _ fⁿIsPow) ⟩
D R f ∧l D R r ∎
From cc9b29419c71cb3631de7c195d451d3e2056829c Mon Sep 17 00:00:00 2001
From: Matthias Hutzler <matthias-hutzler@posteo.net>
Date: Thu, 29 Feb 2024 13:42:35 +0100
Subject: [PATCH 31/37] slightly clearer comment
---
Cubical/Algebra/Lattice/Properties.agda | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/Cubical/Algebra/Lattice/Properties.agda b/Cubical/Algebra/Lattice/Properties.agda
index e1c812c59c..9e59a5dfec 100644
--- a/Cubical/Algebra/Lattice/Properties.agda
+++ b/Cubical/Algebra/Lattice/Properties.agda
@@ -79,7 +79,7 @@ module Order (L' : Lattice ℓ) where
IndPosetPath : JoinPoset ≡ MeetPoset
IndPosetPath = PosetPath _ _ .fst ((idEquiv _) , isposetequiv ≤Equiv )
- -- transport inequalities from ≤m to ≤j
+ -- transport some inequalities from ≤m to ≤j
∧lIsMinJoin : ∀ x y z → z ≤j x → z ≤j y → z ≤j x ∧l y
∧lIsMinJoin _ _ _ z≤jx z≤jy = ≤m→≤j _ _ (∧lIsMin _ _ _ (≤j→≤m _ _ z≤jx) (≤j→≤m _ _ z≤jy))
From 758e50f20d85a727063b8b6a2dc7af0b26c8c1bb Mon Sep 17 00:00:00 2001
From: Matthias Hutzler <matthias-hutzler@posteo.net>
Date: Thu, 29 Feb 2024 13:48:02 +0100
Subject: [PATCH 32/37] polish module definition
---
Cubical/Algebra/Lattice/Properties.agda | 4 ++--
1 file changed, 2 insertions(+), 2 deletions(-)
diff --git a/Cubical/Algebra/Lattice/Properties.agda b/Cubical/Algebra/Lattice/Properties.agda
index 9e59a5dfec..7051f72a54 100644
--- a/Cubical/Algebra/Lattice/Properties.agda
+++ b/Cubical/Algebra/Lattice/Properties.agda
@@ -48,8 +48,8 @@ module LatticeTheory (L' : Lattice ℓ) where
1lRightAnnihilates∨l : ∀ (x : L) → x ∨l 1l ≡ 1l
1lRightAnnihilates∨l _ = ∨lComm _ _ ∙ 1lLeftAnnihilates∨l _
- module ∧l where
- open CommMonoidTheory (Semilattice→CommMonoid (Lattice→MeetSemilattice L')) public
+ -- Provide an interface to CommMonoid lemmas about _∧l_.
+ module ∧l = CommMonoidTheory (Semilattice→CommMonoid (Lattice→MeetSemilattice L'))
∧lLdist∧l : ∀ x y z → x ∧l (y ∧l z) ≡ (x ∧l y) ∧l (x ∧l z)
∧lLdist∧l x y z = congL _∧l_ (sym (∧lIdem _)) ∙ ∧l.commAssocSwap x x y z
From 04644091aef1c7a7835b5142fade4ac1d16f5d52 Mon Sep 17 00:00:00 2001
From: Matthias Hutzler <matthias-hutzler@posteo.net>
Date: Thu, 29 Feb 2024 23:20:51 +0100
Subject: [PATCH 33/37] cleanup imports
---
.../Algebra/ZariskiLattice/Properties.agda | 31 +++----------------
1 file changed, 4 insertions(+), 27 deletions(-)
diff --git a/Cubical/Algebra/ZariskiLattice/Properties.agda b/Cubical/Algebra/ZariskiLattice/Properties.agda
index 7214241ffb..f552208598 100644
--- a/Cubical/Algebra/ZariskiLattice/Properties.agda
+++ b/Cubical/Algebra/ZariskiLattice/Properties.agda
@@ -4,51 +4,32 @@ module Cubical.Algebra.ZariskiLattice.Properties where
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function
-open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Isomorphism
-open import Cubical.Foundations.Univalence
open import Cubical.Foundations.HLevels
-open import Cubical.Foundations.Transport
-open import Cubical.Foundations.Powerset using (ℙ ; ⊆-refl-consequence)
+open import Cubical.Foundations.Powerset using (ℙ)
renaming (_∈_ to _∈ₚ_ ; ∈-isProp to ∈ₚ-isProp)
-import Cubical.Data.Empty as ⊥
-open import Cubical.Data.Bool hiding (_≤_)
-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.Sigma.Base
+open import Cubical.Data.Nat using (ℕ)
open import Cubical.Data.Sigma.Properties
open import Cubical.Data.FinData
-open import Cubical.Data.Unit
-open import Cubical.Relation.Nullary
-open import Cubical.Relation.Binary
open import Cubical.Relation.Binary.Order.Poset
-open import Cubical.Algebra.Ring
-open import Cubical.Algebra.Ring.Properties
-open import Cubical.Algebra.Ring.BigOps
open import Cubical.Algebra.CommRing
open import Cubical.Algebra.CommRing.Localisation
-open import Cubical.Algebra.CommRing.BinomialThm
open import Cubical.Algebra.CommRing.Ideal
open import Cubical.Algebra.CommRing.FGIdeal
open import Cubical.Algebra.CommRing.RadicalIdeal
-open import Cubical.Tactics.CommRingSolver.Reflection
+open import Cubical.Tactics.CommRingSolver
open import Cubical.Algebra.Semilattice
open import Cubical.Algebra.Lattice
open import Cubical.Algebra.DistLattice
-open import Cubical.Algebra.DistLattice.Basis
-open import Cubical.Algebra.DistLattice.BigOps
open import Cubical.Algebra.DistLattice.Downset
-open import Cubical.Algebra.Matrix
open import Cubical.Algebra.ZariskiLattice.Base
open import Cubical.Algebra.ZariskiLattice.UniversalProperty
open import Cubical.HITs.SetQuotients as SQ
-open import Cubical.HITs.PropositionalTruncation as PT
+import Cubical.HITs.PropositionalTruncation as PT
private variable ℓ : Level
@@ -59,15 +40,11 @@ module _ (R : CommRing ℓ) where
open DistLatticeStr ⦃...⦄
open PosetStr ⦃...⦄
- open RingTheory (CommRing→Ring R)
- open Sum (CommRing→Ring R)
open CommRingTheory R
open Exponentiation R
- open BinomialThm R
open CommIdeal R
open RadicalIdeal R
open isCommIdeal
- open ProdFin R
open ZarLat R
open ZarLatUniversalProp R
From bec3d8146ae6b6bc902e187acc4c5efdf56705aa Mon Sep 17 00:00:00 2001
From: Matthias Hutzler <matthias-hutzler@posteo.net>
Date: Thu, 29 Feb 2024 23:42:11 +0100
Subject: [PATCH 34/37] cleanup some more
---
Cubical/Algebra/ZariskiLattice/Properties.agda | 8 --------
1 file changed, 8 deletions(-)
diff --git a/Cubical/Algebra/ZariskiLattice/Properties.agda b/Cubical/Algebra/ZariskiLattice/Properties.agda
index f552208598..3982a65bf6 100644
--- a/Cubical/Algebra/ZariskiLattice/Properties.agda
+++ b/Cubical/Algebra/ZariskiLattice/Properties.agda
@@ -37,18 +37,14 @@ private variable ℓ : Level
module _ (R : CommRing ℓ) where
open Iso
open CommRingStr ⦃...⦄
- open DistLatticeStr ⦃...⦄
open PosetStr ⦃...⦄
- open CommRingTheory R
open Exponentiation R
open CommIdeal R
open RadicalIdeal R
- open isCommIdeal
open ZarLat R
open ZarLatUniversalProp R
- open IsSupport isSupportD
open JoinSemilattice (Lattice→JoinSemilattice (DistLattice→Lattice ZariskiLattice))
using (IndPoset)
@@ -56,7 +52,6 @@ module _ (R : CommRing ℓ) where
private
instance
_ = R .snd
- _ = ZariskiLattice .snd
_ = IndPoset .snd
⟨_⟩ : {n : ℕ} → FinVec (fst R) n → CommIdeal
@@ -87,12 +82,10 @@ module _ (R : CommRing ℓ) where
module LocDownSetIso (R : CommRing ℓ) (f : R .fst) where
- open Iso
open CommRingStr ⦃...⦄
open DistLatticeStr ⦃...⦄
open PosetStr ⦃...⦄
- open Exponentiation R
open InvertingElementsBase R
open UniversalProp f
@@ -112,7 +105,6 @@ module LocDownSetIso (R : CommRing ℓ) (f : R .fst) where
private
instance
_ = R .snd
- _ = R[1/ f ]AsCommRing .snd
_ = ZariskiLattice R .snd
_ = ZLRPoset .snd
From d4d2196b1c2bc00bff50db7cf671bb038ad6b4b1 Mon Sep 17 00:00:00 2001
From: Matthias Hutzler <matthias-hutzler@posteo.net>
Date: Thu, 29 Feb 2024 23:42:51 +0100
Subject: [PATCH 35/37] forgotten while renaming ZarMap -> Support
---
Cubical/Algebra/ZariskiLattice/UniversalProperty.agda | 4 ++--
1 file changed, 2 insertions(+), 2 deletions(-)
diff --git a/Cubical/Algebra/ZariskiLattice/UniversalProperty.agda b/Cubical/Algebra/ZariskiLattice/UniversalProperty.agda
index cfd480deab..4355fe899c 100644
--- a/Cubical/Algebra/ZariskiLattice/UniversalProperty.agda
+++ b/Cubical/Algebra/ZariskiLattice/UniversalProperty.agda
@@ -71,7 +71,7 @@ module _ (R' : CommRing ℓ) (L' : DistLattice ℓ') where
L = fst L'
record IsSupport (d : R → L) : Type (ℓ-max ℓ ℓ') where
- constructor iszarmap
+ constructor issupport
field
pres0 : d 0r ≡ 0l
@@ -110,7 +110,7 @@ module _ (R' : CommRing ℓ) (L' : DistLattice ℓ') where
supportExpIneq zero x = cong (d x ∨l_) pres1 ∙∙ 1lRightAnnihilates∨l _ ∙∙ sym pres1
supportExpIneq (suc n) x = subst (λ y → d x ≤ y) (sym (supportIdem _ x)) (∨lIdem _)
- -- the crucial lemma about "Zariski maps"
+ -- the crucial lemma about support maps
open CommIdeal R'
open RadicalIdeal R'
open isCommIdeal
From ddc4fa53198b8eb3c3bd8b0cb55c1680648d3e93 Mon Sep 17 00:00:00 2001
From: mzeuner <max@zeuner.net>
Date: Mon, 4 Mar 2024 09:04:14 +0100
Subject: [PATCH 36/37] upstream 1 lemmas
---
Cubical/Algebra/CommRing/FGIdeal.agda | 13 +++++++++++++
Cubical/Algebra/CommRing/RadicalIdeal.agda | 6 ++++--
Cubical/Algebra/ZariskiLattice/Properties.agda | 16 +---------------
3 files changed, 18 insertions(+), 17 deletions(-)
diff --git a/Cubical/Algebra/CommRing/FGIdeal.agda b/Cubical/Algebra/CommRing/FGIdeal.agda
index 446c9bd131..9334f69c1b 100644
--- a/Cubical/Algebra/CommRing/FGIdeal.agda
+++ b/Cubical/Algebra/CommRing/FGIdeal.agda
@@ -11,6 +11,8 @@ open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function
open import Cubical.Foundations.Transport
open import Cubical.Foundations.HLevels
+open import Cubical.Foundations.Powerset using () renaming ( _∈_ to _∈ₚ_
+ ; ∈-isProp to ∈ₚ-isProp)
open import Cubical.Data.Empty as ⊥
open import Cubical.Data.Sigma
@@ -431,3 +433,14 @@ module GeneratingPowers (R' : CommRing ℓ) (n : ℕ) where
path = linearCombination R' α U ^ ((ℕsuc m) ·ℕ n) ≡⟨ cong (_^ ((ℕsuc m) ·ℕ n)) (sym p) ⟩
1r ^ ((ℕsuc m) ·ℕ n) ≡⟨ 1ⁿ≡1 ((ℕsuc m) ·ℕ n) ⟩
1r ∎
+
+
+-- principal ideals containing 1 are generated by units
+module _ {R : CommRing ℓ} {f : fst R} where
+ private ⟨f⟩ = ⟨ replicateFinVec 1 f ⟩[ R ]
+ open CommRingStr (snd R)
+ open CommIdeal R
+
+ containsOne→Unit : 1r ∈ ⟨f⟩ → f ∈ₚ R ˣ
+ containsOne→Unit = PT.rec (∈ₚ-isProp (R ˣ) f)
+ λ (α , 1≡α₀f+0) → α zero , solve! R ∙ sym 1≡α₀f+0
diff --git a/Cubical/Algebra/CommRing/RadicalIdeal.agda b/Cubical/Algebra/CommRing/RadicalIdeal.agda
index 0fdabfb3e7..16faf4c575 100644
--- a/Cubical/Algebra/CommRing/RadicalIdeal.agda
+++ b/Cubical/Algebra/CommRing/RadicalIdeal.agda
@@ -4,7 +4,7 @@ module Cubical.Algebra.CommRing.RadicalIdeal where
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Function
-open import Cubical.Foundations.Powerset using (⊆-isProp)
+open import Cubical.Foundations.Powerset using (⊆-isProp ; ∈-isProp)
open import Cubical.Foundations.HLevels
open import Cubical.Data.Sigma
@@ -95,7 +95,9 @@ module RadicalIdeal (R' : CommRing ℓ) where
∈→∈√ : ∀ (I : CommIdeal) (x : R) → x ∈ I → x ∈ √ I
∈→∈√ I _ x∈I = ∣ 1 , subst-∈ I (sym (·IdR _)) x∈I ∣₁
-
+ -- inverse direction holds for 1
+ 1∈√→1∈ : ∀ (I : CommIdeal) → 1r ∈ √ I → 1r ∈ I
+ 1∈√→1∈ I = PT.rec (∈-isProp (fst I) _) λ (n , 1ⁿ∈I) → subst-∈ I (1ⁿ≡1 n) 1ⁿ∈I
-- important lemma for characterization of the Zariski lattice
open KroneckerDelta (CommRing→Ring R')
diff --git a/Cubical/Algebra/ZariskiLattice/Properties.agda b/Cubical/Algebra/ZariskiLattice/Properties.agda
index 3982a65bf6..ba9813b866 100644
--- a/Cubical/Algebra/ZariskiLattice/Properties.agda
+++ b/Cubical/Algebra/ZariskiLattice/Properties.agda
@@ -58,7 +58,7 @@ module _ (R : CommRing ℓ) where
⟨ V ⟩ = ⟨ V ⟩[ R ]
unitLemmaZarLat : ∀ f → D f ≡ D 1r → f ∈ₚ R ˣ
- unitLemmaZarLat f Df≡D1 = PT.rec (∈ₚ-isProp (R ˣ) f) radicalHelper 1∈√⟨f⟩
+ unitLemmaZarLat f Df≡D1 = containsOne→Unit (1∈√→1∈ _ 1∈√⟨f⟩)
where
D1≤Df : D 1r ≤ D f
D1≤Df = subst (_≤ D f) Df≡D1 (is-refl _)
@@ -66,20 +66,6 @@ module _ (R : CommRing ℓ) where
1∈√⟨f⟩ : 1r ∈ √ ⟨ replicateFinVec 1 f ⟩
1∈√⟨f⟩ = isEquivRel→effectiveIso ∼PropValued ∼EquivRel _ _ .fun D1≤Df .fst zero
- radicalHelper : Σ[ n ∈ ℕ ] 1r ^ n ∈ ⟨ replicateFinVec 1 f ⟩ → f ∈ₚ R ˣ
- radicalHelper (n , 1ⁿ∈⟨f⟩) = PT.rec (∈ₚ-isProp (R ˣ) f) fgHelper 1ⁿ∈⟨f⟩
- where
- fgHelper : Σ[ α ∈ FinVec (fst R) 1 ] 1r ^ n ≡ linearCombination R α (replicateFinVec 1 f)
- → f ∈ₚ R ˣ
- fgHelper (α , 1ⁿ≡α₀f+0) = α zero , path
- where
- path : f · α zero ≡ 1r
- path = f · α zero ≡⟨ solve! R ⟩
- α zero · f + 0r ≡⟨ sym 1ⁿ≡α₀f+0 ⟩
- 1r ^ n ≡⟨ 1ⁿ≡1 n ⟩
- 1r ∎
-
-
module LocDownSetIso (R : CommRing ℓ) (f : R .fst) where
open CommRingStr ⦃...⦄
From ef4ae22842f8d581b2bc80f048ba05387624ed60 Mon Sep 17 00:00:00 2001
From: mzeuner <max@zeuner.net>
Date: Mon, 4 Mar 2024 11:58:38 +0100
Subject: [PATCH 37/37] meet map
---
Cubical/Algebra/DistLattice/BigOps.agda | 9 +++++++++
1 file changed, 9 insertions(+)
diff --git a/Cubical/Algebra/DistLattice/BigOps.agda b/Cubical/Algebra/DistLattice/BigOps.agda
index 1586f3b7f0..9f8f844741 100644
--- a/Cubical/Algebra/DistLattice/BigOps.agda
+++ b/Cubical/Algebra/DistLattice/BigOps.agda
@@ -154,3 +154,12 @@ module Meet (L' : DistLattice ℓ) where
⋀Join1r : ∀ {n} → (V : FinVec L n) → ⋀ (λ i → 1l ∨l V i) ≡ 1l
⋀Join1r V = sym (⋀Joinrdist 1l V) ∙ 1lLeftAnnihilates∨l _
+
+
+module MeetMap {L : DistLattice ℓ} {L' : DistLattice ℓ'} (φ : DistLatticeHom L L') where
+ private module L = Meet L
+ private module L' = Meet L'
+ open BigOpMap (LatticeHom→MeetSemilatticeHom φ)
+
+ pres⋀ : {n : ℕ} (U : FinVec ⟨ L ⟩ n) → φ .fst (L.⋀ U) ≡ L'.⋀ (φ .fst ∘ U)
+ pres⋀ = presBigOp