feat(algebra/homotopy_group): define homotopy groups

hott/algebra/fundamental_group.hlean

@@ -1,87 +0,0 @@
-/-
-Copyright (c) 2015 Floris van Doorn. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Floris van Doorn
-
-fundamental group of a pointed space
--/
-
-import hit.trunc algebra.group types.pointed
-
-open core eq trunc algebra is_trunc pointed
-
-namespace fundamental_group
-  section
-  parameters {A : Type} (a : A)
-  definition carrier [reducible] : Type :=
-  trunc 0 (a = a)
-
-  local abbreviation G := carrier
-
-  definition mul (g h : G) : G :=
-  begin
-    apply trunc.rec_on g, intro p,
-    apply trunc.rec_on h, intro q,
-    exact tr (p ⬝ q)
-  end
-
-  definition inv (g : G) : G :=
-  begin
-    apply trunc.rec_on g, intro p,
-    exact tr p⁻¹
-  end
-
-  definition one : G :=
-  tr idp
-
-  local notation 1 := one
-  local postfix ⁻¹ := inv
-  local infix * := mul
-
-  definition mul_assoc (g₁ g₂ g₃ : G) : g₁ * g₂ * g₃ = g₁ * (g₂ * g₃) :=
-  begin
-    apply trunc.rec_on g₁, intro p₁,
-    apply trunc.rec_on g₂, intro p₂,
-    apply trunc.rec_on g₃, intro p₃,
-    exact ap tr !con.assoc,
-  end
-
-  definition one_mul (g : G) : 1 * g = g :=
-  begin
-    apply trunc.rec_on g, intro p,
-    exact ap tr !idp_con,
-  end
-
-  definition mul_one (g : G) : g * 1 = g :=
-  begin
-    apply trunc.rec_on g, intro p,
-    exact idp,
-  end
-
-  definition mul_left_inv (g : G) : g⁻¹ * g = 1 :=
-  begin
-    apply trunc.rec_on g, intro p,
-    apply ap tr !con.left_inv
-  end
-
-  definition group : group G :=
-  ⦃group,
-    mul          := mul,
-    mul_assoc    := mul_assoc,
-    one          := one,
-    one_mul      := one_mul,
-    mul_one      := mul_one,
-    inv          := inv,
-    mul_left_inv := mul_left_inv,
-   is_hset_carrier := _⦄
-
-  end
-end fundamental_group
-attribute fundamental_group.group [instance] [constructor] [priority 800]
-
-definition fundamental_group [constructor] (A : Type) [H : pointed A]: Group :=
-Group.mk (fundamental_group.carrier (point A)) _
-
-namespace core
-  prefix `π₁`:95 := fundamental_group
-end core

hott/algebra/homotopy_group.hlean

@@ -0,0 +1,53 @@
+/-
+Copyright (c) 2015 Floris van Doorn. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Floris van Doorn
+
+homotopy groups of a pointed space
+-/
+
+import types.pointed .trunc_group
+
+open nat eq pointed trunc is_trunc algebra
+
+namespace eq
+
+  definition homotopy_group [reducible] (n : ℕ) (A : Pointed) : Type :=
+  trunc 0 (Ω[n] A)
+
+  notation `π[`:95 n:0 `] `:0 A:95 := homotopy_group n A
+
+  definition pointed_homotopy_group [instance] [constructor] (n : ℕ) (A : Pointed)
+    : pointed (π[n] A) :=
+  pointed.mk (tr rfln)
+
+  definition group_homotopy_group [instance] [constructor] (n : ℕ) (A : Pointed)
+    : group (π[succ n] A) :=
+  trunc_group concat inverse idp con.assoc idp_con con_idp con.left_inv
+
+  definition comm_group_homotopy_group [constructor] (n : ℕ) (A : Pointed)
+    : comm_group (π[succ (succ n)] A) :=
+  trunc_comm_group concat inverse idp con.assoc idp_con con_idp con.left_inv eckmann_hilton
+
+  local attribute comm_group_homotopy_group [instance]
+
+  definition Pointed_homotopy_group [constructor] (n : ℕ) (A : Pointed) : Pointed :=
+  Pointed.mk (π[n] A)
+
+  definition Group_homotopy_group [constructor] (n : ℕ) (A : Pointed) : Group :=
+  Group.mk (π[succ n] A) _
+
+  definition CommGroup_homotopy_group [constructor] (n : ℕ) (A : Pointed) : CommGroup :=
+  CommGroup.mk (π[succ (succ n)] A) _
+
+  definition fundamental_group [constructor] (A : Pointed) : Group :=
+  Group_homotopy_group zero A
+
+  notation `πP[`:95  n:0    `] `:0 A:95 := Pointed_homotopy_group n A
+  notation `πG[`:95  n:0 ` +1] `:0 A:95 := Group_homotopy_group n A
+  notation `πaG[`:95 n:0 ` +2] `:0 A:95 := CommGroup_homotopy_group n A
+
+  prefix `π₁`:95 := fundamental_group
+
+
+end eq

hott/algebra/trunc_group.hlean

