fix whitespace, modify definition to use updated definition of ≼

Author: anshwad10

Cubical/Algebra/CommRing/RadicalIdeal.agda

@@ -240,7 +240,7 @@ module RadicalIdeal (R' : CommRing ℓ) where
  √·Absorb+ I J = CommIdeal≡Char (√·Absorb+LIncl I J) (√·Absorb+RIncl I J)
 
  √·ContrLIncl : ∀ (I J : CommIdeal) → √ (√ I ·i √ J) ⊆ √ (I ·i J)
- √·ContrLIncl I J x = √·RContrLIncl I J x ∘ subst (x ∈_) (√·LContr I (√ J)) 
+ √·ContrLIncl I J x = √·RContrLIncl I J x ∘ subst (x ∈_) (√·LContr I (√ J))
 
  √Pres·LIncl : ∀ (I J : CommIdeal) → (√ I ·i √ J) ⊆ √ (I ·i J)
  √Pres·LIncl I J x = √·ContrLIncl I J x ∘ ∈→∈√ (√ I ·i √ J) x

Cubical/AlgebraicGeometry/ZariskiLattice/Base.agda

@@ -155,15 +155,15 @@ module ZarLat (R' : CommRing ℓ) where
   ∨a-join (_ , α) (_ , β) (_ , γ) = propBiimpl→Equiv (≼PropValued _ _) (isProp× (≼PropValued _ _) (≼PropValued _ _)) to fo
     where
       to : _
-      to α∨β⊆γ .fst = ⊆-trans _ _ _ 
+      to α∨β⊆γ .fst = ⊆-trans _ _ _
         (√Resp⊆ ⟨ α ⟩ ⟨ α ++Fin β ⟩ (⊆-trans _ _ _ (+iLincl ⟨ α ⟩ ⟨ β ⟩) (FGIdealAddLemmaRIncl _ α β))) α∨β⊆γ
-      to α∨β⊆γ .snd = ⊆-trans _ _ _ 
+      to α∨β⊆γ .snd = ⊆-trans _ _ _
         (√Resp⊆ ⟨ β ⟩ ⟨ α ++Fin β ⟩ (⊆-trans _ _ _ (+iRincl ⟨ α ⟩ ⟨ β ⟩) (FGIdealAddLemmaRIncl _ α β))) α∨β⊆γ
       fo : _
       fo (α⊆γ , β⊆γ) = ⊆-trans _ _ _ (√Resp⊆ ⟨ α ++Fin β ⟩ (⟨ α ⟩ +i ⟨ β ⟩) $ FGIdealAddLemmaLIncl _ α β) λ x x∈√α+β → do
         (n , x^n∈α+β) ← x∈√α+β
         ((y , z) , y∈α , z∈β , x^n≡y+z) ← x^n∈α+β
-        ^∈√→∈√ _ x n $ subst-∈ (√ ⟨ γ ⟩) (sym x^n≡y+z) $ 
+        ^∈√→∈√ _ x n $ subst-∈ (√ ⟨ γ ⟩) (sym x^n≡y+z) $
           √ ⟨ γ ⟩ .snd .+Closed (α⊆γ y (∈→∈√ _ y y∈α)) (β⊆γ z (∈→∈√ _ z z∈β))
 
   ZL-joins : isJoinSemipseudolattice ZLPoset
@@ -184,9 +184,9 @@ module ZarLat (R' : CommRing ℓ) where
       to γ≼α∧β .snd = ⊆-trans _ _ _ γ≼α∧β $ √Resp⊆ ⟨ α ··Fin β ⟩ ⟨ β ⟩ $
                       ⊆-trans _ _ _ (FGIdealMultLemmaLIncl _ α β) (·iRincl ⟨ α ⟩ ⟨ β ⟩)
       fo : _
-      fo (γ≼α , γ≼β) = ⊆-trans _ _ _ (λ x x∈√γ → 
+      fo (γ≼α , γ≼β) = ⊆-trans _ _ _ (λ x x∈√γ →
           ∣ 2 , subst-∈ (√ ⟨ α ⟩ ·i √ ⟨ β ⟩) (solve! R') (prodInProd _ _ x x (γ≼α x x∈√γ) (γ≼β x x∈√γ)) ∣₁
-        ) $ ⊆-trans _ _ _ (√·ContrLIncl ⟨ α ⟩ ⟨ β ⟩) $ 
+        ) $ ⊆-trans _ _ _ (√·ContrLIncl ⟨ α ⟩ ⟨ β ⟩) $
         √Resp⊆ (⟨ α ⟩ ·i ⟨ β ⟩) ⟨ α ··Fin β ⟩ $ FGIdealMultLemmaRIncl _ α β
 
   ZL-meets : isMeetSemipseudolattice ZLPoset

Cubical/AlgebraicGeometry/ZariskiLattice/Properties.agda

@@ -65,7 +65,7 @@ module _ (R : CommRing ℓ) where
     D1≤Df = subst (_≤ D f) Df≡D1 (is-refl _)
 
     1∈√⟨f⟩ : 1r ∈ √ ⟨ replicateFinVec 1 f ⟩
-    1∈√⟨f⟩ = isEquivRel→effectiveIso ∼PropValued ∼EquivRel _ _ .fun D1≤Df .fst zero
+    1∈√⟨f⟩ = √FGIdealCharLImpl _ _ (isEquivRel→effectiveIso ∼PropValued ∼EquivRel _ _ .fun D1≤Df .fst) zero
 
 
   module _ {n : ℕ} (f₁,⋯,fₙ : FinVec (fst R) n) where
@@ -80,9 +80,8 @@ module _ (R : CommRing ℓ) where
       D1≤D[f₁,⋯,fₙ] = subst (_≤ D[f₁,⋯,fₙ]) D[f₁,⋯,fₙ]≡D1 (is-refl _)
 
       1∈√⟨f₁,⋯,fₙ⟩ : 1r ∈ √ ⟨ f₁,⋯,fₙ ⟩
-      1∈√⟨f₁,⋯,fₙ⟩ = isEquivRel→effectiveIso ∼PropValued ∼EquivRel _ _ .fun
-                       D1≤D[f₁,⋯,fₙ] .fst zero
-
+      1∈√⟨f₁,⋯,fₙ⟩ = √FGIdealCharLImpl _ _
+        (isEquivRel→effectiveIso ∼PropValued ∼EquivRel _ _ .fun D1≤D[f₁,⋯,fₙ] .fst) zero
 
 
 module LocDownSetIso (R : CommRing ℓ) (f : R .fst) where

Cubical/AlgebraicGeometry/ZariskiLattice/StructureSheaf.agda

@@ -142,7 +142,7 @@ module _ {ℓ : Level} (R' : CommRing ℓ) where
       _ = snd R[1/ f ]AsCommRing
 
     f∈√⟨g⟩ : f ∈ √ ⟨ g ⟩ₛ
-    f∈√⟨g⟩ = isEquivRel→effectiveIso ∼PropValued ∼EquivRel _ _ .fun Df≤Dg .fst zero
+    f∈√⟨g⟩ = √FGIdealCharLImpl _ _ (isEquivRel→effectiveIso ∼PropValued ∼EquivRel _ _ .fun Df≤Dg .fst) zero
 
 
  -- The structure presheaf on BO
@@ -251,11 +251,11 @@ module _ {ℓ : Level} (R' : CommRing ℓ) where
 
       -- crucial facts about radical ideals
       h∈√⟨f⟩ : h ∈ √ ⟨ f ⟩[ R' ]
-      h∈√⟨f⟩ = isEquivRel→effectiveIso ∼PropValued ∼EquivRel _ _ .fun DHelper .fst zero
+      h∈√⟨f⟩ = √FGIdealCharLImpl _ _ (isEquivRel→effectiveIso ∼PropValued ∼EquivRel _ _ .fun DHelper .fst) zero
 
       f∈√⟨h⟩ : ∀ i → f i ∈ √ ⟨ h ⟩ₛ
-      f∈√⟨h⟩ i = isEquivRel→effectiveIso ∼PropValued ∼EquivRel _ _ .fun
-                   (sym DHelper) .fst i
+      f∈√⟨h⟩ = √FGIdealCharLImpl _ _ (isEquivRel→effectiveIso ∼PropValued ∼EquivRel _ _ .fun
+                   (sym DHelper) .fst)
 
       ff∈√⟨h⟩ : ∀ i j → f i · f j ∈ √ ⟨ h ⟩ₛ
       ff∈√⟨h⟩ i j = √ ⟨ h ⟩ₛ .snd .·Closed (f i) (f∈√⟨h⟩ j)

Cubical/AlgebraicGeometry/ZariskiLattice/StructureSheafPullback.agda

@@ -166,7 +166,7 @@ module _ (R' : CommRing ℓ) where
     Df≤Dg = subst2 _≤_ (sym p) (sym q) 𝔞≤𝔟
 
     f∈√⟨g⟩ : f ∈ √ ⟨ g ⟩
-    f∈√⟨g⟩ = isEquivRel→effectiveIso ∼PropValued ∼EquivRel _ _ .fun Df≤Dg .fst zero
+    f∈√⟨g⟩ = √FGIdealCharLImpl _ _ (isEquivRel→effectiveIso ∼PropValued ∼EquivRel _ _ .fun Df≤Dg .fst) zero
 
 
  open PreSheafFromUniversalProp ZariskiCat P 𝓕 uniqueHom
@@ -278,16 +278,16 @@ module _ (R' : CommRing ℓ) where
     DHelper = Dh≡𝔞∨𝔟 ∙ cong₂ (_∨z_) (sym Df≡𝔞) (sym Dg≡𝔟)
 
     f∈√⟨h⟩ : f ∈ √ ⟨ h ⟩
-    f∈√⟨h⟩ = isEquivRel→effectiveIso ∼PropValued ∼EquivRel _ _ .fun (sym DHelper) .fst zero
+    f∈√⟨h⟩ = √FGIdealCharLImpl _ _ (isEquivRel→effectiveIso ∼PropValued ∼EquivRel _ _ .fun (sym DHelper) .fst) zero
 
     g∈√⟨h⟩ : g ∈ √ ⟨ h ⟩
-    g∈√⟨h⟩ = isEquivRel→effectiveIso ∼PropValued ∼EquivRel _ _ .fun (sym DHelper) .fst one
+    g∈√⟨h⟩ = √FGIdealCharLImpl _ _ (isEquivRel→effectiveIso ∼PropValued ∼EquivRel _ _ .fun (sym DHelper) .fst) one
 
     fg∈√⟨h⟩ : (f · g) ∈ √ ⟨ h ⟩
     fg∈√⟨h⟩ = √ ⟨ h ⟩ .snd .·Closed f g∈√⟨h⟩
 
     1∈fgIdeal : 1r ∈ₕ ⟨ (f /1) , (g /1) ⟩ₕ
-    1∈fgIdeal = helper1 (isEquivRel→effectiveIso ∼PropValued ∼EquivRel _ _ .fun DHelper .fst zero)
+    1∈fgIdeal = helper1 $ √FGIdealCharLImpl _ _ (isEquivRel→effectiveIso ∼PropValued ∼EquivRel _ _ .fun DHelper .fst) zero
      where
      helper1 : h ∈ √ ⟨ f , g ⟩ₚ
              → 1r ∈ₕ ⟨ (f /1) , (g /1) ⟩ₕ