The Structure Sheaf (#941)

* use improved ringsolver

* delete one more line

* apply sing lemma

* getting started on natural iso

* general case of fully faithful cor

* too many problems

* almost global sections

* make things compute

* everything is small now

* start with transport lemma

* big transport lemma

* some nasty paths

* getting started with last proof

* elegant lemma

* back to nicer version

* comm algs have limits

* char of pres limits

* preserving limits and lemma

* lift sheaf diagrams

* begin last lemma

* last lemma

* done

* easy fixes

* more fixes

* loc master file

* del comment

Cubical/Algebra/CommAlgebra/Base.agda

@@ -127,7 +127,6 @@ module _ {R : CommRing ℓ} where
                        x · (r ⋆ y) ∎
     makeIsCommAlgebra .IsCommAlgebra.·Comm = ·Comm
 
-
   module _ (S : CommRing ℓ') where
     open CommRingStr (snd S) renaming (1r to 1S)
     open CommRingStr (snd R) using () renaming (_·_ to _·R_; _+_ to _+R_; 1r to 1R)

Cubical/Algebra/CommAlgebra/Localisation.agda

@@ -25,9 +25,7 @@ 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
+open import Cubical.Algebra.CommRing.Localisation
 open import Cubical.Algebra.Ring
 open import Cubical.Algebra.Algebra
 open import Cubical.Algebra.CommAlgebra.Base
@@ -62,6 +60,8 @@ module AlgLoc (R' : CommRing ℓ)
  S⁻¹RAsCommAlg : CommAlgebra R' ℓ
  S⁻¹RAsCommAlg = toCommAlg (S⁻¹RAsCommRing , /1AsCommRingHom)
 
+ LocCommAlg→CommRingPath : CommAlgebra→CommRing S⁻¹RAsCommAlg ≡ S⁻¹RAsCommRing
+ LocCommAlg→CommRingPath = CommAlgebra→CommRing≡ (S⁻¹RAsCommRing , /1AsCommRingHom)
 
  hasLocAlgUniversalProp : (A : CommAlgebra R' ℓ)
                         → (∀ s → s ∈ S' → _⋆_ (snd A) s (1a (snd A)) ∈ (CommAlgebra→CommRing A) ˣ)
@@ -149,6 +149,12 @@ R[1/_]AsCommAlgebra {R = R} f = S⁻¹RAsCommAlg [ f ⁿ|n≥0] (powersFormMultC
  open AlgLoc R
  open InvertingElementsBase R
 
+module _  {R : CommRing ℓ} (f : fst R) where
+  open InvertingElementsBase R
+  open AlgLoc R [ f ⁿ|n≥0] (powersFormMultClosedSubset f)
+
+  invElCommAlgebra→CommRingPath : CommAlgebra→CommRing R[1/ f ]AsCommAlgebra ≡ R[1/ f ]AsCommRing
+  invElCommAlgebra→CommRingPath = LocCommAlg→CommRingPath
 
 module AlgLocTwoSubsets (R' : CommRing ℓ)
                         (S₁ : ℙ (fst R')) (S₁MultClosedSubset : isMultClosedSubset R' S₁)

Cubical/Algebra/CommAlgebra/Properties.agda

@@ -97,24 +97,29 @@ module CommAlgChar (R : CommRing ℓ) where
   φIsHom = makeIsRingHom (⋆IdL _) (λ _ _ → ⋆DistL+ _ _ _)
            λ x y → cong (λ a → (x ·r y) ⋆ a) (sym (·IdL _)) ∙ ⋆Dist· _ _ _ _
 
+ -- helpful for localisations
+ module _ (Aφ : CommRingWithHom) where
+   open CommRingStr
+   private
+     A = fst Aφ
+   CommAlgebra→CommRing≡ : CommAlgebra→CommRing (toCommAlg Aφ) ≡ A
+   fst (CommAlgebra→CommRing≡ i) = fst A
+   0r (snd (CommAlgebra→CommRing≡ i)) = 0r (snd A)
+   1r (snd (CommAlgebra→CommRing≡ i)) = 1r (snd A)
+   _+_ (snd (CommAlgebra→CommRing≡ i)) = _+_ (snd A)
+   _·_ (snd (CommAlgebra→CommRing≡ i)) = _·_ (snd A)
+   -_ (snd (CommAlgebra→CommRing≡ i)) = -_ (snd A)
+   -- note that the proofs of the axioms might differ!
+   isCommRing (snd (CommAlgebra→CommRing≡ i)) = isProp→PathP (λ i → isPropIsCommRing _ _ _ _ _ )
+              (isCommRing (snd (CommAlgebra→CommRing (toCommAlg Aφ)))) (isCommRing (snd A)) i
 
  CommRingWithHomRoundTrip : (Aφ : CommRingWithHom) → fromCommAlg (toCommAlg Aφ) ≡ Aφ
- CommRingWithHomRoundTrip (A , φ) = ΣPathP (APath , φPathP)
+ CommRingWithHomRoundTrip (A , φ) = ΣPathP (CommAlgebra→CommRing≡ (A , φ) , φPathP)
   where
   open CommRingStr
-  -- note that the proofs of the axioms might differ!
-  APath : fst (fromCommAlg (toCommAlg (A , φ))) ≡ A
-  fst (APath i) = ⟨ A ⟩
-  0r (snd (APath i)) = 0r (snd A)
-  1r (snd (APath i)) = 1r (snd A)
-  _+_ (snd (APath i)) = _+_ (snd A)
-  _·_ (snd (APath i)) = _·_ (snd A)
-  -_ (snd (APath i)) = -_ (snd A)
-  isCommRing (snd (APath i)) = isProp→PathP (λ i → isPropIsCommRing _ _ _ _ _ )
-             (isCommRing (snd (fst (fromCommAlg (toCommAlg (A , φ)))))) (isCommRing (snd A)) i
-
-  -- this only works because fst (APath i) = fst A definitionally!
-  φPathP : PathP (λ i → CommRingHom R (APath i)) (snd (fromCommAlg (toCommAlg (A , φ)))) φ
+  -- this only works because fst (CommAlgebra→CommRing≡ (A , φ) i) = fst A definitionally!
+  φPathP : PathP (λ i → CommRingHom R (CommAlgebra→CommRing≡ (A , φ) i))
+                 (snd (fromCommAlg (toCommAlg (A , φ)))) φ
   φPathP = RingHomPathP _ _ _ _ _ _ λ i x → ·IdR (snd A) (fst φ x) i
 
 

Cubical/Algebra/CommRing/Ideal.agda

@@ -9,7 +9,7 @@ open import Cubical.Foundations.Prelude
 open import Cubical.Foundations.Function
 open import Cubical.Foundations.HLevels
 open import Cubical.Foundations.Powerset renaming ( _∈_ to _∈p_ ; _⊆_ to _⊆p_
-                                                  ; subst-∈ to subst-∈p )
+                                                  ; subst-∈ to subst-∈p)
 
 open import Cubical.Functions.Logic
 

Cubical/Algebra/CommRing/Localisation.agda

@@ -0,0 +1,7 @@
+{-# OPTIONS --safe #-}
+module Cubical.Algebra.CommRing.Localisation where
+
+open import Cubical.Algebra.CommRing.Localisation.Base public
+open import Cubical.Algebra.CommRing.Localisation.UniversalProperty public
+open import Cubical.Algebra.CommRing.Localisation.InvertingElements public
+open import Cubical.Algebra.CommRing.Localisation.Limit public

Cubical/Algebra/CommRing/Localisation/InvertingElements.agda

@@ -20,6 +20,7 @@ open import Cubical.Foundations.Transport
 open import Cubical.Functions.FunExtEquiv
 
 import Cubical.Data.Empty as ⊥
+open import Cubical.Data.Unit
 open import Cubical.Data.Bool
 open import Cubical.Data.Nat renaming ( _+_ to _+ℕ_ ; _·_ to _·ℕ_ ; _^_ to _^ℕ_
                                       ; +-comm to +ℕ-comm ; +-assoc to +ℕ-assoc
@@ -37,6 +38,7 @@ open import Cubical.Algebra.AbGroup
 open import Cubical.Algebra.Monoid
 open import Cubical.Algebra.Ring
 open import Cubical.Algebra.CommRing
+open import Cubical.Algebra.CommRing.Instances.Unit
 open import Cubical.Algebra.CommRing.Localisation.Base
 open import Cubical.Algebra.CommRing.Localisation.UniversalProperty
 open import Cubical.Algebra.CommRing.Ideal
@@ -90,6 +92,21 @@ module InvertingElementsBase (R' : CommRing ℓ) where
  R[1/_]AsCommRing : R → CommRing ℓ
  R[1/ f ]AsCommRing = Loc.S⁻¹RAsCommRing R' [ f ⁿ|n≥0] (powersFormMultClosedSubset f)
 
+ R[1/0]≡0 : R[1/ 0r ]AsCommRing ≡ UnitCommRing
+ R[1/0]≡0 = uaCommRing (e , eIsRHom)
+  where
+  open IsRingHom
+
+  e : R[1/ 0r ]AsCommRing .fst ≃ UnitCommRing .fst
+  e = isContr→Equiv isContrR[1/0] isContrUnit*
+
+  eIsRHom : IsCommRingEquiv (R[1/ 0r ]AsCommRing .snd) e (UnitCommRing .snd)
+  pres0 eIsRHom = refl
+  pres1 eIsRHom = refl
+  pres+ eIsRHom _ _ = refl
+  pres· eIsRHom _ _ = refl
+  pres- eIsRHom _ = refl
+
  -- A useful lemma: (gⁿ/1)≡(g/1)ⁿ in R[1/f]
  ^-respects-/1 : {f g : R} (n : ℕ) → [ (g ^ n) , 1r , PT.∣ 0 , (λ _ → 1r) ∣₁ ] ≡
      Exponentiation._^_ R[1/ f ]AsCommRing [ g , 1r , powersFormMultClosedSubset _ .containsOne ] n
@@ -262,6 +279,29 @@ module InvertingElementsBase (R' : CommRing ℓ) where
                 PT.rec (PisProp s) λ (n , p) → subst P (sym p) (base n)
 
 
+module _ (R : CommRing ℓ) (f : fst R) where
+ open CommRingTheory R
+ open RingTheory (CommRing→Ring R)
+ open Units R
+ open Exponentiation R
+ open InvertingElementsBase R
+ open isMultClosedSubset (powersFormMultClosedSubset f)
+ open S⁻¹RUniversalProp R [ f ⁿ|n≥0] (powersFormMultClosedSubset f)
+ open CommRingStr (snd R)
+ open PathToS⁻¹R
+
+ invertingUnitsPath : f ∈ R ˣ → R[1/ f ]AsCommRing ≡ R
+ invertingUnitsPath f∈Rˣ = S⁻¹RChar _ _ _ _ (idCommRingHom R) (char f∈Rˣ)
+   where
+   char : f ∈ R ˣ → PathToS⁻¹R _ _ (powersFormMultClosedSubset f)
+                                 _ (idCommRingHom R)
+   φS⊆Aˣ (char f∈Rˣ) = powersPropElim (∈-isProp _)
+                           λ n → ^-presUnit _ n f∈Rˣ
+   kerφ⊆annS (char _) _ r≡0 = ∣ (1r , containsOne) , ·IdL _ ∙ r≡0 ∣₁
+   surχ (char _) r = ∣ (r , 1r , containsOne)
+                                , cong (r ·_) (transportRefl _) ∙ ·IdR _ ∣₁
+
+
 module RadicalLemma (R' : CommRing ℓ) (f g : (fst R')) where
  open IsRingHom
  open isMultClosedSubset
@@ -307,8 +347,7 @@ module RadicalLemma (R' : CommRing ℓ) (f g : (fst R')) where
                       (Exponentiation.^-presUnit _ _ n (unitHelper f∈√⟨g⟩))
 
 
-
-module DoubleLoc (R' : CommRing ℓ) (f g : (fst R')) where
+module DoubleLoc (R' : CommRing ℓ) (f g : fst R') where
  open isMultClosedSubset
  open CommRingStr (snd R')
  open CommRingTheory R'

Cubical/Algebra/CommRing/Localisation/Limit.agda

@@ -1,18 +1,13 @@
 {-
-
   This file contains a proof of the following fact:
   For a commutative ring R with elements f₁ , ... , fₙ ∈ R such that
   ⟨ f₁ , ... , fₙ ⟩ = ⟨ 1 ⟩ = R we get an (exact) equalizer diagram of the following form:
-
       0 → R → ∏ᵢ R[1/fᵢ] ⇉ ∏ᵢⱼ R[1/fᵢfⱼ]
-
   where the two maps ∏ᵢ R[1/fᵢ] → ∏ᵢⱼ R[1/fᵢfⱼ] are induced by the two canonical maps
   R[1/fᵢ] → R[1/fᵢfⱼ] and R[1/fⱼ] → R[1/fᵢfⱼ].
-
   Using the well-known correspondence between equalizers of products and limits,
   we express the above fact through limits over the diagrams defined in
   Cubical.Categories.DistLatticeSheaf.Diagram
-
 -}
 
 {-# OPTIONS --safe --experimental-lossy-unification #-}
@@ -535,16 +530,14 @@ module _ (R' : CommRing ℓ) {n : ℕ} (f : FinVec (fst R') (suc n)) where
 
 
 {-
-
  Putting everything together with the limit machinery:
  If ⟨ f₁ , ... , fₙ ⟩ = R, then R = lim { R[1/fᵢ] → R[1/fᵢfⱼ] ← R[1/fⱼ] }
-
 -}
  open Category (CommRingsCategory {ℓ})
  open Cone
  open Functor
 
- locDiagram : Functor (DLShfDiag (suc n)) CommRingsCategory
+ locDiagram : Functor (DLShfDiag (suc n) ℓ) CommRingsCategory
  F-ob locDiagram (sing i) = R[1/ f i ]AsCommRing
  F-ob locDiagram (pair i j _) = R[1/ f i · f j ]AsCommRing
  F-hom locDiagram idAr = idCommRingHom _