From 72226e5ec142a36cae49d74105891180b162765d Mon Sep 17 00:00:00 2001
From: Felix Cherubini <felix.cherubini@posteo.de>
Date: Wed, 7 Aug 2024 15:08:42 +0200
Subject: [PATCH] universal property of polynomials as rings

---
 .../Polynomials/Typevariate/OnCoproduct.agda  | 48 ++++++++++++++-----
 .../Polynomials/Typevariate/Properties.agda   |  8 +++-
 Cubical/Algebra/CommRing/Properties.agda      |  1 +
 3 files changed, 44 insertions(+), 13 deletions(-)

diff --git a/Cubical/Algebra/CommRing/Instances/Polynomials/Typevariate/OnCoproduct.agda b/Cubical/Algebra/CommRing/Instances/Polynomials/Typevariate/OnCoproduct.agda
index eea5dda7a..3290a2276 100644
--- a/Cubical/Algebra/CommRing/Instances/Polynomials/Typevariate/OnCoproduct.agda
+++ b/Cubical/Algebra/CommRing/Instances/Polynomials/Typevariate/OnCoproduct.agda
@@ -10,7 +10,7 @@
 module Cubical.Algebra.CommRing.Instances.Polynomials.Typevariate.OnCoproduct where
 
 open import Cubical.Foundations.Prelude
-open import Cubical.Foundations.Function using (_∘_)
+open import Cubical.Foundations.Function using (_∘_; _$_)
 open import Cubical.Foundations.Structure using (⟨_⟩)
 
 open import Cubical.Data.Sum as ⊎
@@ -45,10 +45,13 @@ module CalculatePolynomialsOnCoproduct (R : CommRing ℓ) (I J : Type ℓ) where
     mapVars (inr j) = var j
 
     to∘MapVars : to .fst ∘ mapVars ≡ var
-    to∘MapVars = funExt λ {(inl i) → to .fst (constPolynomial _ _ $cr var i)
-                                         ≡⟨ cong (λ z → z i) (evalInduce (R [ I ⊎ J ]) (constPolynomial R (I ⊎ J)) (var ∘ inl)) ⟩
-                                     var (inl i) ∎;
-                           (inr j) → (to .fst (var j) ≡⟨ cong (λ z → z j) evalVarTo ⟩ var (inr j) ∎)}
+    to∘MapVars =
+      funExt λ {(inl i) → to .fst (constPolynomial _ _ $cr var i)
+                              ≡⟨ cong (λ z → z i)
+                                      (evalInduce (R [ I ⊎ J ])
+                                                  (constPolynomial R (I ⊎ J)) (var ∘ inl)) ⟩
+                          var (inl i) ∎;
+                (inr j) → (to .fst (var j) ≡⟨ cong (λ z → z j) evalVarTo ⟩ var (inr j) ∎)}
 
     from : CommRingHom (R [ I ⊎ J ]) ((R [ I ]) [ J ])
     from = inducedHom
@@ -59,7 +62,7 @@ module CalculatePolynomialsOnCoproduct (R : CommRing ℓ) (I J : Type ℓ) where
     evalVarFrom : from .fst ∘ var ≡ mapVars
     evalVarFrom = evalInduce ((R [ I ]) [ J ]) (constPolynomial (R [ I ]) J ∘cr constPolynomial R I) mapVars
 
-    toFrom : to ∘cr from ≡ (idCommRingHom _)
+    toFrom : to ∘cr from ≡ (idCommRingHom (R [ I ⊎ J ]))
     toFrom =
       idByIdOnVars
         (to ∘cr from)
@@ -68,14 +71,35 @@ module CalculatePolynomialsOnCoproduct (R : CommRing ℓ) (I J : Type ℓ) where
         (to .fst ∘ from .fst ∘ var       ≡⟨ cong (to .fst ∘_) evalVarFrom ⟩
          to .fst ∘ mapVars               ≡⟨ to∘MapVars ⟩
          var ∎)
