-- Copyright (c) 2008-2015, David Amos. All rights reserved.


module Math.Projects.ChevalleyGroup.Exceptional where

import Prelude hiding ( (*>) )

import Data.List as L

-- import Math.Algebra.Field.Base

-- import Math.Algebra.Field.Extension hiding ( (<+>), (<*>) )

import Math.Core.Field
import Math.Algebra.LinearAlgebra

import Math.Algebra.Group.PermutationGroup hiding (fromList)
-- import Math.Algebra.Group.SchreierSims as SS

import Math.Algebra.Group.RandomSchreierSims as RSS

import Math.Combinatorics.FiniteGeometry (ptsAG)


-- Follows Conway's notation


-- The octonion xinf + x0 i0 + x1 i1 + ... + x6 i6

-- is represented as O [(-1,xinf),(0,x0),(1,x1),...,(6,x6)]

-- where a list element may be omitted if the coefficient is zero



newtype Octonion k = O [(Int,k)] deriving (Octonion k -> Octonion k -> Bool
(Octonion k -> Octonion k -> Bool)
-> (Octonion k -> Octonion k -> Bool) -> Eq (Octonion k)
forall k. Eq k => Octonion k -> Octonion k -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Octonion k -> Octonion k -> Bool
$c/= :: forall k. Eq k => Octonion k -> Octonion k -> Bool
== :: Octonion k -> Octonion k -> Bool
$c== :: forall k. Eq k => Octonion k -> Octonion k -> Bool
Eq, Eq (Octonion k)
Eq (Octonion k) =>
(Octonion k -> Octonion k -> Ordering)
-> (Octonion k -> Octonion k -> Bool)
-> (Octonion k -> Octonion k -> Bool)
-> (Octonion k -> Octonion k -> Bool)
-> (Octonion k -> Octonion k -> Bool)
-> (Octonion k -> Octonion k -> Octonion k)
-> (Octonion k -> Octonion k -> Octonion k)
-> Ord (Octonion k)
Octonion k -> Octonion k -> Bool
Octonion k -> Octonion k -> Ordering
Octonion k -> Octonion k -> Octonion k
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall k. Ord k => Eq (Octonion k)
forall k. Ord k => Octonion k -> Octonion k -> Bool
forall k. Ord k => Octonion k -> Octonion k -> Ordering
forall k. Ord k => Octonion k -> Octonion k -> Octonion k
min :: Octonion k -> Octonion k -> Octonion k
$cmin :: forall k. Ord k => Octonion k -> Octonion k -> Octonion k
max :: Octonion k -> Octonion k -> Octonion k
$cmax :: forall k. Ord k => Octonion k -> Octonion k -> Octonion k
>= :: Octonion k -> Octonion k -> Bool
$c>= :: forall k. Ord k => Octonion k -> Octonion k -> Bool
> :: Octonion k -> Octonion k -> Bool
$c> :: forall k. Ord k => Octonion k -> Octonion k -> Bool
<= :: Octonion k -> Octonion k -> Bool
$c<= :: forall k. Ord k => Octonion k -> Octonion k -> Bool
< :: Octonion k -> Octonion k -> Bool
$c< :: forall k. Ord k => Octonion k -> Octonion k -> Bool
compare :: Octonion k -> Octonion k -> Ordering
$ccompare :: forall k. Ord k => Octonion k -> Octonion k -> Ordering
$cp1Ord :: forall k. Ord k => Eq (Octonion k)
Ord)

i0, i1, i2, i3, i4, i5, i6 :: Octonion Q
i0 :: Octonion Q
i0 = [(Int, Q)] -> Octonion Q
forall k. [(Int, k)] -> Octonion k
O [(0,1)]
i1 :: Octonion Q
i1 = [(Int, Q)] -> Octonion Q
forall k. [(Int, k)] -> Octonion k
O [(1,1)]
i2 :: Octonion Q
i2 = [(Int, Q)] -> Octonion Q
forall k. [(Int, k)] -> Octonion k
O [(2,1)]
i3 :: Octonion Q
i3 = [(Int, Q)] -> Octonion Q
forall k. [(Int, k)] -> Octonion k
O [(3,1)]
i4 :: Octonion Q
i4 = [(Int, Q)] -> Octonion Q
forall k. [(Int, k)] -> Octonion k
O [(4,1)]
i5 :: Octonion Q
i5 = [(Int, Q)] -> Octonion Q
forall k. [(Int, k)] -> Octonion k
O [(5,1)]
i6 :: Octonion Q
i6 = [(Int, Q)] -> Octonion Q
forall k. [(Int, k)] -> Octonion k
O [(6,1)]

