Pointwise ring and algebra structure

Cubical/Algebra/CommAlgebra/Instances/Pointwise.agda

@@ -0,0 +1,26 @@
+{-# OPTIONS --safe #-}
+module Cubical.Algebra.CommAlgebra.Instances.Pointwise where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.HLevels
+
+open import Cubical.Algebra.CommRing.Base
+open import Cubical.Algebra.CommRing.Instances.Pointwise
+open import Cubical.Algebra.CommAlgebra.Base
+
+private
+  variable
+    ℓ : Level
+
+pointwiseAlgebra :  {R : CommRing ℓ} (X : Type ℓ) (A : CommAlgebra R ℓ) → CommAlgebra R ℓ
+pointwiseAlgebra {R = R} X A =
+  let open CommAlgebraStr (snd A)
+      isSetX→A = isOfHLevelΠ 2 (λ (x : X) → isSetCommRing (CommAlgebra→CommRing A))
+  in commAlgebraFromCommRing
+       (pointwiseRing X (CommAlgebra→CommRing A))
+       (λ r f → (λ x → r ⋆ (f x)))
+       (λ r s f i x → ⋆-assoc r s (f x) i)
+       (λ r s f i x → ⋆-ldist r s (f x) i)
+       (λ r f g i x → ⋆-rdist r (f x) (g x) i)
+       (λ f i x → ⋆-lid (f x) i)
+       λ r f g i x → ⋆-lassoc r (f x) (g x) i

Cubical/Algebra/CommRing/Instances/Pointwise.agda

@@ -0,0 +1,32 @@
+{-# OPTIONS --safe #-}
+module Cubical.Algebra.CommRing.Instances.Pointwise where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.HLevels
+
+open import Cubical.Algebra.CommRing.Base
+
+private
+  variable
+    ℓ : Level
+
+pointwiseRing : (X : Type ℓ) (R : CommRing ℓ) → CommRing ℓ
+pointwiseRing X R =
+  let open CommRingStr (snd R)
+      isSetX→R = isOfHLevelΠ 2 (λ _ → isSetCommRing R)
+  in (X → fst R) ,
+     (commringstr
+       (λ _ → 0r) (λ _ → 1r)
+       (λ f g → (λ x → f x + g x))
+       (λ f g → (λ x → f x · g x))
+       (λ f → (λ x → - f x))
+       (makeIsCommRing
+         isSetX→R
+         (λ f g h i x → +Assoc (f x) (g x) (h x) i)
+         (λ f i x → +Rid (f x) i)
+         (λ f i x → +Rinv (f x) i)
+         (λ f g i x → +Comm (f x) (g x) i)
+         (λ f g h i x → ·Assoc (f x) (g x) (h x) i)
+         (λ f i x → ·Rid (f x) i)
+         (λ f g h i x → ·Rdist+ (f x) (g x) (h x) i)
+         λ f g i x → ·-comm (f x) (g x) i))