Add initial commutative algebra

Cubical/Algebra/CommAlgebra/Base.agda

@@ -160,6 +160,52 @@ module _ {R : CommRing ℓ} where
   CommAlgebraHom : (M N : CommAlgebra R ℓ') → Type (ℓ-max ℓ ℓ')
   CommAlgebraHom M N = Σ[ f ∈ (⟨ M ⟩ → ⟨ N ⟩) ] IsCommAlgebraHom (M .snd) f (N .snd)
 
+  module _ {M N : CommAlgebra R ℓ'} where
+    open CommAlgebraStr {{...}}
+    open IsAlgebraHom
+    private
+      instance
+        _ = snd M
+        _ = snd N
+
+    makeCommAlgebraHom : (f : fst M → fst N)
+                           → (fPres1 : f 1a ≡ 1a)
+                           → (fPres+ : (x y : fst M) → f (x + y) ≡ f x + f y)
+                           → (fPres· : (x y : fst M) → f (x · y) ≡ f x · f y)
+                           → (fPres⋆ : (r : fst R) (x : fst M) → f (r ⋆ x) ≡ r ⋆ f x)
+                           → CommAlgebraHom M N
+    makeCommAlgebraHom f fPres1 fPres+ fPres· fPres⋆ = f , isHom
+      where fPres0 =
+                    f 0a                  ≡⟨ sym (+-rid _) ⟩
+                    f 0a + 0a             ≡⟨ cong (λ u → f 0a + u) (sym (+-rinv (f 0a))) ⟩
+                    f 0a + (f 0a - f 0a)  ≡⟨ +-assoc (f 0a) (f 0a) (- f 0a) ⟩
+                    (f 0a + f 0a) - f 0a  ≡⟨ cong (λ u → u - f 0a) (sym (fPres+ 0a 0a)) ⟩
+                    f (0a + 0a) - f 0a    ≡⟨ cong (λ u → f u - f 0a) (+-lid 0a) ⟩
+                    f 0a - f 0a           ≡⟨ +-rinv (f 0a) ⟩
+                    0a ∎
+
+            isHom : IsCommAlgebraHom (snd M) f (snd N)
+            pres0 isHom = fPres0
+            pres1 isHom = fPres1
+            pres+ isHom = fPres+
+            pres· isHom = fPres·
+            pres- isHom = (λ x →
+                               f (- x) ≡⟨ sym (+-rid _) ⟩
+                               (f (- x) + 0a) ≡⟨ cong (λ u → f (- x) + u) (sym (+-rinv (f x))) ⟩
+                               (f (- x) + (f x - f x)) ≡⟨ +-assoc _ _ _ ⟩
+                               ((f (- x) + f x) - f x) ≡⟨ cong (λ u → u - f x) (sym (fPres+ _ _)) ⟩
+                               (f ((- x) + x) - f x) ≡⟨ cong (λ u → f u - f x) (+-linv x) ⟩
+                               (f 0a - f x) ≡⟨ cong (λ u → u - f x) fPres0 ⟩
+                               (0a - f x) ≡⟨ +-lid _ ⟩ (- f x) ∎)
+            pres⋆ isHom = fPres⋆
+
+    isPropIsCommAlgebraHom : (f : fst M → fst N) → isProp (IsCommAlgebraHom (snd M) f (snd N))
+    isPropIsCommAlgebraHom f = isPropIsAlgebraHom
+                                 (CommRing→Ring R)
+                                 (snd (CommAlgebra→Algebra M))
+                                 f
+                                 (snd (CommAlgebra→Algebra N))
+
 isPropIsCommAlgebra : (R : CommRing ℓ) {A : Type ℓ'}
   (0a 1a : A)
   (_+_ _·_ : A → A → A)

Cubical/Algebra/CommAlgebra/Instances/Initial.agda

@@ -0,0 +1,80 @@
+{-# OPTIONS --safe #-}
+module Cubical.Algebra.CommAlgebra.Instances.Initial where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.HLevels
+open import Cubical.Foundations.Isomorphism
+
+open import Cubical.Data.Unit
+open import Cubical.Data.Sigma.Properties using (Σ≡Prop)
+
+open import Cubical.Algebra.CommRing
+open import Cubical.Algebra.Ring
+open import Cubical.Algebra.Algebra.Base using (IsAlgebraHom)
+open import Cubical.Algebra.CommAlgebra.Base
+
+private
+  variable
+    ℓ : Level
+
+module _ ((R , str) : CommRing ℓ) where
+
+  initialCAlg : CommAlgebra (R , str) ℓ
+  initialCAlg =
+    let open CommRingStr str
+    in  (R , commalgebrastr _ _ _ _ _ (λ r x → r · x)
+                    (makeIsCommAlgebra (isSetRing (CommRing→Ring (R , str)))
+                       +Assoc +Rid +Rinv +Comm
+                       ·Assoc ·Lid
+                       ·Ldist+ ·-comm
+                        (λ x y z → sym (·Assoc x y z)) ·Ldist+ ·Rdist+ ·Lid
+                         λ x y z → sym (·Assoc x y z)))
+
+
+  module _ (A : CommAlgebra (R , str) ℓ) where
+    open CommAlgebraStr ⦃... ⦄
+    private
+      instance
+        _ : CommAlgebraStr (R , str) (fst A)
+        _ = snd A
+        _ : CommAlgebraStr (R , str) R
+        _ = snd initialCAlg
+
+    _*_ : R → (fst A) → (fst A)
+    r * a = CommAlgebraStr._⋆_ (snd A) r a
+
+    initialMap : CommAlgebraHom initialCAlg A
+    initialMap =
+      makeCommAlgebraHom {M = initialCAlg} {N = A}
+        (λ r → r * 1a)
+        (⋆-lid _)
+        (λ x y → ⋆-ldist x y 1a)
+        (λ x y →  (x · y) * 1a ≡⟨ ⋆-assoc _ _ _ ⟩
+                           x * (y * 1a)                   ≡[ i ]⟨ x * (·Lid (y * 1a) (~ i)) ⟩
+                           x * (1a · (y * 1a))            ≡⟨ sym (⋆-lassoc _ _ _) ⟩
+                           (x * 1a) · (y * 1a) ∎)
+        (λ r x → (r · x) * 1a   ≡⟨ ⋆-assoc _ _ _ ⟩
+                         (r * (x * 1a)) ∎)
+
+    initialMapEq : (f : CommAlgebraHom initialCAlg A)
+                   → f ≡ initialMap
+    initialMapEq f =
+      let open IsAlgebraHom (snd f)
+      in Σ≡Prop
+           (isPropIsCommAlgebraHom {M = initialCAlg} {N = A})
+             λ i x →
+               ((fst f) x                              ≡⟨ cong (fst f) (sym (·Rid _)) ⟩
+               fst f (x · 1a)                          ≡⟨ pres⋆ x 1a ⟩
+               CommAlgebraStr._⋆_ (snd A) x (fst f 1a) ≡⟨ cong
+                                                           (λ u → (snd A CommAlgebraStr.⋆ x) u)
+                                                           pres1 ⟩
+               (CommAlgebraStr._⋆_ (snd A) x 1a) ∎) i
+
+    initialityIso : Iso (CommAlgebraHom initialCAlg A) (Unit* {ℓ = ℓ})
+    initialityIso = iso (λ _ → tt*)
+                        (λ _ → initialMap)
+                        (λ {tt*x → refl})
+                        λ f → sym (initialMapEq f)
+
+    initialityPath : CommAlgebraHom initialCAlg A ≡ Unit*
+    initialityPath = isoToPath initialityIso