From af4ba3d2fb9bc0c7475be759156f05519cc5488e Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Wed, 2 Mar 2016 16:23:24 -0500 Subject: [PATCH] feat(hott): prove that the (n+1)-sphere is n-connected --- hott/algebra/homotopy_group.hlean | 9 ++++ hott/homotopy/connectedness.hlean | 12 ++++- hott/homotopy/sphere.hlean | 75 +++++++++++++++++++------------ hott/types/trunc.hlean | 10 +++++ 4 files changed, 76 insertions(+), 30 deletions(-) diff --git a/hott/algebra/homotopy_group.hlean b/hott/algebra/homotopy_group.hlean index c386ce9f8c..8844ba18c0 100644 --- a/hott/algebra/homotopy_group.hlean +++ b/hott/algebra/homotopy_group.hlean @@ -49,6 +49,15 @@ namespace eq : π*[n] A ≃* π*[n] B := ptrunc_pequiv 0 (iterated_loop_space_pequiv n H) + set_option pp.coercions true + set_option pp.numerals false + definition phomotopy_group_pequiv_loop_ptrunc [constructor] (k : ℕ) (A : Type*) : + π*[k] A ≃* Ω[k] (ptrunc k A) := + begin + refine !iterated_loop_ptrunc_pequiv⁻¹ᵉ* ⬝e* _, + rewrite [trunc_index.zero_add] + end + open equiv unit theorem trivial_homotopy_of_is_set (A : Type*) [H : is_set A] (n : ℕ) : πg[n+1] A = G0 := begin diff --git a/hott/homotopy/connectedness.hlean b/hott/homotopy/connectedness.hlean index e14a84bb39..0cf9697a68 100644 --- a/hott/homotopy/connectedness.hlean +++ b/hott/homotopy/connectedness.hlean @@ -3,7 +3,7 @@ Copyright (c) 2015 Ulrik Buchholtz. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Ulrik Buchholtz, Floris van Doorn -/ -import types.trunc types.eq types.arrow_2 types.fiber .susp +import types.trunc types.arrow_2 .sphere open eq is_trunc is_equiv nat equiv trunc function fiber funext pi @@ -245,7 +245,7 @@ namespace homotopy -- Theorem 8.2.1 open susp - definition is_conn_susp [instance] (n : ℕ₋₂) (A : Type) + theorem is_conn_susp [instance] (n : ℕ₋₂) (A : Type) [H : is_conn n A] : is_conn (n .+1) (susp A) := is_contr.mk (tr north) begin @@ -274,4 +274,12 @@ namespace homotopy } end + open trunc_index + theorem is_conn_sphere [instance] (n : ℕ₋₁) : is_conn (n.-1) (sphere n) := + begin + induction n with n IH, + { apply is_trunc_trunc}, + { rewrite [succ_sub_one, sphere.sphere_succ], apply is_conn_susp} + end + end homotopy diff --git a/hott/homotopy/sphere.hlean b/hott/homotopy/sphere.hlean index a6a084a342..be051dfeb3 100644 --- a/hott/homotopy/sphere.hlean +++ b/hott/homotopy/sphere.hlean @@ -25,11 +25,7 @@ inductive sphere_index : Type₀ := | minus_one : sphere_index | succ : sphere_index → sphere_index -namespace trunc_index - definition sub_one [reducible] (n : sphere_index) : trunc_index := - sphere_index.rec_on n -2 (λ n k, k.+1) - postfix `.-1`:(max+1) := sub_one -end trunc_index +notation `ℕ₋₁` := sphere_index namespace sphere_index /- @@ -37,27 +33,26 @@ namespace sphere_index from 0 and up this comes from a coercion from num to sphere_index (via nat) -/ - definition has_zero_sphere_index [instance] : has_zero sphere_index := - has_zero.mk (succ minus_one) - - definition has_one_sphere_index [instance] : has_one sphere_index := - has_one.mk (succ (succ minus_one)) - postfix `.+1`:(max+1) := sphere_index.succ postfix `.+2`:(max+1) := λ(n : sphere_index), (n .+1 .+1) notation `-1` := minus_one - notation `ℕ₋₁` := sphere_index - definition add_plus_one (n m : sphere_index) : sphere_index := + 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) : sphere_index := + 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)) - protected definition le (n m : sphere_index) : Type₀ := + protected definition le (n m : ℕ₋₁) : Type₀ := sphere_index.rec_on n (λm, unit) (λ n p m, sphere_index.rec_on m (λ p, empty) (λ m q p, p m) p) m infix `+1+`:65 := sphere_index.add_plus_one @@ -65,34 +60,55 @@ namespace sphere_index 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 sphere_index := + definition has_le_sphere_index [instance] : has_le ℕ₋₁ := has_le.mk sphere_index.le - definition succ_le_succ {n m : sphere_index} (H : n ≤ m) : n.+1 ≤ m.+1 := proof H qed - definition le_of_succ_le_succ {n m : sphere_index} (H : n.+1 ≤ m.+1) : n ≤ m := proof H qed - definition minus_two_le (n : sphere_index) : -1 ≤ n := star - definition empty_of_succ_le_minus_two {n : sphere_index} (H : n .+1 ≤ -1) : empty := H + definition succ_le_succ {n m : ℕ₋₁} (H : n ≤ m) : n.+1 ≤ m.+1 := proof H qed + definition le_of_succ_le_succ {n m : ℕ₋₁} (H : n.+1 ≤ m.+1) : n ≤ m := proof H qed + definition minus_two_le (n : ℕ₋₁) : -1 ≤ n := star + definition empty_of_succ_le_minus_two {n : ℕ₋₁} (H : n .+1 ≤ -1) : empty := H - definition of_nat [coercion] [reducible] (n : nat) : sphere_index := + definition of_nat [coercion] [reducible] (n : nat) : ℕ₋₁ := (nat.rec_on n -1 (λ n k, k.+1)).+1 - definition trunc_index_of_sphere_index [coercion] [reducible] (n : sphere_index) : trunc_index := - (sphere_index.rec_on n -2 (λ n k, k.+1)).+1 - - definition sub_one [reducible] (n : ℕ) : sphere_index := + definition sub_one [reducible] (n : ℕ) : ℕ₋₁ := nat.rec_on n -1 (λ n k, k.+1) postfix `.-1`:(max+1) := sub_one - open trunc_index + definition succ_sub_one (n : ℕ) : (nat.succ n).-1 = n :> ℕ₋₁ := + idp + +end sphere_index +open 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 [coercion] [reducible] (n : ℕ₋₁) : ℕ₋₂ := + n.-1.+1 + definition sub_two_eq_sub_one_sub_one (n : ℕ) : n.-2 = n.-1.-1 := nat.rec_on n idp (λn p, ap trunc_index.succ p) -end sphere_index + 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) = trunc_index.of_nat n :> ℕ₋₂ := + begin + induction n with n IH, + { reflexivity}, + { exact ap trunc_index.succ IH} + end + +end trunc_index open sphere_index equiv -definition sphere : sphere_index → Type₀ +definition sphere : ℕ₋₁ → Type₀ | -1 := empty | n.+1 := susp (sphere n) @@ -109,6 +125,9 @@ namespace sphere end ops open sphere.ops + definition sphere_minus_one : S -1 = empty := idp + definition sphere_succ (n : ℕ₋₁) : S n.+1 = susp (S n) := idp + definition equator (n : ℕ) : map₊ (S. n) (Ω (S. (succ n))) := pmap.mk (λa, merid a ⬝ (merid base)⁻¹) !con.right_inv diff --git a/hott/types/trunc.hlean b/hott/types/trunc.hlean index 546d9d32bf..784c4bd237 100644 --- a/hott/types/trunc.hlean +++ b/hott/types/trunc.hlean @@ -77,6 +77,16 @@ namespace is_trunc /- more theorems about truncation indices -/ + definition zero_add (n : ℕ₋₂) : (0 : ℕ₋₂) + n = n := + begin + cases n with n, reflexivity, + cases n with n, reflexivity, + induction n with n IH, reflexivity, exact ap succ IH + end + + definition add_zero (n : ℕ₋₂) : n + (0 : ℕ₋₂) = n := + by reflexivity + definition succ_add_nat (n : ℕ₋₂) (m : ℕ) : n.+1 + m = (n + m).+1 := by induction m with m IH; reflexivity; exact ap succ IH