52dd6cf90b
This commit adds truncated 2-quotients, groupoid quotients, Eilenberg MacLane spaces, chain complexes, the long exact sequence of homotopy groups, the Freudenthal Suspension Theorem, Whitehead's principle, and the computation of homotopy groups of almost all spheres which are known in HoTT.
394 lines
13 KiB
Text
394 lines
13 KiB
Text
/-
|
||
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
|
||
|
||
Declaration of the n-spheres
|
||
-/
|
||
|
||
import .susp types.trunc
|
||
|
||
open eq nat susp bool is_trunc unit pointed algebra
|
||
|
||
/-
|
||
We can define spheres with the following possible indices:
|
||
- trunc_index (defining S^-2 = S^-1 = empty)
|
||
- nat (forgetting that S^-1 = empty)
|
||
- nat, but counting wrong (S^0 = empty, S^1 = bool, ...)
|
||
- some new type "integers >= -1"
|
||
We choose the last option here.
|
||
-/
|
||
|
||
/- Sphere levels -/
|
||
|
||
inductive sphere_index : Type₀ :=
|
||
| minus_one : sphere_index
|
||
| succ : sphere_index → sphere_index
|
||
|
||
notation `ℕ₋₁` := sphere_index
|
||
|
||
namespace trunc_index
|
||
definition sub_one [reducible] (n : ℕ₋₁) : ℕ₋₂ :=
|
||
sphere_index.rec_on n -2 (λ n k, k.+1)
|
||
postfix `..-1`:(max+1) := sub_one
|
||
|
||
definition of_sphere_index [reducible] (n : ℕ₋₁) : ℕ₋₂ :=
|
||
n..-1.+1
|
||
|
||
-- we use a double dot to distinguish with the notation .-1 in trunc_index (of type ℕ → ℕ₋₂)
|
||
end trunc_index
|
||
|
||
namespace sphere_index
|
||
/-
|
||
notation for sphere_index is -1, 0, 1, ...
|
||
from 0 and up this comes from a coercion from num to sphere_index (via nat)
|
||
-/
|
||
|
||
postfix `.+1`:(max+1) := sphere_index.succ
|
||
postfix `.+2`:(max+1) := λ(n : sphere_index), (n .+1 .+1)
|
||
notation `-1` := minus_one
|
||
|
||
definition has_zero_sphere_index [instance] : has_zero ℕ₋₁ :=
|
||
has_zero.mk (succ minus_one)
|
||
|
||
definition has_one_sphere_index [instance] : has_one ℕ₋₁ :=
|
||
has_one.mk (succ (succ minus_one))
|
||
|
||
definition add_plus_one (n m : ℕ₋₁) : ℕ₋₁ :=
|
||
sphere_index.rec_on m n (λ k l, l .+1)
|
||
|
||
-- addition of sphere_indices, where (-1 + -1) is defined to be -1.
|
||
protected definition add (n m : ℕ₋₁) : ℕ₋₁ :=
|
||
sphere_index.cases_on m
|
||
(sphere_index.cases_on n -1 id)
|
||
(sphere_index.rec n (λn' r, succ r))
|
||
|
||
inductive le (a : ℕ₋₁) : ℕ₋₁ → Type :=
|
||
| sp_refl : le a a
|
||
| step : Π {b}, le a b → le a (b.+1)
|
||
|
||
infix ` +1+ `:65 := sphere_index.add_plus_one
|
||
|
||
definition has_add_sphere_index [instance] [priority 2000] [reducible] : has_add ℕ₋₁ :=
|
||
has_add.mk sphere_index.add
|
||
|
||
definition has_le_sphere_index [instance] : has_le ℕ₋₁ :=
|
||
has_le.mk sphere_index.le
|
||
|
||
definition sub_one [reducible] (n : ℕ) : ℕ₋₁ :=
|
||
nat.rec_on n -1 (λ n k, k.+1)
|
||
|
||
postfix `..-1`:(max+1) := sub_one
|
||
|
||
definition of_nat [coercion] [reducible] (n : ℕ) : ℕ₋₁ :=
|
||
n..-1.+1
|
||
|
||
-- we use a double dot to distinguish with the notation .-1 in trunc_index (of type ℕ → ℕ₋₂)
|
||
|
||
definition add_one [reducible] (n : ℕ₋₁) : ℕ :=
|
||
sphere_index.rec_on n 0 (λ n k, nat.succ k)
|
||
|
||
definition add_plus_one_of_nat (n m : ℕ) : (n +1+ m) = sphere_index.of_nat (n + m + 1) :=
|
||
begin
|
||
induction m with m IH,
|
||
{ reflexivity },
|
||
{ exact ap succ IH}
|
||
end
|
||
|
||
definition succ_sub_one (n : ℕ) : (nat.succ n)..-1 = n :> ℕ₋₁ :=
|
||
idp
|
||
|
||
definition add_sub_one (n m : ℕ) : (n + m)..-1 = n..-1 +1+ m..-1 :> ℕ₋₁ :=
|
||
begin
|
||
induction m with m IH,
|
||
{ reflexivity },
|
||
{ exact ap succ IH }
|
||
end
|
||
|
||
definition succ_le_succ {n m : ℕ₋₁} (H : n ≤ m) : n.+1 ≤[ℕ₋₁] m.+1 :=
|
||
by induction H with m H IH; apply le.sp_refl; exact le.step IH
|
||
|
||
definition minus_one_le (n : ℕ₋₁) : -1 ≤[ℕ₋₁] n :=
|
||
by induction n with n IH; apply le.sp_refl; exact le.step IH
|
||
|
||
open decidable
|
||
protected definition has_decidable_eq [instance] : Π(n m : ℕ₋₁), decidable (n = m)
|
||
| has_decidable_eq -1 -1 := inl rfl
|
||
| has_decidable_eq (n.+1) -1 := inr (by contradiction)
|
||
| has_decidable_eq -1 (m.+1) := inr (by contradiction)
|
||
| has_decidable_eq (n.+1) (m.+1) :=
|
||
match has_decidable_eq n m with
|
||
| inl xeqy := inl (by rewrite xeqy)
|
||
| inr xney := inr (λ h : succ n = succ m, by injection h with xeqy; exact absurd xeqy xney)
|
||
end
|
||
|
||
definition not_succ_le_minus_two {n : sphere_index} (H : n .+1 ≤[ℕ₋₁] -1) : empty :=
|
||
by cases H
|
||
|
||
protected definition le_trans {n m k : ℕ₋₁} (H1 : n ≤[ℕ₋₁] m) (H2 : m ≤[ℕ₋₁] k) : n ≤[ℕ₋₁] k :=
|
||
begin
|
||
induction H2 with k H2 IH,
|
||
{ exact H1},
|
||
{ exact le.step IH}
|
||
end
|
||
|
||
definition le_of_succ_le_succ {n m : ℕ₋₁} (H : n.+1 ≤[ℕ₋₁] m.+1) : n ≤[ℕ₋₁] m :=
|
||
begin
|
||
cases H with m H',
|
||
{ apply le.sp_refl},
|
||
{ exact sphere_index.le_trans (le.step !le.sp_refl) H'}
|
||
end
|
||
|
||
theorem not_succ_le_self {n : ℕ₋₁} : ¬n.+1 ≤[ℕ₋₁] n :=
|
||
begin
|
||
induction n with n IH: intro H,
|
||
{ exact not_succ_le_minus_two H},
|
||
{ exact IH (le_of_succ_le_succ H)}
|
||
end
|
||
|
||
protected definition le_antisymm {n m : ℕ₋₁} (H1 : n ≤[ℕ₋₁] m) (H2 : m ≤[ℕ₋₁] n) : n = m :=
|
||
begin
|
||
induction H2 with n H2 IH,
|
||
{ reflexivity},
|
||
{ exfalso, apply @not_succ_le_self n, exact sphere_index.le_trans H1 H2}
|
||
end
|
||
|
||
protected definition le_succ {n m : ℕ₋₁} (H1 : n ≤[ℕ₋₁] m): n ≤[ℕ₋₁] m.+1 :=
|
||
le.step H1
|
||
|
||
definition add_plus_one_minus_one (n : ℕ₋₁) : n +1+ -1 = n := idp
|
||
definition add_plus_one_succ (n m : ℕ₋₁) : n +1+ (m.+1) = (n +1+ m).+1 := idp
|
||
definition minus_one_add_plus_one (n : ℕ₋₁) : -1 +1+ n = n :=
|
||
begin induction n with n IH, reflexivity, exact ap succ IH end
|
||
definition succ_add_plus_one (n m : ℕ₋₁) : (n.+1) +1+ m = (n +1+ m).+1 :=
|
||
begin induction m with m IH, reflexivity, exact ap succ IH end
|
||
|
||
definition sphere_index_of_nat_add_one (n : ℕ₋₁) : sphere_index.of_nat (add_one n) = n.+1 :=
|
||
begin induction n with n IH, reflexivity, exact ap succ IH end
|
||
|
||
definition add_one_succ (n : ℕ₋₁) : add_one (n.+1) = succ (add_one n) :=
|
||
by reflexivity
|
||
|
||
definition add_one_sub_one (n : ℕ) : add_one (n..-1) = n :=
|
||
begin induction n with n IH, reflexivity, exact ap nat.succ IH end
|
||
|
||
definition add_one_of_nat (n : ℕ) : add_one n = nat.succ n :=
|
||
ap nat.succ (add_one_sub_one n)
|
||
|
||
definition sphere_index.of_nat_succ (n : ℕ)
|
||
: sphere_index.of_nat (nat.succ n) = (sphere_index.of_nat n).+1 :=
|
||
begin induction n with n IH, reflexivity, exact ap succ IH end
|
||
|
||
/-
|
||
warning: if this coercion is available, the coercion ℕ → ℕ₋₂ is the composition of the coercions
|
||
ℕ → ℕ₋₁ → ℕ₋₂. We don't want this composition as coercion, because it has worse computational
|
||
properties. You can rewrite it with trans_to_of_sphere_index_eq defined below.
|
||
-/
|
||
attribute trunc_index.of_sphere_index [coercion]
|
||
|
||
end sphere_index open sphere_index
|
||
|
||
definition weak_order_sphere_index [trans_instance] [reducible] : weak_order sphere_index :=
|
||
weak_order.mk le sphere_index.le.sp_refl @sphere_index.le_trans @sphere_index.le_antisymm
|
||
|
||
namespace trunc_index
|
||
definition sub_two_eq_sub_one_sub_one (n : ℕ) : n.-2 = n..-1..-1 :=
|
||
begin
|
||
induction n with n IH,
|
||
{ reflexivity},
|
||
{ exact ap trunc_index.succ IH}
|
||
end
|
||
|
||
definition of_nat_sub_one (n : ℕ)
|
||
: (sphere_index.of_nat n)..-1 = (trunc_index.sub_two n).+1 :=
|
||
begin
|
||
induction n with n IH,
|
||
{ reflexivity},
|
||
{ exact ap trunc_index.succ IH}
|
||
end
|
||
|
||
definition sub_one_of_sphere_index (n : ℕ)
|
||
: of_sphere_index n..-1 = (trunc_index.sub_two n).+1 :=
|
||
begin
|
||
induction n with n IH,
|
||
{ reflexivity},
|
||
{ exact ap trunc_index.succ IH}
|
||
end
|
||
|
||
definition succ_sub_one (n : ℕ₋₁) : n.+1..-1 = n :> ℕ₋₂ :=
|
||
idp
|
||
|
||
definition of_sphere_index_of_nat (n : ℕ)
|
||
: of_sphere_index (sphere_index.of_nat n) = of_nat n :> ℕ₋₂ :=
|
||
begin
|
||
induction n with n IH,
|
||
{ reflexivity},
|
||
{ exact ap trunc_index.succ IH}
|
||
end
|
||
|
||
definition trans_to_of_sphere_index_eq (n : ℕ)
|
||
: trunc_index._trans_to_of_sphere_index n = of_nat n :> ℕ₋₂ :=
|
||
of_sphere_index_of_nat n
|
||
|
||
definition trunc_index_of_nat_add_one (n : ℕ₋₁)
|
||
: trunc_index.of_nat (add_one n) = (of_sphere_index n).+1 :=
|
||
begin induction n with n IH, reflexivity, exact ap succ IH end
|
||
|
||
definition of_sphere_index_succ (n : ℕ₋₁) : of_sphere_index (n.+1) = (of_sphere_index n).+1 :=
|
||
begin induction n with n IH, reflexivity, exact ap succ IH end
|
||
|
||
end trunc_index
|
||
|
||
open sphere_index equiv
|
||
|
||
definition sphere (n : ℕ₋₁) : Type₀ := iterate_susp (add_one n) empty
|
||
|
||
namespace sphere
|
||
|
||
export [notation] sphere_index
|
||
|
||
definition base {n : ℕ} : sphere n := north
|
||
definition pointed_sphere [instance] [constructor] (n : ℕ) : pointed (sphere n) :=
|
||
pointed.mk base
|
||
definition psphere [constructor] (n : ℕ) : Type* := pointed.mk' (sphere n)
|
||
|
||
|
||
namespace ops
|
||
abbreviation S := sphere
|
||
notation `S.` := psphere
|
||
end ops
|
||
open sphere.ops
|
||
|
||
definition sphere_minus_one : S -1 = empty := idp
|
||
definition sphere_succ [unfold_full] (n : ℕ₋₁) : S n.+1 = susp (S n) := idp
|
||
definition psphere_succ [unfold_full] (n : ℕ) : S. (n + 1) = psusp (S. n) := idp
|
||
definition psphere_eq_iterate_susp (n : ℕ)
|
||
: S. n = pointed.MK (iterate_susp (succ n) empty) !north :=
|
||
begin
|
||
esimp,
|
||
apply ap (λx, pointed.MK (susp x) (@north x)); apply ap (λx, iterate_susp x empty),
|
||
apply add_one_sub_one
|
||
end
|
||
|
||
|
||
definition equator (n : ℕ) : map₊ (S. n) (Ω (S. (succ n))) :=
|
||
pmap.mk (λa, merid a ⬝ (merid base)⁻¹) !con.right_inv
|
||
|
||
definition surf {n : ℕ} : Ω[n] S. n :=
|
||
nat.rec_on n (proof @base 0 qed)
|
||
(begin intro m s, refine cast _ (apn m (equator m) s),
|
||
exact ap carrier !loop_space_succ_eq_in⁻¹ end)
|
||
|
||
|
||
definition bool_of_sphere : S 0 → bool :=
|
||
proof susp.rec ff tt (λx, empty.elim x) qed
|
||
|
||
definition sphere_of_bool : bool → S 0
|
||
| ff := proof north qed
|
||
| tt := proof south qed
|
||
|
||
definition sphere_equiv_bool : S 0 ≃ bool :=
|
||
equiv.MK bool_of_sphere
|
||
sphere_of_bool
|
||
(λb, match b with | tt := idp | ff := idp end)
|
||
(λx, proof susp.rec_on x idp idp (empty.rec _) qed)
|
||
|
||
definition sphere_eq_bool : S 0 = bool :=
|
||
ua sphere_equiv_bool
|
||
|
||
definition sphere_eq_pbool : S. 0 = pbool :=
|
||
pType_eq sphere_equiv_bool idp
|
||
|
||
-- TODO1: the commented-out part makes the forward function below "apn _ surf"
|
||
-- TODO2: we could make this a pointed equivalence
|
||
definition pmap_sphere (A : Type*) (n : ℕ) : map₊ (S. n) A ≃ Ω[n] A :=
|
||
begin
|
||
-- fapply equiv_change_fun,
|
||
-- {
|
||
revert A, induction n with n IH: intro A,
|
||
{ apply tr_rev (λx, x →* _ ≃ _) sphere_eq_pbool, apply pmap_bool_equiv},
|
||
{ refine susp_adjoint_loop (S. n) A ⬝e !IH ⬝e _, rewrite [loop_space_succ_eq_in]}
|
||
-- },
|
||
-- { intro f, exact apn n f surf},
|
||
-- { revert A, induction n with n IH: intro A f,
|
||
-- { exact sorry},
|
||
-- { exact sorry}}
|
||
end
|
||
|
||
protected definition elim {n : ℕ} {P : Type*} (p : Ω[n] P) : map₊ (S. n) P :=
|
||
to_inv !pmap_sphere p
|
||
|
||
-- definition elim_surf {n : ℕ} {P : Type*} (p : Ω[n] P) : apn n (sphere.elim p) surf = p :=
|
||
-- begin
|
||
-- induction n with n IH,
|
||
-- { esimp [apn,surf,sphere.elim,pmap_sphere], apply sorry},
|
||
-- { apply sorry}
|
||
-- end
|
||
|
||
end sphere
|
||
|
||
namespace sphere
|
||
open is_conn trunc_index sphere_index sphere.ops
|
||
|
||
-- Corollary 8.2.2
|
||
theorem is_conn_sphere [instance] (n : ℕ₋₁) : is_conn (n..-1) (S n) :=
|
||
begin
|
||
induction n with n IH,
|
||
{ apply is_conn_minus_two },
|
||
{ rewrite [trunc_index.succ_sub_one n, sphere.sphere_succ],
|
||
apply is_conn_susp }
|
||
end
|
||
|
||
theorem is_conn_psphere [instance] (n : ℕ) : is_conn (n.-1) (S. n) :=
|
||
transport (λx, is_conn x (sphere n)) (of_nat_sub_one n) (is_conn_sphere n)
|
||
|
||
end sphere
|
||
|
||
open sphere sphere.ops
|
||
|
||
namespace is_trunc
|
||
open trunc_index
|
||
variables {n : ℕ} {A : Type}
|
||
definition is_trunc_of_pmap_sphere_constant
|
||
(H : Π(a : A) (f : map₊ (S. n) (pointed.Mk a)) (x : S n), f x = f base) : is_trunc (n.-2.+1) A :=
|
||
begin
|
||
apply iff.elim_right !is_trunc_iff_is_contr_loop,
|
||
intro a,
|
||
apply is_trunc_equiv_closed, apply pmap_sphere,
|
||
fapply is_contr.mk,
|
||
{ exact pmap.mk (λx, a) idp},
|
||
{ intro f, fapply pmap_eq,
|
||
{ intro x, esimp, refine !respect_pt⁻¹ ⬝ (!H ⬝ !H⁻¹)},
|
||
{ rewrite [▸*,con.right_inv,▸*,con.left_inv]}}
|
||
end
|
||
|
||
definition is_trunc_iff_map_sphere_constant
|
||
(H : Π(f : S n → A) (x : S n), f x = f base) : is_trunc (n.-2.+1) A :=
|
||
begin
|
||
apply is_trunc_of_pmap_sphere_constant,
|
||
intros, cases f with f p, esimp at *, apply H
|
||
end
|
||
|
||
definition pmap_sphere_constant_of_is_trunc' [H : is_trunc (n.-2.+1) A]
|
||
(a : A) (f : map₊ (S. n) (pointed.Mk a)) (x : S n) : f x = f base :=
|
||
begin
|
||
let H' := iff.elim_left (is_trunc_iff_is_contr_loop n A) H a,
|
||
note H'' := @is_trunc_equiv_closed_rev _ _ _ !pmap_sphere H',
|
||
have p : (f = pmap.mk (λx, f base) (respect_pt f)),
|
||
by apply is_prop.elim,
|
||
exact ap10 (ap pmap.to_fun p) x
|
||
end
|
||
|
||
definition pmap_sphere_constant_of_is_trunc [H : is_trunc (n.-2.+1) A]
|
||
(a : A) (f : map₊ (S. n) (pointed.Mk a)) (x y : S n) : f x = f y :=
|
||
let H := pmap_sphere_constant_of_is_trunc' a f in !H ⬝ !H⁻¹
|
||
|
||
definition map_sphere_constant_of_is_trunc [H : is_trunc (n.-2.+1) A]
|
||
(f : S n → A) (x y : S n) : f x = f y :=
|
||
pmap_sphere_constant_of_is_trunc (f base) (pmap.mk f idp) x y
|
||
|
||
definition map_sphere_constant_of_is_trunc_self [H : is_trunc (n.-2.+1) A]
|
||
(f : S n → A) (x : S n) : map_sphere_constant_of_is_trunc f x x = idp :=
|
||
!con.right_inv
|
||
|
||
end is_trunc
|