fromList :: [k] -> Octonion k
fromList as :: [k]
as = [(Int, k)] -> Octonion k
forall k. [(Int, k)] -> Octonion k
O ([(Int, k)] -> Octonion k) -> [(Int, k)] -> Octonion k
forall a b. (a -> b) -> a -> b
$ ((Int, k) -> Bool) -> [(Int, k)] -> [(Int, k)]
forall a. (a -> Bool) -> [a] -> [a]
filter ((k -> k -> Bool
forall a. Eq a => a -> a -> Bool
/=0) (k -> Bool) -> ((Int, k) -> k) -> (Int, k) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int, k) -> k
forall a b. (a, b) -> b
snd) ([(Int, k)] -> [(Int, k)]) -> [(Int, k)] -> [(Int, k)]
forall a b. (a -> b) -> a -> b
$ [Int] -> [k] -> [(Int, k)]
forall a b. [a] -> [b] -> [(a, b)]
zip [-1..6] [k]
as

toList :: Octonion a -> [a]
toList (O xs :: [(Int, a)]
xs) = [(Int, a)] -> [Int] -> [a]
forall a a. (Eq a, Num a) => [(a, a)] -> [a] -> [a]
toList' [(Int, a)]
xs [-1..6] where
    toList' :: [(a, a)] -> [a] -> [a]
toList' ((i :: a
i,a :: a
a):xs :: [(a, a)]
xs) (j :: a
j:js :: [a]
js) =
        if a
i a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
j then a
a a -> [a] -> [a]
forall a. a -> [a] -> [a]
: [(a, a)] -> [a] -> [a]
toList' [(a, a)]
xs [a]
js else 0 a -> [a] -> [a]
forall a. a -> [a] -> [a]
: [(a, a)] -> [a] -> [a]
toList' ((a
i,a
a)(a, a) -> [(a, a)] -> [(a, a)]
forall a. a -> [a] -> [a]
:[(a, a)]
xs) [a]
js
    toList' [] (j :: a
j:js :: [a]
js) = 0 a -> [a] -> [a]
forall a. a -> [a] -> [a]
: [(a, a)] -> [a] -> [a]
toList' [] [a]
js
    toList' _ [] = []

expose :: Octonion k -> [(Int, k)]
expose (O ts :: [(Int, k)]
ts) = [(Int, k)]
ts

instance Show k => Show (Octonion k) where
    show :: Octonion k -> String
show (O []) = "0"
    show (O ts :: [(Int, k)]
ts) = let c :: Char
c:cs :: String
cs = ((Int, k) -> String) -> [(Int, k)] -> String
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Int, k) -> String
forall a a. (Eq a, Num a, Show a, Show a) => (a, a) -> String
showTerm [(Int, k)]
ts
                  in if Char
c Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== '+' then String
cs else Char
cChar -> ShowS
forall a. a -> [a] -> [a]
:String
cs
        where showTerm :: (a, a) -> String
showTerm (i :: a
i,a :: a
a) = a -> String
forall a. Show a => a -> String
showCoeff a
a String -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> a -> String
forall a a. (Eq a, Num a, Show a, Show a) => a -> a -> String
showImag a
a a
i
              showCoeff :: a -> String
showCoeff a :: a
a = case a -> String
forall a. Show a => a -> String
show a
a of
                            "1" -> "+"
                            "-1" -> "-"
                            '-':cs :: String
cs -> '-'Char -> ShowS
forall a. a -> [a] -> [a]
:String
cs
                            cs :: String
cs -> '+'Char -> ShowS
forall a. a -> [a] -> [a]
:String
cs
              showImag :: a -> a -> String
showImag a :: a
a i :: a
i | a
i a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== -1 = case a -> String
forall a. Show a => a -> String
show a
a of
                                       "1" -> "1"
                                       "-1" -> "1"
                                       otherwise :: String
otherwise -> ""
                           | Bool
otherwise = "i" String -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
i

instance (Ord k, Num k) => Num (Octonion k) where -- Ord k not strictly required, but keeps nf simpler

    O ts :: [(Int, k)]
