Pointwise Algebra (#2381)

* Pointwise `Algebra`

* temporary commit

* better `CHANGELOG` entry?

* begin removing redundant `module` implementation

* finish removing redundant `module` implementation

* make `liftRel` implicitly quantified

CHANGELOG.md

@@ -78,6 +78,12 @@ Deprecated names
 New modules
 -----------
 
+* Pointwise lifting of algebraic structures `IsX` and bundles `X` from
+  carrier set `C` to function space `A → C`:
+  ```
+  Algebra.Construct.Pointwise
+  ```
+
 * Raw bundles for module-like algebraic structures:
   ```
   Algebra.Module.Bundles.Raw

src/Algebra/Construct/Pointwise.agda

@@ -0,0 +1,184 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- For each `IsX` algebraic structure `S`, lift the structure to the
+-- 'pointwise' function space `A → S`: categorically, this is the
+-- *power* object in the relevant category of `X` objects and morphisms
+--
+-- NB the module is parametrised only wrt `A`
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Algebra.Construct.Pointwise {a} (A : Set a) where
+
+open import Algebra.Bundles
+open import Algebra.Core using (Op₁; Op₂)
+open import Algebra.Structures
+open import Data.Product.Base using (_,_)
+open import Function.Base using (id; _∘′_; const)
+open import Level
+open import Relation.Binary.Core using (Rel)
+open import Relation.Binary.Bundles using (Setoid)
+open import Relation.Binary.Structures using (IsEquivalence)
+
+
+private
+
+  variable
+    c ℓ : Level
+    C : Set c
+    _≈_ : Rel C ℓ
+    ε 0# 1# : C
+    _⁻¹ -_ : Op₁ C
+    _∙_ _+_ _*_ : Op₂ C
+
+  lift₀ : C → A → C
+  lift₀ = const
+
+  lift₁ : Op₁ C → Op₁ (A → C)
+  lift₁ = _∘′_
+
+  lift₂ : Op₂ C → Op₂ (A → C)
+  lift₂ _∙_ g h x = (g x) ∙ (h x)
+
+  liftRel : Rel C ℓ → Rel (A → C) (a ⊔ ℓ)
+  liftRel _≈_ g h = ∀ {x} → (g x) ≈ (h x)
+
+
+------------------------------------------------------------------------
+-- Setoid structure: here rather than elsewhere? (could be imported?)
+
+isEquivalence : IsEquivalence _≈_ → IsEquivalence (liftRel _≈_)
+isEquivalence isEquivalence = record
+  { refl = λ {f x} → refl {f x}
+  ; sym = λ f≈g → sym f≈g
+  ; trans = λ f≈g g≈h → trans f≈g g≈h
+  }
+  where open IsEquivalence isEquivalence
+
+------------------------------------------------------------------------
+-- Structures
+
+isMagma : IsMagma _≈_ _∙_ → IsMagma (liftRel _≈_) (lift₂ _∙_)
+isMagma isMagma = record
+  { isEquivalence = isEquivalence M.isEquivalence
+  ; ∙-cong = λ g h → M.∙-cong g h
+  }
+  where module M = IsMagma isMagma
+
+isSemigroup : IsSemigroup _≈_ _∙_ → IsSemigroup (liftRel _≈_) (lift₂ _∙_)
+isSemigroup isSemigroup = record
+  { isMagma = isMagma M.isMagma
+  ; assoc = λ f g h → M.assoc (f _) (g _) (h _)
+  }
+  where module M = IsSemigroup isSemigroup
+
+isBand : IsBand _≈_ _∙_ → IsBand (liftRel _≈_) (lift₂ _∙_)
+isBand isBand = record
+  { isSemigroup = isSemigroup M.isSemigroup
+  ; idem = λ f → M.idem (f _)
+  }
+  where module M = IsBand isBand
+
+isCommutativeSemigroup : IsCommutativeSemigroup _≈_ _∙_ →
+                         IsCommutativeSemigroup (liftRel _≈_) (lift₂ _∙_)
+isCommutativeSemigroup isCommutativeSemigroup = record
+  { isSemigroup = isSemigroup M.isSemigroup
+  ; comm = λ f g → M.comm (f _) (g _)
+  }
+  where module M = IsCommutativeSemigroup isCommutativeSemigroup
+
+isMonoid : IsMonoid _≈_ _∙_ ε → IsMonoid (liftRel _≈_) (lift₂ _∙_) (lift₀ ε)
+isMonoid isMonoid = record
+  { isSemigroup = isSemigroup M.isSemigroup
+  ; identity = (λ f → M.identityˡ (f _)) , λ f → M.identityʳ (f _)
+  }
+  where module M = IsMonoid isMonoid
+
+isCommutativeMonoid : IsCommutativeMonoid _≈_ _∙_ ε →
+                      IsCommutativeMonoid (liftRel _≈_) (lift₂ _∙_) (lift₀ ε)
+isCommutativeMonoid isCommutativeMonoid = record
+  { isMonoid = isMonoid M.isMonoid
+  ; comm = λ f g → M.comm (f _) (g _)
+  }
+  where module M = IsCommutativeMonoid isCommutativeMonoid
+
+isGroup : IsGroup _≈_ _∙_ ε _⁻¹ →
+          IsGroup (liftRel _≈_) (lift₂ _∙_) (lift₀ ε) (lift₁ _⁻¹)
+isGroup isGroup = record
+  { isMonoid = isMonoid M.isMonoid
+  ; inverse = (λ f → M.inverseˡ (f _)) , λ f → M.inverseʳ (f _)
+  ; ⁻¹-cong = λ f → M.⁻¹-cong f
+  }
+  where module M = IsGroup isGroup
+
+isAbelianGroup : IsAbelianGroup _≈_ _∙_ ε _⁻¹ →
+                 IsAbelianGroup (liftRel _≈_) (lift₂ _∙_) (lift₀ ε) (lift₁ _⁻¹)
+isAbelianGroup isAbelianGroup = record
+  { isGroup = isGroup M.isGroup
+  ; comm = λ f g → M.comm (f _) (g _)
+  }
+  where module M = IsAbelianGroup isAbelianGroup
+
+isSemiringWithoutAnnihilatingZero : IsSemiringWithoutAnnihilatingZero _≈_ _+_ _*_ 0# 1# →
+  IsSemiringWithoutAnnihilatingZero (liftRel _≈_) (lift₂ _+_) (lift₂ _*_) (lift₀ 0#) (lift₀ 1#)
+isSemiringWithoutAnnihilatingZero isSemiringWithoutAnnihilatingZero = record
+  { +-isCommutativeMonoid = isCommutativeMonoid M.+-isCommutativeMonoid
+  ; *-cong =  λ g h → M.*-cong g h
+  ; *-assoc =  λ f g h → M.*-assoc (f _) (g _) (h _)
+  ; *-identity = (λ f → M.*-identityˡ (f _)) , λ f → M.*-identityʳ (f _)
+  ; distrib = (λ f g h → M.distribˡ (f _) (g _) (h _)) , λ f g h → M.distribʳ (f _) (g _) (h _)
+  }
+  where module M = IsSemiringWithoutAnnihilatingZero isSemiringWithoutAnnihilatingZero
+
+isSemiring : IsSemiring _≈_ _+_ _*_ 0# 1# →
+             IsSemiring (liftRel _≈_) (lift₂ _+_) (lift₂ _*_) (lift₀ 0#) (lift₀ 1#)
+isSemiring isSemiring = record
+  { isSemiringWithoutAnnihilatingZero = isSemiringWithoutAnnihilatingZero M.isSemiringWithoutAnnihilatingZero
+  ; zero = (λ f → M.zeroˡ (f _)) , λ f → M.zeroʳ (f _)
+  }
+  where module M = IsSemiring isSemiring
+
+isRing : IsRing _≈_ _+_ _*_ -_ 0# 1# →
+         IsRing (liftRel _≈_) (lift₂ _+_) (lift₂ _*_) (lift₁ -_) (lift₀ 0#) (lift₀ 1#)
+isRing isRing = record
+  { +-isAbelianGroup = isAbelianGroup M.+-isAbelianGroup
+  ; *-cong = λ g h → M.*-cong g h
+  ; *-assoc = λ f g h → M.*-assoc (f _) (g _) (h _)
+  ; *-identity = (λ f → M.*-identityˡ (f _)) , λ f → M.*-identityʳ (f _)
+  ; distrib = (λ f g h → M.distribˡ (f _) (g _) (h _)) , λ f g h → M.distribʳ (f _) (g _) (h _)
+  }
+  where module M = IsRing isRing
+
+
+------------------------------------------------------------------------
+-- Bundles
+
+magma : Magma c ℓ → Magma (a ⊔ c) (a ⊔ ℓ)
+magma m = record { isMagma = isMagma (Magma.isMagma m) }
+
+semigroup : Semigroup c ℓ → Semigroup (a ⊔ c) (a ⊔ ℓ)
+semigroup m = record { isSemigroup = isSemigroup (Semigroup.isSemigroup m) }
+
+band : Band c ℓ → Band (a ⊔ c) (a ⊔ ℓ)
+band m = record { isBand = isBand (Band.isBand m) }
+
+commutativeSemigroup : CommutativeSemigroup c ℓ → CommutativeSemigroup (a ⊔ c) (a ⊔ ℓ)
+commutativeSemigroup m = record { isCommutativeSemigroup = isCommutativeSemigroup (CommutativeSemigroup.isCommutativeSemigroup m) }
+
+monoid : Monoid c ℓ → Monoid (a ⊔ c) (a ⊔ ℓ)
+monoid m = record { isMonoid = isMonoid (Monoid.isMonoid m) }
+
+group : Group c ℓ → Group (a ⊔ c) (a ⊔ ℓ)
+group m = record { isGroup = isGroup (Group.isGroup m) }
+
+abelianGroup : AbelianGroup c ℓ → AbelianGroup (a ⊔ c) (a ⊔ ℓ)
+abelianGroup m = record { isAbelianGroup = isAbelianGroup (AbelianGroup.isAbelianGroup m) }
+
+semiring : Semiring c ℓ → Semiring (a ⊔ c) (a ⊔ ℓ)
+semiring m = record { isSemiring = isSemiring (Semiring.isSemiring m) }
+
+ring : Ring c ℓ → Ring (a ⊔ c) (a ⊔ ℓ)
+ring m = record { isRing = isRing (Ring.isRing m) }
+