Open subschemes (#1096)

* (wip) for Zariski coverage on CommRing

(with Max Zeuner)

* pullback stability

* only zero case left

* finish zero case

* def standard affine open

* finish standard affine opens

* towards opens of affines

* discussion

* little progress

* towards separatedness

* separatedness

* locality

* towards aff cover

* give up

* finish

* cleanup

* use inline ring solver

* fix

* more fixes

* fix accidentally public module

manually cherry-picked from 93d52b5

* avoid code duplication

manually cherry-picked from 73cc74a

* improve comment

manually cherry-picked from 2c4d6d1

* slightly improve comment

* named module StandardOpens

manually cherry-picked from d41b178

* indent by two spaces

* less whitespace

* avoid duplication in PosetDownset

* fix copy-paste errors in comment

* cleanup JoinMap

* don't re-prove monoid lemmas

* slightly clearer comment

* polish module definition

* cleanup imports

* cleanup some more

* forgotten while renaming ZarMap -> Support

* upstream 1 lemmas

* meet map

---------

Co-authored-by: Matthias Hutzler <[email protected]>

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

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')

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
@@ -34,7 +34,7 @@ open import Cubical.Relation.Binary.Order.Poset
 
 private
   variable
-    ℓ : Level
+    ℓ ℓ' : Level
 
 module KroneckerDelta (L' : DistLattice ℓ) where
  private
@@ -107,6 +107,15 @@ 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 BigOpMap (LatticeHom→JoinSemilatticeHom φ)
+
+  pres⋁ : {n : ℕ} (U : FinVec ⟨ L ⟩ n) → φ .fst (L.⋁ U) ≡ L'.⋁ (φ .fst ∘ U)
+  pres⋁ = presBigOp
+
+
 module Meet (L' : DistLattice ℓ) where
  private
   L = fst L'
@@ -145,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

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)

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

Cubical/Algebra/Lattice/Properties.agda

@@ -29,25 +29,30 @@ 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 ∎
+  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 _
+  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 ∎
+  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 _
+  1lRightAnnihilates∨l : ∀ (x : L) → x ∨l 1l ≡ 1l
+  1lRightAnnihilates∨l _ = ∨lComm _ _ ∙ 1lLeftAnnihilates∨l _
 
+  -- 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
 
 
 module Order (L' : Lattice ℓ) where
@@ -74,13 +79,16 @@ 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))
 
  ∧≤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 ⦃...⦄