Structure Sheaf on Basic Opens

Cubical/Algebra/Algebra/Base.agda

@@ -242,7 +242,7 @@ isGroupoidAlgebra _ _ = isOfHLevelRespectEquiv 2 (AlgebraPath _ _) (isSetAlgebra
 -- Smart constructor for ring homomorphisms
 -- that infers the other equations from pres1, pres+, and pres·
 
-module _  {R : Ring ℓ} {A : Algebra R ℓ} {B : Algebra R ℓ'} {f : ⟨ A ⟩ → ⟨ B ⟩} where
+module _  {R : Ring ℓ} {A : Algebra R ℓ'} {B : Algebra R ℓ''} {f : ⟨ A ⟩ → ⟨ B ⟩} where
 
   private
     module A = AlgebraStr (A .snd)

Cubical/Algebra/CommAlgebra/Base.agda

@@ -164,6 +164,16 @@ module _ {R : CommRing ℓ} where
                                   → CommAlgebraEquiv A B → CommAlgebraHom A B
   CommAlgebraEquiv→CommAlgebraHom (e , eIsHom) = e .fst , eIsHom
 
+  CommAlgebraHom→CommRingHom : (A : CommAlgebra R ℓ') (B : CommAlgebra R ℓ'')
+                              → CommAlgebraHom A B
+                              → CommRingHom (CommAlgebra→CommRing A) (CommAlgebra→CommRing B)
+  fst (CommAlgebraHom→CommRingHom A B f) = fst f
+  IsRingHom.pres0 (snd (CommAlgebraHom→CommRingHom A B f)) = IsAlgebraHom.pres0 (snd f)
+  IsRingHom.pres1 (snd (CommAlgebraHom→CommRingHom A B f)) = IsAlgebraHom.pres1 (snd f)
+  IsRingHom.pres+ (snd (CommAlgebraHom→CommRingHom A B f)) = IsAlgebraHom.pres+ (snd f)
+  IsRingHom.pres· (snd (CommAlgebraHom→CommRingHom A B f)) = IsAlgebraHom.pres· (snd f)
+  IsRingHom.pres- (snd (CommAlgebraHom→CommRingHom A B f)) = IsAlgebraHom.pres- (snd f)
+
   module _ {M N : CommAlgebra R ℓ'} where
     open CommAlgebraStr {{...}}
     open IsAlgebraHom

Cubical/Algebra/CommAlgebra/Localisation.agda

@@ -7,10 +7,13 @@ open import Cubical.Foundations.HLevels
 open import Cubical.Foundations.Function
 open import Cubical.Foundations.Isomorphism
 open import Cubical.Foundations.Equiv.HalfAdjoint
-open import Cubical.Foundations.SIP
 open import Cubical.Foundations.Powerset
 
 open import Cubical.Data.Sigma
+open import Cubical.Data.Nat renaming ( _+_ to _+ℕ_ ; _·_ to _·ℕ_
+                                      ; +-comm to +ℕ-comm ; +-assoc to +ℕ-assoc
+                                      ; ·-assoc to ·ℕ-assoc ; ·-comm to ·ℕ-comm)
+open import Cubical.Data.FinData
 
 open import Cubical.Reflection.StrictEquiv
 
@@ -19,6 +22,9 @@ open import Cubical.Algebra.Semigroup
 open import Cubical.Algebra.Monoid
 open import Cubical.Algebra.CommRing.Base
 open import Cubical.Algebra.CommRing.Properties
+open import Cubical.Algebra.CommRing.Ideal
+open import Cubical.Algebra.CommRing.FGIdeal
+open import Cubical.Algebra.CommRing.RadicalIdeal
 open import Cubical.Algebra.CommRing.Localisation.Base
 open import Cubical.Algebra.CommRing.Localisation.UniversalProperty
 open import Cubical.Algebra.CommRing.Localisation.InvertingElements
@@ -27,6 +33,8 @@ open import Cubical.Algebra.Algebra
 open import Cubical.Algebra.CommAlgebra.Base
 open import Cubical.Algebra.CommAlgebra.Properties
 
+open import Cubical.Algebra.RingSolver.Reflection
+
 open import Cubical.HITs.SetQuotients as SQ
 open import Cubical.HITs.PropositionalTruncation as PT
 
@@ -125,14 +133,23 @@ module AlgLoc (R' : CommRing ℓ)
  isContrHomS⁻¹RS⁻¹R : isContr (CommAlgebraHom S⁻¹RAsCommAlg S⁻¹RAsCommAlg)
  isContrHomS⁻¹RS⁻¹R = S⁻¹RHasAlgUniversalProp S⁻¹RAsCommAlg S⋆1⊆S⁻¹Rˣ
 
+ S⁻¹RAlgCharEquiv : (A' : CommRing ℓ) (φ : CommRingHom R' A')
+                  → PathToS⁻¹R  R' S' SMultClosedSubset A' φ
+                  → CommAlgebraEquiv S⁻¹RAsCommAlg (toCommAlg (A' , φ))
+ S⁻¹RAlgCharEquiv A' φ cond = toCommAlgebraEquiv _ _
+                                (S⁻¹RCharEquiv R' S' SMultClosedSubset A' φ cond)
+                                (RingHom≡ (S⁻¹RHasUniversalProp A' φ (cond .φS⊆Aˣ) .fst .snd))
+  where open PathToS⁻¹R
+
 
 -- the special case of localizing at a single element
-R[1/_]AsCommAlgebra : {R : CommRing ℓ} → ⟨ R ⟩ → CommAlgebra R ℓ
+R[1/_]AsCommAlgebra : {R : CommRing ℓ} → fst R → CommAlgebra R ℓ
 R[1/_]AsCommAlgebra {R = R} f = S⁻¹RAsCommAlg [ f ⁿ|n≥0] (powersFormMultClosedSubset f)
  where
  open AlgLoc R
  open InvertingElementsBase R
 
+
 module AlgLocTwoSubsets (R' : CommRing ℓ)
                         (S₁ : ℙ (fst R')) (S₁MultClosedSubset : isMultClosedSubset R' S₁)
                         (S₂ : ℙ (fst R')) (S₂MultClosedSubset : isMultClosedSubset R' S₂) where
@@ -223,3 +240,76 @@ module AlgLocTwoSubsets (R' : CommRing ℓ)
     S₂⊆S₁⁻¹Rˣ s₂ s₂∈S₂ =
       transport (λ i → _⋆_ ⦃ (sym S₁⁻¹R≡S₂⁻¹R) i .snd ⦄ s₂ (1a ⦃ (sym S₁⁻¹R≡S₂⁻¹R) i .snd ⦄)
                      ∈ (CommAlgebra→CommRing ((sym S₁⁻¹R≡S₂⁻¹R) i)) ˣ) (S₂⋆1⊆S₂⁻¹Rˣ s₂ s₂∈S₂)
+
+
+
+-- A crucial result for the construction of the structure sheaf
+module DoubleAlgLoc (R : CommRing ℓ) (f g : (fst R)) where
+ open Exponentiation R
+ open InvertingElementsBase
+ open CommRingStr (snd R) hiding (·Rid)
+ open isMultClosedSubset
+ open DoubleLoc R f g hiding (R[1/fg]≡R[1/f][1/g])
+ open CommAlgChar R
+ open AlgLoc R ([_ⁿ|n≥0] R (f · g)) (powersFormMultClosedSubset R (f · g))
+             renaming (S⁻¹RAlgCharEquiv to R[1/fg]AlgCharEquiv)
+ open CommIdeal R hiding (subst-∈) renaming (_∈_ to _∈ᵢ_)
+ open isCommIdeal
+ open RadicalIdeal R
+
+ private
+  ⟨_⟩ : (fst R) → CommIdeal
+  ⟨ f ⟩ = ⟨ replicateFinVec 1 f ⟩[ R ]
+
+  R[1/fg]AsCommAlgebra = R[1/_]AsCommAlgebra {R = R} (f · g)
+  R[1/fg]ˣ = R[1/_]AsCommRing R (f · g) ˣ
+
+  R[1/g]AsCommAlgebra = R[1/_]AsCommAlgebra {R = R} g
+  R[1/g]ˣ = R[1/_]AsCommRing R g ˣ
+
+  R[1/f][1/g]AsCommRing = R[1/_]AsCommRing (R[1/_]AsCommRing R f)
+                                [ g , 1r , powersFormMultClosedSubset R f .containsOne ]
+  R[1/f][1/g]AsCommAlgebra = toCommAlg (R[1/f][1/g]AsCommRing , /1/1AsCommRingHom)
+
+ R[1/fg]≡R[1/f][1/g] : R[1/fg]AsCommAlgebra ≡ R[1/f][1/g]AsCommAlgebra
+ R[1/fg]≡R[1/f][1/g] = uaCommAlgebra (R[1/fg]AlgCharEquiv _ _ pathtoR[1/fg])
+
+ doubleLocCancel : g ∈ᵢ √ ⟨ f ⟩ → R[1/f][1/g]AsCommAlgebra ≡ R[1/g]AsCommAlgebra
+ doubleLocCancel g∈√⟨f⟩ = sym R[1/fg]≡R[1/f][1/g] ∙ isContrR[1/fg]≡R[1/g] toUnit1 toUnit2 .fst
+  where
+  open S⁻¹RUniversalProp R ([_ⁿ|n≥0] R g) (powersFormMultClosedSubset R g)
+                           renaming (_/1 to _/1ᵍ)
+  open S⁻¹RUniversalProp R ([_ⁿ|n≥0] R (f · g)) (powersFormMultClosedSubset R (f · g))
+                           renaming (_/1 to _/1ᶠᵍ)
+  open AlgLocTwoSubsets R ([_ⁿ|n≥0] R (f · g)) (powersFormMultClosedSubset R (f · g))
+                          ([_ⁿ|n≥0] R g) (powersFormMultClosedSubset R g)
+                          renaming (isContrS₁⁻¹R≡S₂⁻¹R to isContrR[1/fg]≡R[1/g])
+  open CommAlgebraStr ⦃...⦄ hiding (_·_ ; _+_)
+  instance
+   _ = snd R[1/fg]AsCommAlgebra
+   _ = snd R[1/g]AsCommAlgebra
+
+  toUnit1 : ∀ s → s ∈ [_ⁿ|n≥0] R (f · g) → s ⋆ 1a ∈ R[1/g]ˣ
+  toUnit1 s s∈[fgⁿ|n≥0] = subst-∈ R[1/g]ˣ (sym (·Rid (s /1ᵍ)))
+                            (RadicalLemma.toUnit R g (f · g) (radHelper _ _ g∈√⟨f⟩) s s∈[fgⁿ|n≥0])
+   where
+   radHelper : ∀ x y → x ∈ᵢ √ ⟨ y ⟩ → x ∈ᵢ √ ⟨ y · x ⟩
+   radHelper x y = PT.rec ((√ ⟨ y · x ⟩) .fst x .snd) (uncurry helper1)
+    where
+    helper1 : (n : ℕ) → x ^ n ∈ᵢ ⟨ y ⟩ → x ∈ᵢ √ ⟨ y · x ⟩
+    helper1 n = PT.rec ((√ ⟨ y · x ⟩) .fst x .snd) (uncurry helper2)
+     where
+     helper2 : (α : FinVec (fst R) 1)
+             → x ^ n ≡ linearCombination R α (replicateFinVec 1 y)
+             → x ∈ᵢ √ ⟨ y · x ⟩
+     helper2 α p = ∣ (suc n) , ∣ α , cong (x ·_) p ∙ useSolver x y (α zero) ∣ ∣
+      where
+      useSolver : ∀ x y a → x · (a · y + 0r) ≡ a · (y · x) + 0r
+      useSolver = solve R
+
+  toUnit2 : ∀ s → s ∈ [_ⁿ|n≥0] R g → s ⋆ 1a ∈ R[1/fg]ˣ
+  toUnit2 s s∈[gⁿ|n≥0] = subst-∈ R[1/fg]ˣ (sym (·Rid (s /1ᶠᵍ)))
+                           (RadicalLemma.toUnit R (f · g) g radHelper s s∈[gⁿ|n≥0])
+   where
+   radHelper : (f · g) ∈ᵢ √ ⟨ g ⟩
+   radHelper = ·Closed (snd (√ ⟨ g ⟩)) f (∈→∈√ _ _ (indInIdeal R _ zero))

Cubical/Algebra/CommAlgebra/Properties.agda

@@ -119,6 +119,55 @@ module CommAlgChar (R : CommRing ℓ) where
  rightInv CommAlgIso = CommRingWithHomRoundTrip
  leftInv CommAlgIso = CommAlgRoundTrip
 
+ open RingHoms
+ isCommRingWithHomHom : (A B : CommRingWithHom) → CommRingHom (fst A) (fst B) → Type ℓ
+ isCommRingWithHomHom (_ , f) (_ , g) h = h ∘r f ≡ g
+
+ CommRingWithHomHom : CommRingWithHom → CommRingWithHom → Type ℓ
+ CommRingWithHomHom (A , f) (B , g) = Σ[ h ∈ CommRingHom A B ] h ∘r f ≡ g
+
+ toCommAlgebraHom : (A B : CommRingWithHom) (h : CommRingHom (fst A) (fst B))
+                  → isCommRingWithHomHom A B h
+                  → CommAlgebraHom (toCommAlg A) (toCommAlg B)
+ toCommAlgebraHom (A , f) (B , g) h commDiag =
+   makeCommAlgebraHom (fst h) (pres1 (snd h)) (pres+ (snd h)) (pres· (snd h)) pres⋆h
+   where
+   open CommRingStr ⦃...⦄
+   instance
+    _ = snd A
+    _ = snd B
+   pres⋆h : ∀ r x → fst h (fst f r · x) ≡ fst g r · fst h x
+   pres⋆h r x = fst h (fst f r · x)       ≡⟨ pres· (snd h) _ _ ⟩
+                fst h (fst f r) · fst h x ≡⟨ cong (λ φ → fst φ r · fst h x) commDiag ⟩
+                fst g r · fst h x ∎
+
+ fromCommAlgebraHom : (A B : CommAlgebra R ℓ) → CommAlgebraHom A B
+                    → CommRingWithHomHom (fromCommAlg A) (fromCommAlg B)
+ fst (fst (fromCommAlgebraHom A B f)) = fst f
+ pres0 (snd (fst (fromCommAlgebraHom A B f))) = IsAlgebraHom.pres0 (snd f)
+ pres1 (snd (fst (fromCommAlgebraHom A B f))) = IsAlgebraHom.pres1 (snd f)
+ pres+ (snd (fst (fromCommAlgebraHom A B f))) = IsAlgebraHom.pres+ (snd f)
+ pres· (snd (fst (fromCommAlgebraHom A B f))) = IsAlgebraHom.pres· (snd f)
+ pres- (snd (fst (fromCommAlgebraHom A B f))) = IsAlgebraHom.pres- (snd f)
+ snd (fromCommAlgebraHom A B f) =
+  RingHom≡ (funExt (λ x → IsAlgebraHom.pres⋆ (snd f) x 1a ∙ cong (x ⋆_) (IsAlgebraHom.pres1 (snd f))))
+  where
+  open CommAlgebraStr (snd A) using (1a)
+  open CommAlgebraStr (snd B) using (_⋆_)
+
+ isCommRingWithHomEquiv : (A B : CommRingWithHom) → CommRingEquiv (fst A) (fst B) → Type ℓ
+ isCommRingWithHomEquiv A B e = isCommRingWithHomHom A B (RingEquiv→RingHom e)
+
+ CommRingWithHomEquiv : CommRingWithHom → CommRingWithHom → Type ℓ
+ CommRingWithHomEquiv A B = Σ[ e ∈ CommRingEquiv (fst A) (fst B) ] isCommRingWithHomEquiv A B e
+
+ toCommAlgebraEquiv : (A B : CommRingWithHom) (e : CommRingEquiv (fst A) (fst B))
+                    → isCommRingWithHomEquiv A B e
+                    → CommAlgebraEquiv (toCommAlg A) (toCommAlg B)
+ fst (toCommAlgebraEquiv A B e eCommDiag) = e .fst
+ snd (toCommAlgebraEquiv A B e eCommDiag) = toCommAlgebraHom A B _ eCommDiag .snd
+
+
 
 module CommAlgebraHoms {R : CommRing ℓ} where
   open AlgebraHoms

Cubical/Algebra/CommAlgebra/Unit.agda

@@ -0,0 +1,32 @@
+{-# OPTIONS --safe #-}
+module Cubical.Algebra.CommAlgebra.Unit where
+
+open import Cubical.Foundations.Prelude
+
+open import Cubical.Data.Unit
+
+open import Cubical.Algebra.Ring
+open import Cubical.Algebra.CommRing
+open import Cubical.Algebra.CommAlgebra
+
+private
+  variable
+    ℓ ℓ' : Level
+
+open CommAlgebraStr
+
+module _ (R : CommRing ℓ) where
+
+  UnitCommAlgebra : CommAlgebra R ℓ'
+  fst UnitCommAlgebra = Unit*
+  0a (snd UnitCommAlgebra) = tt*
+  1a (snd UnitCommAlgebra) = tt*
+  _+_ (snd UnitCommAlgebra) = λ _ _ → tt*
+  _·_ (snd UnitCommAlgebra) = λ _ _ → tt*
+  - snd UnitCommAlgebra = λ _ → tt*
+  _⋆_ (snd UnitCommAlgebra) = λ _ _ → tt*
+  isCommAlgebra (snd UnitCommAlgebra) = makeIsCommAlgebra isSetUnit*
+       (λ _ _ _ → refl) (λ { tt* → refl }) (λ _ → refl) (λ _ _ → refl)
+       (λ _ _ _ → refl) (λ { tt* → refl }) (λ _ _ _ → refl) (λ _ _ → refl)
+       (λ _ _ _ → refl) (λ _ _ _ → refl)
+       (λ _ _ _ → refl) (λ { tt* → refl }) (λ _ _ _ → refl)