polynomial ring is fp

agda · Aug 30, 2024 · 12dedb4 · 12dedb4
1 parent 9ce0eff
commit 12dedb4
Show file tree

Hide file tree

Showing 3 changed files with 21 additions and 9 deletions.
diff --git a/Cubical/Algebra/CommAlgebra/FGIdeal.agda b/Cubical/Algebra/CommAlgebra/FGIdeal.agda
@@ -33,5 +33,5 @@ syntax generatedIdeal A V = ⟨ V ⟩[ A ]
 module _ {R : CommRing ℓ} (A : CommAlgebra R ℓ) where
   open CommRingStr (A .fst .snd)
 
-  0FGIdeal : {n : ℕ} → ⟨ replicateFinVec n 0r ⟩[ A ] ≡ (0Ideal R A)
-  0FGIdeal = 0FGIdealCommRing (CommAlgebra→CommRing A)
+  0FGIdeal≡0Ideal : {n : ℕ} → ⟨ replicateFinVec n 0r ⟩[ A ] ≡ (0Ideal R A)
+  0FGIdeal≡0Ideal = 0FGIdealCommRing (CommAlgebra→CommRing A)
diff --git a/Cubical/Algebra/CommAlgebra/FP/Base.agda b/Cubical/Algebra/CommAlgebra/FP/Base.agda
@@ -27,9 +27,8 @@ private
     ℓ ℓ' : Level
 
 module _ (R : CommRing ℓ) where
-  abstract
-    Polynomials : (n : ℕ) → CommAlgebra R ℓ
-    Polynomials n = R [ Fin n ]ₐ
+  Polynomials : (n : ℕ) → CommAlgebra R ℓ
+  Polynomials n = R [ Fin n ]ₐ
 
   FPCAlgebra : {m : ℕ} (n : ℕ) (relations : FinVec ⟨ Polynomials n ⟩ₐ m) → CommAlgebra R ℓ
   FPCAlgebra n relations = Polynomials n / ⟨ relations ⟩[ Polynomials n ]

diff --git a/Cubical/Algebra/CommAlgebra/FP/Instances.agda b/Cubical/Algebra/CommAlgebra/FP/Instances.agda
@@ -7,7 +7,7 @@
   * R/⟨x₁,...,xₙ⟩    = R[⊥]/⟨x₁,...,xₙ⟩
   * R/⟨x⟩            (as special case of the above)
 -}
-{-# OPTIONS --safe #-}
+{-# OPTIONS --safe --lossy-unification #-}
 module Cubical.Algebra.CommAlgebra.FP.Instances where
 
 open import Cubical.Foundations.Prelude
@@ -30,7 +30,7 @@ open import Cubical.Algebra.CommRing.FGIdeal using (inclOfFGIdeal)
 open import Cubical.Algebra.CommAlgebra
 open import Cubical.Algebra.CommAlgebra.Instances.Polynomials
 open import Cubical.Algebra.CommAlgebra.QuotientAlgebra
-open import Cubical.Algebra.CommAlgebra.Ideal using (IdealsIn)
+open import Cubical.Algebra.CommAlgebra.Ideal using (IdealsIn; 0Ideal)
 open import Cubical.Algebra.CommAlgebra.FGIdeal
 -- open import Cubical.Algebra.CommAlgebra.Instances.Initial
 open import Cubical.Algebra.CommAlgebra.Instances.Unit
@@ -44,18 +44,31 @@ private
 
 module _ (R : CommRing ℓ) where
   open FinitePresentation
-{-
 
   module _ (n : ℕ) where
+    private
+      abstract
+        p : 0Ideal R (Polynomials R n) ≡ ⟨ emptyFinVec ⟨ Polynomials R n ⟩ₐ ⟩[ _ ]
+        p = sym $ 0FGIdeal≡0Ideal (Polynomials R n)
+
+      compute :
+        CommAlgebraEquiv (Polynomials R n) $ (Polynomials R n) / ⟨ emptyFinVec ⟨ Polynomials R n ⟩ₐ ⟩[ _ ]
+      compute =
+        transport (λ i → CommAlgebraEquiv (Polynomials R n) ((Polynomials R n) / (p i))) $
+          zeroIdealQuotient (Polynomials R n)
+
     polynomialsFP : FinitePresentation R (Polynomials R n)
     polynomialsFP =
       record {
         n = n ;
         m = 0 ;
         relations = emptyFinVec ⟨ Polynomials R n ⟩ₐ ;
-        equiv = invCommAlgebraEquiv {!zeroIdealQuotient!}
+        equiv = invCommAlgebraEquiv compute
       }
 
+{-
+
+
   {- Every (multivariate) polynomial algebra is finitely presented -}
   module _ (n : ℕ) where
     private