Use CommIdeal everywhere (#691)

* WIP: Use CommIdeal * Use CommIdeal for CommRing-Quotients * Use CommIdeal for FGIdeals * Remove obsolete comment * Fix usages in CommAlgebra * Fix usages in CommAlgebra * Remove obsolete comment
agda · Apr 4, 2022 · 3ba70b9 · 3ba70b9
1 parent fa0fa06
commit 3ba70b9
Show file tree

Hide file tree

Showing 5 changed files with 43 additions and 36 deletions.
diff --git a/Cubical/Algebra/CommAlgebra/Ideal.agda b/Cubical/Algebra/CommAlgebra/Ideal.agda
@@ -24,4 +24,4 @@ module _ {R : CommRing ℓ} (A : CommAlgebra R ℓ) where
               → (0-closed : 0a ∈ I)
               → (·-closedLeft : {x : fst A} → (r : fst A) → x ∈ I → r · x ∈ I)
               → IdealsIn
-  makeIdeal = makeIdealCommRing (CommAlgebra→CommRing A)
+  makeIdeal = makeIdealCommRing {R = CommAlgebra→CommRing A}
diff --git a/Cubical/Algebra/CommAlgebra/QuotientAlgebra.agda b/Cubical/Algebra/CommAlgebra/QuotientAlgebra.agda
@@ -8,6 +8,7 @@ open import Cubical.HITs.SetQuotients hiding (_/_)
 
 open import Cubical.Algebra.CommRing
 open import Cubical.Algebra.CommRing.QuotientRing renaming (_/_ to _/Ring_) hiding ([_]/)
+open import Cubical.Algebra.CommRing.Ideal hiding (IdealsIn)
 open import Cubical.Algebra.CommAlgebra
 open import Cubical.Algebra.CommAlgebra.Ideal
 open import Cubical.Algebra.Ring
@@ -47,6 +48,7 @@ module _ {R : CommRing ℓ} (A : CommAlgebra R ℓ) where
                                        r ⋆ (x · y) ∎) i ]
 
           where
+                open CommIdeal using (isCommIdeal)
                 eq : (r : fst R) (x y : fst A) → x - y ∈ (fst I) →  [ r ⋆ x ] ≡ [ r ⋆ y ]
                 eq r x y x-y∈I = eq/ _ _
                   (subst (λ u → u ∈ fst I)
@@ -56,7 +58,7 @@ module _ {R : CommRing ℓ} (A : CommAlgebra R ℓ) where
                                                             - ⋆-lassoc r 1a y i ⟩
                     r ⋆ (1a · x) - r ⋆ (1a · y)     ≡[ i ]⟨ r ⋆ (·Lid x i) - r ⋆ (·Lid y i) ⟩
                     r ⋆ x - r ⋆ y ∎ )
-                  (isIdeal.·-closedLeft (snd I) _ x-y∈I))
+                  (isCommIdeal.·Closed (snd I) _ x-y∈I))
 
 
 [_]/ : {R : CommRing ℓ} {A : CommAlgebra R ℓ} {I : IdealsIn A}

diff --git a/Cubical/Algebra/CommRing/FGIdeal.agda b/Cubical/Algebra/CommRing/FGIdeal.agda
@@ -90,12 +90,10 @@ module _ (Ring@(R , str) : CommRing ℓ) where
                                                             ∙∙ ∑Ext λ i → ·Assoc r (α .fst i) (V i)
 
   generatedIdeal : {n : ℕ} → FinVec R n → IdealsIn Ring
-  generatedIdeal V = makeIdeal Ring
-                               (λ x → isLinearCombination V x , isPropPropTrunc)
-                               (isLinearCombination+ V)
-                               (isLinearCombination0 V)
-                               λ r → isLinearCombinationL· V r
-
+  fst (generatedIdeal V) = λ x → isLinearCombination V x , isPropPropTrunc
+  CommIdeal.isCommIdeal.+Closed (snd (generatedIdeal V)) = isLinearCombination+ V
+  CommIdeal.isCommIdeal.contains0 (snd (generatedIdeal V)) = isLinearCombination0 V
+  CommIdeal.isCommIdeal.·Closed (snd (generatedIdeal V)) = λ r → isLinearCombinationL· V r
 
 open CommIdeal.isCommIdeal
 genIdeal : {n : ℕ} (R : CommRing ℓ) → FinVec (fst R) n → CommIdeal.CommIdeal R

diff --git a/Cubical/Algebra/CommRing/Ideal.agda b/Cubical/Algebra/CommRing/Ideal.agda
@@ -34,33 +34,6 @@ private
   variable
     ℓ : Level
 