ts + :: Octonion k -> Octonion k -> Octonion k
+ O us :: [(Int, k)]
us = [(Int, k)] -> Octonion k
forall k. [(Int, k)] -> Octonion k
O ([(Int, k)] -> Octonion k) -> [(Int, k)] -> Octonion k
forall a b. (a -> b) -> a -> b
$ [(Int, k)] -> [(Int, k)]
forall a b. (Num b, Ord a, Ord b) => [(a, b)] -> [(a, b)]
nf ([(Int, k)] -> [(Int, k)]) -> [(Int, k)] -> [(Int, k)]
forall a b. (a -> b) -> a -> b
$ [(Int, k)]
ts [(Int, k)] -> [(Int, k)] -> [(Int, k)]
forall a. [a] -> [a] -> [a]
++ [(Int, k)]
us
    negate :: Octonion k -> Octonion k
negate (O ts :: [(Int, k)]
ts) = [(Int, k)] -> Octonion k
forall k. [(Int, k)] -> Octonion k
O ([(Int, k)] -> Octonion k) -> [(Int, k)] -> Octonion k
forall a b. (a -> b) -> a -> b
$ ((Int, k) -> (Int, k)) -> [(Int, k)] -> [(Int, k)]
forall a b. (a -> b) -> [a] -> [b]
map (\(i :: Int
i,a :: k
a) -> (Int
i,-k
a)) [(Int, k)]
ts
    O ts :: [(Int, k)]
ts * :: Octonion k -> Octonion k -> Octonion k
* O us :: [(Int, k)]
us = [(Int, k)] -> Octonion k
forall k. [(Int, k)] -> Octonion k
O ([(Int, k)] -> Octonion k) -> [(Int, k)] -> Octonion k
forall a b. (a -> b) -> a -> b
$ [(Int, k)] -> [(Int, k)]
forall a b. (Num b, Ord a, Ord b) => [(a, b)] -> [(a, b)]
nf [(Int, k) -> (Int, k) -> (Int, k)
forall a a. (Num a, Integral a) => (a, a) -> (a, a) -> (a, a)
m (Int, k)
t (Int, k)
u | (Int, k)
t <- [(Int, k)]
ts, (Int, k)
u <- [(Int, k)]
us]
    fromInteger :: Integer -> Octonion k
fromInteger 0 = [(Int, k)] -> Octonion k
forall k. [(Int, k)] -> Octonion k
O []
    fromInteger n :: Integer
n = [(Int, k)] -> Octonion k
forall k. [(Int, k)] -> Octonion k
O [(-1, Integer -> k
forall a. Num a => Integer -> a
fromInteger Integer
n)]

nf :: [(a, b)] -> [(a, b)]
nf ts :: [(a, b)]
ts = [(a, b)] -> [(a, b)]
forall a b. (Eq a, Eq b, Num b) => [(a, b)] -> [(a, b)]
nf' ([(a, b)] -> [(a, b)]) -> [(a, b)] -> [(a, b)]
forall a b. (a -> b) -> a -> b
$ [(a, b)] -> [(a, b)]
forall a. Ord a => [a] -> [a]
L.sort [(a, b)]
ts where
    nf' :: [(a, b)] -> [(a, b)]
nf' ((i1 :: a
i1,a1 :: b
a1):(i2 :: a
i2,a2 :: b
a2):ts :: [(a, b)]
ts) =
        if a
i1 a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
i2
        then if b
a1b -> b -> b
forall a. Num a => a -> a -> a
+b
a2 b -> b -> Bool
forall a. Eq a => a -> a -> Bool
== 0 then [(a, b)] -> [(a, b)]
nf' [(a, b)]
ts else [(a, b)] -> [(a, b)]
nf' ((a
i1,b
a1b -> b -> b
forall a. Num a => a -> a -> a
+b
a2)(a, b) -> [(a, b)] -> [(a, b)]
forall a. a -> [a] -> [a]
:[(a, b)]
ts)
        else (a
i1,b
a1) (a, b) -> [(a, b)] -> [(a, b)]
forall a. a -> [a] -> [a]
: [(a, b)] -> [(a, b)]
nf' ((a
i2,b
a2)(a, b) -> [(a, b)] -> [(a, b)]
forall a. a -> [a] -> [a]
:[(a, b)]
ts)
    nf' ts :: [(a, b)]
ts = [(a, b)]
ts

