update to new interface for comm ring homs

Cubical/AlgebraicGeometry/Functorial/ZFunctors/OpenSubscheme.agda

@@ -27,7 +27,6 @@ open import Cubical.Data.Nat using (ℕ)
 
 open import Cubical.Data.FinData
 
-open import Cubical.Algebra.Ring
 open import Cubical.Algebra.CommRing
 open import Cubical.Algebra.CommRing.Localisation
 open import Cubical.Algebra.Semilattice
@@ -66,8 +65,7 @@ module StandardOpens {ℓ : Level} (R : CommRing ℓ) (f : R .fst) where
   open isIsoC
   open DistLatticeStr ⦃...⦄
   open CommRingStr ⦃...⦄
-  open IsRingHom
-  open RingHoms
+  open IsCommRingHom
   open IsLatticeHom
   open ZarLat
 
@@ -84,7 +82,7 @@ module StandardOpens {ℓ : Level} (R : CommRing ℓ) (f : R .fst) where
   D = yonedaᴾ ZarLatFun R .inv (ZL.D R f)
 
   SpR[1/f]≅⟦Df⟧ : NatIso (Sp .F-ob R[1/ f ]AsCommRing) ⟦ D ⟧ᶜᵒ
-  N-ob (trans SpR[1/f]≅⟦Df⟧) B φ = (φ ∘r /1AsCommRingHom) , ∨lRid _ ∙ path
+  N-ob (trans SpR[1/f]≅⟦Df⟧) B φ = (φ ∘cr /1AsCommRingHom) , ∨lRid _ ∙ path
     where
     open CommRingHomTheory φ
     open IsSupport (ZL.isSupportD B)
@@ -98,18 +96,18 @@ module StandardOpens {ℓ : Level} (R : CommRing ℓ) (f : R .fst) where
     path : ZL.D B (φ .fst (f /1)) ≡ 1l
     path = supportUnit _ isUnitφ[f/1]
 
-  N-hom (trans SpR[1/f]≅⟦Df⟧) _ = funExt λ _ → Σ≡Prop (λ _ → squash/ _ _) (RingHom≡ refl)
+  N-hom (trans SpR[1/f]≅⟦Df⟧) _ = funExt λ _ → Σ≡Prop (λ _ → squash/ _ _) (CommRingHom≡ refl)
 
   inv (nIso SpR[1/f]≅⟦Df⟧ B) (φ , Dφf≡D1) = invElemUniversalProp B φ isUnitφf .fst .fst
     where
     instance _ = ZariskiLattice B .snd
     isUnitφf : φ .fst f ∈ B ˣ
-    isUnitφf = unitLemmaZarLat B (φ $r f) (sym (∨lRid _) ∙ Dφf≡D1)
+    isUnitφf = unitLemmaZarLat B (φ $cr f) (sym (∨lRid _) ∙ Dφf≡D1)
 
   sec (nIso SpR[1/f]≅⟦Df⟧ B) =
-    funExt λ _ → Σ≡Prop (λ _ → squash/ _ _) (RingHom≡ (invElemUniversalProp _ _ _ .fst .snd))
+    funExt λ _ → Σ≡Prop (λ _ → squash/ _ _) (CommRingHom≡ (invElemUniversalProp _ _ _ .fst .snd))
   ret (nIso SpR[1/f]≅⟦Df⟧ B) =
-    funExt λ φ → cong fst (invElemUniversalProp B (φ ∘r /1AsCommRingHom) _ .snd (φ , refl))
+    funExt λ φ → cong fst (invElemUniversalProp B (φ ∘cr /1AsCommRingHom) _ .snd (φ , refl))
 
   isAffineD : isAffineCompactOpen D
   isAffineD = ∣ R[1/ f ]AsCommRing , SpR[1/f]≅⟦Df⟧ ∣₁
@@ -128,8 +126,7 @@ module _ {ℓ : Level} (R : CommRing ℓ) (W : CompactOpen (Sp ⟅ R ⟆)) where
   open DistLatticeStr ⦃...⦄
   open CommRingStr ⦃...⦄
   open PosetStr ⦃...⦄
-  open IsRingHom
-  open RingHoms
+  open IsCommRingHom
   open IsLatticeHom
   open ZarLat
 

Cubical/AlgebraicGeometry/ZariskiLattice/StructureSheafPullback.agda

@@ -36,7 +36,6 @@ open import Cubical.Relation.Nullary
 open import Cubical.Relation.Binary
 open import Cubical.Relation.Binary.Order.Poset
 
-open import Cubical.Algebra.Ring
 open import Cubical.Algebra.Ring.Properties
 open import Cubical.Algebra.Ring.BigOps
 open import Cubical.Algebra.Algebra
