Add Algebra.Action.* and friends

CHANGELOG.md

@@ -57,6 +57,26 @@ Deprecated names
 New modules
 -----------
 
+* Bundles for left- and right- actions:
+  ```
+  Algebra.Action.Bundles
+  ```
+
+* The free `Monoid` actions over a `SetoidAction`:
+  ```
+  Algebra.Action.Construct.FreeMonoid
+  ```
+
+* The left- and right- regular actions (of a `Monoid`) over itself:
+  ```
+  Algebra.Action.Construct.Self
+  ```
+
+* Structures for left- and right- actions:
+  ```
+  Algebra.Action.Structures
+  ```
+
 * Raw bundles for module-like algebraic structures:
   ```
   Algebra.Module.Bundles.Raw

src/Algebra/Action/Bundles.agda

@@ -0,0 +1,140 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Setoid Actions and Monoid Actions
+------------------------------------------------------------------------
+
+------------------------------------------------------------------------
+-- Currently, this module (attempts to) systematically distinguish
+-- between left- and right- actions, but unfortunately, trying to avoid
+-- long names such as `Algebra.Action.Bundles.MonoidAction.LeftAction`
+-- leads to the possibly/probably suboptimal use of `Left` and `Right` as
+-- submodule names, when these are intended only to be used qualified by
+-- the type of Action to which they refer, eg. as MonoidAction.Left etc.
+------------------------------------------------------------------------
+
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Algebra.Action.Bundles where
+
+open import Algebra.Action.Structures using (IsLeftAction; IsRightAction)
+open import Algebra.Bundles using (Monoid)
+
+open import Data.List.Base using ([]; _++_)
+import Data.List.Relation.Binary.Equality.Setoid as ≋
+open import Level using (Level; _⊔_)
+
+open import Relation.Binary.Bundles using (Setoid)
+
+private
+  variable
+    a c r ℓ : Level
+
+
+------------------------------------------------------------------------
+-- Basic definition: a Setoid action yields underlying action structure
+
+module SetoidAction (S : Setoid c ℓ) (A : Setoid a r) where
+
+  private
+
+    module S = Setoid S
+    module A = Setoid A
+
+    open ≋ S using (≋-refl)
+
+  record Left : Set (a ⊔ r ⊔ c ⊔ ℓ) where
+
+    field
+      isLeftAction : IsLeftAction S._≈_ A._≈_
+
+    open IsLeftAction isLeftAction public
+
+    ▷-congˡ : ∀ {m x y} → x A.≈ y → m ▷ x A.≈ m ▷ y
+    ▷-congˡ x≈y = ▷-cong S.refl x≈y
+
+    ▷-congʳ : ∀ {m n x} → m S.≈ n → m ▷ x A.≈ n ▷ x
+    ▷-congʳ m≈n = ▷-cong m≈n A.refl
+
+    []-act : ∀ x → [] ▷⋆ x A.≈ x
+    []-act _ = []-act-cong A.refl
+
+    ++-act : ∀ ms ns x → (ms ++ ns) ▷⋆ x A.≈ ms ▷⋆ ns ▷⋆ x
+    ++-act ms ns x = ++-act-cong ms ≋-refl A.refl
+
+  record Right : Set (a ⊔ r ⊔ c ⊔ ℓ) where
+
+    field
+      isRightAction : IsRightAction S._≈_ A._≈_
+
+    open IsRightAction isRightAction public
+
+    ◁-congˡ : ∀ {x y m} → x A.≈ y → x ◁ m A.≈ y ◁ m
+    ◁-congˡ x≈y = ◁-cong x≈y S.refl
+
+    ◁-congʳ : ∀ {m n x} → m S.≈ n → x ◁ m A.≈ x ◁ n
+    ◁-congʳ m≈n = ◁-cong A.refl m≈n
+
+    ++-act : ∀ x ms ns → x ◁⋆ (ms ++ ns) A.≈ x ◁⋆ ms ◁⋆ ns
+    ++-act x ms ns = ++-act-cong A.refl ms ≋-refl
+
+    []-act : ∀ x → x ◁⋆ [] A.≈ x
+    []-act x = []-act-cong A.refl
+
+
+------------------------------------------------------------------------
+-- A Setoid action yields an iterated List action
+
+module ListAction {S : Setoid c ℓ} {A : Setoid a r} where
+
+  open SetoidAction
+
+  open ≋ S using (≋-setoid)
+
+  leftAction : (left : Left S A) → Left ≋-setoid A
+  leftAction left = record
+    { isLeftAction = record
+      { _▷_ = _▷⋆_
+      ; ▷-cong = ▷⋆-cong
+      }
+    }
+    where open Left left
+
+  rightAction : (right : Right S A) → Right ≋-setoid A
+  rightAction right = record
+    { isRightAction = record
+      { _◁_ = _◁⋆_
+      ; ◁-cong = ◁⋆-cong
+      }
+    }
+    where open Right right
+
+
+------------------------------------------------------------------------
+-- Definition: indexed over an underlying SetoidAction
+
+module MonoidAction (M : Monoid c ℓ) (A : Setoid a r) where
+
+  private
+
+    open module M = Monoid M using (ε; _∙_; setoid)
+    open module A = Setoid A using (_≈_)
+
+  record Left (leftAction : SetoidAction.Left setoid A) : Set (a ⊔ r ⊔ c ⊔ ℓ)
+    where
+
+    open SetoidAction.Left leftAction public
+
+    field
+      ∙-act  : ∀ m n x → m ∙ n ▷ x ≈ m ▷ n ▷ x
+      ε-act  : ∀ x → ε ▷ x ≈ x
+
+  record Right (rightAction : SetoidAction.Right setoid A) : Set (a ⊔ r ⊔ c ⊔ ℓ)
+    where
+
+    open SetoidAction.Right rightAction public
+
+    field
+      ∙-act  : ∀ x m n → x ◁ m ∙ n ≈ x ◁ m ◁ n
+      ε-act  : ∀ x → x ◁ ε ≈ x

src/Algebra/Action/Construct/FreeMonoid.agda

@@ -0,0 +1,78 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- The free MonoidAction on a SetoidAction, arising from ListAction
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+open import Relation.Binary.Bundles using (Setoid)
+
+module Algebra.Action.Construct.FreeMonoid
+  {a c r ℓ} (M : Setoid c ℓ) (S : Setoid a r)
+  where
+
+open import Algebra.Action.Bundles
+open import Algebra.Action.Structures using (IsLeftAction; IsRightAction)
+open import Algebra.Bundles using (Monoid)
+open import Algebra.Structures using (IsMonoid)
+
+open import Data.List.Base using (List; []; _++_)
+import Data.List.Properties as List
+import Data.List.Relation.Binary.Equality.Setoid as ≋
+open import Data.Product.Base using (_,_)
+
+open import Function.Base using (_∘_)
+
+open import Level using (Level; _⊔_)
+
+
+------------------------------------------------------------------------
+-- First: define the Monoid structure on List M.Carrier
+-- NB should be defined somewhere under `Data.List`!?
+
+private
+
+  open ≋ M using (_≋_; ≋-refl; ≋-reflexive; ≋-isEquivalence; ++⁺)
+
+  isMonoid : IsMonoid _≋_ _++_ []
+  isMonoid = record
+    { isSemigroup = record
+      { isMagma = record
+        { isEquivalence = ≋-isEquivalence
+        ; ∙-cong = ++⁺
+        }
+      ; assoc = λ xs ys zs → ≋-reflexive (List.++-assoc xs ys zs)
+      }
+    ; identity = (λ _ → ≋-refl) , ≋-reflexive ∘ List.++-identityʳ
+    }
+
+  monoid : Monoid c (c ⊔ ℓ)
+  monoid = record { isMonoid = isMonoid }
+
+
+------------------------------------------------------------------------
+-- Second: define the actions of that Monoid
+
+open MonoidAction monoid S
+
+module _ (left : SetoidAction.Left M S) where
+
+  open SetoidAction.Left left
+
+  leftAction : Left (ListAction.leftAction left)
+  leftAction = record
+    { ∙-act = ++-act
+    ; ε-act = []-act
+    }
+
+module _ (right : SetoidAction.Right M S) where
+
+  open SetoidAction.Right right
+
+  rightAction : Right (ListAction.rightAction right)
+  rightAction = record
+    { ∙-act = ++-act
+    ; ε-act = []-act
+    }
+

src/Algebra/Action/Construct/Self.agda

@@ -0,0 +1,40 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Left- and right- regular actions
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Algebra.Action.Construct.Self where
+
+open import Algebra.Action.Bundles
+open import Algebra.Action.Structures using (IsLeftAction; IsRightAction)
+open import Algebra.Bundles using (Monoid)
+
+------------------------------------------------------------------------
+-- Left- and Right- Actions of a Monoid over itself
+
+module Regular {c ℓ} (M : Monoid c ℓ) where
+
+  open Monoid M
+  open MonoidAction M setoid
+
+  isLeftAction : IsLeftAction _≈_ _≈_
+  isLeftAction = record { _▷_ = _∙_ ; ▷-cong = ∙-cong }
+
+  isRightAction : IsRightAction _≈_ _≈_
+  isRightAction = record { _◁_ = _∙_ ; ◁-cong = ∙-cong }
+
+  leftAction : Left record { isLeftAction = isLeftAction }
+  leftAction = record
+    { ∙-act = assoc
+    ; ε-act = identityˡ
+    }
+
+  rightAction : Right record { isRightAction = isRightAction }
+  rightAction = record
+    { ∙-act = λ x m n → sym (assoc x m n)
+    ; ε-act = identityʳ
+    }
+

src/Algebra/Action/Structures.agda

@@ -0,0 +1,92 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Structure of the Action of one (pre-)Setoid on another
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+open import Relation.Binary.Core using (Rel)
+
+module Algebra.Action.Structures
+  {c a ℓ r} {M : Set c} {A : Set a} (_≈ᴹ_ : Rel M ℓ) (_≈_ : Rel A r)
+  where
+
+open import Data.List.Base
+  using (List; []; _∷_; _++_; foldl; foldr)
+open import Data.List.NonEmpty.Base
+  using (List⁺; _∷_)
+open import Data.List.Relation.Binary.Pointwise as Pointwise
+  using (Pointwise; []; _∷_)
+open import Function.Base using (id)
+open import Level using (Level; _⊔_)
+
+private
+  variable
+    x y z : A
+    m n p : M
+    ms ns ps : List M
+
+
+------------------------------------------------------------------------
+-- Basic definitions: fix notation
+
+record IsLeftAction : Set (a ⊔ r ⊔ c ⊔ ℓ) where
+  infixr 5 _▷_ _▷⋆_ _▷⁺_
+
+  field
+    _▷_  : M → A → A
+    ▷-cong : m ≈ᴹ n → x ≈ y → (m ▷ x) ≈ (n ▷ y)
+
+-- derived form: iterated action, satisfying congruence
+
+  _▷⋆_ : List M → A → A
+  ms ▷⋆ a = foldr _▷_ a ms
+
+  _▷⁺_ : List⁺ M → A → A
+  (m ∷ ms) ▷⁺ a = m ▷ ms ▷⋆ a
+
+  ▷⋆-cong : Pointwise _≈ᴹ_ ms ns → x ≈ y → (ms ▷⋆ x) ≈ (ns ▷⋆ y)
+  ▷⋆-cong []            x≈y = x≈y
+  ▷⋆-cong (m≈n ∷ ms≋ns) x≈y = ▷-cong m≈n (▷⋆-cong ms≋ns x≈y)
+
+  ▷⁺-cong : m ≈ᴹ n → Pointwise _≈ᴹ_ ms ns → x ≈ y → ((m ∷ ms) ▷⁺ x) ≈ ((n ∷ ns) ▷⁺ y)
+  ▷⁺-cong m≈n ms≋ns x≈y = ▷-cong m≈n (▷⋆-cong ms≋ns x≈y)
+
+  ++-act-cong : ∀ ms → Pointwise _≈ᴹ_ ps (ms ++ ns) →
+                x ≈ y → (ps ▷⋆ x) ≈ (ms ▷⋆ ns ▷⋆ y)
+  ++-act-cong []       ps≋ns             x≈y = ▷⋆-cong ps≋ns x≈y
+  ++-act-cong (m ∷ ms) (p≈m ∷ ps≋ms++ns) x≈y = ▷-cong p≈m (++-act-cong ms ps≋ms++ns x≈y)
+
+  []-act-cong : x ≈ y → ([] ▷⋆ x) ≈ y
+  []-act-cong = id
+
+record IsRightAction : Set (a ⊔ r ⊔ c ⊔ ℓ) where
+  infixl 5 _◁_ _◁⋆_ _◁⁺_
+
+  field
+    _◁_  : A → M → A
+    ◁-cong : x ≈ y → m ≈ᴹ n → (x ◁ m) ≈ (y ◁ n)
+
+-- derived form: iterated action, satisfying congruence
+
+  _◁⋆_ : A → List M → A
+  a ◁⋆ ms = foldl _◁_ a ms
+
+  _◁⁺_ : A → List⁺ M → A
+  a ◁⁺ (m ∷ ms) = a ◁ m ◁⋆ ms
+
+  ◁⋆-cong : x ≈ y → Pointwise _≈ᴹ_ ms ns → (x ◁⋆ ms) ≈ (y ◁⋆ ns)
+  ◁⋆-cong x≈y []            = x≈y
+  ◁⋆-cong x≈y (m≈n ∷ ms≋ns) = ◁⋆-cong (◁-cong x≈y m≈n) ms≋ns
+
+  ◁⁺-cong : x ≈ y → m ≈ᴹ n → Pointwise _≈ᴹ_ ms ns → (x ◁⁺ (m ∷ ms)) ≈ (y ◁⁺ (n ∷ ns))
+  ◁⁺-cong x≈y m≈n ms≋ns = ◁⋆-cong (◁-cong x≈y m≈n) (ms≋ns)
+
+  ++-act-cong : x ≈ y → ∀ ms → Pointwise _≈ᴹ_ ps (ms ++ ns) →
+               (x ◁⋆ ps) ≈ (y ◁⋆ ms ◁⋆ ns)
+  ++-act-cong x≈y []       ps≋ns             = ◁⋆-cong x≈y ps≋ns
+  ++-act-cong x≈y (m ∷ ms) (p≈m ∷ ps≋ms++ns) = ++-act-cong (◁-cong x≈y p≈m) ms ps≋ms++ns
+
+  []-act-cong : x ≈ y → (x ◁⋆ []) ≈ y
+  []-act-cong = id