m :: (a, a) -> (a, a) -> (a, a)
m (-1,a :: a
a) (i :: a
i,b :: a
b) = (a
i,a
aa -> a -> a
forall a. Num a => a -> a -> a
*a
b)
m (i :: a
i,a :: a
a) (-1,b :: a
b) = (a
i,a
aa -> a -> a
forall a. Num a => a -> a -> a
*a
b)
m (i :: a
i,a :: a
a) (j :: a
j,b :: a
b) =
    case (a
ja -> a -> a
forall a. Num a => a -> a -> a
-a
i) a -> a -> a
forall a. Integral a => a -> a -> a
`mod` 7 of
    0 -> (-1,-a
aa -> a -> a
forall a. Num a => a -> a -> a
*a
b)
    1 -> ( (a
ia -> a -> a
forall a. Num a => a -> a -> a
+3) a -> a -> a
forall a. Integral a => a -> a -> a
`mod` 7, a
aa -> a -> a
forall a. Num a => a -> a -> a
*a
b)	-- i_n+1 * i_n+2 == i_n+4

    2 -> ( (a
ia -> a -> a
forall a. Num a => a -> a -> a
+6) a -> a -> a
forall a. Integral a => a -> a -> a
`mod` 7, a
aa -> a -> a
forall a. Num a => a -> a -> a
*a
b)	-- i_n+2 * i_n+4 == i_n+1

    3 -> ( (a
ia -> a -> a
forall a. Num a => a -> a -> a
+1) a -> a -> a
forall a. Integral a => a -> a -> a
`mod` 7, -a
aa -> a -> a
forall a. Num a => a -> a -> a
*a
b)	-- i_n+1 * i_n+4 == -i_n+2

    4 -> ( (a
ia -> a -> a
forall a. Num a => a -> a -> a
+5) a -> a -> a
forall a. Integral a => a -> a -> a
`mod` 7, a
aa -> a -> a
forall a. Num a => a -> a -> a
*a
b)	-- i_n+4 * i_n+1 == i_n+2

    5 -> ( (a
ia -> a -> a
forall a. Num a => a -> a -> a
+4) a -> a -> a
forall a. Integral a => a -> a -> a
`mod` 7, -a
aa -> a -> a
forall a. Num a => a -> a -> a
*a
b)	-- i_n+4 * i_n+2 == -i_n+1

    6 -> ( (a
ia -> a -> a
forall a. Num a => a -> a -> a
+2) a -> a -> a
forall a. Integral a => a -> a -> a
`mod` 7, -a
aa -> a -> a
forall a. Num a => a -> a -> a
*a
b)	-- i_n+2 * i_n+1 == -i_n+4



conj :: Octonion k -> Octonion k
conj (O ts :: [(Int, k)]
ts) = [(Int, k)] -> Octonion k
forall k. [(Int, k)] -> Octonion k
O ([(Int, k)] -> Octonion k) -> [(Int, k)] -> Octonion k
forall a b. (a -> b) -> a -> b
$ ((Int, k) -> (Int, k)) -> [(Int, k)] -> [(Int, k)]
forall a b. (a -> b) -> [a] -> [b]
map (\(i :: Int
i,a :: k
a) -> if Int
i Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== -1 then (Int
i,k
a) else (Int
i,-k
a)) [(Int, k)]
ts

sqnorm :: Octonion a -> a
sqnorm (O ts :: [(Int, a)]
ts) = [a] -> a
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum [a
aa -> Integer -> a
forall a b. (Num a, Integral b) => a -> b -> a
^2 | (i :: Int
i,a :: a
a) <- [(Int, a)]
ts]

instance (Ord k, Num k, Fractional k) => Fractional (Octonion k) where
    recip :: Octonion k -> Octonion k
recip x :: Octonion k
x = let O x' :: [(Int, k)]
x' = Octonion k -> Octonion k
forall k. Num k => Octonion k -> Octonion k
conj Octonion k
x
                  xx' :: k
xx' = Octonion k -> k
forall a. Num a => Octonion a -> a
sqnorm Octonion k
x
              in [(Int, k)] -> Octonion k
