From HoTT Require Import Basics Types.From HoTT Require Import Basics Types.
From HoTT.WildCat Require Import Core Equiv NatTrans Yoneda.
Require Import Pointed.
Require Import Truncations.Core Truncations.Connectedness.
Require Import Spaces.Int Spaces.Circle Spaces.Spheres.
From HoTT.Algebra.AbGroups Require Import AbelianGroup Z.
Require Import Homotopy.HomotopyGroup.
Require Import Homotopy.HSpaceS1.
Require Import Homotopy.Hopf.

(** * We show that the nth homotopy group of the n-sphere is the integers, for n >= 1. *)

Local Open Scope wc_iso_scope.
Local Open Scope pointed_scope.

(** The fundamental group of the 1-sphere / circle. *)

Section Pi1S1.
  Context `{Univalence}.

  Theorem pi1_circle : Pi 1 [Circle, base] ≅ abgroup_Z.
H: Univalence
Pi 1 [Circle, base] ≅ abgroup_Z
  Proof.
H: Univalence
Pi 1 [Circle, base] ≅ abgroup_Z
    (** We give the isomorphism backwards, so we check the operation is preserved coming from the integer side. *)
    symmetry.
H: Univalence
abgroup_Z ≅ Pi 1 [Circle, base]
    srapply Build_GroupIsomorphism'.
H: Univalence
abgroup_Z <~> Pi 1 [Circle, base]
H: Univalence
IsSemiGroupPreserving ?f
    {
H: Univalence
abgroup_Z <~> Pi 1 [Circle, base] equiv_via (base = base).
H: Univalence
abgroup_Z <~> base = base
H: Univalence
base = base <~> Pi 1 [Circle, base]
      2: exact (equiv_tr 0 (loops [Circle, base])).
H: Univalence
abgroup_Z <~> base = base
      symmetry.
H: Univalence
base = base <~> abgroup_Z
      exact equiv_loopCircle_int. }
H: Univalence
IsSemiGroupPreserving
  (equiv_composeR' equiv_loopCircle_int^-1
     (equiv_tr 0 (loops [Circle, base])))
    intros a b.
H: Univalence
a, b: abgroup_Z
equiv_composeR' equiv_loopCircle_int^-1 (equiv_tr 0 (loops [Circle, base]))
  (sg_op a b) =
sg_op
  (equiv_composeR' equiv_loopCircle_int^-1
     (equiv_tr 0 (loops [Circle, base])) a)
  (equiv_composeR' equiv_loopCircle_int^-1
     (equiv_tr 0 (loops [Circle, base])) b)
    cbn; apply ap.
H: Univalence
a, b: abgroup_Z
Circle_decode base (a + b)%int = Circle_decode base a @ Circle_decode base b
    apply loopexp_add.
  Defined.

  Theorem pi1_s1 : Pi 1 (psphere 1) ≅ abgroup_Z.
H: Univalence
Pi 1 (psphere 1) ≅ abgroup_Z
  Proof.
H: Univalence
Pi 1 (psphere 1) ≅ abgroup_Z
    etransitivity.
H: Univalence
Pi 1 (psphere 1) ≅ ?Goal
H: Univalence
?Goal ≅ abgroup_Z
    2: exact pi1_circle.
H: Univalence
Pi 1 (psphere 1) ≅ Pi 1 [Circle, base]
    apply groupiso_pi_functor.
H: Univalence
psphere 1 <~>* [Circle, base]
    apply pequiv_S1_Circle.
  Defined.

End Pi1S1.

(** The second homotopy group of the 2-sphere is the integers. *)

Section Pi2S2.

  Definition ptr_loops_s2_s1 `{Univalence}
    : pTr 1 (loops (psphere 2)) <~>* psphere 1
    := (licata_finster (psphere 1))^-1*.

  Definition pi2_s2 `{Univalence}
    : Pi 2 (psphere 2) $<~> abgroup_Z.
H: Univalence
Pi 2 (psphere 2) ≅ abgroup_Z
  Proof.
H: Univalence
Pi 2 (psphere 2) ≅ abgroup_Z
    refine (pi1_s1 $oE _).
H: Univalence
Pi 2 (psphere 2) ≅ Pi 1 (psphere 1)
    change (Pi 2 ?X) with (Pi 1 (loops X)).
H: Univalence
Pi 1 (loops (psphere 2)) ≅ Pi 1 (psphere 1)
    symmetry; exact (grp_iso_Pi_connected_hspace (psphere 1)).
    (* The last line can also be replaced with
         exact (compose_cate (A:=Group) (emap (Pi 1) ptr_loops_s2_s1)
                                        (grp_iso_pi_Tr _ _)). *)
  Defined.

End Pi2S2.

(** For n >= 1, the nth homotopy group of the n-sphere is the integers. *)

Section PinSn.
  Definition pin_sn `{Univalence} (n : nat)
    : Pi n.+1 (psphere n.+1) $<~> abgroup_Z.