-IdealsIn : (R : CommRing ℓ) → Type _
-IdealsIn R = IdealsInRing (CommRing→Ring R)
-
-module _ (Ring@(R , str) : CommRing ℓ) where
-  open CommRingStr str
-  makeIdeal : (I : R → hProp ℓ)
-              → (+-closed : {x y : R} → x ∈p I → y ∈p I → (x + y) ∈p I)
-              → (0r-closed : 0r ∈p I)
-              → (·-closedLeft : {x : R} → (r : R) → x ∈p I → r · x ∈p I)
-              → IdealsIn (R , str)
-  makeIdeal I +-closed 0r-closed ·-closedLeft = I ,
-    (record
-       { +-closed = +-closed
-       ; -closed = λ x∈pI → subst-∈p I (useSolver _)
-                             (·-closedLeft (- 1r) x∈pI)
-       ; 0r-closed = 0r-closed
-       ; ·-closedLeft = ·-closedLeft
-       ; ·-closedRight = λ r x∈pI →
-                       subst-∈p I
-                             (·Comm r _)
-                             (·-closedLeft r x∈pI)
-       })
-       where useSolver : (x : R) → - 1r · x ≡ - x
-             useSolver = solve Ring
-
-
--- better?
 module CommIdeal (R' : CommRing ℓ) where
  private R = fst R'
  open CommRingStr (snd R')
@@ -329,3 +302,37 @@ module CommIdeal (R' : CommRing ℓ) where
 
  ·iAbsorb+i : ∀ (I J : CommIdeal) → I +i (I ·i J) ≡ I
  ·iAbsorb+i I J = CommIdeal≡Char (·iAbsorb+iLIncl I J) (·iAbsorb+iRIncl I J)
+
+
+IdealsIn : (R : CommRing ℓ) → Type _
+IdealsIn R = CommIdeal.CommIdeal R
+
+module _ {R : CommRing ℓ} where
+  open CommRingStr (snd R)
+  open isIdeal
+  open CommIdeal R
+  open isCommIdeal
+  makeIdeal : (I : fst R → hProp ℓ)
+              → (+-closed : {x y : fst R} → x ∈p I → y ∈p I → (x + y) ∈p I)
+              → (0r-closed : 0r ∈p I)
+              → (·-closedLeft : {x : fst R} → (r : fst R) → x ∈p I → r · x ∈p I)
+              → IdealsIn R
+  fst (makeIdeal I +-closed 0r-closed ·-closedLeft) = I
+  +Closed (snd (makeIdeal I +-closed 0r-closed ·-closedLeft)) = +-closed
+  contains0 (snd (makeIdeal I +-closed 0r-closed ·-closedLeft)) = 0r-closed
+  ·Closed (snd (makeIdeal I +-closed 0r-closed ·-closedLeft)) = ·-closedLeft
+
+
+  CommIdeal→Ideal : IdealsIn R → IdealsInRing (CommRing→Ring R)
+  fst (CommIdeal→Ideal I) = fst I
+  +-closed (snd (CommIdeal→Ideal I)) = +Closed (snd I)
+  -closed (snd (CommIdeal→Ideal I)) =  λ x∈pI → subst-∈p (fst I) (useSolver _)
+                                                           (·Closed (snd I) (- 1r) x∈pI)
+                                         where useSolver : (x : fst R) → - 1r · x ≡ - x
+                                               useSolver = solve R
+  0r-closed (snd (CommIdeal→Ideal I)) = contains0 (snd I)
+  ·-closedLeft (snd (CommIdeal→Ideal I)) = ·Closed (snd I)
+  ·-closedRight (snd (CommIdeal→Ideal I)) = λ r x∈pI →
+                                             subst-∈p (fst I)
+                                                   (·Comm r _)
+                                                   (·Closed (snd I) r x∈pI)
diff --git a/Cubical/Algebra/CommRing/QuotientRing.agda b/Cubical/Algebra/CommRing/QuotientRing.agda
@@ -21,7 +21,7 @@ R / I =
                              (elimProp2 (λ _ _ → squash/ _ _)
                                         commEq))
    where
-       asRing = (CommRing→Ring R) /Ring I
+       asRing = (CommRing→Ring R) /Ring (CommIdeal→Ideal I)
        _·/_ : fst asRing → fst asRing → fst asRing
        _·/_ = RingStr._·_ (snd asRing)
        commEq : (x y : fst R) → ([ x ] ·/ [ y ]) ≡ ([ y ] ·/ [ x ])