-{-
-    fromTo : from ∘cr to ≡ (idCommRingHom _)
+
+    {- from and to are R[I]-algebra homomorphisms:
+       this is true definitionally for to.
+    -}
+    fromAlgebraHom : from ∘cr I→I+J ≡ constPolynomial (R [ I ]) J
+    fromAlgebraHom =
+      hom≡ByValuesOnVars
+        ((R [ I ]) [ J ]) (constPolynomial (R [ I ]) J ∘cr constPolynomial R I)
+        (from ∘cr I→I+J) (constPolynomial (R [ I ]) J)
+        refl refl
+        (funExt
+        (λ i →  (from ∘cr I→I+J) .fst (var i)
+                  ≡⟨ cong (from .fst)
+                          (evalOnVars (R [ I ⊎ J ])
+                                      (constPolynomial R (I ⊎ J))
+                                      (var ∘ inl) i) ⟩
+                from .fst (var (inl i))
+                  ≡⟨ evalOnVars ((R [ I ]) [ J ])
+                     (constPolynomial (R [ I ]) J ∘cr constPolynomial R I)
+                     mapVars (inl i) ⟩
+                 constPolynomial (R [ I ]) J $cr var i ∎))
+
+    fromTo : from ∘cr to ≡ (idCommRingHom $ (R [ I ]) [ J ])
     fromTo =
       idByIdOnVars
         (from ∘cr to)
         (from .fst ∘ to .fst ∘ constPolynomial (R [ I ]) J .fst ≡⟨⟩
-         from .fst ∘ I→I+J .fst
-           ≡⟨ cong fst (hom≡ByValuesOnVars ((R [ I ]) [ J ]) {!from ∘cr I→I+J!} {!I→I+J!} {!!} {!!} {!!} {!!}) ⟩
+         from .fst ∘ I→I+J .fst ≡⟨ cong fst fromAlgebraHom ⟩
          constPolynomial (R [ I ]) J .fst ∎)
-        (from .fst ∘ to .fst ∘ var ≡⟨ {!!} ⟩ var ∎)
--}
+        (from .fst ∘ to .fst ∘ var ≡⟨ cong (from .fst ∘_) (funExt $ evalOnVars (R [ I ⊎ J ]) I→I+J (var ∘ inr) )  ⟩
+         from .fst ∘ var ∘ inr     ≡⟨ (funExt $ λ j → evalOnVars _ _ _ (inr j)) ⟩
+         var ∎)
diff --git a/Cubical/Algebra/CommRing/Instances/Polynomials/Typevariate/Properties.agda b/Cubical/Algebra/CommRing/Instances/Polynomials/Typevariate/Properties.agda
index 65675589b..0af77c592 100644
--- a/Cubical/Algebra/CommRing/Instances/Polynomials/Typevariate/Properties.agda
+++ b/Cubical/Algebra/CommRing/Instances/Polynomials/Typevariate/Properties.agda
@@ -223,9 +223,15 @@ module _  {R : CommRing ℓ} {I : Type ℓ'} (S : CommRing ℓ'') (f : CommRingH
   opaque
     unfolding var
     evalInduce : ∀ (φ : I → ⟨ S ⟩)
-                     → evalVar (inducedHom S f φ) ≡ φ
+                 → evalVar (inducedHom S f φ) ≡ φ
     evalInduce φ = refl
 
+  opaque
+    unfolding var
+    evalOnVars : ∀ (φ : I → ⟨ S ⟩)
+                 → (i : I) → inducedHom S f φ .fst (var i) ≡ φ i
+    evalOnVars φ i = refl
+
   opaque
     unfolding var
     induceEval : (g : CommRingHom (R [ I ]) S)
diff --git a/Cubical/Algebra/CommRing/Properties.agda b/Cubical/Algebra/CommRing/Properties.agda
index ea3424ab1..da9ac7a4d 100644
--- a/Cubical/Algebra/CommRing/Properties.agda
+++ b/Cubical/Algebra/CommRing/Properties.agda
@@ -162,6 +162,7 @@ module _ where
     RingHom→CommRingHom
       (compRingHom (CommRingHom→RingHom f) (CommRingHom→RingHom g))
 
+  infixr 9 _∘cr_ -- same as functions
   _∘cr_ : {R : CommRing ℓ} {S : CommRing ℓ'} {T : CommRing ℓ''}
         → CommRingHom S T → CommRingHom R S → CommRingHom R T
   g ∘cr f = compCommRingHom f g