From f11169b8f2d4430fa05b2aa42ad2d0f781e93511 Mon Sep 17 00:00:00 2001
From: Ulrik Buchholtz <ulrikbuchholtz@gmail.com>
Date: Sun, 6 Mar 2016 19:41:58 -0500
Subject: [PATCH] feat(hott): the quaternionic hopf fibration

---
 hott/homotopy/hopf.hlean              |   5 +
 hott/homotopy/quaternionic_hopf.hlean | 128 ++++++++++++++++++++++++++
 2 files changed, 133 insertions(+)
 create mode 100644 hott/homotopy/quaternionic_hopf.hlean

diff --git a/hott/homotopy/hopf.hlean b/hott/homotopy/hopf.hlean
index 161e42246..d199ace9d 100644
--- a/hott/homotopy/hopf.hlean
+++ b/hott/homotopy/hopf.hlean
@@ -23,6 +23,11 @@ section
   definition one_mul (a : A) : 1 * a = a := !h_space.one_mul
   definition mul_one (a : A) : a * 1 = a := !h_space.mul_one
 
+  definition h_space_equiv_closed {B : Type} (f : A ≃ B) : h_space B :=
+  ⦃ h_space, one := f 1, mul := (λb b', f (f⁻¹ b * f⁻¹ b')),
+    one_mul := by intro b; rewrite [to_left_inv,one_mul,to_right_inv],
+    mul_one := by intro b; rewrite [to_left_inv,mul_one,to_right_inv] ⦄
+
   /- Lemma 8.5.5.
      If A is 0-connected, then left and right multiplication are equivalences -/
   variable [K : is_conn 0 A]
diff --git a/hott/homotopy/quaternionic_hopf.hlean b/hott/homotopy/quaternionic_hopf.hlean
new file mode 100644
index 000000000..08e65736f
--- /dev/null
+++ b/hott/homotopy/quaternionic_hopf.hlean
@@ -0,0 +1,128 @@
+/-
+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
+
+The H-space structure on S³ and the quaternionic Hopf fibration
+ (using the imaginaroid structure on S⁰).
+-/
+
+import .complex_hopf .imaginaroid
+
+open eq equiv is_equiv circle is_conn trunc is_trunc sphere_index sphere susp
+open imaginaroid
+
+namespace hopf
+
+  definition involutive_neg_empty [instance] : involutive_neg empty :=
+  ⦃ involutive_neg, neg := empty.elim, neg_neg := by intro a; induction a ⦄
+
+  definition involutive_neg_circle [instance] : involutive_neg circle :=
+  involutive_neg_susp
+
+  definition has_star_circle [instance] : has_star circle :=
+  has_star_susp
+
+  -- this is the "natural" conjugation defined using the base-loop recursor
+  definition circle_star [reducible] : S¹ → S¹ :=
+  circle.elim base loop⁻¹
+
+  definition circle_neg_id (x : S¹) : -x = x :=
+  begin
+    fapply (rec2_on x),
+    { exact seg2⁻¹ },
+    { exact seg1 },
+    { apply eq_pathover, rewrite ap_id, krewrite elim_merid,
+      apply square_of_eq, reflexivity },
+    { apply eq_pathover, rewrite ap_id, krewrite elim_merid,
+      apply square_of_eq, apply trans (con.left_inv seg2),
+      apply inverse, exact con.left_inv seg1 }
+  end
+
+  definition circle_mul_neg (x y : S¹) : x * (-y) = - x * y :=
+  by rewrite [circle_neg_id,circle_neg_id]
+
+  definition circle_star_eq (x : S¹) : x* = circle_star x :=
+  begin
+    fapply (rec2_on x),
+    { reflexivity },
+    { exact seg2⁻¹ ⬝ (tr_constant seg1 base)⁻¹ },
+    { apply eq_pathover, krewrite elim_merid, rewrite elim_seg1,
+      apply square_of_eq, apply trans
+        (ap (λw, w ⬝ (tr_constant seg1 base)⁻¹) (con.right_inv seg2)⁻¹),
+      apply con.assoc },
+    { apply eq_pathover, krewrite elim_merid, rewrite elim_seg2,
+      apply square_of_eq, rewrite [↑loop,con_inv,inv_inv,idp_con],
+      apply con.assoc }
+  end
+
+  open prod prod.ops
+
+  definition circle_norm (x : S¹) : x * x* = 1 :=
+  begin
+    rewrite circle_star_eq, induction x,
+    { reflexivity },
+    { apply eq_pathover, rewrite ap_constant,
+      krewrite [ap_compose' (λz : S¹ × S¹, circle_mul z.1 z.2)
+                            (λa : S¹, (a, circle_star a))],
+      rewrite [ap_compose' (prod_functor (λa : S¹, a) circle_star)
+                           (λa : S¹, (a, a))],
+      rewrite ap_diagonal,
+      krewrite [ap_prod_functor (λa : S¹, a) circle_star loop loop],
+      rewrite [ap_id,↑circle_star], krewrite elim_loop,
+      krewrite (ap_binary circle_mul loop loop⁻¹),
+      rewrite [ap_inv,↑circle_mul,elim_loop,ap_id,↑circle_turn,con.left_inv],
+      constructor }
+  end
+
+  definition circle_star_mul (x y : S¹) : (x * y)* = y* * x* :=
+  begin
+    induction x,
+    { apply inverse, exact circle_mul_base (y*) },
+    { apply eq_pathover, induction y,
+      { exact natural_square_tr 
+          (λa : S¹, ap (λb : S¹, b*) (circle_mul_base a)) loop },
+      { apply is_prop.elimo } }
+  end
+
+  definition imaginaroid_sphere_zero [instance]
+    : imaginaroid (sphere (-1.+1)) :=
+  ⦃ imaginaroid,
+    neg_neg := susp_neg_neg,
+    mul := circle_mul,
+    one_mul := circle_base_mul,
+    mul_one := circle_mul_base,
+    mul_neg := circle_mul_neg,
+    norm := circle_norm,
+    star_mul := circle_star_mul ⦄
+
+  local attribute sphere [reducible]
+  open sphere.ops
+
+  definition sphere_three_h_space [instance] : h_space (S 3) :=
+  @h_space_equiv_closed (join S¹ S¹)
+      (cd_h_space (S -1.+1) circle_assoc) (S 3) (join.spheres 1 1)
+
+  /- once we know that connectivity is downward closed,
+     we can replace this with an appeal to is_conn_sphere -/
+  definition is_conn_sphere_three : is_conn 0 (S 3) :=
+  begin
+    fapply is_contr.mk,
+    { exact tr (north : sphere -1.+2.+2) },
+    { intro x, induction x with x,
+      induction x with x,
+      { reflexivity },
+      { apply ap tr, exact merid (north : sphere -1.+2.+1) },
+      { apply is_prop.elimo }, }
+  end
+
+  local attribute is_conn_sphere_three [instance]
+
+  definition quaternionic_hopf : S 7 → S 4 :=
+  begin
+    intro x, apply @sigma.pr1 (susp (S 3)) (hopf (S 3)),
+    apply inv (hopf.total (S 3)), apply inv (join.spheres 3 3), exact x
+  end
+
+end hopf
+