forall k. [(Int, k)] -> Octonion k
O ([(Int, k)] -> Octonion k) -> [(Int, k)] -> Octonion k
forall a b. (a -> b) -> a -> b
$ ((Int, k) -> (Int, k)) -> [(Int, k)] -> [(Int, k)]
forall a b. (a -> b) -> [a] -> [b]
map (\(i :: Int
i,a :: k
a) -> (Int
i,k
ak -> k -> k
forall a. Fractional a => a -> a -> a
/k
xx')) [(Int, k)]
x'


isOrthogonal :: Octonion a -> Octonion a -> Bool
isOrthogonal (O ts :: [(Int, a)]
ts) (O us :: [(Int, a)]
us) = [(Int, a)] -> [(Int, a)] -> a
forall a b. (Ord a, Num b) => [(a, b)] -> [(a, b)] -> b
dot [(Int, a)]
ts [(Int, a)]
us a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== 0 where
    dot :: [(a, b)] -> [(a, b)] -> b
dot ((i :: a
i,a :: b
a):ts :: [(a, b)]
ts) ((j :: a
j,b :: b
b):us :: [(a, b)]
us) =
        case a -> a -> Ordering
forall a. Ord a => a -> a -> Ordering
compare a
i a
j of
        EQ -> b
ab -> b -> b
forall a. Num a => a -> a -> a
*b
b b -> b -> b
forall a. Num a => a -> a -> a
+ [(a, b)] -> [(a, b)] -> b
dot [(a, b)]
ts [(a, b)]
us
        LT -> [(a, b)] -> [(a, b)] -> b
dot [(a, b)]
ts ((a
j,b
b)(a, b) -> [(a, b)] -> [(a, b)]
forall a. a -> [a] -> [a]
:[(a, b)]
us)
        GT -> [(a, b)] -> [(a, b)] -> b
dot ((a
i,b
a)(a, b) -> [(a, b)] -> [(a, b)]
forall a. a -> [a] -> [a]
:[(a, b)]
ts) [(a, b)]
us
    dot _ _ = 0

antiCommutes :: a -> a -> Bool
antiCommutes x :: a
x y :: a
y = a
xa -> a -> a
forall a. Num a => a -> a -> a
*a
y a -> a -> a
forall a. Num a => a -> a -> a
+ a
ya -> a -> a
forall a. Num a => a -> a -> a
*a
x a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== 0

-- anti-commuting and being orthogonal appear to be equivalent for unit imaginary octonions,

-- provided we're not in characteristic 2



-- OCTONIONS OVER FINITE FIELDS


{-
octonions fq = map O $ octonions' [-1..6] where
    octonions' (i:is) = [if a == 0 then ts else (i,a):ts | a <- fq, ts <- octonions' is]
    octonions' [] = [[]]
-}
octonions :: [k] -> [Octonion k]
octonions fq :: [k]
fq = ([k] -> Octonion k) -> [[k]] -> [Octonion k]
forall a b. (a -> b) -> [a] -> [b]
map [k] -> Octonion k
forall k. (Eq k, Num k) => [k] -> Octonion k
fromList ([[k]] -> [Octonion k]) -> [[k]] -> [Octonion k]
forall a b. (a -> b) -> a -> b
$ Int -> [k] -> [[k]]
forall a. Int -> [a] -> [[a]]
ptsAG 8 [k]
fq

isUnit :: Octonion a -> Bool
isUnit x :: Octonion a
x = Octonion a -> a
forall a. Num a => Octonion a -> a
sqnorm Octonion a
x a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== 1

unitImagOctonions :: [a] -> [Octonion a]
unitImagOctonions fq :: [a]
fq = (Octonion a -> Bool) -> [Octonion a] -> [Octonion a]
forall a. (a -> Bool) -> [a] -> [a]
filter Octonion a -> Bool
forall a. (Eq a, Num a) => Octonion a -> Bool
isUnit ([Octonion a] -> [Octonion a]) -> [Octonion a] -> [Octonion a]
forall a b. (a -> b) -> a -> b
$ ([a] -> Octonion a) -> [[a]] -> [Octonion a]
forall a b. (a -> b) -> [a] -> [b]
map ([a] -> Octonion a
forall k. (Eq k, Num k) => [k] -> Octonion k
fromList ([a] -> Octonion a) -> ([a] -> [a]) -> [a] -> Octonion a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (0a -> [a] -> [a]
forall a. a -> [a] -> [a]
:)) ([[a]] -> [Octonion a]) -> [[a]] -> [Octonion a]
forall a b. (a -> b) -> a -> b
$ Int -> [a] -> [[a]]
forall a. Int -> [a] -> [[a]]
ptsAG 7 [a]
fq


-- given the images of i0, i1, i2, return the automorphism

-- the inputs must be pure imaginary unit octonions

-- and we must have isOrthogonal i0 i1, isOrthogonal i0 i2, isOrthogonal i1 i2, and isOrthogonal (i0*i1) i2

autFrom :: Octonion a -> Octonion a -> Octonion a -> [[a]]
autFrom i0' :: Octonion a
i0' i1' :: Octonion a
i1' i2' :: Octonion a
i2' =
    let 0:r0 :: [a]
r0 = Octonion a -> [a]
forall a. Num a => Octonion a -> [a]
toList Octonion a
i0'
        0:r1 :: [a]
r1 = Octonion a -> [a]
forall a. Num a => Octonion a -> [a]
toList Octonion a
i1'
        0:r2 :: [a]
r2 = Octonion a -> [a]
forall a. Num a => Octonion a -> [a]
toList Octonion a
i2'
        0:r3 :: [a]
r3 = Octonion a -> [a]
forall a. Num a => Octonion a -> [a]
toList (Octonion a -> [a]) -> Octonion a -> [a]
forall a b. (a -> b) -> a -> b
$ Octonion a
i0'Octonion a -> Octonion a -> Octonion a
forall a. Num a => a -> a -> a
*Octonion a
i1'
        0:r4 :: [a]
r4 = Octonion a -> [a]
forall a. Num a => Octonion a -> [a]
toList (Octonion a -> [a]) -> Octonion a -> [a]
forall a b. (a -> b) -> a -> b
$ Octonion a
i1'Octonion a -> Octonion a -> Octonion a
forall a. Num a => a -> a -> a
*Octonion a
i2'
        0:r5 :: [a]
r5 = Octonion a -> [a]
forall a. Num a => Octonion a -> [a]
toList (Octonion a -> [a]) -> Octonion a -> [a]
forall a b. (a -> b) -> a -> b
$ Octonion a
i0'Octonion a -> Octonion a -> Octonion a
forall a. Num a => a -> a -> a
*(Octonion a
i1'Octonion a -> Octonion a -> Octonion a
forall a. Num a => a -> a -> a
*Octonion a
i2')
        0:r6 :: [a]
r6 = Octonion a -> [a]
forall a. Num a => Octonion a -> [a]
toList (Octonion a -> [a]) -> Octonion a -> [a]
forall a b. (a -> b) -> a -> b
$ Octonion a
i0'Octonion a -> Octonion a -> Octonion a
forall a. Num a => a -> a -> a
*Octonion a
i2'
    in [[a]
r0,[a]
r1,[a]
r2,[a]
r3,[a]
r4,[a]
r5,[a]
r6]


x :: Octonion k
x %^ :: Octonion k -> [[k]] -> Octonion k
%^ g :: [[k]]
g =
    let a :: k
a:as :: [k]
as = Octonion k -> [k]
forall a. Num a => Octonion a -> [a]
toList Octonion k
x
    in [k] -> Octonion k
forall k. (Eq k, Num k) => [k] -> Octonion k
fromList ([k] -> Octonion k) -> [k] -> Octonion k
forall a b. (a -> b) -> a -> b
$ k
a k -> [k] -> [k]
forall a. a -> [a] -> [a]
: ([k]
as [k] -> [[k]] -> [k]
forall a. Num a => [a] -> [[a]] -> [a]
<*>> [[k]]
g)


-- G2(3)


alpha3 :: [[F3]]
alpha3 = Octonion F3 -> Octonion F3 -> Octonion F3 -> [[F3]]
forall a.
(Ord a, Num a) =>
Octonion a -> Octonion a -> Octonion a -> [[a]]
autFrom ([(Int, F3)] -> Octonion F3
forall k. [(Int, k)] -> Octonion k
O [(1,1::F3)]) ([(Int, F3)] -> Octonion F3
forall k. [(Int, k)] -> Octonion k
O [(2,1)]) ([(Int, F3)] -> Octonion F3
forall k. [(Int, k)] -> Octonion k
O [(3,1)])
beta3 :: [[F3]]
beta3 = Octonion F3 -> Octonion F3 -> Octonion F3 -> [[F3]]
forall a.
(Ord a, Num a) =>
Octonion a -> Octonion a -> Octonion a -> [[a]]
autFrom ([(Int, F3)] -> Octonion F3
forall k. [(Int, k)] -> Octonion k
O [(0,1::F3)]) ([(Int, F3)] -> Octonion F3
forall k. [(Int, k)] -> Octonion k
O [(2,1)]) ([(Int, F3)] -> Octonion F3
forall k. [(Int, k)] -> Octonion k
O [(4,1)])

gamma3s :: [Octonion F3]
gamma3s = [Octonion F3
x | Octonion F3
x <- [F3] -> [Octonion F3]
forall a. (Eq a, Num a) => [a] -> [Octonion a]
unitImagOctonions [F3]
f3, Octonion F3 -> Octonion F3 -> Bool
forall a. (Eq a, Num a) => Octonion a -> Octonion a -> Bool
isOrthogonal ([(Int, F3)] -> Octonion F3
forall k. [(Int, k)] -> Octonion k
O [(0,1)]) Octonion F3
x, Octonion F3 -> Octonion F3 -> Bool
forall a. (Eq a, Num a) => Octonion a -> Octonion a -> Bool
isOrthogonal ([(Int, F3)] -> Octonion F3
forall k. [(Int, k)] -> Octonion k
O [(1,1)]) Octonion F3
x, Octonion F3 -> Octonion F3 -> Bool
forall a. (Eq a, Num a) => Octonion a -> Octonion a -> Bool
isOrthogonal ([(Int, F3)] -> Octonion F3
forall k. [(Int, k)] -> Octonion k
O [(3,1)]) Octonion F3
x]

gamma3 :: [[F3]]
gamma3 = Octonion F3 -> Octonion F3 -> Octonion F3 -> [[F3]]
forall a.
(Ord a, Num a) =>
Octonion a -> Octonion a -> Octonion a -> [[a]]
autFrom ([(Int, F3)] -> Octonion F3
forall k. [(Int, k)] -> Octonion k
O [(0,1::F3)]) ([(Int, F3)] -> Octonion F3
forall k. [(Int, k)] -> Octonion k
O [(1,1)]) ([(Int, F3)] -> Octonion F3
forall k. [(Int, k)] -> Octonion k
O [(2,1),(4,1),(5,1),(6,1)])

alpha3' :: Permutation (Octonion F3)
alpha3' = [(Octonion F3, Octonion F3)] -> Permutation (Octonion F3)
forall a. Ord a => [(a, a)] -> Permutation a
fromPairs [(Octonion F3
x, Octonion F3
x Octonion F3 -> [[F3]] -> Octonion F3
forall k. (Eq k, Num k) => Octonion k -> [[k]] -> Octonion k
%^ [[F3]]
alpha3) | Octonion F3
x <- [F3] -> [Octonion F3]
forall a. (Eq a, Num a) => [a] -> [Octonion a]
unitImagOctonions [F3]
f3]
beta3' :: Permutation (Octonion F3)
beta3' = [(Octonion F3, Octonion F3)] -> Permutation (Octonion F3)
forall a. Ord a => [(a, a)] -> Permutation a
fromPairs [(Octonion F3
x, Octonion F3
x Octonion F3 -> [[F3]] -> Octonion F3
forall k. (Eq k, Num k) => Octonion k -> [[k]] -> Octonion k
%^ [[F3]]
beta3) | Octonion F3
x <- [F3] -> [Octonion F3]
forall a. (Eq a, Num a) => [a] -> [Octonion a]
unitImagOctonions [F3]
f3]
gamma3' :: Permutation (Octonion F3)
gamma3' = [(Octonion F3, Octonion F3)] -> Permutation (Octonion F3)
forall a. Ord a => [(a, a)] -> Permutation a
fromPairs [(Octonion F3
x, Octonion F3
x Octonion F3 -> [[F3]] -> Octonion F3
forall k. (Eq k, Num k) => Octonion k -> [[k]] -> Octonion k
%^ [[F3]]
gamma3) | Octonion F3
x <- [F3] -> [Octonion F3]
forall a. (Eq a, Num a) => [a] -> [Octonion a]
unitImagOctonions [F3]
f3]

-- |Generators for G2(3), a finite simple group of order 4245696,

-- as a permutation group on the 702 unit imaginary octonions over F3

g2_3 :: [Permutation (Octonion F3)]
g2_3 :: [Permutation (Octonion F3)]
g2_3 = [Permutation (Octonion F3)
alpha3', Permutation (Octonion F3)
beta3', Permutation (Octonion F3)
gamma3']
-- These three together generate a group of order 4245696, which is therefore the whole of G2(3)


-- Unit imaginary octonions form one orbit under the action of G2


-- [alpha', beta', gamma'] generate G2(3) as a permutation group on 702 points (the number of unit imaginary octonions over F3)

-- Interestingly, http://brauer.maths.qmul.ac.uk/Atlas/v3/exc/G23/ doesn't seem to have this permutation representation



-- G2(4)


alpha4 :: [[F4]]
alpha4 = Octonion F4 -> Octonion F4 -> Octonion F4 -> [[F4]]
forall a.
(Ord a, Num a) =>
Octonion a -> Octonion a -> Octonion a -> [[a]]
autFrom ([(Int, F4)] -> Octonion F4
forall k. [(Int, k)] -> Octonion k
O [(1,1::F4)]) ([(Int, F4)] -> Octonion F4
forall k. [(Int, k)] -> Octonion k
O [(2,1)]) ([(Int, F4)] -> Octonion F4
forall k. [(Int, k)] -> Octonion k
O [(3,1)])
beta4 :: [[F4]]
beta4 = Octonion F4 -> Octonion F4 -> Octonion F4 -> [[F4]]
forall a.
(Ord a, Num a) =>
Octonion a -> Octonion a -> Octonion a -> [[a]]
autFrom ([(Int, F4)] -> Octonion F4
forall k. [(Int, k)] -> Octonion k
O [(0,1::F4)]) ([(Int, F4)] -> Octonion F4
forall k. [(Int, k)] -> Octonion k
O [(2,1)]) ([(Int, F4)] -> Octonion F4
forall k. [(Int, k)] -> Octonion k
O [(4,1)])

gamma4s :: [Octonion F4]
gamma4s = [Octonion F4
x | Octonion F4
x <- [F4] -> [Octonion F4]
forall a. (Eq a, Num a) => [a] -> [Octonion a]
unitImagOctonions [F4]
f4, Octonion F4 -> Octonion F4 -> Bool
forall a. (Eq a, Num a) => Octonion a -> Octonion a -> Bool
isOrthogonal ([(Int, F4)] -> Octonion F4
forall k. [(Int, k)] -> Octonion k
O [(0,1)]) Octonion F4
x, Octonion F4 -> Octonion F4 -> Bool
forall a. (Eq a, Num a) => Octonion a -> Octonion a -> Bool
isOrthogonal ([(Int, F4)] -> Octonion F4
forall k. [(Int, k)] -> Octonion k
O [(1,1)]) Octonion F4
x, Octonion F4 -> Octonion F4 -> Bool
forall a. (Eq a, Num a) => Octonion a -> Octonion a -> Bool
isOrthogonal ([(Int, F4)] -> Octonion F4
forall k. [(Int, k)] -> Octonion k
O [(3,1)]) Octonion F4
x]

-- gamma4 = autFrom (O [(0,1::F4)]) (O [(1,1)]) (O [(5,embed x),(6,embed $ 1+x)])

gamma4 :: [[F4]]
gamma4 = Octonion F4 -> Octonion F4 -> Octonion F4 -> [[F4]]
forall a.
(Ord a, Num a) =>
Octonion a -> Octonion a -> Octonion a -> [[a]]
autFrom ([(Int, F4)] -> Octonion F4
forall k. [(Int, k)] -> Octonion k
O [(0,1::F4)]) ([(Int, F4)] -> Octonion F4
forall k. [(Int, k)] -> Octonion k
O [(1,1)]) ([(Int, F4)] -> Octonion F4
forall k. [(Int, k)] -> Octonion k
O [(5,F4
a4),(6,1F4 -> F4 -> F4
forall a. Num a => a -> a -> a
+F4
a4)])

alpha4' :: Permutation (Octonion F4)
alpha4' = [(Octonion F4, Octonion F4)] -> Permutation (Octonion F4)
forall a. Ord a => [(a, a)] -> Permutation a
fromPairs [(Octonion F4
x, Octonion F4
x Octonion F4 -> [[F4]] -> Octonion F4
forall k. (Eq k, Num k) => Octonion k -> [[k]] -> Octonion k
%^ [[F4]]
alpha4) | Octonion F4
x <- [F4] -> [Octonion F4]
forall a. (Eq a, Num a) => [a] -> [Octonion a]
unitImagOctonions [F4]
f4]
beta4' :: Permutation (Octonion F4)
beta4' = [(Octonion F4, Octonion F4)] -> Permutation (Octonion F4)
forall a. Ord a => [(a, a)] -> Permutation a
fromPairs [(Octonion F4
x, Octonion F4
x Octonion F4 -> [[F4]] -> Octonion F4
forall k. (Eq k, Num k) => Octonion k -> [[k]] -> Octonion k
%^ [[F4]]
beta4) | Octonion F4
x <- [F4] -> [Octonion F4]
forall a. (Eq a, Num a) => [a] -> [Octonion a]
unitImagOctonions [F4]
f4]
gamma4' :: Permutation (Octonion F4)
gamma4' = [(Octonion F4, Octonion F4)] -> Permutation (Octonion F4)
forall a. Ord a => [(a, a)] -> Permutation a
fromPairs [(Octonion F4
x, Octonion F4
x Octonion F4 -> [[F4]] -> Octonion F4
forall k. (Eq k, Num k) => Octonion k -> [[k]] -> Octonion k
%^ [[F4]]
gamma4) | Octonion F4
x <- [F4] -> [Octonion F4]
forall a. (Eq a, Num a) => [a] -> [Octonion a]
unitImagOctonions [F4]
f4]

-- Haven't checked whether these generate whole group - can be expected to run a long time