@@ -358,7 +357,7 @@ module _ (R' : CommRing ℓ) where
     R[1/h][1/fg]AsCommRing = InvertingElementsBase.R[1/_]AsCommRing
                                R[1/ h ]AsCommRing ((f /1) · (g /1))
 
-    open IsRingHom
+    open IsCommRingHom
     /1/1AsCommRingHomFG : CommRingHom R' R[1/h][1/fg]AsCommRing
     fst /1/1AsCommRingHomFG r = [ [ r , 1r , ∣ 0 , refl ∣₁ ] , 1r , ∣ 0 , refl ∣₁ ]
     pres0 (snd /1/1AsCommRingHomFG) = refl
@@ -375,20 +374,20 @@ module _ (R' : CommRing ℓ) where
     open Cospan
     open Pullback
     open RingHoms
-    isRHomR[1/h]→R[1/h][1/f] : theRingPullback .pbPr₂ ∘r /1AsCommRingHom ≡ /1/1AsCommRingHom f
-    isRHomR[1/h]→R[1/h][1/f] = RingHom≡ (funExt (λ x → refl))
+    isRHomR[1/h]→R[1/h][1/f] : theRingPullback .pbPr₂ ∘cr /1AsCommRingHom ≡ /1/1AsCommRingHom f
+    isRHomR[1/h]→R[1/h][1/f] = CommRingHom≡ (funExt (λ x → refl))
 
-    isRHomR[1/h]→R[1/h][1/g] : theRingPullback .pbPr₁ ∘r /1AsCommRingHom ≡ /1/1AsCommRingHom g
-    isRHomR[1/h]→R[1/h][1/g] = RingHom≡ (funExt (λ x → refl))
+    isRHomR[1/h]→R[1/h][1/g] : theRingPullback .pbPr₁ ∘cr /1AsCommRingHom ≡ /1/1AsCommRingHom g
+    isRHomR[1/h]→R[1/h][1/g] = CommRingHom≡ (funExt (λ x → refl))
 
-    isRHomR[1/h][1/f]→R[1/h][1/fg] : theRingCospan .s₂ ∘r /1/1AsCommRingHom f ≡ /1/1AsCommRingHomFG
-    isRHomR[1/h][1/f]→R[1/h][1/fg] = RingHom≡ (funExt
+    isRHomR[1/h][1/f]→R[1/h][1/fg] : theRingCospan .s₂ ∘cr /1/1AsCommRingHom f ≡ /1/1AsCommRingHomFG
+    isRHomR[1/h][1/f]→R[1/h][1/fg] = CommRingHom≡ (funExt
       (λ x → cong [_] (≡-× (cong [_] (≡-× (cong (x ·_) (transportRefl 1r) ∙ ·IdR x)
           (Σ≡Prop (λ _ → isPropPropTrunc) (cong (1r ·_) (transportRefl 1r) ∙ ·IdR 1r))))
           (Σ≡Prop (λ _ → isPropPropTrunc) (cong (1r ·_) (transportRefl 1r) ∙ ·IdR 1r)))))
 
-    isRHomR[1/h][1/g]→R[1/h][1/fg] : theRingCospan .s₁ ∘r /1/1AsCommRingHom g ≡ /1/1AsCommRingHomFG
-    isRHomR[1/h][1/g]→R[1/h][1/fg] = RingHom≡ (funExt
+    isRHomR[1/h][1/g]→R[1/h][1/fg] : theRingCospan .s₁ ∘cr /1/1AsCommRingHom g ≡ /1/1AsCommRingHomFG
+    isRHomR[1/h][1/g]→R[1/h][1/fg] = CommRingHom≡ (funExt
       (λ x → cong [_] (≡-× (cong [_] (≡-× (cong (x ·_) (transportRefl 1r) ∙ ·IdR x)
           (Σ≡Prop (λ _ → isPropPropTrunc) (cong (1r ·_) (transportRefl 1r) ∙ ·IdR 1r))))
           (Σ≡Prop (λ _ → isPropPropTrunc) (cong (1r ·_) (transportRefl 1r) ∙ ·IdR 1r)))))
@@ -435,7 +434,7 @@ module _ (R' : CommRing ℓ) where
       p i = InvertingElementsBase.R[1/_]AsCommRing R[1/ h ]AsCommRing (eqInR[1/h] i)
 
       q : PathP (λ i → CommRingHom R' (p i)) /1/1AsCommRingHomFG (/1/1AsCommRingHom (f · g))
-      q = toPathP (RingHom≡ (funExt (
+      q = toPathP (CommRingHom≡ (funExt (
             λ x → cong [_] (≡-× (cong [_] (≡-× (transportRefl _ ∙ transportRefl x)
                 (Σ≡Prop (λ _ → isPropPropTrunc) (transportRefl 1r))))
                 (Σ≡Prop (λ _ → isPropPropTrunc) (transportRefl 1r))))))