From d53320cb0fb4b9cda6fc3b4b490928879f94b0e6 Mon Sep 17 00:00:00 2001
From: Ulrik Buchholtz <ulrikbuchholtz@gmail.com>
Date: Sun, 6 Mar 2016 15:44:49 -0500
Subject: [PATCH] feat(hott): the imaginaroid version of the cayley dickson
 construction

---
 hott/homotopy/imaginaroid.hlean | 269 ++++++++++++++++++++++++++++++++
 1 file changed, 269 insertions(+)
 create mode 100644 hott/homotopy/imaginaroid.hlean

diff --git a/hott/homotopy/imaginaroid.hlean b/hott/homotopy/imaginaroid.hlean
new file mode 100644
index 000000000..29e9de7a1
--- /dev/null
+++ b/hott/homotopy/imaginaroid.hlean
@@ -0,0 +1,269 @@
+/-
+Copyright (c) 2016 Ulrik Buchholtz and Egbert Rijke. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Ulrik Buchholtz, Egbert Rijke
+
+Cayley-Dickson construction via imaginaroids
+-/
+
+import algebra.group cubical.square types.pi .hopf
+
+open eq eq.ops equiv susp hopf
+open [notation] sum
+
+namespace imaginaroid
+
+structure has_star [class] (A : Type) :=
+(star : A → A)
+
+reserve postfix `*` : (max+1)
+postfix `*` := has_star.star
+
+structure involutive_neg [class] (A : Type) extends has_neg A :=
+(neg_neg : ∀a, neg (neg a) = a)
+
+section
+  variable {A : Type}
+  variable [H : involutive_neg A]
+  include H
+
+  theorem neg_neg (a : A) : - -a = a := !involutive_neg.neg_neg
+end
+
+section
+  /- In this section we construct, when A has a negation,
+     a unit, a negation and a conjugation on susp A.
+     The unit 1 is north, so south is -1.
+     The negation must then swap north and south,
+     while the conjugation fixes the poles and negates on meridians.
+  -/
+  variable {A : Type}
+
+  definition has_one_susp [instance] : has_one (susp A) :=
+  ⦃ has_one, one := north ⦄
+
+  variable [H : has_neg A]
+  include H
+
+  definition susp_neg : susp A → susp A :=
+  susp.elim south north (λa, (merid (neg a))⁻¹)
+
+  definition has_neg_susp [instance] : has_neg (susp A) :=
+  ⦃ has_neg, neg := susp_neg⦄
+
+  definition susp_star : susp A → susp A :=
+  susp.elim north south (λa, merid (neg a))
+
+  definition has_star_susp [instance] : has_star (susp A) :=
+  ⦃ has_star, star := susp_star ⦄
+end
+
+section
+  -- If negation on A is involutive, so is negation on susp A
+  variable {A : Type}
+  variable [H : involutive_neg A]
+  include H
+
+  definition susp_neg_neg (x : susp A) : - - x = x :=
+  begin
+    induction x with a,
+    { reflexivity },
+    { reflexivity },
+    { apply eq_pathover, rewrite ap_id,
+      rewrite (ap_compose' (λy, -y)),
+      krewrite susp.elim_merid, rewrite ap_inv,
+      krewrite susp.elim_merid, rewrite neg_neg,
+      rewrite inv_inv, apply hrefl }
+  end
+
+  definition involutive_neg_susp [instance] : involutive_neg (susp A) :=
+  ⦃ involutive_neg, neg_neg := susp_neg_neg ⦄
+
+  definition susp_star_star (x : susp A) : x** = x :=
+  begin
+    induction x with a,
+    { reflexivity },
+    { reflexivity },
+    { apply eq_pathover, rewrite ap_id,
+      krewrite (ap_compose' (λy, y*)),
+      do 2 krewrite susp.elim_merid, rewrite neg_neg,
+      apply hrefl }
+  end
+
+  definition susp_neg_star (x : susp A) : (-x)* = -x* :=
+  begin
+    induction x with a,
+    { reflexivity },
+    { reflexivity },
+    { apply eq_pathover,
+      krewrite [ap_compose' (λy, y*),ap_compose' (λy, -y) (λy, y*)],
+      do 3 krewrite susp.elim_merid, rewrite ap_inv, krewrite susp.elim_merid,
+      apply hrefl }
+  end
+end
+
+structure imaginaroid [class] (A : Type)
+  extends involutive_neg A, has_mul (susp A) :=
+(one_mul : ∀x, mul one x = x)
+(mul_one : ∀x, mul x one = x)
+(mul_neg : ∀x y, mul x (@susp_neg A ⦃ has_neg, neg := neg ⦄ y) =
+           @susp_neg A ⦃ has_neg, neg := neg ⦄ (mul x y))
+(norm : ∀x, mul x (@susp_star A ⦃ has_neg, neg := neg ⦄ x) = one)
+(star_mul : ∀x y, @susp_star A ⦃ has_neg, neg := neg ⦄ (mul x y)
+  = mul (@susp_star A ⦃ has_neg, neg := neg ⦄ y)
+        (@susp_star A ⦃ has_neg, neg := neg ⦄ x))
+
+section
+  variable {A : Type}
+  variable [H : imaginaroid A]
+  include H
+
+  theorem one_mul (x : susp A) : 1 * x = x := !imaginaroid.one_mul
+  theorem mul_one (x : susp A) : x * 1 = x := !imaginaroid.mul_one
+  theorem mul_neg (x y : susp A) : x * -y = -x * y := !imaginaroid.mul_neg
+
+  /- this should not be an instance because we typically construct
+     the h_space structure on susp A before defining
+     the imaginaroid structure on A -/
+  definition imaginaroid_h_space : h_space (susp A) :=
+  ⦃ h_space, one := one, mul := mul, one_mul := one_mul, mul_one := mul_one ⦄
+
+  theorem norm (x : susp A) : x * x* = 1 := !imaginaroid.norm
+  theorem star_mul (x y : susp A) : (x * y)* = y* * x* := !imaginaroid.star_mul
+  theorem one_star : 1* = 1 :> susp A := idp
+
+  theorem neg_mul (x y : susp A) : (-x) * y = -x * y :=
+  calc
+    (-x) * y = ((-x) * y)**  : susp_star_star
+         ... = (y* * (-x)*)* : star_mul
+         ... = (y* * -x*)*   : susp_neg_star
+         ... = (-y* * x*)*   : mul_neg
+         ... = -(y* * x*)*   : susp_neg_star
+         ... = -x** * y**    : star_mul
+         ... = -x * y**      : susp_star_star
+         ... = -x * y        : susp_star_star
+
+  theorem norm' (x : susp A) : x* * x = 1 :=
+  calc
+    x* * x = (x* * x)**  : susp_star_star
+       ... = (x* * x**)* : star_mul
+       ... = 1*          : norm
+       ... = 1           : one_star
+end
+
+/- Here we prove that if A has an associative imaginaroid structure,
+   then join (susp A) (susp A) gets an h_space structure -/
+section
+  parameter A : Type
+  parameter [H : imaginaroid A]
+  parameter (assoc : Πa b c : susp A, (a * b) * c = a * b * c)
+  include A H assoc
+
+  open join
+
+  section lemmata
+    parameters (a b c d : susp A)
+
+    local abbreviation f : susp A → susp A :=
+    λx, a * c * (-x)
+
+    local abbreviation g : susp A → susp A :=
+    λy, c * y * b
+
+    definition lemma_1 : f (-1) = a * c :=
+    calc
+      a * c * (- -1) = a * c * 1  : idp
+                 ... = a * c      : mul_one
+
+    definition lemma_2 : f (c* * a* * d * b*) = - d * b* :=
+    calc
+      a * c * (-c* * a* * d * b*)
+        = a * (-c * c* * a* * d * b*)     : mul_neg
+    ... = -a * c * c* * a* * d * b*       : mul_neg
+    ... = -(a * c) * c* * a* * d * b*     : assoc
+    ... = -((a * c) * c*) * a* * d * b*   : assoc
+    ... = -(a * c * c*) * a* * d * b*     : assoc
+    ... = -(a * 1) * a* * d * b*          : norm
+    ... = -a * a* * d * b*                : mul_one
+    ... = -(a * a*) * d * b*              : assoc
+    ... = -1 * d * b*                     : norm
+    ... = -d * b*                         : one_mul
+
+    definition lemma_3 : g 1 = c * b :=
+    calc
+      c * 1 * b = c * b : one_mul
+
+    definition lemma_4 : g (c* * a* * d * b*) = a* * d :=
+    calc
+      c * (c* * a* * d * b*) * b
+        = (c * c* * a* * d * b*) * b      : assoc
+    ... = ((c * c*) * a* * d * b*) * b    : assoc
+    ... = (1 * a* * d * b*) * b           : norm
+    ... = (a* * d * b*) * b               : one_mul
+    ... = a* * (d * b*) * b               : assoc
+    ... = a* * d * b* * b                 : assoc
+    ... = a* * d * 1                      : norm'
+    ... = a* * d                          : mul_one
+  end lemmata
+
+  /-
+    in the algebraic form, the Cayley-Dickson multiplication has:
+
+      (a,b) * (c,d) = (a * c - d * b*, a* * d + c * b)
+
+    here we do the spherical form.
+  -/
+  definition cd_mul (x y : join (susp A) (susp A)) : join (susp A) (susp A) :=
+  begin
+    induction x with a b a b,
+    { induction y with c d c d,
+      { exact inl (a * c) },
+      { exact inr (a* * d) },
+      { apply glue }
+    },
+    { induction y with c d c d,
+      { exact inr (c * b) },
+      { exact inl (- d * b*) },
+      { apply inverse, apply glue }
+    },
+    { induction y with c d c d,
+      { apply glue },
+      { apply inverse, apply glue },
+      { apply eq_pathover,
+        krewrite [join.elim_glue,join.elim_glue],
+        change join.diamond (a * c) (-d * b*) (c * b) (a* * d),
+        rewrite [-(lemma_1 a c),-(lemma_2 a b c d),
+                 -(lemma_3 b c),-(lemma_4 a b c d)],
+        apply join.ap_diamond (f a c) (g b c),
+        generalize (c* * a* * d * b*), clear a b c d,
+        intro x, induction x with i,
+        { apply join.vdiamond, reflexivity },
+        { apply join.hdiamond, reflexivity },
+        { apply join.twist_diamond } } }
+  end
+
+  definition cd_one_mul (x : join (susp A) (susp A)) : cd_mul (inl 1) x = x :=
+  begin
+    induction x with a b a b,
+    { apply ap inl, apply one_mul },
+    { apply ap inr, apply one_mul },
+    { apply eq_pathover, rewrite ap_id, unfold cd_mul, krewrite join.elim_glue,
+      apply join.hsquare }
+  end
+
+  definition cd_mul_one (x : join (susp A) (susp A)) : cd_mul x (inl 1) = x :=
+  begin
+    induction x with a b a b,
+    { apply ap inl, apply mul_one },
+    { apply ap inr, apply one_mul },
+    { apply eq_pathover, rewrite ap_id, unfold cd_mul, krewrite join.elim_glue,
+      apply join.hsquare }
+  end
+
+  definition cd_h_space [instance] : h_space (join (susp A) (susp A)) :=
+  ⦃ h_space, one := inl one, mul := cd_mul,
+    one_mul := cd_one_mul, mul_one := cd_mul_one ⦄
+
+end
+
+end imaginaroid