H: Univalence
n: nat
Pi n.+1 (psphere n.+1) ≅ abgroup_Z
  Proof.
H: Univalence
n: nat
Pi n.+1 (psphere n.+1) ≅ abgroup_Z
    destruct n.
H: Univalence
Pi 1 (psphere 1) ≅ abgroup_Z
H: Univalence
n: nat
Pi n.+2 (psphere n.+2) ≅ abgroup_Z
    1: exact pi1_s1.
H: Univalence
n: nat
Pi n.+2 (psphere n.+2) ≅ abgroup_Z
    induction n as [|n IHn].
H: Univalence
Pi 2 (psphere 2) ≅ abgroup_Z
H: Univalence
n: nat
IHn: Pi n.+2 (psphere n.+2) ≅ abgroup_Z
Pi n.+3 (psphere n.+3) ≅ abgroup_Z
    1: exact pi2_s2.
H: Univalence
n: nat
IHn: Pi n.+2 (psphere n.+2) ≅ abgroup_Z
Pi n.+3 (psphere n.+3) ≅ abgroup_Z
    refine (_ $oE groupiso_pi_loops n.+1 (psphere n.+3)).
H: Univalence
n: nat
IHn: Pi n.+2 (psphere n.+2) ≅ abgroup_Z
Pi n.+2 (loops (psphere n.+3)) ≅ abgroup_Z
    refine (IHn $oE _).
H: Univalence
n: nat
IHn: Pi n.+2 (psphere n.+2) ≅ abgroup_Z
Pi n.+2 (loops (psphere n.+3)) ≅ Pi n.+2 (psphere n.+2)
    symmetry.
H: Univalence
n: nat
IHn: Pi n.+2 (psphere n.+2) ≅ abgroup_Z
Pi n.+2 (psphere n.+2) ≅ Pi n.+2 (loops (psphere n.+3))
    snapply (grp_iso_pi_connmap _ (loop_susp_unit (psphere n.+2))).
H: Univalence
n: nat
IHn: Pi n.+2 (psphere n.+2) ≅ abgroup_Z
IsConnMap (Tr n.+2%nat) (loop_susp_unit (psphere n.+2))
    (* The (n+2)-sphere is (n+1)-connected, so [loop_susp_unit] is [n +2+ n]-connected.  Since [n.+2 <= n +2+ n], we're done, after some [trunc_index] juggling. *)
    apply (isconnmap_pred_add n.-2).
H: Univalence
n: nat
IHn: Pi n.+2 (psphere n.+2) ≅ abgroup_Z
IsConnMap (Tr (n.-2 +2+ n.+2%nat)) (loop_susp_unit (psphere n.+2))
    rewrite 2 trunc_index_add_succ.
H: Univalence
n: nat
IHn: Pi n.+2 (psphere n.+2) ≅ abgroup_Z
IsConnMap (Tr (n.-2 +2+ trunc_index_inc (-2) n.+2).+2)
  (loop_susp_unit (psphere n.+2))
    change (IsConnMap (Tr (n +2+ n)) (loop_susp_unit (psphere n.+2))).
H: Univalence
n: nat
IHn: Pi n.+2 (psphere n.+2) ≅ abgroup_Z
IsConnMap (Tr (n +2+ n)) (loop_susp_unit (psphere n.+2))
    rapply conn_map_loop_susp_unit.
  Defined.
End PinSn.