Examples of finite presentations of CommAlgebra's

Cubical/Algebra/Algebra/Properties.agda

@@ -31,9 +31,6 @@ private
   variable
     ℓ ℓ' ℓ'' ℓ''' : Level
 
-
-
-
 module AlgebraTheory (R : Ring ℓ) (A : Algebra R ℓ') where
   open RingStr (snd R) renaming (_+_ to _+r_ ; _·_ to _·r_)
   open AlgebraStr (A .snd)
@@ -77,6 +74,11 @@ module AlgebraHoms {R : Ring ℓ} where
   compIsAlgebraHom {g = g} {f} gh fh .pres- x = cong g (fh .pres- x) ∙ gh .pres- (f x)
   compIsAlgebraHom {g = g} {f} gh fh .pres⋆ r x = cong g (fh .pres⋆ r x) ∙ gh .pres⋆ r (f x)
 
+  _∘≃a_ : {A B C : Algebra R ℓ'}
+         → AlgebraEquiv B C → AlgebraEquiv A B → AlgebraEquiv A C
+  _∘≃a_  g f .fst = compEquiv (fst f) (fst g)
+  _∘≃a_  g f .snd = compIsAlgebraHom (g .snd) (f .snd)
+
   compAlgebraHom : {A : Algebra R ℓ'} {B : Algebra R ℓ''} {C : Algebra R ℓ'''}
               → AlgebraHom A B → AlgebraHom B C → AlgebraHom A C
   compAlgebraHom f g .fst = g .fst ∘ f .fst

Cubical/Algebra/CommAlgebra/Base.agda

@@ -23,7 +23,7 @@ open import Cubical.Reflection.RecordEquiv
 
 private
   variable
-    ℓ ℓ' ℓ'' ℓ''' : Level
+    ℓ ℓ' ℓ'' : Level
 
 record IsCommAlgebra (R : CommRing ℓ) {A : Type ℓ'}
                      (0a : A) (1a : A)

Cubical/Algebra/CommAlgebra/FGIdeal.agda

@@ -1,22 +1,37 @@
 {-# OPTIONS --safe #-}
 module Cubical.Algebra.CommAlgebra.FGIdeal where
 open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Structure
+open import Cubical.Foundations.Powerset
 
 open import Cubical.Data.FinData
 open import Cubical.Data.Nat
 open import Cubical.Data.Vec
 
 open import Cubical.Algebra.CommRing
-open import Cubical.Algebra.CommRing.FGIdeal renaming (generatedIdeal to generatedIdealCommRing)
+open import Cubical.Algebra.CommRing.FGIdeal using ()
+            renaming (generatedIdeal to generatedIdealCommRing;
+                      indInIdeal to ringIncInIdeal;
+                      0FGIdeal to 0FGIdealCommRing)
 open import Cubical.Algebra.CommAlgebra
 open import Cubical.Algebra.CommAlgebra.Ideal
 
 private
   variable
     ℓ : Level
+    R : CommRing ℓ
+
+generatedIdeal : {n : ℕ} (A : CommAlgebra R ℓ) → FinVec (fst A) n → IdealsIn A
+generatedIdeal A = generatedIdealCommRing (CommAlgebra→CommRing A)
+
+incInIdeal :   {n : ℕ} (A : CommAlgebra R ℓ)
+              (U : FinVec ⟨ A ⟩ n) (i : Fin n) → U i ∈ fst (generatedIdeal A U)
+incInIdeal A = ringIncInIdeal (CommAlgebra→CommRing A)
+
+syntax generatedIdeal A V = ⟨ V ⟩[ A ]
 
 module _ {R : CommRing ℓ} (A : CommAlgebra R ℓ) where
   open CommAlgebraStr (snd A)
 
-  generatedIdeal : {n : ℕ} → FinVec (fst A) n → IdealsIn A
-  generatedIdeal = generatedIdealCommRing (CommAlgebra→CommRing A)
+  0FGIdeal : {n : ℕ} → ⟨ replicateFinVec n 0a ⟩[ A ] ≡ (0Ideal A)
+  0FGIdeal = 0FGIdealCommRing (CommAlgebra→CommRing A)