Zariski coverage on CommRing^op (#1082)

* use improved ringsolver * delete one more line * (wip) for Zariski coverage on CommRing (with Max Zeuner) * pullback stability * 1 ideal lemma * add using * big op fix --------- Co-authored-by: Matthias Hutzler <[email protected]>
agda · Feb 7, 2024 · cbb8351 · cbb8351
1 parent faf6bec
commit cbb8351
Show file tree

Hide file tree

Showing 6 changed files with 191 additions and 30 deletions.
diff --git a/Cubical/Algebra/CommRing/Localisation/InvertingElements.agda b/Cubical/Algebra/CommRing/Localisation/InvertingElements.agda
@@ -279,6 +279,40 @@ module InvertingElementsBase (R' : CommRing ℓ) where
                 PT.rec (PisProp s) λ (n , p) → subst P (sym p) (base n)
 
 
+
+ -- A more specialized universal property.
+ -- (Just ask f to become invertible, not all its powers.)
+ module UniversalProp (f : R) where
+   open S⁻¹RUniversalProp R' [ f ⁿ|n≥0] (powersFormMultClosedSubset f) public
+   open CommRingHomTheory
+
+   invElemUniversalProp : (A : CommRing ℓ) (φ : CommRingHom R' A)
+                        → (φ .fst f ∈ A ˣ)
+                        → ∃![ χ ∈ CommRingHom R[1/ f ]AsCommRing A ]
+                            (fst χ) ∘ (fst /1AsCommRingHom) ≡ (fst φ)
+   invElemUniversalProp A φ φf∈Aˣ =
+     S⁻¹RHasUniversalProp A φ
+       (powersPropElim (λ _ → ∈-isProp _ _)
+       (λ n → subst-∈ (A ˣ) (sym (pres^ φ f n)) (Exponentiation.^-presUnit A _ n φf∈Aˣ)))
+
+
+-- "functorial action" of localizing away from an element
+module _ {A B : CommRing ℓ} (φ : CommRingHom A B) (f : fst A) where
+  open CommRingStr (snd B)
+  private
+    module A = InvertingElementsBase A
+    module B = InvertingElementsBase B
+    module AU = A.UniversalProp f
+    module BU = B.UniversalProp (φ $r f)
+
+    φ/1 = BU./1AsCommRingHom ∘cr φ
+
+  uniqInvElemHom : ∃![ χ ∈ CommRingHom A.R[1/ f ]AsCommRing B.R[1/ φ $r f ]AsCommRing ]
+                     (fst χ) ∘ (fst AU./1AsCommRingHom) ≡ (fst φ/1)
+  uniqInvElemHom = AU.invElemUniversalProp _ φ/1 (BU.S/1⊆S⁻¹Rˣ _ ∣ 1 , sym (·IdR _) ∣₁)
+
+
+
 module _ (R : CommRing ℓ) (f : fst R) where
  open CommRingTheory R
  open RingTheory (CommRing→Ring R)

diff --git a/Cubical/Algebra/CommRing/Localisation/Limit.agda b/Cubical/Algebra/CommRing/Localisation/Limit.agda
@@ -64,7 +64,7 @@ module _ (R' : CommRing ℓ) {n : ℕ} (f : FinVec (fst R') (suc n)) where
  open CommRingTheory R'
  open RingTheory (CommRing→Ring R')
  open Sum (CommRing→Ring R')
- open CommIdeal R' hiding (subst-∈)
+ open CommIdeal R'
  open InvertingElementsBase R'
  open Exponentiation R'
  open CommRingStr ⦃...⦄

diff --git a/Cubical/Algebra/CommRing/Properties.agda b/Cubical/Algebra/CommRing/Properties.agda
@@ -200,34 +200,6 @@ module CommRingEquivs where
  fst (idCommRingEquiv A) = idEquiv (fst A)
  snd (idCommRingEquiv A) = makeIsRingHom refl (λ _ _ → refl) (λ _ _ → refl)
 
-module CommRingHomTheory {A' B' : CommRing ℓ} (φ : CommRingHom A' B') where
- open Units A' renaming (Rˣ to Aˣ ; _⁻¹ to _⁻¹ᵃ ; ·-rinv to ·A-rinv ; ·-linv to ·A-linv)
- private A = fst A'
- open CommRingStr (snd A') renaming (_·_ to _·A_ ; 1r to 1a)
- open Units B' renaming (Rˣ to Bˣ ; _⁻¹ to _⁻¹ᵇ ; ·-rinv to ·B-rinv)
- open CommRingStr (snd B') renaming  ( _·_ to _·B_ ; 1r to 1b
-                                     ; ·IdL to ·B-lid ; ·IdR to ·B-rid
-                                     ; ·Assoc to ·B-assoc)
-
- private
-   f = fst φ
- open IsRingHom (φ .snd)
-
- RingHomRespInv : (r : A) ⦃ r∈Aˣ : r ∈ Aˣ ⦄ → f r ∈ Bˣ
- RingHomRespInv r = f (r ⁻¹ᵃ) , (sym (pres· r (r ⁻¹ᵃ)) ∙∙ cong (f) (·A-rinv r) ∙∙ pres1)
-
- φ[x⁻¹]≡φ[x]⁻¹ : (r : A) ⦃ r∈Aˣ : r ∈ Aˣ ⦄ ⦃ φr∈Bˣ : f r ∈ Bˣ ⦄
-               → f (r ⁻¹ᵃ) ≡ (f r) ⁻¹ᵇ
- φ[x⁻¹]≡φ[x]⁻¹ r ⦃ r∈Aˣ ⦄ ⦃ φr∈Bˣ ⦄ =
-  f (r ⁻¹ᵃ)                         ≡⟨ sym (·B-rid _) ⟩
-  f (r ⁻¹ᵃ) ·B 1b                   ≡⟨ congR _·B_ (sym (·B-rinv _)) ⟩
-  f (r ⁻¹ᵃ) ·B ((f r) ·B (f r) ⁻¹ᵇ) ≡⟨ ·B-assoc _ _ _ ⟩
-  f (r ⁻¹ᵃ) ·B (f r) ·B (f r) ⁻¹ᵇ   ≡⟨ congL _·B_ (sym (pres· _ _)) ⟩
-  f (r ⁻¹ᵃ ·A r) ·B (f r) ⁻¹ᵇ       ≡⟨ cong (λ x → f x ·B (f r) ⁻¹ᵇ) (·A-linv _) ⟩
-  f 1a ·B (f r) ⁻¹ᵇ                 ≡⟨ congL _·B_ pres1 ⟩
-  1b ·B (f r) ⁻¹ᵇ                   ≡⟨ ·B-lid _ ⟩
-  (f r) ⁻¹ᵇ                         ∎
-
 
 module Exponentiation (R' : CommRing ℓ) where
  open CommRingStr (snd R')
@@ -276,6 +248,40 @@ module Exponentiation (R' : CommRing ℓ) where
  ^-presUnit f (suc n) f∈Rˣ = RˣMultClosed f (f ^ n) ⦃ f∈Rˣ ⦄ ⦃ ^-presUnit f n f∈Rˣ ⦄
 
 
+module CommRingHomTheory {A' B' : CommRing ℓ} (φ : CommRingHom A' B') where
+ open Units A' renaming (Rˣ to Aˣ ; _⁻¹ to _⁻¹ᵃ ; ·-rinv to ·A-rinv ; ·-linv to ·A-linv)
+ open Units B' renaming (Rˣ to Bˣ ; _⁻¹ to _⁻¹ᵇ ; ·-rinv to ·B-rinv)
+ open Exponentiation A' renaming (_^_ to _^ᵃ_) using ()
+ open Exponentiation B' renaming (_^_ to _^ᵇ_) using ()
+ open CommRingStr ⦃...⦄
+ private
+   A = fst A'
+   f = fst φ
+   instance
+     _ = A' .snd
+     _ = B' .snd
+ open IsRingHom (φ .snd)
+
+ RingHomRespInv : (r : A) ⦃ r∈Aˣ : r ∈ Aˣ ⦄ → f r ∈ Bˣ
+ RingHomRespInv r = f (r ⁻¹ᵃ) , (sym (pres· r (r ⁻¹ᵃ)) ∙∙ cong (f) (·A-rinv r) ∙∙ pres1)
+
+ φ[x⁻¹]≡φ[x]⁻¹ : (r : A) ⦃ r∈Aˣ : r ∈ Aˣ ⦄ ⦃ φr∈Bˣ : f r ∈ Bˣ ⦄
+               → f (r ⁻¹ᵃ) ≡ (f r) ⁻¹ᵇ
+ φ[x⁻¹]≡φ[x]⁻¹ r ⦃ r∈Aˣ ⦄ ⦃ φr∈Bˣ ⦄ =
+  f (r ⁻¹ᵃ)                         ≡⟨ sym (·IdR _) ⟩
+  f (r ⁻¹ᵃ) · 1r                   ≡⟨ congR _·_ (sym (·B-rinv _)) ⟩
+  f (r ⁻¹ᵃ) · ((f r) · (f r) ⁻¹ᵇ) ≡⟨ ·Assoc _ _ _ ⟩
+  f (r ⁻¹ᵃ) · (f r) · (f r) ⁻¹ᵇ   ≡⟨ congL _·_ (sym (pres· _ _)) ⟩
+  f (r ⁻¹ᵃ · r) · (f r) ⁻¹ᵇ       ≡⟨ cong (λ x → f x · (f r) ⁻¹ᵇ) (·A-linv _) ⟩
+  f 1r · (f r) ⁻¹ᵇ                 ≡⟨ congL _·_ pres1 ⟩
+  1r · (f r) ⁻¹ᵇ                   ≡⟨ ·IdL _ ⟩
+  (f r) ⁻¹ᵇ                         ∎
+
+ pres^ : (x : A) (n : ℕ) → f (x ^ᵃ n) ≡ f x ^ᵇ n
+ pres^ x zero = pres1
+ pres^ x (suc n) = pres· _ _ ∙ cong (f x ·_) (pres^ x n)
+
+
 -- like in Ring.Properties we provide helpful lemmas here
 module CommRingTheory (R' : CommRing ℓ) where
  open CommRingStr (snd R')

diff --git a/Cubical/Algebra/Monoid/BigOp.agda b/Cubical/Algebra/Monoid/BigOp.agda
@@ -57,3 +57,17 @@ module MonoidBigOp (M' : Monoid ℓ) where
 
  bigOpSplit++ {n = zero} V W = sym (·IdL _)
  bigOpSplit++ {n = suc n} V W = cong (V zero ·_) (bigOpSplit++ (V ∘ suc) W) ∙ ·Assoc _ _ _
+
+
+module BigOpMap {M : Monoid ℓ} {M' : Monoid ℓ'} (φ : MonoidHom M M') where
+  private module M = MonoidBigOp M
+  private module M' = MonoidBigOp M'
+  open IsMonoidHom (φ .snd)
+  open MonoidStr ⦃...⦄
+  private instance
+    _ = M .snd
+    _ = M' .snd
+
+  presBigOp : {n : ℕ} (U : FinVec ⟨ M ⟩ n) → φ .fst (M.bigOp U) ≡ M'.bigOp (φ .fst ∘ U)
+  presBigOp {n = zero} U = presε
+  presBigOp {n = suc n} U = pres· _ _ ∙ cong (φ .fst (U zero) ·_) (presBigOp (U ∘ suc))
diff --git a/Cubical/Algebra/Semiring/BigOps.agda b/Cubical/Algebra/Semiring/BigOps.agda
@@ -14,7 +14,7 @@ open import Cubical.Algebra.Monoid
 open import Cubical.Algebra.Monoid.BigOp
 
 private variable
-  ℓ : Level
+  ℓ ℓ' : Level
 
 
 module KroneckerDelta (S : Semiring ℓ) where

diff --git a/Cubical/Categories/Site/Instances/ZariskiCommRing.agda b/Cubical/Categories/Site/Instances/ZariskiCommRing.agda
@@ -0,0 +1,107 @@
+{-# OPTIONS --safe --lossy-unification #-}
+module Cubical.Categories.Site.Instances.ZariskiCommRing where
+
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Function
+open import Cubical.Foundations.Structure
+
+open import Cubical.Data.Nat using (ℕ)
+open import Cubical.Data.Sigma
+open import Cubical.Data.FinData
+
+open import Cubical.Algebra.Ring
+open import Cubical.Algebra.Ring.BigOps
+open import Cubical.Algebra.CommRing
+open import Cubical.Algebra.CommRing.Localisation
+open import Cubical.Algebra.CommRing.Ideal
+open import Cubical.Algebra.CommRing.FGIdeal
+
+open import Cubical.Categories.Category
+open import Cubical.Categories.Instances.CommRings
+open import Cubical.Categories.Site.Coverage
+open import Cubical.Categories.Constructions.Slice
+
+open import Cubical.HITs.PropositionalTruncation as PT
+
+private
+  variable
+    ℓ ℓ' ℓ'' : Level
+
+open Coverage
+open SliceOb
+
+-- the type of unimodular vectors, i.e. generators of the 1-ideal
+record UniModVec (R : CommRing ℓ) : Type ℓ where
+  open CommRingStr (str R)
+  open CommIdeal R using (_∈_)
+
+  field
+    n : ℕ
+    f : FinVec ⟨ R ⟩ n
+    isUniMod : 1r ∈ ⟨ f ⟩[ R ]
+
+module _ {A : CommRing ℓ} {B : CommRing ℓ'} (φ : CommRingHom A B) where
+  open UniModVec
+  open IsRingHom ⦃...⦄
+  open CommRingStr ⦃...⦄
+  open Sum (CommRing→Ring B)
+  open SumMap _ _ φ
+  private
+    module A = CommIdeal A
+    module B = CommIdeal B
+
+    instance
+      _ = A .snd
+      _ = B .snd
+      _ = φ .snd
+
+  pullbackUniModVec : UniModVec A → UniModVec B
+  n (pullbackUniModVec um) = um .n
+  f (pullbackUniModVec um) i = φ $r um .f i
+  isUniMod (pullbackUniModVec um) = B.subst-∈ -- 1 ∈ ⟨ f₁ ,..., fₙ ⟩ → 1 ∈ ⟨ φ(f₁) ,..., φ(fₙ) ⟩
+                                      ⟨ φ .fst ∘ um .f ⟩[ B ]
+                                        pres1 (PT.map mapHelper (um .isUniMod))
+    where
+    mapHelper : Σ[ α ∈ FinVec ⟨ A ⟩ _ ] 1r ≡ linearCombination A α (um .f)
+              → Σ[ β ∈ FinVec ⟨ B ⟩ _ ] φ $r 1r ≡ linearCombination B β (φ .fst ∘ um .f)
+    fst (mapHelper (α , 1≡∑αf)) = φ .fst ∘ α
+    snd (mapHelper (α , 1≡∑αf)) =
+      subst (λ x → φ $r x ≡ linearCombination B (φ .fst ∘ α) (φ .fst ∘ um .f))
+            (sym 1≡∑αf)
+            (∑Map _ ∙ ∑Ext (λ _ → pres· _ _))
+
+
+{-
+
+  For 1 ∈ ⟨ f₁ ,..., fₙ ⟩ we get a cover by arrows _/1 : R → R[1/fᵢ] for i=1,...,n
+  Pullback along φ : A → B is given by the induced arrows A[1/fᵢ] → B[1/φ(fᵢ)]
+
+-}
+zariskiCoverage : Coverage (CommRingsCategory {ℓ = ℓ} ^op) ℓ ℓ-zero
+fst (covers zariskiCoverage R) = UniModVec R
+fst (snd (covers zariskiCoverage R) um) = Fin n --patches
+  where
+  open UniModVec um
+S-ob (snd (snd (covers zariskiCoverage R) um) i) = R[1/ f i ]AsCommRing
+  where
+  open UniModVec um
+  open InvertingElementsBase R
+S-arr (snd (snd (covers zariskiCoverage R) um) i) = /1AsCommRingHom
+  where
+  open UniModVec um
+  open InvertingElementsBase.UniversalProp R (f i)
+pullbackStability zariskiCoverage {c = A} um {d = B} φ =
+  ∣ pullbackUniModVec φ um , (λ i → ∣ i , ψ i , RingHom≡ (sym (ψComm i)) ∣₁) ∣₁
+  where
+  open UniModVec
+  module A = InvertingElementsBase A
+  module B = InvertingElementsBase B
+  module AU = A.UniversalProp
+  module BU = B.UniversalProp
+
+  ψ : (i : Fin (um .n)) → CommRingHom A.R[1/ um .f i ]AsCommRing B.R[1/ φ $r um .f i ]AsCommRing
+  ψ i = uniqInvElemHom φ (um .f i) .fst .fst
+
+  ψComm : ∀ i → (ψ i .fst) ∘ (AU._/1 (um .f i)) ≡ (BU._/1 (φ $r um .f i)) ∘ φ .fst
+  ψComm i = uniqInvElemHom φ (um .f i) .fst .snd