Universal property of list-based polynomials

Cubical/Algebra/Algebra/Properties.agda

@@ -46,6 +46,13 @@ module AlgebraTheory (R : Ring ℓ) (A : Algebra R ℓ') where
                        (0r ⋆ x) + (0r ⋆ x) ∎
     in RingTheory.+Idempotency→0 (Algebra→Ring A) (0r ⋆ x) idempotent-+
 
+  0a-absorbs : (r : ⟨ R ⟩) → r ⋆ 0a ≡ 0a
+  0a-absorbs r = RingTheory.+Idempotency→0 (Algebra→Ring A) (r ⋆ 0a) helper
+    where helper =
+             r ⋆ 0a              ≡⟨ cong (λ u → r ⋆ u) (sym (RingTheory.0Idempotent (Algebra→Ring A))) ⟩
+             r ⋆ (0a + 0a)       ≡⟨ ⋆DistR+ r 0a 0a ⟩
+             (r ⋆ 0a) + (r ⋆ 0a) ∎
+
   ⋆Dist· : (x y : ⟨ R ⟩) (a b : ⟨ A ⟩) → (x ·r y) ⋆ (a · b) ≡ (x ⋆ a) · (y ⋆ b)
   ⋆Dist· x y a b = (x ·r y) ⋆ (a · b) ≡⟨ ⋆AssocR _ _ _ ⟩
                    a · ((x ·r y) ⋆ b) ≡⟨ cong (a ·_) (⋆Assoc _ _ _) ⟩

Cubical/Algebra/CommAlgebra/UnivariatePolyList.agda

@@ -2,29 +2,218 @@
 module Cubical.Algebra.CommAlgebra.UnivariatePolyList where
 
 open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Structure
 open import Cubical.Foundations.Isomorphism
 
+open import Cubical.Data.Sigma
+
 open import Cubical.Algebra.Ring
 open import Cubical.Algebra.CommRing
+open import Cubical.Algebra.AbGroup
 open import Cubical.Algebra.CommAlgebra
+open import Cubical.Algebra.Algebra
 open import Cubical.Algebra.CommRing.Instances.Polynomials.UnivariatePolyList
 open import Cubical.Algebra.Polynomials.UnivariateList.Base
 open import Cubical.Algebra.Polynomials.UnivariateList.Properties
 
+open import Cubical.Tactics.CommRingSolver.Reflection
+
 private variable
-  ℓ : Level
+  ℓ ℓ' : Level
 
 module _ (R : CommRing ℓ) where
-  open CommRingStr ⦃...⦄
+  open RingStr ⦃...⦄    -- Not CommRingStr, so it can be used together with AlgebraStr
   open PolyModTheory R
   private
     ListPoly = UnivariatePolyList R
     instance
-      _ = snd ListPoly
-      _ = snd R
+      _ = snd (CommRing→Ring ListPoly)
+      _ = snd (CommRing→Ring R)
 
   ListPolyCommAlgebra : CommAlgebra R ℓ
   ListPolyCommAlgebra =
     Iso.inv (CommAlgChar.CommAlgIso R)
             (ListPoly ,
              constantPolynomialHom R)
+
+  {- Universal Property -}
+  module _ (A : Algebra (CommRing→Ring R) ℓ') where
+    open AlgebraStr ⦃...⦄ using (_⋆_; 0a; 1a; ⋆IdL; ⋆DistL+; ⋆DistR+; ⋆AssocL; ⋆AssocR; ⋆Assoc)
+    private instance
+      _ = snd A
+      _ = snd (Algebra→Ring A)
+      _ = snd (CommAlgebra→Algebra ListPolyCommAlgebra)
+
+    module _ (x : ⟨ A ⟩) where
+      open AlgebraTheory using (0-actsNullifying; 0a-absorbs)
+      open RingTheory using (0RightAnnihilates; 0LeftAnnihilates)
+      open AbGroupTheory using (comm-4)
+      open PolyMod using (ElimProp; elimProp2; isSetPoly)
+
+      private
+        X : ⟨ ListPolyCommAlgebra ⟩
+        X = 0r ∷ 1r ∷ []
+
+      inducedMap : ⟨ ListPolyCommAlgebra ⟩ → ⟨ A ⟩
+      inducedMap [] = 0a
+      inducedMap (a ∷ p) = a ⋆ 1a + (x · inducedMap p)
+      inducedMap (drop0 i) = eq i
+        where
+          eq = 0r ⋆ 1a + (x · 0a) ≡[ i ]⟨  0-actsNullifying (CommRing→Ring R) A 1a i + (x · 0a) ⟩
+               0a + (x · 0a)      ≡⟨ +IdL (x · 0a) ⟩
+               x · 0a             ≡⟨ 0RightAnnihilates (Algebra→Ring A) x ⟩
+               0a ∎
+
+      private
+        ϕ = inducedMap
+        inducedMap1 : ϕ (1r ∷ []) ≡ 1a
+        inducedMap1 =
+          ϕ [ 1r ]            ≡⟨⟩
+          1r ⋆ 1a + (x · 0a)  ≡[ i ]⟨ ⋆IdL 1a i + 0RightAnnihilates (Algebra→Ring A) x i ⟩
+          1a + 0a             ≡⟨ +IdR 1a ⟩
+          1a ∎
+
+        inducedMapGenerator : ϕ X ≡ x
+        inducedMapGenerator =
+          0r ⋆ 1a + (x · ϕ (1r ∷ [])) ≡[ i ]⟨  0-actsNullifying
+                                       (CommRing→Ring R) A 1a i + (x · ϕ (1r ∷ [])) ⟩
+          0a + (x · ϕ (1r ∷ []))      ≡⟨ +IdL _ ⟩
+          x · ϕ (1r ∷ [])             ≡[ i ]⟨ x · inducedMap1 i ⟩
+          x · 1a                      ≡⟨ ·IdR _ ⟩
+          x ∎
+
+        inducedMapPolyConst⋆ : (r : ⟨ R ⟩) (p : _) → ϕ (r PolyConst* p) ≡ r ⋆ ϕ p
+        inducedMapPolyConst⋆ r =
+          ElimProp R
+            (λ p → ϕ (r PolyConst* p) ≡ r ⋆ ϕ p)
+            (ϕ (r PolyConst* []) ≡⟨⟩
+             ϕ []       ≡⟨⟩
+             0a                  ≡⟨ sym (0a-absorbs (CommRing→Ring R) A r) ⟩
+             r ⋆ 0a ∎)
+            (λ s p IH →
+              ϕ (r PolyConst* (s ∷ p))              ≡⟨⟩
+              ϕ ((r · s) ∷ (r PolyConst* p))        ≡⟨⟩
+              (r · s) ⋆ 1a + x · ϕ (r PolyConst* p) ≡[ i ]⟨ ⋆Assoc r s 1a i + x · IH i ⟩
+              r ⋆ (s ⋆ 1a) + x · (r ⋆ ϕ p)          ≡⟨ step s p ⟩
+              r ⋆ (s ⋆ 1a) + r ⋆ (x · ϕ p)          ≡⟨ sym (⋆DistR+ r (s ⋆ 1a) (x · ϕ p)) ⟩
+              r ⋆ (s ⋆ 1a + x · ϕ p)                ≡⟨⟩
+              r ⋆ ϕ (s ∷ p) ∎)
+            (is-set _ _)
+            where
+              step : (s : ⟨ R ⟩) (p : _) → _ ≡ _
+              step s p i = r ⋆ (s ⋆ 1a) + sym (⋆AssocR r x (ϕ p)) i
+
+        inducedMap⋆ : (r : ⟨ R ⟩) (p : _) → ϕ (r ⋆ p) ≡ r ⋆ ϕ p
+        inducedMap⋆ r p =
+          ϕ (r ⋆ p)                   ≡⟨ cong ϕ (sym (PolyConst*≡Poly* r p)) ⟩
+          ϕ (r PolyConst* p)          ≡⟨ inducedMapPolyConst⋆ r p ⟩
+          r ⋆ ϕ p ∎
+
+        inducedMap+ : (p q : _) → ϕ (p + q) ≡ ϕ p + ϕ q
+        inducedMap+ =
+          elimProp2 R
+            (λ x y → ϕ (x + y) ≡ ϕ x + ϕ y)
+            (0a ≡⟨ sym (+IdR _) ⟩ 0a + 0a ∎)
+            (λ r p _ →
+              ϕ ((r ∷ p) + []) ≡⟨⟩
+              ϕ (r ∷ p)        ≡⟨ sym (+IdR _) ⟩
+              (ϕ (r ∷ p) + 0a) ∎)
+            (λ s q _ →
+              ϕ ([] + (s ∷ q)) ≡⟨⟩
+              ϕ (s ∷ q)        ≡⟨ sym (+IdL _) ⟩
+              0a + ϕ (s ∷ q)   ∎)
+            (λ r s p q IH →
+              ϕ ((r ∷ p) + (s ∷ q))                   ≡⟨⟩
+              ϕ (r + s ∷ p + q)                       ≡⟨⟩
+              (r + s) ⋆ 1a + x · ϕ (p + q)            ≡[ i ]⟨ (r + s) ⋆ 1a + x · IH i ⟩
+              (r + s) ⋆ 1a + (x · (ϕ p + ϕ q))        ≡[ i ]⟨ step1 r s p q i ⟩
+              (r ⋆ 1a + s ⋆ 1a) + (x · ϕ p + x · ϕ q) ≡⟨ comm-4 (Algebra→AbGroup A) _ _ _ _ ⟩
+              (r ⋆ 1a + x · ϕ p) + (s ⋆ 1a + x · ϕ q) ≡⟨⟩
+              ϕ (r ∷ p) + ϕ (s ∷ q) ∎)
+            (is-set _ _)
+            where step1 : (r s : ⟨ R ⟩) (p q : _) → _ ≡ _
+                  step1 r s p q i = ⋆DistL+ r s 1a i + ·DistR+ x (ϕ p) (ϕ q) i
+                  M = (AbGroup→CommMonoid (Algebra→AbGroup A))
+
+        inducedMap· : (p q : _) → ϕ (p · q) ≡ ϕ p · ϕ q
+        inducedMap· p q =
+          ElimProp R
+            (λ p → ϕ (p · q) ≡ ϕ p · ϕ q)
+            (ϕ ([] · q)      ≡⟨⟩
+             ϕ []            ≡⟨⟩
+             0a                       ≡⟨ sym (0LeftAnnihilates (Algebra→Ring A) _) ⟩
+             0a · ϕ q ∎)
+            (λ r p IH →
+              ϕ ((r ∷ p) · q)                           ≡⟨⟩
+              ϕ ((r PolyConst* q) + (0r ∷ (p · q)))     ≡⟨ step1 r p ⟩
+              ϕ (r PolyConst* q) + ϕ (0r ∷ (p · q))     ≡⟨ step2 r p ⟩
+              ϕ (r ⋆ q) + ϕ (0r ∷ (p · q))              ≡⟨ step3 r p ⟩
+              r ⋆ ϕ q + ϕ (0r ∷ (p · q))                ≡⟨ step4 r p ⟩
+              r ⋆ ϕ q + (0a + x · ϕ (p · q))            ≡⟨ step5 r p ⟩
+              r ⋆ ϕ q + x · ϕ (p · q)                   ≡⟨ step6 r p IH ⟩
+              r ⋆ ϕ q + x · (ϕ p · ϕ q)                 ≡⟨ step7 r p ⟩
+              r ⋆ (1a · ϕ q) + (x · ϕ p) · ϕ q          ≡⟨ step8 r p ⟩
+              (r ⋆ 1a) · ϕ q + (x · ϕ p) · ϕ q          ≡⟨ sym (·DistL+ _ _ _) ⟩
+              (r ⋆ 1a + x · ϕ p) · ϕ q                  ≡⟨⟩
+              ϕ (r ∷ p) · ϕ q ∎)
+            (is-set _ _) p
+          where
+            step1 : (r : ⟨ R ⟩) (p : _) → _ ≡ _
+            step1 r p = inducedMap+ (r PolyConst* q) (0r ∷ (p Poly* q))
+
+            step2 : (r : ⟨ R ⟩) (p : _) → _ ≡ _
+            step2 r p i = ϕ (PolyConst*≡Poly* r q i) + ϕ (0r ∷ (p Poly* q))
+
+            step3 : (r : ⟨ R ⟩) (p : _) → _ ≡ _
+            step3 r p i = inducedMap⋆ r q i + ϕ (0r ∷ (p Poly* q))
+
+            step4 : (r : ⟨ R ⟩) (p : _) → _ ≡ _
+            step4 r p i = r ⋆ ϕ q + (0-actsNullifying (CommRing→Ring R) A 1a i + x · ϕ (p · q))
+
+            step5 : (r : ⟨ R ⟩) (p : _) → _ ≡ _
+            step5 r p i = r ⋆ ϕ q + +IdL (x · ϕ (p · q)) i
+
+            step6 : (r : ⟨ R ⟩) (p : _) → _ → _ ≡ _
+            step6 r p IH i = r ⋆ ϕ q + x · IH i
+
+            step7 : (r : ⟨ R ⟩) (p : _) → _ ≡ _
+            step7 r p i = r ⋆ (sym (·IdL (ϕ q)) i) + ·Assoc x (ϕ p) (ϕ q) i
+
+            step8 : (r : ⟨ R ⟩) (p : _) → _ ≡ _
+            step8 r p i = sym (⋆AssocL r 1a (ϕ q)) i + (x · ϕ p) · ϕ q
+
+      inducedHom : AlgebraHom (CommAlgebra→Algebra ListPolyCommAlgebra) A
+      fst inducedHom = inducedMap
+      snd inducedHom = makeIsAlgebraHom inducedMap1 inducedMap+ inducedMap· inducedMap⋆
+
+      inducedHomOnGenerator : fst inducedHom X ≡ x
+      inducedHomOnGenerator = inducedMapGenerator
+
+      {- Uniqueness -}
+      inducedHomUnique : (f : AlgebraHom (CommAlgebra→Algebra ListPolyCommAlgebra) A)
+                         → fst f X ≡ x
+                         → f ≡ inducedHom
+      inducedHomUnique f fX≡x =
+        Σ≡Prop
+          (λ _ → isPropIsAlgebraHom _ _ _ _)
+          λ i p → pwEq p i
+        where
+        open IsAlgebraHom (snd f)
+        pwEq : (p : ⟨ ListPolyCommAlgebra ⟩) → fst f p ≡ fst inducedHom p
+        pwEq =
+          ElimProp R
+            (λ p → fst f p ≡ fst inducedHom p)
+            pres0
+            (λ r p IH →
+              fst f (r ∷ p)                    ≡[ i ]⟨ fst f ((sym (+IdR r) i) ∷ sym (Poly+Lid p) i) ⟩
+              fst f ([ r ] + (0r ∷ p))         ≡[ i ]⟨ fst f ([ useSolver r i ] + sym (X*Poly p) i) ⟩
+              fst f (r ⋆ 1a + X · p)           ≡⟨ pres+ (r ⋆ 1a) (X · p) ⟩
+              fst f (r ⋆ 1a) + fst f (X · p)   ≡[ i ]⟨ pres⋆ r 1a i + pres· X p i ⟩
+              r ⋆ fst f 1a + fst f X · fst f p ≡[ i ]⟨ r ⋆ pres1 i + fX≡x i · fst f p ⟩
+              r ⋆ 1a + x · fst f p             ≡[ i ]⟨ r ⋆ 1a + (x · IH i) ⟩
+              r ⋆ 1a + x · inducedMap p        ≡⟨⟩
+              inducedMap (r ∷ p) ∎)
+            (is-set _ _)
+          where
+            useSolver : (r : ⟨ R ⟩) → r ≡ (r · 1r) + 0r
+            useSolver = solve R

Cubical/Algebra/Polynomials/UnivariateList/Base.agda

@@ -1,7 +1,7 @@
 {-# OPTIONS --safe #-}
 module Cubical.Algebra.Polynomials.UnivariateList.Base where
 
-{-A
+{-
 Polynomials over commutative rings
 ==================================
 -}
@@ -62,18 +62,32 @@ module PolyMod (R' : CommRing ℓ) where
    f (x ∷ p) = cons* x p (f p)
    f (drop0 i) = drop0* i
 
-
   -- Given a proposition (as type) ϕ ranging over polynomials, we prove it by:
   -- ElimProp.f ϕ ⌜proof for base case []⌝ ⌜proof for induction case a ∷ p⌝
   --           ⌜proof that ϕ actually is a proposition over the domain of polynomials⌝
   module _ (B : Poly R' → Type ℓ')
-                  ([]* : B [])
-                  (cons* : (r : R) (p : Poly R') (b : B p) → B (r ∷ p))
-                  (BProp : {p : Poly R'} → isProp (B p)) where
+           ([]* : B [])
+           (cons* : (r : R) (p : Poly R') (b : B p) → B (r ∷ p))
+           (BProp : {p : Poly R'} → isProp (B p)) where
    ElimProp : (p : Poly R') → B p
    ElimProp = Elim.f B []* cons* (toPathP (BProp (transport (λ i → B (drop0 i)) (cons* 0r [] []*)) []*))
 
 
+  module _ (B         : Poly R' → Poly R' → Type ℓ')
+           ([][]*     : B [] [])
+           (cons[]*   : (r : R) (p : Poly R') (b : B p []) → B (r ∷ p) [])
+           ([]cons*   : (r : R) (p : Poly R') (b : B [] p) → B [] (r ∷ p))
+           (conscons* : (r s : R) (p q : Poly R') (b : B p q) → B (r ∷ p) (s ∷ q))
+           (BProp     : {p q : Poly R'} → isProp (B p q)) where
+
+    elimProp2 : (p q : Poly R') → B p q
+    elimProp2 =
+      ElimProp
+        (λ p → (q : Poly R') → B p q)
+        (ElimProp (B []) [][]* (λ r p b → []cons* r p b) BProp)
+        (λ r p b → ElimProp (λ q → B (r ∷ p) q) (cons[]* r p (b [])) (λ s q b' → conscons* r s p q (b q)) BProp)
+        (isPropΠ (λ _ → BProp))
+
   module Rec (B : Type ℓ')
              ([]* : B)
              (cons* : R → B → B)

Cubical/Algebra/Polynomials/UnivariateList/Properties.agda

@@ -228,6 +228,17 @@ module PolyModTheory (R' : CommRing ℓ) where
     (r PolyConst* [ s ]) Poly+ []                      ≡⟨ Poly+Rid _ ⟩
     [ r · s ] ∎
 
+  PolyConst*≡Poly* : (r : R) (x : Poly R') → r PolyConst* x ≡ [ r ] Poly* x
+  PolyConst*≡Poly* r =
+    ElimProp
+      (λ x → (r PolyConst* x) ≡ ([ r ] Poly* x))
+      (sym drop0)
+      (λ s x IH →
+         r PolyConst* (s ∷ x)                   ≡⟨⟩
+         (r PolyConst* (s ∷ x)) Poly+ []        ≡[ i ]⟨ (r PolyConst* (s ∷ x)) Poly+ (sym drop0 i) ⟩
+         (r PolyConst* (s ∷ x)) Poly+ (0r ∷ []) ≡⟨⟩
+         [ r ] Poly* (s ∷ x)    ∎)
+      (isSetPoly _ _)
 
   -- For any polynomial p we have: p Poly* [ 1r ] = p
   Poly*Lid : ∀ q → 1P Poly* q ≡ q
@@ -246,6 +257,29 @@ module PolyModTheory (R' : CommRing ℓ) where
                            r ∷ p ∎
 
 
+
+  X*Poly : (p : Poly R') → (0r ∷ 1r ∷ []) Poly* p ≡ 0r ∷ p
+  X*Poly =
+    ElimProp (λ p → (0r ∷ 1r ∷ []) Poly* p ≡ 0r ∷ p)
+             ((0r ∷ [ 1r ]) Poly* [] ≡⟨ (0PLeftAnnihilates (0r ∷ [ 1r ])) ⟩
+              []     ≡⟨ sym drop0 ⟩
+              [ 0r ] ∎)
+             (λ r p _ →
+                (0r ∷ [ 1r ]) Poly* (r ∷ p)                                  ≡⟨⟩
+                (0r PolyConst* (r ∷ p)) Poly+ (0r ∷ ([ 1r ] Poly* (r ∷ p)))  ≡⟨ step r p ⟩
+                [ 0r ] Poly+ (0r ∷ ([ 1r ] Poly* (r ∷ p)))                   ≡⟨ step2 r p ⟩
+                [] Poly+ (0r ∷ (r ∷ p))                                      ≡⟨⟩
+                0r ∷ r ∷ p ∎)
+             (isSetPoly _ _)
+
+             where
+               step : (r : _) → (p : _) → _ ≡ _
+               step r p i = (0rLeftAnnihilatesPoly (r ∷ p) i) Poly+ (0r ∷ ([ 1r ] Poly* (r ∷ p)))
+
+               step2 : (r : _) → (p : _) → _ ≡ _
+               step2 r p i = drop0 i Poly+ (0r ∷ Poly*Lid (r ∷ p) i)
+
+
   -- Distribution of indeterminate: (p + q)x = px + qx
   XLDistrPoly+ : ∀ p q → (0r ∷ (p Poly+ q)) ≡ ((0r ∷ p) Poly+ (0r ∷ q))
   XLDistrPoly+ =

Cubical/Algebra/Polynomials/UnivariateList/UniversalProperty.agda

@@ -0,0 +1,8 @@
+{-# OPTIONS --safe #-}
+module Cubical.Algebra.Polynomials.UnivariateList.UniversalProperty where
+
+{-
+  Export an CommAlgebra-Instance for the UnivariateList-Polynomials.
+  Also export the universal property with respect to not-necessarily commutative algebras.
+-}
+open import Cubical.Algebra.CommAlgebra.UnivariatePolyList public