Require Import Basics Types.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import WildCat.
Require Import Pointed.
Require Import Truncations.Core Truncations.Connectedness.
Require Import Spaces.Int Spaces.Circle Spaces.Spheres.
Require Import Algebra.AbGroups.
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}.

  Local Open Scope pointed_scope.

  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)
    refine (compose_cate (b:=Pi 1 (pTr 1 (loops (psphere 2)))) _ _).
H: Univalence
Pi 1 (pTr 1 (loops (psphere 2))) ≅ Pi 1 (psphere 1)
H: Univalence
Pi 1 (loops (psphere 2))
≅ Pi 1 (pTr 1 (loops (psphere 2)))
    1: exact (emap (Pi 1) ptr_loops_s2_s1).
H: Univalence
Pi 1 (loops (psphere 2))
≅ Pi 1 (pTr 1 (loops (psphere 2)))
    apply 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))
    exact _. (* [conn_map_loop_susp_unit] *)
  Defined.
End PinSn.