WIP

Cubical/Algebra/CommAlgebra/FP/Base.agda

@@ -1,4 +1,4 @@
-{-# OPTIONS --safe #-}
+{-# OPTIONS --safe --lossy-unification #-}
 module Cubical.Algebra.CommAlgebra.FP.Base where
 
 open import Cubical.Foundations.Prelude
@@ -11,6 +11,7 @@ open import Cubical.Foundations.Structure
 open import Cubical.Data.FinData
 open import Cubical.Data.Nat
 open import Cubical.Data.Vec
+open import Cubical.Data.Sigma
 
 open import Cubical.HITs.PropositionalTruncation
 
@@ -30,20 +31,30 @@ module _ (R : CommRing ℓ) where
   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 ]
-
-  record FinitePresentation (A : CommAlgebra R ℓ') : Type (ℓ-max ℓ ℓ') where
+  record FinitePresentation : Type ℓ where
     no-eta-equality
     field
       n : ℕ
       m : ℕ
       relations : FinVec ⟨ Polynomials n ⟩ₐ m
-      equiv : CommAlgebraEquiv (FPCAlgebra n relations) A
 
-  abstract
-    isFP : (A : CommAlgebra R ℓ') → Type (ℓ-max ℓ ℓ')
-    isFP A = ∥ FinitePresentation A ∥₁
+    opaque
+      ideal : IdealsIn R (Polynomials n)
+      ideal = ⟨ relations ⟩[ Polynomials n ]
+
+    opaque
+      algebra : CommAlgebra R ℓ
+      algebra = Polynomials n / ideal
+
+      π : CommAlgebraHom (Polynomials n) algebra
+      π = quotientHom (Polynomials n) ideal
+
+      generator : (i : Fin n) → ⟨ algebra ⟩ₐ
+      generator = ⟨ π ⟩ₐ→ ∘ var
+
+  isFP : (A : CommAlgebra R ℓ') → Type (ℓ-max ℓ ℓ')
+  isFP A = ∃[ p ∈ FinitePresentation ] CommAlgebraEquiv (FinitePresentation.algebra p) A
 
-    isFPIsProp : {A : CommAlgebra R ℓ} → isProp (isFP A)
+  opaque
+    isFPIsProp : {A : CommAlgebra R ℓ'} → isProp (isFP A)
     isFPIsProp = isPropPropTrunc

Cubical/Algebra/CommAlgebra/FP/Instances.agda

@@ -32,7 +32,7 @@ open import Cubical.Algebra.CommAlgebra.Instances.Polynomials
 open import Cubical.Algebra.CommAlgebra.QuotientAlgebra
 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.Initial
 open import Cubical.Algebra.CommAlgebra.Instances.Unit
 
 open import Cubical.Algebra.CommAlgebra.FP.Base
@@ -48,7 +48,7 @@ module _ (R : CommRing ℓ) where
   {- Every (multivariate) polynomial algebra is finitely presented -}
   module _ (n : ℕ) where
     private
-      abstract
+      opaque
         p : 0Ideal R (Polynomials R n) ≡ ⟨ emptyFinVec ⟨ Polynomials R n ⟩ₐ ⟩[ _ ]
         p = sym $ 0FGIdeal≡0Ideal (Polynomials R n)
 
@@ -59,29 +59,44 @@ module _ (R : CommRing ℓ) where
         transport (λ i → CommAlgebraEquiv (Polynomials R n) ((Polynomials R n) / (p i))) $
           zeroIdealQuotient (Polynomials R n)
 
-    polynomialsFP : FinitePresentation R (Polynomials R n)
+    polynomialsFP : FinitePresentation R
     polynomialsFP =
       record {
         n = n ;
         m = 0 ;
-        relations = emptyFinVec ⟨ Polynomials R n ⟩ₐ ;
-        equiv = invCommAlgebraEquiv compute
+        relations = emptyFinVec ⟨ Polynomials R n ⟩ₐ
       }
 
-{-
-
+    opaque
+      unfolding algebra ideal
+      isFPPolynomials : isFP R (Polynomials R n)
+      isFPPolynomials = ∣ polynomialsFP , invCommAlgebraEquiv compute ∣₁
 
 
   {- The initial R-algebra is finitely presented -}
   private
     R[⊥] : CommAlgebra R ℓ
-    R[⊥] = Polynomials 0
+    R[⊥] = Polynomials R 0
 
-    emptyGen : FinVec (fst R[⊥]) 0
+    emptyGen : FinVec ⟨ R[⊥] ⟩ₐ 0
     emptyGen = λ ()
 
+    initialAlgFP : FinitePresentation R
+    initialAlgFP = record { n = 0 ; m = 0 ; relations = emptyGen }
+
     R[⊥]/⟨0⟩ : CommAlgebra R ℓ
-    R[⊥]/⟨0⟩ = FPAlgebra 0 emptyGen
+    R[⊥]/⟨0⟩ = algebra initialAlgFP
+{-
+
+    R[⊥]/⟨0⟩IsInitial : (B : CommAlgebra R ℓ)
+                     → isContr (CommAlgebraHom R[⊥]/⟨0⟩ B)
+    R[⊥]/⟨0⟩IsInitial B = {!!} , {!!}
+      where
+        iHom : CommAlgebraHom R[⊥]/⟨0⟩ B
+        iHom = inducedHom 0 emptyGen B (λ ()) (λ ())
+        uniqueness : (f : CommAlgebraHom R[⊥]/⟨0⟩ B) →
+                     iHom ≡ f
+        uniqueness f = unique 0 emptyGen B (λ ()) (λ ()) f (λ ())
 
   R[⊥]/⟨0⟩IsInitial : (B : CommAlgebra R ℓ)
                      → isContr (CommAlgebraHom R[⊥]/⟨0⟩ B)

Cubical/Algebra/CommAlgebra/FP/Properties.agda

@@ -0,0 +1,33 @@
+{-# OPTIONS --safe #-}
+{-
+  Universal property of finitely presented algebras
+-}
+module Cubical.Algebra.CommAlgebra.FP.Properties where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Equiv
+open import Cubical.Foundations.Isomorphism
+open import Cubical.Foundations.Function
+open import Cubical.Foundations.HLevels
+open import Cubical.Foundations.Structure
+
+open import Cubical.Data.FinData
+open import Cubical.Data.Nat
+open import Cubical.Data.Vec
+
+open import Cubical.HITs.PropositionalTruncation
+
+open import Cubical.Algebra.CommRing
+open import Cubical.Algebra.CommAlgebra
+open import Cubical.Algebra.CommAlgebra.Instances.Polynomials
+open import Cubical.Algebra.CommAlgebra.QuotientAlgebra
+open import Cubical.Algebra.CommAlgebra.Ideal
+open import Cubical.Algebra.CommAlgebra.FGIdeal
+open import Cubical.Algebra.CommAlgebra.FP.Base
+
+
+private
+  variable
+    ℓ ℓ' : Level
+
+module _ (R : CommRing ℓ) (fp : FinitePresentation R) where

Cubical/Algebra/CommAlgebra/Instances/Polynomials.agda

@@ -2,30 +2,57 @@
 module Cubical.Algebra.CommAlgebra.Instances.Polynomials where
 
 open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Function using (_$_; _∘_)
+open import Cubical.Foundations.Structure using (withOpaqueStr)
+open import Cubical.Foundations.Isomorphism using (isoFunInjective)
+
+open import Cubical.Data.Nat
+open import Cubical.Data.FinData
 
 open import Cubical.Algebra.CommRing.Base
 open import Cubical.Algebra.CommAlgebra.Base
-open import Cubical.Algebra.CommRing.Instances.Polynomials.Typevariate
+open import Cubical.Algebra.CommRing.Instances.Polynomials.Typevariate as Poly hiding (var)
+import Cubical.Algebra.CommRing.Instances.Polynomials.Typevariate.UniversalProperty
+  as Poly
 
 private
   variable
     ℓ ℓ' ℓ'' : Level
 
-opaque
-  _[_]ₐ : (R : CommRing ℓ) (I : Type ℓ') → CommAlgebra R (ℓ-max ℓ ℓ')
-  R [ I ]ₐ = (R [ I ]) , constPolynomial R I
+_[_]ₐ : (R : CommRing ℓ) (I : Type ℓ') → CommAlgebra R (ℓ-max ℓ ℓ')
+R [ I ]ₐ = (R [ I ]) , constPolynomial R I
+
+module _ {R : CommRing ℓ} where
+  evPolyIn : {n : ℕ} (A : CommAlgebra R ℓ')
+            → ⟨ R [ Fin n ]ₐ ⟩ₐ → FinVec ⟨ A ⟩ₐ n → ⟨ A ⟩ₐ
+  evPolyIn {n = n} A P v = Poly.inducedHom (CommAlgebra→CommRing A) (A .snd) v $cr P
+
+module _ {R : CommRing ℓ} {I : Type ℓ'} where
+  var : I → ⟨ R [ I ]ₐ ⟩ₐ
+  var = Poly.var
+
+  inducedHom : (A : CommAlgebra R ℓ'') (φ : I → ⟨ A ⟩ₐ )
+             → CommAlgebraHom (R [ I ]ₐ) A
+  inducedHom A ϕ =
+    CommAlgebraHomFromCommRingHom
+      f
+      (λ _ _ → refl)
+    where f : CommRingHom _ _
+          f = Poly.inducedHom (CommAlgebra→CommRing A) (A .snd) ϕ
+
+  inducedHomUnique :
+    (A : CommAlgebra R ℓ'') (φ : I → ⟨ A ⟩ₐ )
+    → (f : CommAlgebraHom (R [ I ]ₐ) A) → ((i : I) → ⟨ f ⟩ₐ→ ∘ var ≡ φ)
+    → f ≡ inducedHom A φ
+  inducedHomUnique A φ f p = {!isoFunInjective (homMapIso A) f (inducedHom A φ) λ j i → p i j!}
+    --
 
 {-
 evaluateAt : {R : CommRing ℓ} {I : Type ℓ'} (A : CommAlgebra R ℓ'')
              (f : CommAlgebraHom (R [ I ]) A)
              → (I → fst A)
 evaluateAt A f x = f $a (Construction.var x)
 
-inducedHom : {R : CommRing ℓ} {I : Type ℓ'} (A : CommAlgebra R ℓ'')
-             (φ : I → fst A )
-             → CommAlgebraHom (R [ I ]) A
-inducedHom A φ = Theory.inducedHom A φ
-
 
 homMapIso : {R : CommRing ℓ} {I : Type ℓ''} (A : CommAlgebra R ℓ')
              → Iso (CommAlgebraHom (R [ I ]) A) (I → (fst A))

Cubical/Algebra/CommRing/Instances/Polynomials/Typevariate/Properties.agda

@@ -14,7 +14,7 @@ open import Cubical.HITs.SetTruncation
 
 open import Cubical.Algebra.CommRing
 open import Cubical.Algebra.CommRing.Instances.Polynomials.Typevariate.Base
-open import Cubical.Algebra.CommRing.Instances.Polynomials.Typevariate.UniversalProperty public
+open import Cubical.Algebra.CommRing.Instances.Polynomials.Typevariate.UniversalProperty
 
 open import Cubical.Data.Empty as ⊥
 open import Cubical.Data.Sigma