@@ -0,0 +1,96 @@
+/-
+Copyright (c) 2015 Floris van Doorn. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Floris van Doorn
+
+truncating an ∞-group to a group
+-/
+
+import hit.trunc algebra.group
+
+open eq is_trunc trunc
+
+namespace algebra
+
+  section
+  parameters (A : Type) (mul : A → A → A) (inv : A → A) (one : A)
+    {mul_assoc : ∀a b c, mul (mul a b) c = mul a (mul b c)}
+    {one_mul : ∀a, mul one a = a} {mul_one : ∀a, mul a one = a}
+    {mul_left_inv : ∀a, mul (inv a) a = one}
+
+  local abbreviation G := trunc 0 A
+
+  include mul_assoc one_mul mul_one mul_left_inv
+  definition trunc_mul [unfold 9 10] (g h : G) : G :=
+  begin
+    apply trunc.rec_on g, intro p,
+    apply trunc.rec_on h, intro q,
+    exact tr (mul p q)
+  end
+
+  definition trunc_inv [unfold 9] (g : G) : G :=
+  begin
+    apply trunc.rec_on g, intro p,
+    exact tr (inv p)
+  end
+
+  definition trunc_one [constructor] : G :=
+  tr one
+
+  local notation 1 := trunc_one
+  local postfix ⁻¹ := trunc_inv
+  local infix * := trunc_mul
+
+  definition trunc_mul_assoc [unfold 9 10 11] (g₁ g₂ g₃ : G) : g₁ * g₂ * g₃ = g₁ * (g₂ * g₃) :=
+  begin
+    apply trunc.rec_on g₁, intro p₁,
+    apply trunc.rec_on g₂, intro p₂,
+    apply trunc.rec_on g₃, intro p₃,
+    exact ap tr !mul_assoc,
+  end
+
+  definition trunc_one_mul [unfold 9] (g : G) : 1 * g = g :=
+  begin
+    apply trunc.rec_on g, intro p,
+    exact ap tr !one_mul
+  end
+
+  definition trunc_mul_one [unfold 9] (g : G) : g * 1 = g :=
+  begin
+    apply trunc.rec_on g, intro p,
+    exact ap tr !mul_one
+  end
+
+  definition trunc_mul_left_inv [unfold 9] (g : G) : g⁻¹ * g = 1 :=
+  begin
+    apply trunc.rec_on g, intro p,
+    exact ap tr !mul_left_inv
+  end
+
+  definition trunc_mul_comm [unfold 10 11] (mul_comm : ∀a b, mul a b = mul b a) (g h : G)
+    : g * h = h * g :=
+  begin
+    apply trunc.rec_on g, intro p,
+    apply trunc.rec_on h, intro q,
+    exact ap tr !mul_comm
+  end
+
+  parameters (mul_assoc) (one_mul) (mul_one) (mul_left_inv) {A}
+
+  definition trunc_group [constructor] : group G :=
+  ⦃group,
+    mul          := trunc_mul,
+    mul_assoc    := trunc_mul_assoc,
+    one          := trunc_one,
+    one_mul      := trunc_one_mul,
+    mul_one      := trunc_mul_one,
+    inv          := trunc_inv,
+    mul_left_inv := trunc_mul_left_inv,
+   is_hset_carrier := _⦄
+
+
+  definition trunc_comm_group [constructor] (mul_comm : ∀a b, mul a b = mul b a) : comm_group G :=
+  ⦃comm_group, trunc_group, mul_comm := trunc_mul_comm mul_comm⦄
+
+  end
+end algebra

hott/homotopy/circle.hlean

@@ -8,7 +8,7 @@ Declaration of the circle
 
 import .sphere
 import types.bool types.int.hott types.equiv
-import algebra.fundamental_group algebra.hott
+import algebra.homotopy_group algebra.hott
 
 open eq susp bool sphere_index is_equiv equiv equiv.ops is_trunc pi
 
@@ -161,6 +161,9 @@ namespace circle
   definition pointed_circle [instance] [constructor] : pointed circle :=
   pointed.mk base
 
+  definition Circle [constructor] : Type* := pointed.mk' circle
+  notation `S¹.` := Circle
+
   definition loop_neq_idp : loop ≠ idp :=
   assume H : loop = idp,
   have H2 : Π{A : Type₁} {a : A} {p : a = a}, p = idp,
@@ -244,13 +247,13 @@ namespace circle
 
   --the carrier of π₁(S¹) is the set-truncation of base = base.
   open core algebra trunc equiv.ops
-  definition fg_carrier_equiv_int : π₁(S¹) ≃ ℤ :=
+  definition fg_carrier_equiv_int : π[1](S¹.) ≃ ℤ :=
   trunc_equiv_trunc 0 base_eq_base_equiv ⬝e !trunc_equiv
 
   definition con_comm_base (p q : base = base) : p ⬝ q = q ⬝ p :=
   eq_of_fn_eq_fn base_eq_base_equiv (by esimp;rewrite [+encode_con,add.comm])
 
-  definition fundamental_group_of_circle : π₁(S¹) = group_integers :=
+  definition fundamental_group_of_circle : π₁(S¹.) = group_integers :=
   begin
     apply (Group_eq fg_carrier_equiv_int),
     intros g h,

hott/types/pointed.hlean

@@ -73,7 +73,9 @@ namespace pointed
   prefix `Ω`:(max+5) := Loop_space
   notation `Ω[`:95 n:0 `] `:0 A:95 := Iterated_loop_space n A
 
-  definition refln [constructor] {A : Type*} {n : ℕ} : Ω[n] A := pt
+  definition rfln  [constructor] [reducible] {A : Type*} {n : ℕ} : Ω[n] A := pt
+  definition refln [constructor] [reducible] (A : Type*) (n : ℕ) : Ω[n] A := pt
+  definition refln_eq_refl (A : Type*) (n : ℕ) : rfln = rfl :> Ω[succ n] A := rfl
 
   definition iterated_loop_space [unfold 3] (A : Type) [H : pointed A] (n : ℕ) : Type :=
   Ω[n] (pointed.mk' A)