{-# language CPP #-}
{-# language DerivingStrategies #-}
{-# language FlexibleInstances #-}
{-# language PackageImports #-}
{-# language PatternSynonyms #-}
{-# language Safe #-}
#if MIN_VERSION_base(4,12,0)
{-# language TypeOperators #-}
#endif
{-# language ViewPatterns #-}
-- |
-- Module       : Data.Group
-- Copyright    : (c) 2020-2021 Emily Pillmore
-- License      : BSD-style
--
-- Maintainer   : Emily Pillmore <emilypi@cohomolo.gy>,
--                Reed Mullanix <reedmullanix@gmail.com>
-- Stability    : stable
-- Portability  : non-portable
--
-- This module contains definitions for 'Group' and 'Abelian',
-- along with the relevant combinators.
--
module Data.Group
( -- * Groups
  -- $groups
  G.Group(..)
  -- * Group combinators
, minus
, gtimes
, (><)
  -- ** Conjugation
, conjugate
, unconjugate
, pattern Conjugate
  -- ** Elements
, pattern Inverse
, pattern IdentityElem
  -- ** Abelianization
, Abelianizer(..)
, abelianize
, commutate
, pattern Abelianized
, pattern Quotiented
  -- * Abelian groups
  -- $abelian
, G.Abelian
) where


import Data.Bool
import "groups" Data.Group as G
import Data.Monoid

import Prelude hiding (negate, exponent)

-- $setup
--
-- >>> :set -XPackageImports
-- >>> import qualified Prelude
-- >>> import "group-theory" Data.Group
-- >>> import Data.Monoid
-- >>> import Data.Semigroup
-- >>> import Data.Word
-- >>> :set -XTypeApplications
-- >>> :set -XFlexibleContexts

infixr 6 ><

-- -------------------------------------------------------------------- --
-- Group combinators

{- $groups

The typeclass of groups (types with an associative binary operation that
has an identity, and all inverses, i.e. a 'Monoid' with all inverses),
representing the structural symmetries of a mathematical object.

Instances should satisfy the following:

[Right identity] @ x '<>' 'mempty' = x@
[Left identity]  @'mempty' '<>' x = x@
[Associativity]  @ x '<>' (y '<>' z) = (x '<>' y) '<>' z@
[Concatenation]  @ 'mconcat' = 'foldr' ('<>') 'mempty'@
[Right inverses] @ x '<>' 'invert' x = 'mempty' @
[Left inverses]  @ 'invert' x '<>' x = 'mempty' @

Some types can be viewed as a group in more than one way,
e.g. both addition and multiplication on numbers.
In such cases we often define @newtype@s and make those instances
of 'Group', e.g. 'Data.Semigroup.Sum' and 'Data.Semigroup.Product'.
Often in practice such differences between addition and
multiplication-like operations matter (e.g. when defining rings), and
so, classes "additive" (the underlying operation is addition-like) and
"multiplicative" group classes are provided in vis 'Data.Group.Additive.AdditiveGroup' and
'Data.Group.Multiplicative.MultiplicativeGroup'.

Categorically, 'Group's may be viewed single-object groupoids.
-}

-- | An alias to 'pow'.
--
-- Similar to 'Data.Semigroup.stimes' from 'Data.Semigroup', but handles
-- negative powers by using 'invert' appropriately.
--
-- === __Examples:__
--
-- >>> gtimes 2 (Sum 3)
-- Sum {getSum = 6}
-- >>> gtimes (-3) (Sum 3)
-- Sum {getSum = -9}
--
gtimes :: (Group a, Integral n) => n -> a -> a
gtimes :: n -> a -> a
gtimes = (a -> n -> a) -> n -> a -> a
forall a b c. (a -> b -> c) -> b -> a -> c
flip a -> n -> a
forall m x. (Group m, Integral x) => m -> x -> m
pow
{-# inline gtimes #-}

-- | 'Group' subtraction.
--
-- This function denotes principled 'Group' subtraction, where
-- @a `minus` b@ translates into @a <> invert b@. This is because
-- subtraction as an operator is non-associative, but the operation
-- described in terms of addition and inversion is.
--
minus :: Group a => a -> a -> a
minus :: a -> a -> a
minus a
a a
b = a
a a -> a -> a
forall a. Semigroup a => a -> a -> a
<> a -> a
forall m. Group m => m -> m
invert a
b
{-# inline minus #-}

-- | Apply @('<>')@, commuting its arguments. When the group is abelian,
-- @a <> b@ is identically @b <> a@.
--
(><) :: Group a => a -> a -> a
a
a >< :: a -> a -> a
>< a
b = a
b a -> a -> a
forall a. Semigroup a => a -> a -> a
<> a
a
{-# inline (><) #-}

-- -------------------------------------------------------------------- --
-- Group conjugation

-- | Conjugate an element of a group by another element.
-- When the group is abelian, conjugation is the identity.
--
-- Symbolically, this is \( (g,a) \mapsto gag^{-1} \).
--
-- === __Examples__:
--
-- >>> let x = Sum (3 :: Int)
-- >>> conjugate x x
-- Sum {getSum = 3}
--
conjugate :: Group a => a -> a -> a
conjugate :: a -> a -> a
conjugate a
g a
a = (a
g a -> a -> a
forall a. Semigroup a => a -> a -> a
<> a
a) a -> a -> a
forall a. Group a => a -> a -> a
`minus` a
g
{-# inline conjugate #-}

-- | Apply an inverse conjugate to a conjugated element.
--
-- @
-- unconjugate . conjugate = id
-- conjugate . unconjugate = id
-- @
--
-- === __Examples__:
--
-- >>> let x = Sum (3 :: Int)
-- >>> unconjugate x (conjugate x x)
-- Sum {getSum = 3}
--
unconjugate :: Group a => a -> a -> a
unconjugate :: a -> a -> a
unconjugate a
g a
a = a -> a
forall m. Group m => m -> m
invert a
g a -> a -> a
forall a. Semigroup a => a -> a -> a
<> a
a a -> a -> a
forall a. Semigroup a => a -> a -> a
<> a
g

-- | Bidirectional pattern for conjugation by a group element
--
-- __Note:__ When the underlying 'Group' is abelian, this
-- pattern is the identity.
--
pattern Conjugate :: Group a => (a,a) -> (a,a)
pattern $bConjugate :: (a, a) -> (a, a)
$mConjugate :: forall r a. Group a => (a, a) -> ((a, a) -> r) -> (Void# -> r) -> r
Conjugate t <- (\(g,a) -> (g, conjugate g a) -> t) where
  Conjugate (a
g,a
a) = (a
g, a -> a -> a
forall a. Group a => a -> a -> a
unconjugate a
g a
a)
{-# complete Conjugate #-}

-- | Bidirectional pattern for inverse elements.
pattern Inverse :: (Group g) => g -> g
pattern $bInverse :: g -> g
$mInverse :: forall r g. Group g => g -> (g -> r) -> (Void# -> r) -> r
Inverse t <- (invert -> t) where
    Inverse g
g = g -> g
forall m. Group m => m -> m
invert g
g

-- | Bidirectional pattern for the identity element.
pattern IdentityElem :: (Eq m, Monoid m) => m
pattern $bIdentityElem :: m
$mIdentityElem :: forall r m.
(Eq m, Monoid m) =>
m -> (Void# -> r) -> (Void# -> r) -> r
IdentityElem <- ((== mempty) -> True) where
  IdentityElem = m
forall a. Monoid a => a
mempty

-- -------------------------------------------------------------------- --
-- Abelianization

-- | Quotient a pair of group elements by their commutator.
--
-- The of the quotient \( G / [G,G] \) forms an abelian group, and 'Abelianizer'
-- forms a functor from the category of groups to the category of Abelian groups.
-- This functor is left adjoint to the inclusion functor \( Ab \rightarrow Grp \),
-- forming a monad in \( Grp \).
--
data Abelianizer a = Quot | Commuted a
  deriving stock (Abelianizer a -> Abelianizer a -> Bool
(Abelianizer a -> Abelianizer a -> Bool)
-> (Abelianizer a -> Abelianizer a -> Bool) -> Eq (Abelianizer a)
forall a. Eq a => Abelianizer a -> Abelianizer a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Abelianizer a -> Abelianizer a -> Bool
$c/= :: forall a. Eq a => Abelianizer a -> Abelianizer a -> Bool
== :: Abelianizer a -> Abelianizer a -> Bool
$c== :: forall a. Eq a => Abelianizer a -> Abelianizer a -> Bool
Eq, Int -> Abelianizer a -> ShowS
[Abelianizer a] -> ShowS
Abelianizer a -> String
(Int -> Abelianizer a -> ShowS)
-> (Abelianizer a -> String)
-> ([Abelianizer a] -> ShowS)
-> Show (Abelianizer a)
forall a. Show a => Int -> Abelianizer a -> ShowS
forall a. Show a => [Abelianizer a] -> ShowS
forall a. Show a => Abelianizer a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Abelianizer a] -> ShowS
$cshowList :: forall a. Show a => [Abelianizer a] -> ShowS
show :: Abelianizer a -> String
$cshow :: forall a. Show a => Abelianizer a -> String
showsPrec :: Int -> Abelianizer a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> Abelianizer a -> ShowS
Show)

instance Functor Abelianizer where
  fmap :: (a -> b) -> Abelianizer a -> Abelianizer b
fmap a -> b
_ Abelianizer a
Quot = Abelianizer b
forall a. Abelianizer a
Quot
  fmap a -> b
f (Commuted a
a) = b -> Abelianizer b
forall a. a -> Abelianizer a
Commuted (a -> b
f a
a)

instance Applicative Abelianizer where
  pure :: a -> Abelianizer a
pure = a -> Abelianizer a
forall a. a -> Abelianizer a
Commuted

  Abelianizer (a -> b)
Quot <*> :: Abelianizer (a -> b) -> Abelianizer a -> Abelianizer b
<*> Abelianizer a
_ = Abelianizer b
forall a. Abelianizer a
Quot
  Abelianizer (a -> b)
_ <*> Abelianizer a
Quot = Abelianizer b
forall a. Abelianizer a
Quot
  Commuted a -> b
f <*> Commuted a
a = b -> Abelianizer b
forall a. a -> Abelianizer a
Commuted (a -> b
f a
a)

instance Monad Abelianizer where
  return :: a -> Abelianizer a
return = a -> Abelianizer a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
  >> :: Abelianizer a -> Abelianizer b -> Abelianizer b
(>>) = Abelianizer a -> Abelianizer b -> Abelianizer b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
(*>)

  Abelianizer a
Quot >>= :: Abelianizer a -> (a -> Abelianizer b) -> Abelianizer b
>>= a -> Abelianizer b
_ = Abelianizer b
forall a. Abelianizer a
Quot
  Commuted a
a >>= a -> Abelianizer b
f = a -> Abelianizer b
f a
a

instance Foldable Abelianizer where
  foldMap :: (a -> m) -> Abelianizer a -> m
foldMap a -> m
_ Abelianizer a
Quot = m
forall a. Monoid a => a
mempty
  foldMap a -> m
f (Commuted a
a) = a -> m
f a
a

instance Traversable Abelianizer where
  traverse :: (a -> f b) -> Abelianizer a -> f (Abelianizer b)
traverse a -> f b
_ Abelianizer a
Quot = Abelianizer b -> f (Abelianizer b)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Abelianizer b
forall a. Abelianizer a
Quot
  traverse a -> f b
f (Commuted a
a) = b -> Abelianizer b
forall a. a -> Abelianizer a
Commuted (b -> Abelianizer b) -> f b -> f (Abelianizer b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> f b
f a
a

instance Semigroup g => Semigroup (Abelianizer g) where
  Abelianizer g
Quot <> :: Abelianizer g -> Abelianizer g -> Abelianizer g
<> Abelianizer g
t = Abelianizer g
t
  Abelianizer g
t <> Abelianizer g
Quot = Abelianizer g
t
  Commuted g
a <> Commuted g
b = g -> Abelianizer g
forall a. a -> Abelianizer a
Commuted (g
a g -> g -> g
forall a. Semigroup a => a -> a -> a
<> g
b)

instance Monoid g => Monoid (Abelianizer g) where
  mempty :: Abelianizer g
mempty = Abelianizer g
forall a. Abelianizer a
Quot

instance (Eq g, Group g) => Group (Abelianizer g) where
  invert :: Abelianizer g -> Abelianizer g
invert Abelianizer g
Quot = Abelianizer g
forall a. Abelianizer a
Quot
  invert (Commuted g
IdentityElem) = Abelianizer g
forall a. Abelianizer a
Quot
  invert (Commuted g
a) = g -> Abelianizer g
forall a. a -> Abelianizer a
Commuted (g -> g
forall m. Group m => m -> m
invert g
a)

-- | Take the commutator of two elements of a group.
--
commutate :: Group g => g -> g -> g
commutate :: g -> g -> g
commutate g
g g
g' = g
g g -> g -> g
forall a. Semigroup a => a -> a -> a
<> g
g' g -> g -> g
forall a. Semigroup a => a -> a -> a
<> g -> g
forall m. Group m => m -> m
invert g
g g -> g -> g
forall a. Semigroup a => a -> a -> a
<> g -> g
forall m. Group m => m -> m
invert g
g'
{-# inline commutate #-}

-- | Quotient a pair of group elements by their commutator.
--
-- Ranging over the entire group, this operation constructs
-- the quotient of the group by its commutator sub-group
-- \( G / [G,G] \).
--
abelianize :: (Eq g, Group g) => g -> g -> Abelianizer g
abelianize :: g -> g -> Abelianizer g
abelianize g
g g
g'
  | g
x g -> g -> Bool
forall a. Eq a => a -> a -> Bool
== g
forall a. Monoid a => a
mempty = Abelianizer g
forall a. Abelianizer a
Quot
  | Bool
otherwise = g -> Abelianizer g
forall a. a -> Abelianizer a
Commuted g
x
  where
    x :: g
x = g -> g -> g
forall a. Group a => a -> a -> a
commutate g
g g
g'
{-# inline abelianize #-}

-- | A unidirectional pattern synonym for elements of a group
-- modulo commutators which are __not__ the identity.
--
pattern Abelianized :: (Eq g, Group g) => g -> (g,g)
pattern $mAbelianized :: forall r g.
(Eq g, Group g) =>
(g, g) -> (g -> r) -> (Void# -> r) -> r
Abelianized x <- (uncurry abelianize -> Commuted x)

-- | A unidirectional pattern synonym for elements of a group
-- modulo commutators which are the identity.
--
pattern Quotiented :: (Eq g, Group g) => (g,g)
pattern $mQuotiented :: forall r g.
(Eq g, Group g) =>
(g, g) -> (Void# -> r) -> (Void# -> r) -> r
Quotiented <- (uncurry abelianize -> Quot)

-- -------------------------------------------------------------------- --
-- Abelian (commutative) groups

{- $abelian
Commutative 'Group's.

Instances of 'Abelian' satisfy the following laws:

[Commutativity] @x <> y = y <> x@
-}