CayleyDickson.agda

module _ where

data _≡_ {A : Set} : A → A → Set where
  refl : ∀ (x : A) → x ≡ x

data GroupAxioms {A : Set} (id : A) (inv : A → A) (op : A → A → A) : Set where
  GroupAxioms! :
      ∀ (x : A) → op x id ≡ x
    → ∀ (x : A) → op id x ≡ x
    → ∀ (x : A) → op x (inv x) ≡ id
    → ∀ (x : A) → op (inv x) x ≡ id
    → GroupAxioms id inv op

record Group (A : Set) : Set where
  constructor
    Group!
  field
    id  : A
    inv : A → A
    op  : A → A → A
    pf  : GroupAxioms id inv op

postulate
  FieldAxioms : {A : Set} (sum prod : Group A) → Set

record Field {A : Set} : Set where
  constructor
    Field!
  field
    elems : A
    conj  : A → A
    sum   : Group A
    prod  : Group A
    pf    : FieldAxioms prod sum

record _×_ (A B : Set) : Set where
  constructor _,_
  field
    fst : A
    snd : B

postulate
  cdc-group-inductive :
      {A : Set}
    → {id : A} {inv : A → A} {op : A → A → A} 
    → (id' : A × A) (inv' : A × A → A × A) (op' : A × A → A × A → A × A) 
    → (pf : GroupAxioms id inv op)
    → GroupAxioms id' inv' op'
  cdc-field-inductive :
      {A : Set}
    → (sum  prod  : Group A)
    → (sum' prod' : Group A × A)
    → (pf : FieldAxioms sum prod)
    → FieldAxioms sum' prod'

-- Cayley-Dickson Construction
CDC : Field → Field
CDC (Field! elems conj sum prod pf) = Field! A² conj' sum' prod' pf'
  where
    sumOp  = Group.op  sum
    prodOp  = Group.op  prod
    infix 2 _*_ 
    infix 1 _+_
    _*_ = prodOp
    _+_ = sumOp
    fst = _×_.fst
    snd = _×_.snd
    sumId  = Group.id  sum
    sumInv = Group.inv sum
    prodId  = Group.id  prod
    prodInv = Group.inv prod
    A² = (elems × elems)
    conj' : A² → A²
    conj' (a , b) = conj a , (Group.inv sum) b
    sum' : Group (A²)
    sum'  = Group! sumId' sumInv' sumOp' (cdc-group-inductive sumId' sumInv' sumOp' pf)
      where
        sumId'   = λ (x : A²) → sumId  (fst x) , sumId  (snd x)
        sumInv'  = λ (x : A²) → sumInv (fst x) , sumInv (snd x)
        sumOp'   = λ (x y : A²) → sumOp  (fst x) (fst y) , sumOp (snd x) (snd y)
    prod' : Group (A²)
    prod' = Group! prodId' prodInv' prodOp' (cdc-group-inductive prodId' prodInv' prodOp' pf)
      where
          prodId'  = λ (x : A²)   → prodId (fst x) , sumId  (snd x)
          prodInv' = λ (x : A²)   →
            let
              a   = fst x
              b   = snd x
              a†  = conj a
              -b  = sumInv b
              ǁxǁ⁻² = prodInv (a * a + b * b)
            in
              (ǁxǁ⁻² * a†) , (ǁxǁ⁻² * -b)
          prodOp' = λ (x y : A²) →
            let
              a   = fst x
              b   = snd x
              c   = fst y
              d   = snd y
              -b  = sumInv b
              c†  = conj c
              d†  = conj d
            in
              (a * c + d† * -b) , (d * a + b * c†)
    pf' = cdc-field-inductive sum' prod' pf