Add Algebra.Action.* and friends

CHANGELOG.md

@@ -158,6 +158,31 @@ 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
+  ```
+
+* Basic definitions for left- and right- actions:
+  ```
+  Algebra.Action.Definitions
+  ```
+
+* Structures for left- and right- actions:
+  ```
+  Algebra.Action.Structures
+  ```
+
 * `Algebra.Module.Properties.{Bimodule|LeftModule|RightModule}`.
 
 * `Data.List.Base.{and|or|any|all}` have been lifted out into `Data.Bool.ListAction`.

src/Algebra/Action/Bundles.agda

@@ -0,0 +1,137 @@
+------------------------------------------------------------------------
+-- 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
+
+import Algebra.Action.Definitions as Definitions
+open import Algebra.Action.Structures using (IsLeftAction; IsRightAction)
+open import Algebra.Bundles using (Magma; Monoid)
+open import Level using (Level; _⊔_)
+open import Data.List.Base using ([]; _++_)
+import Data.List.Relation.Binary.Equality.Setoid as ≋
+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
+
+
+------------------------------------------------------------------------
+-- Definitions: indexed over an underlying SetoidAction
+
+module MagmaAction (M : Magma c ℓ) (A : Setoid a r) where
+
+  private
+
+    open module M = Magma M using (_∙_; setoid)
+    open module A = Setoid A using (_≈_)
+    open Definitions M._≈_ _≈_
+
+  record Left (leftAction : SetoidAction.Left setoid A) : Set (a ⊔ r ⊔ c ⊔ ℓ)
+    where
+
+    open SetoidAction.Left leftAction public
+
+    field
+      ∙-act  : IsActionˡ _▷_ _∙_
+
+  record Right (rightAction : SetoidAction.Right setoid A) : Set (a ⊔ r ⊔ c ⊔ ℓ)
+    where
+
+    open SetoidAction.Right rightAction public
+
+    field
+      ∙-act  : IsActionʳ _◁_ _∙_
+
+
+module MonoidAction (M : Monoid c ℓ) (A : Setoid a r) where
+
+  private
+
+    open module M = Monoid M using (ε; _∙_; setoid)
+    open module A = Setoid A using (_≈_)
+    open Definitions M._≈_ _≈_
+
+  record Left (leftAction : SetoidAction.Left setoid A) : Set (a ⊔ r ⊔ c ⊔ ℓ)
+    where
+
+    open SetoidAction.Left leftAction public
+
+    field
+      ∙-act  : IsActionˡ _▷_ _∙_
+      ε-act  : IsIdentityˡ _▷_ ε
+
+  record Right (rightAction : SetoidAction.Right setoid A) : Set (a ⊔ r ⊔ c ⊔ ℓ)
+    where
+
+    open SetoidAction.Right rightAction public
+
+    field
+      ∙-act  : IsActionʳ _◁_ _∙_
+      ε-act  : IsIdentityʳ _◁_ ε

src/Algebra/Action/Construct/FreeMonoid.agda

@@ -0,0 +1,70 @@
+------------------------------------------------------------------------
+-- 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 ℓ} (S : Setoid c ℓ) (A : 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 Data.List.Relation.Binary.Equality.Setoid.Properties S using (monoid)
+
+
+------------------------------------------------------------------------
+-- A Setoid action yields an iterated ListS action, which is
+-- the underlying SetoidAction of the FreeMonoid construction
+
+module SetoidActions where
+
+  open SetoidAction
+  open Monoid monoid 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
+
+
+------------------------------------------------------------------------
+-- Now: define the MonoidActions of the (Monoid based on) ListS on A
+
+module MonoidActions where
+
+  open MonoidAction monoid A
+
+  leftAction : (left : SetoidAction.Left S A) → Left (SetoidActions.leftAction left)
+  leftAction left = record
+    { ∙-act = ++-act
+    ; ε-act = []-act
+    }
+    where open SetoidAction.Left left
+
+  rightAction : (right : SetoidAction.Right S A) → Right (SetoidActions.rightAction right)
+  rightAction right = record
+    { ∙-act = ++-act
+    ; ε-act = []-act
+    }
+    where open SetoidAction.Right right
+

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/Definitions.agda

@@ -0,0 +1,51 @@
+------------------------------------------------------------------------
+-- 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; _Preserves₂_⟶_⟶_)
+
+module Algebra.Action.Definitions
+  {c a ℓ r} {M : Set c} {A : Set a} (_≈ᴹ_ : Rel M ℓ) (_≈_ : Rel A r)
+  where
+
+open import Algebra.Core using (Op₂)
+open import Function.Base using (id)
+open import Level using (Level; _⊔_)
+
+private
+  variable
+    x y : A
+    m n : M
+
+
+
+------------------------------------------------------------------------
+-- Basic definitions: fix notation
+
+Actˡ : Set (c ⊔ a)
+Actˡ = M → A → A
+
+Actʳ : Set (c ⊔ a)
+Actʳ = A → M → A
+
+Congruentˡ : Actˡ → Set (c ⊔ a ⊔ ℓ ⊔ r)
+Congruentˡ _▷_ = _▷_ Preserves₂ _≈ᴹ_ ⟶ _≈_ ⟶ _≈_
+
+Congruentʳ : Actʳ → Set (c ⊔ a ⊔ ℓ ⊔ r)
+Congruentʳ _◁_ = _◁_ Preserves₂ _≈_ ⟶ _≈ᴹ_ ⟶ _≈_
+
+IsActionˡ  : Actˡ → Op₂ M → Set (c ⊔ a ⊔ r)
+IsActionˡ _▷_ _∙_ = ∀ m n x → ((m ∙ n) ▷ x) ≈ (m ▷ (n ▷ x))
+
+IsIdentityˡ : Actˡ → M → Set (a ⊔ r)
+IsIdentityˡ _▷_ ε = ∀ x → (ε ▷ x) ≈ x
+
+IsActionʳ  : Actʳ → Op₂ M → Set (c ⊔ a ⊔ r)
+IsActionʳ _◁_ _∙_ = ∀ x m n → (x ◁ (m ∙ n)) ≈ ((x ◁ m) ◁ n)
+
+IsIdentityʳ : Actʳ → M → Set (a ⊔ r)
+IsIdentityʳ _◁_ ε = ∀ x → (x ◁ ε) ≈ x