lr-acts-0.0.1: Left and right actions, semidirect products and torsors
Copyright(c) Alice Rixte 2024
LicenseBSD 3
Maintaineralice.rixte@u-bordeaux.fr
Stabilityunstable
Portabilitynon-portable (GHC extensions)
Safe HaskellNone
LanguageHaskell2010

Data.Act.Cyclic

Description

Presentation

Cyclic actions

A cyclic action (see LActCyclic or RActCyclic) is an action such that every element of the actee set can be obtained by acting on some generator, which we call here the origin of the actee set.

For example, Sum Integer acts cyclically on Integer because for every n :: Integer, we have Sum n <>$ O == n. In this example, 0 is a generator of the action LAct Int (Sum Int) and in this library, we will call it lorigin.

This gives us a way to lift any actee element into an action element. In this library, we call that lifting lshift (resp. rshift). In the previous example we get lshift = Sum.

Actions generated by a subset of generators

In a more general setting, this library also provides LActGen and RActGen. In theory, they should be superclasses of LActCyclic and RActCyclic. In practice it is annoying to need Eq instances for defining lgenerators and rgenerators. Please open an issue if you actually need this.

Usage

>>> {-# LANGUAGE TypeApplications #-}
>>> import Data.Act.Cyclic
>>> import Data.Semigroup
>>> lorigin @(Sum Int) :: Int
0
>>> lshift (4 :: Int) :: Sum Int
Sum {getSum = 4}

Formal algebraic definitions

In algebraic terms, a subset u of the set x is a generating set of the action LAct x s if for every x :: x, there exists a pair (u,s) :: (u,s) such that s <>$ u = x. When the set u is finite, the action LAct x s is said to be finitely generated. When the set u is a singleton, the action is said to be cyclic.

When the previous decomposition is unique, the action is said to be free. If it is both free and cyclic, it is 1-free.

(See Monoids, Acts and Categories by Mati Kilp, Ulrich Knauer, Alexander V. Mikhalev, definition 1.5.1, p.63.)

Remark : Freeness could be represented with classes LActFree and LActOneFree that have no methods. Feel free to open an issue if you need them.

Synopsis

Cyclic actions

class LAct x s => LActCyclic x s where Source #

A left action generated by a single generator.

Instances must satisfy the following law :

In other words, lorigin is a generator of the action LAct x s.

Methods

lorigin' :: x Source #

The only generator of the action LAct x s.

>>> lorigin' @Int @(Sum Int)
0

To avoid having to use the redundant first type aplication, use lorigin.

lshift :: x -> s Source #

Instances

Instances details
Monoid s => LActCyclic s (ActSelf s) Source # 
Instance details

Defined in Data.Act.Cyclic

Methods

lorigin' :: s Source #

lshift :: s -> ActSelf s Source #

Default x => LActCyclic x (First x) Source # 
Instance details

Defined in Data.Act.Cyclic

Methods

lorigin' :: x Source #

lshift :: x -> First x Source #

Default x => LActCyclic x (First x) Source # 
Instance details

Defined in Data.Act.Cyclic

Methods

lorigin' :: x Source #

lshift :: x -> First x Source #

Num x => LActCyclic x (Product x) Source # 
Instance details

Defined in Data.Act.Cyclic

Methods

lorigin' :: x Source #

lshift :: x -> Product x Source #

Num x => LActCyclic x (Sum x) Source # 
Instance details

Defined in Data.Act.Cyclic

Methods

lorigin' :: x Source #

lshift :: x -> Sum x Source #

(Coercible x s, Monoid s) => LActCyclic x (ActSelf' s) Source # 
Instance details

Defined in Data.Act.Cyclic

Methods

lorigin' :: x Source #

lshift :: x -> ActSelf' s Source #

LActCyclic x s => LActCyclic (Identity x) (Identity s) Source # 
Instance details

Defined in Data.Act.Cyclic

Num x => LActCyclic (Sum x) (Product x) Source # 
Instance details

Defined in Data.Act.Cyclic

Methods

lorigin' :: Sum x Source #

lshift :: Sum x -> Product x Source #

lorigin :: forall s x. LActCyclic x s => x Source #

A version of lorigin' such that the first type application is s.

>>> lorigin @(Sum Int) :: Int
0

class RAct x s => RActCyclic x s where Source #

A right action generated by a single generator.

Instances must satisfy the following law :

In other words, rorigin is a generator of the action RAct x s.

Methods

rorigin' :: x Source #

The only generator of the action RAct x s.

>>> rorigin' @Int @(Sum Int) :: Int
0

To avoid having to use the redundant first type aplication, use rorigin.

rshift :: x -> s Source #

Shifts an element of x into an action rshift x such that rshift x $<> rorigin == x.

Instances

Instances details
Monoid s => RActCyclic s (ActSelf s) Source # 
Instance details

Defined in Data.Act.Cyclic

Methods

rorigin' :: s Source #

rshift :: s -> ActSelf s Source #

Default x => RActCyclic x (Last x) Source # 
Instance details

Defined in Data.Act.Cyclic

Methods

rorigin' :: x Source #

rshift :: x -> Last x Source #

Default x => RActCyclic x (Last x) Source # 
Instance details

Defined in Data.Act.Cyclic

Methods

rorigin' :: x Source #

rshift :: x -> Last x Source #

Num x => RActCyclic x (Product x) Source # 
Instance details

Defined in Data.Act.Cyclic

Methods

rorigin' :: x Source #

rshift :: x -> Product x Source #

Num x => RActCyclic x (Sum x) Source # 
Instance details

Defined in Data.Act.Cyclic

Methods

rorigin' :: x Source #

rshift :: x -> Sum x Source #

(Coercible x s, Monoid s) => RActCyclic x (ActSelf' s) Source # 
Instance details

Defined in Data.Act.Cyclic

Methods

rorigin' :: x Source #

rshift :: x -> ActSelf' s Source #

RActCyclic x s => RActCyclic (Identity x) (Identity s) Source # 
Instance details

Defined in Data.Act.Cyclic

Num x => RActCyclic (Sum x) (Product x) Source # 
Instance details

Defined in Data.Act.Cyclic

Methods

rorigin' :: Sum x Source #

rshift :: Sum x -> Product x Source #

rorigin :: forall s x. RActCyclic x s => x Source #

A version of rorigin' such that the first type application is s.

>>> rorigin @(Sum Int) :: Int
0

Action generated by a subset of generators

class LAct x s => LActGen x s where Source #

A left action generated by a subset of generators lgenerators.

Intuitively, by acting repeteadly on generators with actions of s, we can reach any element of x.

Since the generating subset of x maybe infinite, we give two alternative ways to define it : one using a characteristic function lgenerators and the other using a list lgeneratorsList.

All the above is summarized by the following law that all instances must satisfy :

  1. snd (lshiftFromGen x) <>$ fst (lshiftFromGen x) == x
  2. lgenerators (fst $ lshiftFromGen x) == True
  3. lgenerators x == x `elem' lgeneratorsList proxy

Minimal complete definition

Nothing

Methods

lgenerators' :: x -> Bool Source #

The set of origins of the action LAct x s.

This is a subset of x, represented as its characteristic function, meaning the function that returns True for all elements of x that are origins of the action and False otherwise.

To use lgenerators, you need TypeApplications:

>>> lgenerators' @Int @(Sum Int) 4
False
>>> lgenerators' @Int @(Sum Int) 0
True

To avoid having to use the redundant first type aplication, use lgenerators.

default lgenerators' :: Eq x => x -> Bool Source #

lgeneratorsList' :: [x] Source #

The set of origins of the action LAct x s seen as a list.

You can let this function undefined if the set of origins cannot be represented as a list.

>>> lgeneratorsList' @Int @(Sum Int)
[0]

To avoid having to use the redundant first type aplication, use lgeneratorsList.

default lgeneratorsList' :: LActCyclic x s => [x] Source #

lshiftFromGen :: x -> (x, s) Source #

Returns a point's associated genrator u along with an action s such that s <>$ u == x.

default lshiftFromGen :: LActCyclic x s => x -> (x, s) Source #

Instances

Instances details
(Eq s, Monoid s) => LActGen s (ActSelf s) Source # 
Instance details

Defined in Data.Act.Cyclic

(Eq x, Num x) => LActGen x (Product x) Source # 
Instance details

Defined in Data.Act.Cyclic

(Eq x, Num x) => LActGen x (Sum x) Source # 
Instance details

Defined in Data.Act.Cyclic

(Eq x, Coercible x s, Monoid s) => LActGen x (ActSelf' s) Source # 
Instance details

Defined in Data.Act.Cyclic

LActGen x s => LActGen (Identity x) (Identity s) Source # 
Instance details

Defined in Data.Act.Cyclic

(Eq x, Num x) => LActGen (Sum x) (Product x) Source # 
Instance details

Defined in Data.Act.Cyclic

lgenerators :: forall s x. LActGen x s => x -> Bool Source #

A version of lgenerators' such that the first type application is s.

>>> lgenerators @(Sum Int) (4 :: Int)
False
>>> lgenerators @(Sum Int) (0 :: Int)
True

lgeneratorsList :: forall s x. LActGen x s => [x] Source #

A version of lgeneratorsList' such that the first type application is s.

>>> lgeneratorsList @(Sum Int) :: [Int]
[0]

lorigins :: forall s x. LActGen x s => [x] Source #

An alias for lgeneratorsList.

class RAct x s => RActGen x s where Source #

A right action generated by a subset of generators lgenerators.

Intuitively, by acting repeteadly on generators with actions of s, we can reach any element of x.

Since the generating subset of x maybe infinite, we give two alternative ways to define it : one using a characteristic function rgenerators and the other using a list rgeneratorsList.

All the above is summarized by the following law that all instances must satisfy :

  1. rgenerators (fst $ rshiftFromGen x) == True
  2. fst (rshiftFromGen x) $<> snd (rshiftFromGen x) == x
  3. rgenerators x == x `elem' rgeneratorsList x

Minimal complete definition

Nothing

Methods

rgenerators' :: x -> Bool Source #

The set of origins of the action RAct x s.

This is a subset of x, represented as its characteristic function, meaning the function that returns True for all elements of x that are origins of the action and False otherwise.

To use rgenerators, you need TypeApplications:

>>> rgenerators' @(Sum Int) (4 :: Int)
False
>>> rgenerators' @(Sum Int) (0 :: Int)
True

To avoid having to use the redundant first type aplication, use rgenerators.

default rgenerators' :: Eq x => x -> Bool Source #

rgeneratorsList' :: [x] Source #

The set of origins of the action RAct x s seen as a list.

You can let this function undefined if the set of origins cannot be represented as a list.

>>> rgeneratorsList' @(Sum Int) :: [Int]
[0]

default rgeneratorsList' :: RActCyclic x s => [x] Source #

rshiftFromGen :: x -> (x, s) Source #

Returns a point's associated generator u along with an action s such that u $<> s == x.

default rshiftFromGen :: RActCyclic x s => x -> (x, s) Source #

Instances

Instances details
(Eq s, Monoid s) => RActGen s (ActSelf s) Source # 
Instance details

Defined in Data.Act.Cyclic

(Eq x, Num x) => RActGen x (Product x) Source # 
Instance details

Defined in Data.Act.Cyclic

(Eq x, Num x) => RActGen x (Sum x) Source # 
Instance details

Defined in Data.Act.Cyclic

(Eq x, Coercible x s, Monoid s) => RActGen x (ActSelf' s) Source # 
Instance details

Defined in Data.Act.Cyclic

RActGen x s => RActGen (Identity x) (Identity s) Source # 
Instance details

Defined in Data.Act.Cyclic

(Eq x, Num x) => RActGen (Sum x) (Product x) Source # 
Instance details

Defined in Data.Act.Cyclic

rgenerators :: forall s x. RActGen x s => x -> Bool Source #

A version of rgenerators' such that the first type application is s.

>>> rgenerators @(Sum Int) (4 :: Int)
False
>>> rgenerators @(Sum Int) (0 :: Int)
True

rgeneratorsList :: forall s x. RActGen x s => [x] Source #

A version of rgeneratorsList' such that the first type application is s.

>>> rgeneratorsList @(Sum Int) :: [Int]
[0]

rorigins :: forall s x. RActGen x s => [x] Source #

An alias for rgeneratorsList.