diff --git a/Cubical/Algebra/CommRing/Localisation/InvertingElements.agda b/Cubical/Algebra/CommRing/Localisation/InvertingElements.agda index be3dd9d176..37a56b2037 100644 --- 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 index 316c491e84..c8c755f512 100644 --- 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 index b8d2033797..14900652e1 100644 --- 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 index 803074aaf2..04818eb665 100644 --- 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 index 957d6502c6..5b068cc4c7 100644 --- 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 new file mode 100644 index 0000000000..3405f09c76 --- /dev/null +++ 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