    -- 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