From 341a53b880c50f04ff896207950d9171b2423364 Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Thu, 22 Sep 2016 15:42:46 -0400 Subject: [PATCH] feat(pointed): make the naming in the pointed library more consistent. Also start on a naming conventions file --- hott/algebra/homotopy_group.hlean | 152 +++++----- hott/homotopy/EM.hlean | 4 +- hott/homotopy/LES_of_homotopy_groups.hlean | 316 ++++++++++----------- hott/homotopy/circle.hlean | 14 +- hott/homotopy/complex_hopf.hlean | 4 +- hott/homotopy/freudenthal.hlean | 22 +- hott/homotopy/homotopy_group.hlean | 58 ++-- hott/homotopy/sphere.hlean | 60 ++-- hott/homotopy/sphere2.hlean | 16 +- hott/homotopy/susp.hlean | 8 +- hott/naming_conventions.md | 14 + hott/types/pointed.hlean | 106 ++++--- hott/types/trunc.hlean | 32 +-- 13 files changed, 403 insertions(+), 403 deletions(-) create mode 100644 hott/naming_conventions.md diff --git a/hott/algebra/homotopy_group.hlean b/hott/algebra/homotopy_group.hlean index c35485594..b4f2e2b7b 100644 --- a/hott/algebra/homotopy_group.hlean +++ b/hott/algebra/homotopy_group.hlean @@ -13,21 +13,17 @@ open nat eq pointed trunc is_trunc algebra group function equiv unit is_equiv -- TODO: consistently make n an argument before A namespace eq - definition phomotopy_group [reducible] [constructor] (n : ℕ) (A : Type*) : Set* := + definition homotopy_group [reducible] [constructor] (n : ℕ) (A : Type*) : Set* := ptrunc 0 (Ω[n] A) - definition homotopy_group [reducible] (n : ℕ) (A : Type*) : Type := - phomotopy_group n A - - notation `π*[`:95 n:0 `]`:0 := phomotopy_group n - notation `π[`:95 n:0 `]`:0 := homotopy_group n + notation `π[`:95 n:0 `]`:0 := homotopy_group n definition group_homotopy_group [instance] [constructor] [reducible] (n : ℕ) (A : Type*) : group (π[succ n] A) := trunc_group concat inverse idp con.assoc idp_con con_idp con.left_inv definition group_homotopy_group2 [instance] (k : ℕ) (A : Type*) : - group (carrier (ptrunctype.to_pType (π*[k + 1] A))) := + group (carrier (ptrunctype.to_pType (π[k + 1] A))) := group_homotopy_group k A definition comm_group_homotopy_group [constructor] [reducible] (n : ℕ) (A : Type*) @@ -58,30 +54,30 @@ namespace eq : tr p *[π[succ n] A] tr q = tr (p ⬝ q) := idp - definition phomotopy_group_pequiv [constructor] (n : ℕ) {A B : Type*} (H : A ≃* B) - : π*[n] A ≃* π*[n] B := + definition homotopy_group_pequiv [constructor] (n : ℕ) {A B : Type*} (H : A ≃* B) + : π[n] A ≃* π[n] B := ptrunc_pequiv_ptrunc 0 (loopn_pequiv_loopn n H) - definition phomotopy_group_pequiv_loop_ptrunc [constructor] (k : ℕ) (A : Type*) : - π*[k] A ≃* Ω[k] (ptrunc k A) := + definition homotopy_group_pequiv_loop_ptrunc [constructor] (k : ℕ) (A : Type*) : + π[k] A ≃* Ω[k] (ptrunc k A) := begin - refine !iterated_loop_ptrunc_pequiv⁻¹ᵉ* ⬝e* _, + refine !loopn_ptrunc_pequiv⁻¹ᵉ* ⬝e* _, exact loopn_pequiv_loopn k (pequiv_of_eq begin rewrite [trunc_index.zero_add] end) end open trunc_index - definition phomotopy_group_ptrunc_of_le [constructor] {k n : ℕ} (H : k ≤ n) (A : Type*) : - π*[k] (ptrunc n A) ≃* π*[k] A := + definition homotopy_group_ptrunc_of_le [constructor] {k n : ℕ} (H : k ≤ n) (A : Type*) : + π[k] (ptrunc n A) ≃* π[k] A := calc - π*[k] (ptrunc n A) ≃* Ω[k] (ptrunc k (ptrunc n A)) - : phomotopy_group_pequiv_loop_ptrunc k (ptrunc n A) + π[k] (ptrunc n A) ≃* Ω[k] (ptrunc k (ptrunc n A)) + : homotopy_group_pequiv_loop_ptrunc k (ptrunc n A) ... ≃* Ω[k] (ptrunc k A) : loopn_pequiv_loopn k (ptrunc_ptrunc_pequiv_left A (of_nat_le_of_nat H)) - ... ≃* π*[k] A : (phomotopy_group_pequiv_loop_ptrunc k A)⁻¹ᵉ* + ... ≃* π[k] A : (homotopy_group_pequiv_loop_ptrunc k A)⁻¹ᵉ* - definition phomotopy_group_ptrunc [constructor] (k : ℕ) (A : Type*) : - π*[k] (ptrunc k A) ≃* π*[k] A := - phomotopy_group_ptrunc_of_le (le.refl k) A + definition homotopy_group_ptrunc [constructor] (k : ℕ) (A : Type*) : + π[k] (ptrunc k A) ≃* π[k] A := + homotopy_group_ptrunc_of_le (le.refl k) A theorem trivial_homotopy_of_is_set (A : Type*) [H : is_set A] (n : ℕ) : πg[n+1] A ≃g G0 := begin @@ -91,67 +87,63 @@ namespace eq apply is_trunc_succ_succ_of_is_set end - definition phomotopy_group_succ_out (A : Type*) (n : ℕ) : π*[n + 1] A = π₁ Ω[n] A := idp + definition homotopy_group_succ_out (A : Type*) (n : ℕ) : π[n + 1] A = π₁ (Ω[n] A) := idp - definition phomotopy_group_succ_in (A : Type*) (n : ℕ) : π*[n + 1] A ≃* π*[n] (Ω A) := - ptrunc_pequiv_ptrunc 0 (loop_space_succ_in A n) + definition homotopy_group_succ_in (A : Type*) (n : ℕ) : π[n + 1] A ≃* π[n] (Ω A) := + ptrunc_pequiv_ptrunc 0 (loopn_succ_in A n) - definition ghomotopy_group_succ_out (A : Type*) (n : ℕ) : πg[n +1] A = π₁ Ω[n] A := idp + definition ghomotopy_group_succ_out (A : Type*) (n : ℕ) : πg[n +1] A = π₁ (Ω[n] A) := idp - definition phomotopy_group_succ_in_con {A : Type*} {n : ℕ} (g h : πg[succ n +1] A) : - phomotopy_group_succ_in A (succ n) (g * h) = - phomotopy_group_succ_in A (succ n) g * phomotopy_group_succ_in A (succ n) h := + definition homotopy_group_succ_in_con {A : Type*} {n : ℕ} (g h : πg[succ n +1] A) : + homotopy_group_succ_in A (succ n) (g * h) = + homotopy_group_succ_in A (succ n) g * homotopy_group_succ_in A (succ n) h := begin induction g with p, induction h with q, esimp, - apply ap tr, apply loop_space_succ_in_con + apply ap tr, apply loopn_succ_in_con end definition ghomotopy_group_succ_in (A : Type*) (n : ℕ) : πg[succ n +1] A ≃g πg[n +1] (Ω A) := begin fapply isomorphism_of_equiv, - { exact phomotopy_group_succ_in A (succ n)}, - { exact phomotopy_group_succ_in_con}, + { exact homotopy_group_succ_in A (succ n)}, + { exact homotopy_group_succ_in_con}, end - definition phomotopy_group_functor [constructor] (n : ℕ) {A B : Type*} (f : A →* B) - : π*[n] A →* π*[n] B := + definition homotopy_group_functor [constructor] (n : ℕ) {A B : Type*} (f : A →* B) + : π[n] A →* π[n] B := ptrunc_functor 0 (apn n f) - definition homotopy_group_functor (n : ℕ) {A B : Type*} (f : A →* B) : π[n] A → π[n] B := - phomotopy_group_functor n f + notation `π→[`:95 n:0 `]`:0 := homotopy_group_functor n - notation `π→*[`:95 n:0 `]`:0 := phomotopy_group_functor n - notation `π→[`:95 n:0 `]`:0 := homotopy_group_functor n - - definition phomotopy_group_functor_phomotopy [constructor] (n : ℕ) {A B : Type*} {f g : A →* B} - (p : f ~* g) : π→*[n] f ~* π→*[n] g := + definition homotopy_group_functor_phomotopy [constructor] (n : ℕ) {A B : Type*} {f g : A →* B} + (p : f ~* g) : π→[n] f ~* π→[n] g := ptrunc_functor_phomotopy 0 (apn_phomotopy n p) - definition phomotopy_group_functor_compose [constructor] (n : ℕ) {A B C : Type*} (g : B →* C) - (f : A →* B) : π→*[n] (g ∘* f) ~* π→*[n] g ∘* π→*[n] f := - ptrunc_functor_phomotopy 0 !apn_compose ⬝* !ptrunc_functor_pcompose + definition homotopy_group_functor_compose [constructor] (n : ℕ) {A B C : Type*} (g : B →* C) + (f : A →* B) : π→[n] (g ∘* f) ~* π→[n] g ∘* π→[n] f := + ptrunc_functor_phomotopy 0 !apn_pcompose ⬝* !ptrunc_functor_pcompose definition is_equiv_homotopy_group_functor [constructor] (n : ℕ) {A B : Type*} (f : A →* B) [is_equiv f] : is_equiv (π→[n] f) := @(is_equiv_trunc_functor 0 _) !is_equiv_apn - definition phomotopy_group_functor_succ_phomotopy_in (n : ℕ) {A B : Type*} (f : A →* B) : - phomotopy_group_succ_in B n ∘* π→*[n + 1] f ~* - π→*[n] (Ω→ f) ∘* phomotopy_group_succ_in A n := + definition homotopy_group_functor_succ_phomotopy_in (n : ℕ) {A B : Type*} (f : A →* B) : + homotopy_group_succ_in B n ∘* π→[n + 1] f ~* + π→[n] (Ω→ f) ∘* homotopy_group_succ_in A n := begin refine !ptrunc_functor_pcompose⁻¹* ⬝* _ ⬝* !ptrunc_functor_pcompose, exact ptrunc_functor_phomotopy 0 (apn_succ_phomotopy_in n f) end - definition is_equiv_phomotopy_group_functor_ap1 (n : ℕ) {A B : Type*} (f : A →* B) - [is_equiv (π→*[n + 1] f)] : is_equiv (π→*[n] (Ω→ f)) := - have is_equiv (phomotopy_group_succ_in B n ∘* π→*[n + 1] f), - from is_equiv_compose _ (π→*[n + 1] f), - have is_equiv (π→*[n] (Ω→ f) ∘ phomotopy_group_succ_in A n), - from is_equiv.homotopy_closed _ (phomotopy_group_functor_succ_phomotopy_in n f), - is_equiv.cancel_right (phomotopy_group_succ_in A n) _ + definition is_equiv_homotopy_group_functor_ap1 (n : ℕ) {A B : Type*} (f : A →* B) + [is_equiv (π→[n + 1] f)] : is_equiv (π→[n] (Ω→ f)) := + have is_equiv (homotopy_group_succ_in B n ∘* π→[n + 1] f), + from is_equiv_compose _ (π→[n + 1] f), + have is_equiv (π→[n] (Ω→ f) ∘ homotopy_group_succ_in A n), + from is_equiv.homotopy_closed _ (homotopy_group_functor_succ_phomotopy_in n f), + is_equiv.cancel_right (homotopy_group_succ_in A n) _ - definition tinverse [constructor] {X : Type*} : π*[1] X →* π*[1] X := + definition tinverse [constructor] {X : Type*} : π[1] X →* π[1] X := ptrunc_functor 0 pinverse definition is_equiv_tinverse [constructor] (A : Type*) : is_equiv (@tinverse A) := @@ -165,7 +157,7 @@ namespace eq { reflexivity} end - definition phomotopy_group_functor_mul [constructor] (n : ℕ) {A B : Type*} (g : A →* B) + definition homotopy_group_functor_mul [constructor] (n : ℕ) {A B : Type*} (g : A →* B) (p q : πg[n+1] A) : (π→[n + 1] g) (p *[πg[n+1] A] q) = (π→[n + 1] g) p *[πg[n+1] B] (π→[n + 1] g) q := begin @@ -179,8 +171,8 @@ namespace eq : πg[n+1] A →g πg[n+1] B := begin fconstructor, - { exact phomotopy_group_functor (n+1) f}, - { apply phomotopy_group_functor_mul} + { exact homotopy_group_functor (n+1) f}, + { apply homotopy_group_functor_mul} end definition homotopy_group_isomorphism_of_pequiv [constructor] (n : ℕ) {A B : Type*} (f : A ≃* B) @@ -190,63 +182,63 @@ namespace eq esimp, apply is_equiv_trunc_functor, apply is_equiv_apn, end - definition homotopy_group_add (A : Type*) (n m : ℕ) : πg[n+m +1] A ≃g πg[n +1] Ω[m] A := + definition homotopy_group_add (A : Type*) (n m : ℕ) : πg[n+m +1] A ≃g πg[n +1] (Ω[m] A) := begin revert A, induction m with m IH: intro A, { reflexivity}, - { esimp [iterated_ploop_space, nat.add], refine !ghomotopy_group_succ_in ⬝g _, refine !IH ⬝g _, + { esimp [loopn, nat.add], refine !ghomotopy_group_succ_in ⬝g _, refine !IH ⬝g _, apply homotopy_group_isomorphism_of_pequiv, - exact !loop_space_succ_in⁻¹ᵉ*} + exact !loopn_succ_in⁻¹ᵉ*} end - theorem trivial_homotopy_add_of_is_set_loop_space {A : Type*} {n : ℕ} (m : ℕ) + theorem trivial_homotopy_add_of_is_set_loopn {A : Type*} {n : ℕ} (m : ℕ) (H : is_set (Ω[n] A)) : πg[m+n+1] A ≃g G0 := !homotopy_group_add ⬝g !trivial_homotopy_of_is_set - theorem trivial_homotopy_le_of_is_set_loop_space {A : Type*} {n : ℕ} (m : ℕ) (H1 : n ≤ m) + theorem trivial_homotopy_le_of_is_set_loopn {A : Type*} {n : ℕ} (m : ℕ) (H1 : n ≤ m) (H2 : is_set (Ω[n] A)) : πg[m+1] A ≃g G0 := obtain (k : ℕ) (p : n + k = m), from le.elim H1, isomorphism_of_eq (ap (λx, πg[x+1] A) (p⁻¹ ⬝ add.comm n k)) ⬝g - trivial_homotopy_add_of_is_set_loop_space k H2 + trivial_homotopy_add_of_is_set_loopn k H2 - definition phomotopy_group_pequiv_loop_ptrunc_con {k : ℕ} {A : Type*} (p q : πg[k +1] A) : - phomotopy_group_pequiv_loop_ptrunc (succ k) A (p * q) = - phomotopy_group_pequiv_loop_ptrunc (succ k) A p ⬝ - phomotopy_group_pequiv_loop_ptrunc (succ k) A q := + definition homotopy_group_pequiv_loop_ptrunc_con {k : ℕ} {A : Type*} (p q : πg[k +1] A) : + homotopy_group_pequiv_loop_ptrunc (succ k) A (p * q) = + homotopy_group_pequiv_loop_ptrunc (succ k) A p ⬝ + homotopy_group_pequiv_loop_ptrunc (succ k) A q := begin refine _ ⬝ !loopn_pequiv_loopn_con, - exact ap (loopn_pequiv_loopn _ _) !iterated_loop_ptrunc_pequiv_inv_con + exact ap (loopn_pequiv_loopn _ _) !loopn_ptrunc_pequiv_inv_con end - definition phomotopy_group_pequiv_loop_ptrunc_inv_con {k : ℕ} {A : Type*} + definition homotopy_group_pequiv_loop_ptrunc_inv_con {k : ℕ} {A : Type*} (p q : Ω[succ k] (ptrunc (succ k) A)) : - (phomotopy_group_pequiv_loop_ptrunc (succ k) A)⁻¹ᵉ* (p ⬝ q) = - (phomotopy_group_pequiv_loop_ptrunc (succ k) A)⁻¹ᵉ* p * - (phomotopy_group_pequiv_loop_ptrunc (succ k) A)⁻¹ᵉ* q := - inv_preserve_binary (phomotopy_group_pequiv_loop_ptrunc (succ k) A) mul concat - (@phomotopy_group_pequiv_loop_ptrunc_con k A) p q + (homotopy_group_pequiv_loop_ptrunc (succ k) A)⁻¹ᵉ* (p ⬝ q) = + (homotopy_group_pequiv_loop_ptrunc (succ k) A)⁻¹ᵉ* p * + (homotopy_group_pequiv_loop_ptrunc (succ k) A)⁻¹ᵉ* q := + inv_preserve_binary (homotopy_group_pequiv_loop_ptrunc (succ k) A) mul concat + (@homotopy_group_pequiv_loop_ptrunc_con k A) p q definition ghomotopy_group_ptrunc [constructor] (k : ℕ) (A : Type*) : πg[k+1] (ptrunc (k+1) A) ≃g πg[k+1] A := begin fapply isomorphism_of_equiv, - { exact phomotopy_group_ptrunc (k+1) A}, + { exact homotopy_group_ptrunc (k+1) A}, { intro g₁ g₂, esimp, - refine _ ⬝ !phomotopy_group_pequiv_loop_ptrunc_inv_con, - apply ap ((phomotopy_group_pequiv_loop_ptrunc (k+1) A)⁻¹ᵉ*), + refine _ ⬝ !homotopy_group_pequiv_loop_ptrunc_inv_con, + apply ap ((homotopy_group_pequiv_loop_ptrunc (k+1) A)⁻¹ᵉ*), refine _ ⬝ !loopn_pequiv_loopn_con , apply ap (loopn_pequiv_loopn (k+1) _), - apply phomotopy_group_pequiv_loop_ptrunc_con} + apply homotopy_group_pequiv_loop_ptrunc_con} end /- some homomorphisms -/ - -- definition is_homomorphism_cast_loop_space_succ_eq_in {A : Type*} (n : ℕ) : - -- is_homomorphism (loop_space_succ_in A (succ n) : πg[n+1+1] A → πg[n+1] (Ω A)) := + -- definition is_homomorphism_cast_loopn_succ_eq_in {A : Type*} (n : ℕ) : + -- is_homomorphism (loopn_succ_in A (succ n) : πg[n+1+1] A → πg[n+1] (Ω A)) := -- begin -- intro g h, induction g with g, induction h with h, -- xrewrite [tr_mul_tr, - + fn_cast_eq_cast_fn _ (λn, tr), tr_mul_tr, ↑cast, -tr_compose, - -- loop_space_succ_eq_in_concat, - + tr_compose], + -- loopn_succ_eq_in_concat, - + tr_compose], -- end definition is_homomorphism_inverse (A : Type*) (n : ℕ) diff --git a/hott/homotopy/EM.hlean b/hott/homotopy/EM.hlean index 638f96f16..d17c0a906 100644 --- a/hott/homotopy/EM.hlean +++ b/hott/homotopy/EM.hlean @@ -220,7 +220,7 @@ namespace EM end ops open ops - definition phomotopy_group_EM (n : ℕ) : π*[n] (EM G n) ≃* pType_of_Group G := + definition homotopy_group_EM (n : ℕ) : π[n] (EM G n) ≃* pType_of_Group G := begin cases n with n, { rexact ptrunc_pequiv 0 (pType_of_Group G) _}, @@ -318,7 +318,7 @@ namespace EM (pEM1_pequiv e)⁻¹ᵉ* ⬝e* pEM1_pequiv !isomorphism.refl open circle int - definition EM_pequiv_circle : K agℤ 1 ≃* S¹. := + definition EM_pequiv_circle : K agℤ 1 ≃* S¹* := !EMadd1_pequiv_pEM1 ⬝e* pEM1_pequiv fundamental_group_of_circle /- loops of EM-spaces -/ diff --git a/hott/homotopy/LES_of_homotopy_groups.hlean b/hott/homotopy/LES_of_homotopy_groups.hlean index 001855606..ad186b6ac 100644 --- a/hott/homotopy/LES_of_homotopy_groups.hlean +++ b/hott/homotopy/LES_of_homotopy_groups.hlean @@ -264,26 +264,26 @@ namespace chain_complex /- Now we are ready to define the long exact sequence of homotopy groups. First we define its carrier -/ - definition loop_spaces : ℕ → Type* + definition loopns : ℕ → Type* | 0 := Y | 1 := X | 2 := pfiber f - | (k+3) := Ω (loop_spaces k) + | (k+3) := Ω (loopns k) /- The maps between the homotopy groups -/ - definition loop_spaces_fun - : Π(n : ℕ), loop_spaces (n+1) →* loop_spaces n + definition loopns_fun + : Π(n : ℕ), loopns (n+1) →* loopns n | 0 := proof f qed | 1 := proof ppoint f qed | 2 := proof boundary_map qed - | (k+3) := proof ap1 (loop_spaces_fun k) qed + | (k+3) := proof ap1 (loopns_fun k) qed - definition loop_spaces_fun_add3 [unfold_full] (n : ℕ) : - loop_spaces_fun (n + 3) = ap1 (loop_spaces_fun n) := + definition loopns_fun_add3 [unfold_full] (n : ℕ) : + loopns_fun (n + 3) = ap1 (loopns_fun n) := proof idp qed - definition fiber_sequence_pequiv_loop_spaces : - Πn, fiber_sequence_carrier n ≃* loop_spaces n + definition fiber_sequence_pequiv_loopns : + Πn, fiber_sequence_carrier n ≃* loopns n | 0 := by reflexivity | 1 := by reflexivity | 2 := by reflexivity @@ -291,22 +291,22 @@ namespace chain_complex begin refine fiber_sequence_carrier_pequiv k ⬝e* _, apply loop_pequiv_loop, - exact fiber_sequence_pequiv_loop_spaces k + exact fiber_sequence_pequiv_loopns k end - definition fiber_sequence_pequiv_loop_spaces_add3 (n : ℕ) - : fiber_sequence_pequiv_loop_spaces (n + 3) = - ap1 (fiber_sequence_pequiv_loop_spaces n) ∘* fiber_sequence_carrier_pequiv n := + definition fiber_sequence_pequiv_loopns_add3 (n : ℕ) + : fiber_sequence_pequiv_loopns (n + 3) = + ap1 (fiber_sequence_pequiv_loopns n) ∘* fiber_sequence_carrier_pequiv n := by reflexivity - definition fiber_sequence_pequiv_loop_spaces_3_phomotopy - : fiber_sequence_pequiv_loop_spaces 3 ~* proof fiber_sequence_carrier_pequiv nat.zero qed := + definition fiber_sequence_pequiv_loopns_3_phomotopy + : fiber_sequence_pequiv_loopns 3 ~* proof fiber_sequence_carrier_pequiv nat.zero qed := begin - refine pwhisker_right _ ap1_id ⬝* _, - apply pid_comp + refine pwhisker_right _ ap1_pid ⬝* _, + apply pid_pcompose end - definition pid_or_pinverse : Π(n : ℕ), loop_spaces n ≃* loop_spaces n + definition pid_or_pinverse : Π(n : ℕ), loopns n ≃* loopns n | 0 := pequiv.rfl | 1 := pequiv.rfl | 2 := pequiv.rfl @@ -321,69 +321,69 @@ namespace chain_complex pid_or_pinverse (n + 4) ~* pinverse ∘* Ω→(pid_or_pinverse (n + 1)) | 0 := begin rewrite [pid_or_pinverse_add4, + to_pmap_pequiv_trans], replace pid_or_pinverse (0 + 1) with pequiv.refl X, - rewrite [loop_pequiv_loop_rfl, ▸*], refine !pid_comp ⬝* _, - exact !comp_pid⁻¹* ⬝* pwhisker_left _ !ap1_id⁻¹* end + rewrite [loop_pequiv_loop_rfl, ▸*], refine !pid_pcompose ⬝* _, + exact !pcompose_pid⁻¹* ⬝* pwhisker_left _ !ap1_pid⁻¹* end | 1 := begin rewrite [pid_or_pinverse_add4, + to_pmap_pequiv_trans], replace pid_or_pinverse (1 + 1) with pequiv.refl (pfiber f), - rewrite [loop_pequiv_loop_rfl, ▸*], refine !pid_comp ⬝* _, - exact !comp_pid⁻¹* ⬝* pwhisker_left _ !ap1_id⁻¹* end + rewrite [loop_pequiv_loop_rfl, ▸*], refine !pid_pcompose ⬝* _, + exact !pcompose_pid⁻¹* ⬝* pwhisker_left _ !ap1_pid⁻¹* end | 2 := begin rewrite [pid_or_pinverse_add4, + to_pmap_pequiv_trans], replace pid_or_pinverse (2 + 1) with pequiv.refl (Ω Y), - rewrite [loop_pequiv_loop_rfl, ▸*], refine !pid_comp ⬝* _, - exact !comp_pid⁻¹* ⬝* pwhisker_left _ !ap1_id⁻¹* end + rewrite [loop_pequiv_loop_rfl, ▸*], refine !pid_pcompose ⬝* _, + exact !pcompose_pid⁻¹* ⬝* pwhisker_left _ !ap1_pid⁻¹* end | (k+3) := begin replace (k + 3 + 1) with (k + 4), rewrite [+ pid_or_pinverse_add4, + to_pmap_pequiv_trans], - refine _ ⬝* pwhisker_left _ !ap1_compose⁻¹*, + refine _ ⬝* pwhisker_left _ !ap1_pcompose⁻¹*, refine _ ⬝* !passoc, apply pconcat2, { refine ap1_phomotopy (pid_or_pinverse_add4_rev k) ⬝* _, - refine !ap1_compose ⬝* _, apply pwhisker_right, apply ap1_pinverse}, + refine !ap1_pcompose ⬝* _, apply pwhisker_right, apply ap1_pinverse}, { refine !ap1_pinverse⁻¹*} end - theorem fiber_sequence_phomotopy_loop_spaces : Π(n : ℕ), - fiber_sequence_pequiv_loop_spaces n ∘* fiber_sequence_fun n ~* - (loop_spaces_fun n ∘* pid_or_pinverse (n + 1)) ∘* fiber_sequence_pequiv_loop_spaces (n + 1) - | 0 := proof proof phomotopy.rfl qed ⬝* pwhisker_right _ !comp_pid⁻¹* qed + theorem fiber_sequence_phomotopy_loopns : Π(n : ℕ), + fiber_sequence_pequiv_loopns n ∘* fiber_sequence_fun n ~* + (loopns_fun n ∘* pid_or_pinverse (n + 1)) ∘* fiber_sequence_pequiv_loopns (n + 1) + | 0 := proof proof phomotopy.rfl qed ⬝* pwhisker_right _ !pcompose_pid⁻¹* qed | 1 := by reflexivity | 2 := begin - refine !pid_comp ⬝* _, - replace loop_spaces_fun 2 with boundary_map, - refine _ ⬝* pwhisker_left _ fiber_sequence_pequiv_loop_spaces_3_phomotopy⁻¹*, + refine !pid_pcompose ⬝* _, + replace loopns_fun 2 with boundary_map, + refine _ ⬝* pwhisker_left _ fiber_sequence_pequiv_loopns_3_phomotopy⁻¹*, apply phomotopy_of_pinv_right_phomotopy, - exact !pid_comp⁻¹* + exact !pid_pcompose⁻¹* end | (k+3) := begin replace (k + 3 + 1) with (k + 1 + 3), - rewrite [fiber_sequence_pequiv_loop_spaces_add3 k, - fiber_sequence_pequiv_loop_spaces_add3 (k+1)], + rewrite [fiber_sequence_pequiv_loopns_add3 k, + fiber_sequence_pequiv_loopns_add3 (k+1)], refine !passoc ⬝* _, refine pwhisker_left _ (fiber_sequence_fun_phomotopy k) ⬝* _, refine !passoc⁻¹* ⬝* _ ⬝* !passoc, apply pwhisker_right, replace (k + 1 + 3) with (k + 4), - xrewrite [loop_spaces_fun_add3, pid_or_pinverse_add4, to_pmap_pequiv_trans], + xrewrite [loopns_fun_add3, pid_or_pinverse_add4, to_pmap_pequiv_trans], refine _ ⬝* !passoc⁻¹*, refine _ ⬝* pwhisker_left _ !passoc⁻¹*, - refine _ ⬝* pwhisker_left _ (pwhisker_left _ !ap1_compose_pinverse), + refine _ ⬝* pwhisker_left _ (pwhisker_left _ !ap1_pcompose_pinverse), refine !passoc⁻¹* ⬝* _ ⬝* !passoc ⬝* !passoc, apply pwhisker_right, - refine !ap1_compose⁻¹* ⬝* _ ⬝* !ap1_compose ⬝* pwhisker_right _ !ap1_compose, + refine !ap1_pcompose⁻¹* ⬝* _ ⬝* !ap1_pcompose ⬝* pwhisker_right _ !ap1_pcompose, apply ap1_phomotopy, - exact fiber_sequence_phomotopy_loop_spaces k + exact fiber_sequence_phomotopy_loopns k end - definition pid_or_pinverse_right : Π(n : ℕ), loop_spaces n →* loop_spaces n + definition pid_or_pinverse_right : Π(n : ℕ), loopns n →* loopns n | 0 := !pid | 1 := !pid | 2 := !pid | (k+3) := Ω→(pid_or_pinverse_right k) ∘* pinverse - definition pid_or_pinverse_left : Π(n : ℕ), loop_spaces n →* loop_spaces n + definition pid_or_pinverse_left : Π(n : ℕ), loopns n →* loopns n | 0 := pequiv.rfl | 1 := pequiv.rfl | 2 := pequiv.rfl @@ -400,63 +400,63 @@ namespace chain_complex by reflexivity theorem pid_or_pinverse_commute_right : Π(n : ℕ), - loop_spaces_fun n ~* pid_or_pinverse_right n ∘* loop_spaces_fun n ∘* pid_or_pinverse (n + 1) - | 0 := proof !comp_pid⁻¹* ⬝* !pid_comp⁻¹* qed - | 1 := proof !comp_pid⁻¹* ⬝* !pid_comp⁻¹* qed - | 2 := proof !comp_pid⁻¹* ⬝* !pid_comp⁻¹* qed + loopns_fun n ~* pid_or_pinverse_right n ∘* loopns_fun n ∘* pid_or_pinverse (n + 1) + | 0 := proof !pcompose_pid⁻¹* ⬝* !pid_pcompose⁻¹* qed + | 1 := proof !pcompose_pid⁻¹* ⬝* !pid_pcompose⁻¹* qed + | 2 := proof !pcompose_pid⁻¹* ⬝* !pid_pcompose⁻¹* qed | (k+3) := begin replace (k + 3 + 1) with (k + 4), - rewrite [pid_or_pinverse_right_add3, loop_spaces_fun_add3], + rewrite [pid_or_pinverse_right_add3, loopns_fun_add3], refine _ ⬝* pwhisker_left _ (pwhisker_left _ !pid_or_pinverse_add4_rev⁻¹*), refine ap1_phomotopy (pid_or_pinverse_commute_right k) ⬝* _, - refine !ap1_compose ⬝* _ ⬝* !passoc⁻¹*, + refine !ap1_pcompose ⬝* _ ⬝* !passoc⁻¹*, apply pwhisker_left, - refine !ap1_compose ⬝* _ ⬝* !passoc ⬝* !passoc, + refine !ap1_pcompose ⬝* _ ⬝* !passoc ⬝* !passoc, apply pwhisker_right, - refine _ ⬝* pwhisker_right _ !ap1_compose_pinverse, + refine _ ⬝* pwhisker_right _ !ap1_pcompose_pinverse, refine _ ⬝* !passoc⁻¹*, - refine !comp_pid⁻¹* ⬝* pwhisker_left _ _, + refine !pcompose_pid⁻¹* ⬝* pwhisker_left _ _, symmetry, apply pinverse_pinverse end theorem pid_or_pinverse_commute_left : Π(n : ℕ), - loop_spaces_fun n ∘* pid_or_pinverse_left (n + 1) ~* pid_or_pinverse n ∘* loop_spaces_fun n - | 0 := proof !comp_pid ⬝* !pid_comp⁻¹* qed - | 1 := proof !comp_pid ⬝* !pid_comp⁻¹* qed - | 2 := proof !comp_pid ⬝* !pid_comp⁻¹* qed - | 3 := proof !comp_pid ⬝* !pid_comp⁻¹* qed + loopns_fun n ∘* pid_or_pinverse_left (n + 1) ~* pid_or_pinverse n ∘* loopns_fun n + | 0 := proof !pcompose_pid ⬝* !pid_pcompose⁻¹* qed + | 1 := proof !pcompose_pid ⬝* !pid_pcompose⁻¹* qed + | 2 := proof !pcompose_pid ⬝* !pid_pcompose⁻¹* qed + | 3 := proof !pcompose_pid ⬝* !pid_pcompose⁻¹* qed | (k+4) := begin replace (k + 4 + 1) with (k + 5), rewrite [pid_or_pinverse_left_add5, pid_or_pinverse_add4, to_pmap_pequiv_trans], replace (k + 4) with (k + 1 + 3), - rewrite [loop_spaces_fun_add3], + rewrite [loopns_fun_add3], refine !passoc⁻¹* ⬝* _ ⬝* !passoc⁻¹*, - refine _ ⬝* pwhisker_left _ !ap1_compose_pinverse, + refine _ ⬝* pwhisker_left _ !ap1_pcompose_pinverse, refine _ ⬝* !passoc, apply pwhisker_right, - refine !ap1_compose⁻¹* ⬝* _ ⬝* !ap1_compose, + refine !ap1_pcompose⁻¹* ⬝* _ ⬝* !ap1_pcompose, exact ap1_phomotopy (pid_or_pinverse_commute_left (k+1)) end - definition LES_of_loop_spaces' [constructor] : type_chain_complex +ℕ := + definition LES_of_loopns' [constructor] : type_chain_complex +ℕ := transfer_type_chain_complex fiber_sequence - (λn, loop_spaces_fun n ∘* pid_or_pinverse (n + 1)) - fiber_sequence_pequiv_loop_spaces - fiber_sequence_phomotopy_loop_spaces + (λn, loopns_fun n ∘* pid_or_pinverse (n + 1)) + fiber_sequence_pequiv_loopns + fiber_sequence_phomotopy_loopns - definition LES_of_loop_spaces [constructor] : type_chain_complex +ℕ := + definition LES_of_loopns [constructor] : type_chain_complex +ℕ := type_chain_complex_cancel_aut - LES_of_loop_spaces' - loop_spaces_fun + LES_of_loopns' + loopns_fun pid_or_pinverse pid_or_pinverse_right (λn x, idp) pid_or_pinverse_commute_right - definition is_exact_LES_of_loop_spaces : is_exact_t LES_of_loop_spaces := + definition is_exact_LES_of_loopns : is_exact_t LES_of_loopns := begin intro n, refine is_exact_at_t_cancel_aut n pid_or_pinverse_left _ _ pid_or_pinverse_commute_left _, @@ -470,38 +470,38 @@ namespace chain_complex PART 3 --------------/ - definition loop_spaces2 [reducible] : +3ℕ → Type* + definition loopns2 [reducible] : +3ℕ → Type* | (n, fin.mk 0 H) := Ω[n] Y | (n, fin.mk 1 H) := Ω[n] X | (n, fin.mk k H) := Ω[n] (pfiber f) - definition loop_spaces2_add1 (n : ℕ) : Π(x : fin 3), - loop_spaces2 (n+1, x) = Ω (loop_spaces2 (n, x)) + definition loopns2_add1 (n : ℕ) : Π(x : fin 3), + loopns2 (n+1, x) = Ω (loopns2 (n, x)) | (fin.mk 0 H) := by reflexivity | (fin.mk 1 H) := by reflexivity | (fin.mk 2 H) := by reflexivity | (fin.mk (k+3) H) := begin exfalso, apply lt_le_antisymm H, apply le_add_left end - definition loop_spaces_fun2 : Π(n : +3ℕ), loop_spaces2 (S n) →* loop_spaces2 n + definition loopns_fun2 : Π(n : +3ℕ), loopns2 (S n) →* loopns2 n | (n, fin.mk 0 H) := proof Ω→[n] f qed | (n, fin.mk 1 H) := proof Ω→[n] (ppoint f) qed - | (n, fin.mk 2 H) := proof Ω→[n] boundary_map ∘* loop_space_succ_in Y n qed + | (n, fin.mk 2 H) := proof Ω→[n] boundary_map ∘* loopn_succ_in Y n qed | (n, fin.mk (k+3) H) := begin exfalso, apply lt_le_antisymm H, apply le_add_left end - definition loop_spaces_fun2_add1_0 (n : ℕ) (H : 0 < succ 2) - : loop_spaces_fun2 (n+1, fin.mk 0 H) ~* - cast proof idp qed ap1 (loop_spaces_fun2 (n, fin.mk 0 H)) := + definition loopns_fun2_add1_0 (n : ℕ) (H : 0 < succ 2) + : loopns_fun2 (n+1, fin.mk 0 H) ~* + cast proof idp qed ap1 (loopns_fun2 (n, fin.mk 0 H)) := by reflexivity - definition loop_spaces_fun2_add1_1 (n : ℕ) (H : 1 < succ 2) - : loop_spaces_fun2 (n+1, fin.mk 1 H) ~* - cast proof idp qed ap1 (loop_spaces_fun2 (n, fin.mk 1 H)) := + definition loopns_fun2_add1_1 (n : ℕ) (H : 1 < succ 2) + : loopns_fun2 (n+1, fin.mk 1 H) ~* + cast proof idp qed ap1 (loopns_fun2 (n, fin.mk 1 H)) := by reflexivity - definition loop_spaces_fun2_add1_2 (n : ℕ) (H : 2 < succ 2) - : loop_spaces_fun2 (n+1, fin.mk 2 H) ~* - cast proof idp qed ap1 (loop_spaces_fun2 (n, fin.mk 2 H)) := - proof !ap1_compose⁻¹* qed + definition loopns_fun2_add1_2 (n : ℕ) (H : 2 < succ 2) + : loopns_fun2 (n+1, fin.mk 2 H) ~* + cast proof idp qed ap1 (loopns_fun2 (n, fin.mk 2 H)) := + proof !ap1_pcompose⁻¹* qed definition nat_of_str [unfold 2] [reducible] {n : ℕ} : ℕ × fin (succ n) → ℕ := λx, succ n * pr1 x + val (pr2 x) @@ -537,126 +537,126 @@ namespace chain_complex note: in the following theorem the (n+1) case is 3 times the same, so maybe this can be simplified -/ - definition loop_spaces2_pequiv' : Π(n : ℕ) (x : fin (nat.succ 2)), - loop_spaces (nat_of_str (n, x)) ≃* loop_spaces2 (n, x) + definition loopns2_pequiv' : Π(n : ℕ) (x : fin (nat.succ 2)), + loopns (nat_of_str (n, x)) ≃* loopns2 (n, x) | 0 (fin.mk 0 H) := by reflexivity | 0 (fin.mk 1 H) := by reflexivity | 0 (fin.mk 2 H) := by reflexivity | (n+1) (fin.mk 0 H) := begin apply loop_pequiv_loop, - rexact loop_spaces2_pequiv' n (fin.mk 0 H) + rexact loopns2_pequiv' n (fin.mk 0 H) end | (n+1) (fin.mk 1 H) := begin apply loop_pequiv_loop, - rexact loop_spaces2_pequiv' n (fin.mk 1 H) + rexact loopns2_pequiv' n (fin.mk 1 H) end | (n+1) (fin.mk 2 H) := begin apply loop_pequiv_loop, - rexact loop_spaces2_pequiv' n (fin.mk 2 H) + rexact loopns2_pequiv' n (fin.mk 2 H) end | n (fin.mk (k+3) H) := begin exfalso, apply lt_le_antisymm H, apply le_add_left end - definition loop_spaces2_pequiv : Π(x : +3ℕ), - loop_spaces (nat_of_str x) ≃* loop_spaces2 x - | (n, x) := loop_spaces2_pequiv' n x + definition loopns2_pequiv : Π(x : +3ℕ), + loopns (nat_of_str x) ≃* loopns2 x + | (n, x) := loopns2_pequiv' n x local attribute loop_pequiv_loop [reducible] /- all cases where n>0 are basically the same -/ - definition loop_spaces_fun2_phomotopy (x : +3ℕ) : - loop_spaces2_pequiv x ∘* loop_spaces_fun (nat_of_str x) ~* - (loop_spaces_fun2 x ∘* loop_spaces2_pequiv (S x)) - ∘* pcast (ap (loop_spaces) (nat_of_str_3S x)) := + definition loopns_fun2_phomotopy (x : +3ℕ) : + loopns2_pequiv x ∘* loopns_fun (nat_of_str x) ~* + (loopns_fun2 x ∘* loopns2_pequiv (S x)) + ∘* pcast (ap (loopns) (nat_of_str_3S x)) := begin cases x with n x, cases x with k H, do 3 (cases k with k; rotate 1), { /-k≥3-/ exfalso, apply lt_le_antisymm H, apply le_add_left}, { /-k=0-/ induction n with n IH, - { refine !pid_comp ⬝* _ ⬝* !comp_pid⁻¹* ⬝* !comp_pid⁻¹*, + { refine !pid_pcompose ⬝* _ ⬝* !pcompose_pid⁻¹* ⬝* !pcompose_pid⁻¹*, reflexivity}, - { refine _ ⬝* !comp_pid⁻¹*, - refine _ ⬝* pwhisker_right _ !loop_spaces_fun2_add1_0⁻¹*, - refine !ap1_compose⁻¹* ⬝* _ ⬝* !ap1_compose, apply ap1_phomotopy, - exact IH ⬝* !comp_pid}}, + { refine _ ⬝* !pcompose_pid⁻¹*, + refine _ ⬝* pwhisker_right _ !loopns_fun2_add1_0⁻¹*, + refine !ap1_pcompose⁻¹* ⬝* _ ⬝* !ap1_pcompose, apply ap1_phomotopy, + exact IH ⬝* !pcompose_pid}}, { /-k=1-/ induction n with n IH, - { refine !pid_comp ⬝* _ ⬝* !comp_pid⁻¹* ⬝* !comp_pid⁻¹*, + { refine !pid_pcompose ⬝* _ ⬝* !pcompose_pid⁻¹* ⬝* !pcompose_pid⁻¹*, reflexivity}, - { refine _ ⬝* !comp_pid⁻¹*, - refine _ ⬝* pwhisker_right _ !loop_spaces_fun2_add1_1⁻¹*, - refine !ap1_compose⁻¹* ⬝* _ ⬝* !ap1_compose, apply ap1_phomotopy, - exact IH ⬝* !comp_pid}}, + { refine _ ⬝* !pcompose_pid⁻¹*, + refine _ ⬝* pwhisker_right _ !loopns_fun2_add1_1⁻¹*, + refine !ap1_pcompose⁻¹* ⬝* _ ⬝* !ap1_pcompose, apply ap1_phomotopy, + exact IH ⬝* !pcompose_pid}}, { /-k=2-/ induction n with n IH, - { refine !pid_comp ⬝* _ ⬝* !comp_pid⁻¹*, - refine !comp_pid⁻¹* ⬝* pconcat2 _ _, - { exact (comp_pid (chain_complex.boundary_map f))⁻¹*}, + { refine !pid_pcompose ⬝* _ ⬝* !pcompose_pid⁻¹*, + refine !pcompose_pid⁻¹* ⬝* pconcat2 _ _, + { exact (pcompose_pid (chain_complex.boundary_map f))⁻¹*}, { refine cast (ap (λx, _ ~* x) !loop_pequiv_loop_rfl)⁻¹ _, reflexivity}}, - { refine _ ⬝* !comp_pid⁻¹*, - refine _ ⬝* pwhisker_right _ !loop_spaces_fun2_add1_2⁻¹*, - refine !ap1_compose⁻¹* ⬝* _ ⬝* !ap1_compose, apply ap1_phomotopy, - exact IH ⬝* !comp_pid}}, + { refine _ ⬝* !pcompose_pid⁻¹*, + refine _ ⬝* pwhisker_right _ !loopns_fun2_add1_2⁻¹*, + refine !ap1_pcompose⁻¹* ⬝* _ ⬝* !ap1_pcompose, apply ap1_phomotopy, + exact IH ⬝* !pcompose_pid}}, end - definition LES_of_loop_spaces2 [constructor] : type_chain_complex +3ℕ := + definition LES_of_loopns2 [constructor] : type_chain_complex +3ℕ := transfer_type_chain_complex2 - LES_of_loop_spaces + LES_of_loopns !fin_prod_nat_equiv_nat nat_of_str_3S - @loop_spaces_fun2 - @loop_spaces2_pequiv + @loopns_fun2 + @loopns2_pequiv begin intro m x, - refine loop_spaces_fun2_phomotopy m x ⬝ _, - apply ap (loop_spaces_fun2 m), apply ap (loop_spaces2_pequiv (S m)), + refine loopns_fun2_phomotopy m x ⬝ _, + apply ap (loopns_fun2 m), apply ap (loopns2_pequiv (S m)), esimp, exact ap010 cast !ap_compose⁻¹ x end - definition is_exact_LES_of_loop_spaces2 : is_exact_t LES_of_loop_spaces2 := + definition is_exact_LES_of_loopns2 : is_exact_t LES_of_loopns2 := begin intro n, apply is_exact_at_t_transfer2, - apply is_exact_LES_of_loop_spaces + apply is_exact_LES_of_loopns end definition LES_of_homotopy_groups' [constructor] : chain_complex +3ℕ := - trunc_chain_complex LES_of_loop_spaces2 + trunc_chain_complex LES_of_loopns2 /-------------- PART 4 --------------/ definition homotopy_groups [reducible] : +3ℕ → Set* - | (n, fin.mk 0 H) := π*[n] Y - | (n, fin.mk 1 H) := π*[n] X - | (n, fin.mk k H) := π*[n] (pfiber f) + | (n, fin.mk 0 H) := π[n] Y + | (n, fin.mk 1 H) := π[n] X + | (n, fin.mk k H) := π[n] (pfiber f) - definition homotopy_groups_pequiv_loop_spaces2 [reducible] - : Π(n : +3ℕ), ptrunc 0 (loop_spaces2 n) ≃* homotopy_groups n + definition homotopy_groups_pequiv_loopns2 [reducible] + : Π(n : +3ℕ), ptrunc 0 (loopns2 n) ≃* homotopy_groups n | (n, fin.mk 0 H) := by reflexivity | (n, fin.mk 1 H) := by reflexivity | (n, fin.mk 2 H) := by reflexivity | (n, fin.mk (k+3) H) := begin exfalso, apply lt_le_antisymm H, apply le_add_left end definition homotopy_groups_fun : Π(n : +3ℕ), homotopy_groups (S n) →* homotopy_groups n - | (n, fin.mk 0 H) := proof π→*[n] f qed - | (n, fin.mk 1 H) := proof π→*[n] (ppoint f) qed + | (n, fin.mk 0 H) := proof π→[n] f qed + | (n, fin.mk 1 H) := proof π→[n] (ppoint f) qed | (n, fin.mk 2 H) := - proof π→*[n] boundary_map ∘* phomotopy_group_succ_in Y n qed + proof π→[n] boundary_map ∘* homotopy_group_succ_in Y n qed | (n, fin.mk (k+3) H) := begin exfalso, apply lt_le_antisymm H, apply le_add_left end - definition homotopy_groups_fun_phomotopy_loop_spaces_fun2 [reducible] - : Π(n : +3ℕ), homotopy_groups_pequiv_loop_spaces2 n ∘* ptrunc_functor 0 (loop_spaces_fun2 n) ~* - homotopy_groups_fun n ∘* homotopy_groups_pequiv_loop_spaces2 (S n) + definition homotopy_groups_fun_phomotopy_loopns_fun2 [reducible] + : Π(n : +3ℕ), homotopy_groups_pequiv_loopns2 n ∘* ptrunc_functor 0 (loopns_fun2 n) ~* + homotopy_groups_fun n ∘* homotopy_groups_pequiv_loopns2 (S n) | (n, fin.mk 0 H) := by reflexivity | (n, fin.mk 1 H) := by reflexivity | (n, fin.mk 2 H) := begin - refine !pid_comp ⬝* _ ⬝* !comp_pid⁻¹*, + refine !pid_pcompose ⬝* _ ⬝* !pcompose_pid⁻¹*, refine !ptrunc_functor_pcompose end | (n, fin.mk (k+3) H) := begin exfalso, apply lt_le_antisymm H, apply le_add_left end @@ -665,32 +665,32 @@ namespace chain_complex transfer_chain_complex LES_of_homotopy_groups' homotopy_groups_fun - homotopy_groups_pequiv_loop_spaces2 - homotopy_groups_fun_phomotopy_loop_spaces_fun2 + homotopy_groups_pequiv_loopns2 + homotopy_groups_fun_phomotopy_loopns_fun2 definition is_exact_LES_of_homotopy_groups : is_exact LES_of_homotopy_groups := begin intro n, apply is_exact_at_transfer, apply is_exact_at_trunc, - apply is_exact_LES_of_loop_spaces2 + apply is_exact_LES_of_loopns2 end variable (n : ℕ) /- the carrier of the fiber sequence is definitionally what we want (as pointed sets) -/ - example : LES_of_homotopy_groups (str_of_nat 6) = π*[2] Y :> Set* := by reflexivity - example : LES_of_homotopy_groups (str_of_nat 7) = π*[2] X :> Set* := by reflexivity - example : LES_of_homotopy_groups (str_of_nat 8) = π*[2] (pfiber f) :> Set* := by reflexivity - example : LES_of_homotopy_groups (str_of_nat 9) = π*[3] Y :> Set* := by reflexivity - example : LES_of_homotopy_groups (str_of_nat 10) = π*[3] X :> Set* := by reflexivity - example : LES_of_homotopy_groups (str_of_nat 11) = π*[3] (pfiber f) :> Set* := by reflexivity + example : LES_of_homotopy_groups (str_of_nat 6) = π[2] Y :> Set* := by reflexivity + example : LES_of_homotopy_groups (str_of_nat 7) = π[2] X :> Set* := by reflexivity + example : LES_of_homotopy_groups (str_of_nat 8) = π[2] (pfiber f) :> Set* := by reflexivity + example : LES_of_homotopy_groups (str_of_nat 9) = π[3] Y :> Set* := by reflexivity + example : LES_of_homotopy_groups (str_of_nat 10) = π[3] X :> Set* := by reflexivity + example : LES_of_homotopy_groups (str_of_nat 11) = π[3] (pfiber f) :> Set* := by reflexivity - definition LES_of_homotopy_groups_0 : LES_of_homotopy_groups (n, 0) = π*[n] Y := + definition LES_of_homotopy_groups_0 : LES_of_homotopy_groups (n, 0) = π[n] Y := by reflexivity - definition LES_of_homotopy_groups_1 : LES_of_homotopy_groups (n, 1) = π*[n] X := + definition LES_of_homotopy_groups_1 : LES_of_homotopy_groups (n, 1) = π[n] X := by reflexivity - definition LES_of_homotopy_groups_2 : LES_of_homotopy_groups (n, 2) = π*[n] (pfiber f) := + definition LES_of_homotopy_groups_2 : LES_of_homotopy_groups (n, 2) = π[n] (pfiber f) := by reflexivity /- @@ -698,13 +698,13 @@ namespace chain_complex -/ definition LES_of_homotopy_groups_fun_0 : - cc_to_fn LES_of_homotopy_groups (n, 0) = π→*[n] f := + cc_to_fn LES_of_homotopy_groups (n, 0) = π→[n] f := by reflexivity definition LES_of_homotopy_groups_fun_1 : - cc_to_fn LES_of_homotopy_groups (n, 1) = π→*[n] (ppoint f) := + cc_to_fn LES_of_homotopy_groups (n, 1) = π→[n] (ppoint f) := by reflexivity definition LES_of_homotopy_groups_fun_2 : cc_to_fn LES_of_homotopy_groups (n, 2) = - π→*[n] boundary_map ∘* phomotopy_group_succ_in Y n := + π→[n] boundary_map ∘* homotopy_group_succ_in Y n := by reflexivity open group @@ -735,10 +735,10 @@ namespace chain_complex Group_LES_of_homotopy_groups (S k) →g Group_LES_of_homotopy_groups k | (k, fin.mk 0 H) := proof homomorphism.mk (cc_to_fn LES_of_homotopy_groups (k + 1, 0)) - (phomotopy_group_functor_mul _ _) qed + (homotopy_group_functor_mul _ _) qed | (k, fin.mk 1 H) := proof homomorphism.mk (cc_to_fn LES_of_homotopy_groups (k + 1, 1)) - (phomotopy_group_functor_mul _ _) qed + (homotopy_group_functor_mul _ _) qed | (k, fin.mk 2 H) := begin apply homomorphism.mk (cc_to_fn LES_of_homotopy_groups (k + 1, 2)), @@ -773,30 +773,30 @@ namespace chain_complex : Π(n : +3ℕ), fibration_sequence_car (S n) →* fibration_sequence_car n | (n, fin.mk 0 H) := proof Ω→[n] f qed | (n, fin.mk 1 H) := proof Ω→[n] g qed - | (n, fin.mk 2 H) := proof Ω→[n] (e ∘* boundary_map f) ∘* loop_space_succ_in Y n qed + | (n, fin.mk 2 H) := proof Ω→[n] (e ∘* boundary_map f) ∘* loopn_succ_in Y n qed | (n, fin.mk (k+3) H) := begin exfalso, apply lt_le_antisymm H, apply le_add_left end definition fibration_sequence_pequiv : Π(x : +3ℕ), - loop_spaces2 f x ≃* fibration_sequence_car x + loopns2 f x ≃* fibration_sequence_car x | (n, fin.mk 0 H) := by reflexivity | (n, fin.mk 1 H) := by reflexivity | (n, fin.mk 2 H) := loopn_pequiv_loopn n e | (n, fin.mk (k+3) H) := begin exfalso, apply lt_le_antisymm H, apply le_add_left end definition fibration_sequence_fun_phomotopy : Π(x : +3ℕ), - fibration_sequence_pequiv x ∘* loop_spaces_fun2 f x ~* + fibration_sequence_pequiv x ∘* loopns_fun2 f x ~* (fibration_sequence_fun x ∘* fibration_sequence_pequiv (S x)) | (n, fin.mk 0 H) := by reflexivity | (n, fin.mk 1 H) := - begin refine !pid_comp ⬝* _, refine apn_phomotopy n p ⬝* _, - refine !apn_compose ⬝* _, reflexivity end - | (n, fin.mk 2 H) := begin refine !passoc⁻¹* ⬝* _ ⬝* !comp_pid⁻¹*, apply pwhisker_right, - refine _ ⬝* !apn_compose⁻¹*, reflexivity end + begin refine !pid_pcompose ⬝* _, refine apn_phomotopy n p ⬝* _, + refine !apn_pcompose ⬝* _, reflexivity end + | (n, fin.mk 2 H) := begin refine !passoc⁻¹* ⬝* _ ⬝* !pcompose_pid⁻¹*, apply pwhisker_right, + refine _ ⬝* !apn_pcompose⁻¹*, reflexivity end | (n, fin.mk (k+3) H) := begin exfalso, apply lt_le_antisymm H, apply le_add_left end definition type_fibration_sequence [constructor] : type_chain_complex +3ℕ := transfer_type_chain_complex - (LES_of_loop_spaces2 f) + (LES_of_loopns2 f) fibration_sequence_fun fibration_sequence_pequiv fibration_sequence_fun_phomotopy @@ -805,7 +805,7 @@ namespace chain_complex begin intro n, apply is_exact_at_t_transfer, - apply is_exact_LES_of_loop_spaces2 + apply is_exact_LES_of_loopns2 end definition fibration_sequence [constructor] : chain_complex +3ℕ := diff --git a/hott/homotopy/circle.hlean b/hott/homotopy/circle.hlean index 86246dd17..e1f3d37b1 100644 --- a/hott/homotopy/circle.hlean +++ b/hott/homotopy/circle.hlean @@ -220,7 +220,7 @@ namespace circle pointed.mk base definition pcircle [constructor] : Type* := pointed.mk' S¹ - notation `S¹.` := pcircle + notation `S¹*` := pcircle definition loop_neq_idp : loop ≠ idp := assume H : loop = idp, @@ -295,13 +295,13 @@ namespace circle --the carrier of π₁(S¹) is the set-truncation of base = base. open algebra trunc group - definition fg_carrier_equiv_int : π[1](S¹.) ≃ ℤ := + definition fg_carrier_equiv_int : π[1](S¹*) ≃ ℤ := trunc_equiv_trunc 0 base_eq_base_equiv ⬝e @(trunc_equiv 0 ℤ) proof _ qed 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¹.) ≃g gℤ := + definition fundamental_group_of_circle : π₁(S¹*) ≃g gℤ := begin apply (isomorphism_of_equiv fg_carrier_equiv_int), intros g h, @@ -310,9 +310,9 @@ namespace circle end open nat - definition homotopy_group_of_circle (n : ℕ) : πg[n+1 +1] S¹. ≃g G0 := + definition homotopy_group_of_circle (n : ℕ) : πg[n+2] S¹* ≃g G0 := begin - refine @trivial_homotopy_add_of_is_set_loop_space S¹. 1 n _, + refine @trivial_homotopy_add_of_is_set_loopn S¹* 1 n _, apply is_trunc_equiv_closed_rev, apply base_eq_base_equiv end @@ -337,8 +337,8 @@ namespace circle proposition is_conn_circle [instance] : is_conn 0 S¹ := sphere.is_conn_sphere -1.+2 - definition is_conn_pcircle [instance] : is_conn 0 S¹. := !is_conn_circle - definition is_trunc_pcircle [instance] : is_trunc 1 S¹. := !is_trunc_circle + definition is_conn_pcircle [instance] : is_conn 0 S¹* := !is_conn_circle + definition is_trunc_pcircle [instance] : is_trunc 1 S¹* := !is_trunc_circle definition circle_mul [reducible] (x y : S¹) : S¹ := circle.elim y (circle_turn y) x diff --git a/hott/homotopy/complex_hopf.hlean b/hott/homotopy/complex_hopf.hlean index aff545afa..e89308bf6 100644 --- a/hott/homotopy/complex_hopf.hlean +++ b/hott/homotopy/complex_hopf.hlean @@ -36,10 +36,10 @@ namespace hopf apply inv (hopf.total S¹), apply inv (join.spheres 1 1), exact x end - definition complex_phopf [constructor] : S. 3 →* S. 2 := + definition complex_phopf [constructor] : S* 3 →* S* 2 := proof pmap.mk complex_hopf idp qed - definition pfiber_complex_phopf : pfiber complex_phopf ≃* S. 1 := + definition pfiber_complex_phopf : pfiber complex_phopf ≃* S* 1 := begin fapply pequiv_of_equiv, { esimp, unfold [complex_hopf], diff --git a/hott/homotopy/freudenthal.hlean b/hott/homotopy/freudenthal.hlean index acd26b15d..2f8a79ceb 100644 --- a/hott/homotopy/freudenthal.hlean +++ b/hott/homotopy/freudenthal.hlean @@ -178,12 +178,12 @@ definition freudenthal_equiv {A : Type*} {n k : ℕ} [is_conn n A] (H : k ≤ 2 freudenthal_pequiv A H definition freudenthal_homotopy_group_pequiv (A : Type*) {n k : ℕ} [is_conn n A] (H : k ≤ 2 * n) - : π*[k + 1] (psusp A) ≃* π*[k] A := + : π[k + 1] (psusp A) ≃* π[k] A := calc - π*[k + 1] (psusp A) ≃* π*[k] (Ω (psusp A)) : phomotopy_group_succ_in (psusp A) k - ... ≃* Ω[k] (ptrunc k (Ω (psusp A))) : phomotopy_group_pequiv_loop_ptrunc k (Ω (psusp A)) + π[k + 1] (psusp A) ≃* π[k] (Ω (psusp A)) : homotopy_group_succ_in (psusp A) k + ... ≃* Ω[k] (ptrunc k (Ω (psusp A))) : homotopy_group_pequiv_loop_ptrunc k (Ω (psusp A)) ... ≃* Ω[k] (ptrunc k A) : loopn_pequiv_loopn k (freudenthal_pequiv A H) - ... ≃* π*[k] A : (phomotopy_group_pequiv_loop_ptrunc k A)⁻¹ᵉ* + ... ≃* π[k] A : (homotopy_group_pequiv_loop_ptrunc k A)⁻¹ᵉ* definition freudenthal_homotopy_group_isomorphism (A : Type*) {n k : ℕ} [is_conn n A] (H : k + 1 ≤ 2 * n) : πg[k+1 +1] (psusp A) ≃g πg[k+1] A := @@ -191,17 +191,17 @@ begin fapply isomorphism_of_equiv, { exact equiv_of_pequiv (freudenthal_homotopy_group_pequiv A H)}, { intro g h, - refine _ ⬝ !phomotopy_group_pequiv_loop_ptrunc_inv_con, - apply ap !phomotopy_group_pequiv_loop_ptrunc⁻¹ᵉ*, + refine _ ⬝ !homotopy_group_pequiv_loop_ptrunc_inv_con, + apply ap !homotopy_group_pequiv_loop_ptrunc⁻¹ᵉ*, refine ap (loopn_pequiv_loopn _ _) _ ⬝ !loopn_pequiv_loopn_con, - refine ap !phomotopy_group_pequiv_loop_ptrunc _ ⬝ !phomotopy_group_pequiv_loop_ptrunc_con, - apply phomotopy_group_succ_in_con} + refine ap !homotopy_group_pequiv_loop_ptrunc _ ⬝ !homotopy_group_pequiv_loop_ptrunc_con, + apply homotopy_group_succ_in_con} end namespace susp definition iterate_psusp_stability_pequiv (A : Type*) {k n : ℕ} [is_conn 0 A] - (H : k ≤ 2 * n) : π*[k + 1] (iterate_psusp (n + 1) A) ≃* π*[k] (iterate_psusp n A) := + (H : k ≤ 2 * n) : π[k + 1] (iterate_psusp (n + 1) A) ≃* π[k] (iterate_psusp n A) := have is_conn n (iterate_psusp n A), by rewrite [-zero_add n]; exact _, freudenthal_homotopy_group_pequiv (iterate_psusp n A) H @@ -227,8 +227,8 @@ namespace susp end definition iterate_susp_stability_pequiv (A : Type) {k n : ℕ} - (H : k + 2 ≤ 2 * n) : π*[k + 1] (pointed.MK (iterate_susp (n + 2) A) !north) ≃* - π*[k ] (pointed.MK (iterate_susp (n + 1) A) !north) := + (H : k + 2 ≤ 2 * n) : π[k + 1] (pointed.MK (iterate_susp (n + 2) A) !north) ≃* + π[k ] (pointed.MK (iterate_susp (n + 1) A) !north) := have is_conn (pred n) (carrier (pointed.MK (iterate_susp (n + 1) A) !north)), from stability_helper2 A H, freudenthal_homotopy_group_pequiv (pointed.MK (iterate_susp (n + 1) A) !north) diff --git a/hott/homotopy/homotopy_group.hlean b/hott/homotopy/homotopy_group.hlean index 1331bc036..d6953bfc1 100644 --- a/hott/homotopy/homotopy_group.hlean +++ b/hott/homotopy/homotopy_group.hlean @@ -34,13 +34,13 @@ namespace is_trunc have H3 : is_contr (ptrunc k A), from is_conn_of_le A (of_nat_le_of_nat H), have H4 : is_contr (Ω[k](ptrunc k A)), from !is_trunc_loop_of_is_trunc, apply is_trunc_equiv_closed_rev, - { apply equiv_of_pequiv (phomotopy_group_pequiv_loop_ptrunc k A)} + { apply equiv_of_pequiv (homotopy_group_pequiv_loop_ptrunc k A)} end -- Corollary 8.3.3 section open sphere sphere.ops sphere_index - theorem homotopy_group_sphere_le (n k : ℕ) (H : k < n) : is_contr (π[k] (S. n)) := + theorem homotopy_group_sphere_le (n k : ℕ) (H : k < n) : is_contr (π[k] (S* n)) := begin cases n with n, { exfalso, apply not_lt_zero, exact H}, @@ -54,12 +54,12 @@ namespace is_trunc @(trivial_homotopy_group_of_is_conn (pfiber f) H2) (H pt) theorem homotopy_group_trunc_of_le (A : Type*) (n k : ℕ) (H : k ≤ n) - : π*[k] (ptrunc n A) ≃* π*[k] A := + : π[k] (ptrunc n A) ≃* π[k] A := begin - refine !phomotopy_group_pequiv_loop_ptrunc ⬝e* _, + refine !homotopy_group_pequiv_loop_ptrunc ⬝e* _, refine loopn_pequiv_loopn _ (ptrunc_ptrunc_pequiv_left _ _) ⬝e* _, exact of_nat_le_of_nat H, - exact !phomotopy_group_pequiv_loop_ptrunc⁻¹ᵉ*, + exact !homotopy_group_pequiv_loop_ptrunc⁻¹ᵉ*, end /- Corollaries of the LES of homotopy groups -/ @@ -96,11 +96,11 @@ namespace is_trunc theorem is_equiv_π_of_is_connected.{u v} {A : pType.{u}} {B : pType.{v}} {n k : ℕ} (f : A →* B) (H2 : k ≤ n) [H : is_conn_fun n f] : is_equiv (π→[k] f) := begin - have π→*[k] pdown.{v u} ∘* π→*[k] (plift_functor f) ∘* π→*[k] pup.{u v} ~* π→*[k] f, + have π→[k] pdown.{v u} ∘* π→[k] (plift_functor f) ∘* π→[k] pup.{u v} ~* π→[k] f, begin - refine pwhisker_left _ !phomotopy_group_functor_compose⁻¹* ⬝* _, - refine !phomotopy_group_functor_compose⁻¹* ⬝* _, - apply phomotopy_group_functor_phomotopy, apply plift_functor_phomotopy + refine pwhisker_left _ !homotopy_group_functor_compose⁻¹* ⬝* _, + refine !homotopy_group_functor_compose⁻¹* ⬝* _, + apply homotopy_group_functor_phomotopy, apply plift_functor_phomotopy end, have π→[k] pdown.{v u} ∘ π→[k] (plift_functor f) ∘ π→[k] pup.{u v} ~ π→[k] f, from this, apply is_equiv.homotopy_closed, rotate 1, @@ -112,8 +112,8 @@ namespace is_trunc end definition π_equiv_π_of_is_connected {A B : Type*} {n k : ℕ} (f : A →* B) - (H2 : k ≤ n) [H : is_conn_fun n f] : π*[k] A ≃* π*[k] B := - pequiv_of_pmap (π→*[k] f) (is_equiv_π_of_is_connected f H2) + (H2 : k ≤ n) [H : is_conn_fun n f] : π[k] A ≃* π[k] B := + pequiv_of_pmap (π→[k] f) (is_equiv_π_of_is_connected f H2) -- TODO: prove this for A and B in different universe levels theorem is_surjective_π_of_is_connected.{u} {A B : pType.{u}} (n : ℕ) (f : A →* B) @@ -128,7 +128,7 @@ namespace is_trunc -/ definition whitehead_principle (n : ℕ₋₂) {A B : Type} [HA : is_trunc n A] [HB : is_trunc n B] (f : A → B) (H' : is_equiv (trunc_functor 0 f)) - (H : Πa k, is_equiv (π→*[k + 1] (pmap_of_map f a))) : is_equiv f := + (H : Πa k, is_equiv (π→[k + 1] (pmap_of_map f a))) : is_equiv f := begin revert A B HA HB f H' H, induction n with n IH: intros, { apply is_equiv_of_is_contr}, @@ -138,24 +138,24 @@ namespace is_trunc apply IH, do 2 (esimp; exact _), { rexact H a 0}, intro p k, - have is_equiv (π→*[k + 1] (Ω→(pmap_of_map f a))), - from is_equiv_phomotopy_group_functor_ap1 (k+1) (pmap_of_map f a), + have is_equiv (π→[k + 1] (Ω→(pmap_of_map f a))), + from is_equiv_homotopy_group_functor_ap1 (k+1) (pmap_of_map f a), have Π(b : A) (p : a = b), - is_equiv (pmap.to_fun (π→*[k + 1] (pmap_of_map (ap f) p))), + is_equiv (pmap.to_fun (π→[k + 1] (pmap_of_map (ap f) p))), begin intro b p, induction p, apply is_equiv.homotopy_closed, exact this, - refine phomotopy_group_functor_phomotopy _ _, + refine homotopy_group_functor_phomotopy _ _, apply ap1_pmap_of_map end, - have is_equiv (phomotopy_group_pequiv _ + have is_equiv (homotopy_group_pequiv _ (pequiv_of_eq_pt (!idp_con⁻¹ : ap f p = Ω→ (pmap_of_map f a) p)) ∘ - pmap.to_fun (π→*[k + 1] (pmap_of_map (ap f) p))), + pmap.to_fun (π→[k + 1] (pmap_of_map (ap f) p))), begin apply is_equiv_compose, exact this a p, end, apply is_equiv.homotopy_closed, exact this, - refine !phomotopy_group_functor_compose⁻¹* ⬝* _, - apply phomotopy_group_functor_phomotopy, + refine !homotopy_group_functor_compose⁻¹* ⬝* _, + apply homotopy_group_functor_phomotopy, fapply phomotopy.mk, { esimp, intro q, refine !idp_con⁻¹}, { esimp, refine !idp_con⁻¹}, @@ -165,23 +165,23 @@ namespace is_trunc definition whitehead_principle_pointed (n : ℕ₋₂) {A B : Type*} [HA : is_trunc n A] [HB : is_trunc n B] [is_conn 0 A] (f : A →* B) - (H : Πk, is_equiv (π→*[k] f)) : is_equiv f := + (H : Πk, is_equiv (π→[k] f)) : is_equiv f := begin apply whitehead_principle n, rexact H 0, intro a k, revert a, apply is_conn.elim -1, - have is_equiv (π→*[k + 1] (pointed_eta_pequiv B ⬝e* (pequiv_of_eq_pt (respect_pt f))⁻¹ᵉ*) - ∘* π→*[k + 1] f ∘* π→*[k + 1] (pointed_eta_pequiv A)⁻¹ᵉ*), + have is_equiv (π→[k + 1] (pointed_eta_pequiv B ⬝e* (pequiv_of_eq_pt (respect_pt f))⁻¹ᵉ*) + ∘* π→[k + 1] f ∘* π→[k + 1] (pointed_eta_pequiv A)⁻¹ᵉ*), begin apply is_equiv_compose - (π→*[k + 1] (pointed_eta_pequiv B ⬝e* (pequiv_of_eq_pt (respect_pt f))⁻¹ᵉ*)), - apply is_equiv_compose (π→*[k + 1] f), + (π→[k + 1] (pointed_eta_pequiv B ⬝e* (pequiv_of_eq_pt (respect_pt f))⁻¹ᵉ*)), + apply is_equiv_compose (π→[k + 1] f), all_goals apply is_equiv_homotopy_group_functor, end, refine @(is_equiv.homotopy_closed _) _ this _, apply to_homotopy, - refine pwhisker_left _ !phomotopy_group_functor_compose⁻¹* ⬝* _, - refine !phomotopy_group_functor_compose⁻¹* ⬝* _, - apply phomotopy_group_functor_phomotopy, apply phomotopy_pmap_of_map + refine pwhisker_left _ !homotopy_group_functor_compose⁻¹* ⬝* _, + refine !homotopy_group_functor_compose⁻¹* ⬝* _, + apply homotopy_group_functor_phomotopy, apply phomotopy_pmap_of_map end open pointed.ops @@ -236,7 +236,7 @@ namespace is_trunc have H3 : Πa, is_contr (ptrunc n (pfiber (pmap_of_map f a))), begin intro a, apply is_contr_of_trivial_homotopy_nat_pointed n, - { intro k H, apply is_trunc_equiv_closed_rev, exact phomotopy_group_ptrunc_of_le H _, + { intro k H, apply is_trunc_equiv_closed_rev, exact homotopy_group_ptrunc_of_le H _, rexact @is_contr_of_is_embedding_of_is_surjective +3ℕ (LES_of_homotopy_groups (pmap_of_map f a)) (k, 0) (is_exact_LES_of_homotopy_groups _ _) diff --git a/hott/homotopy/sphere.hlean b/hott/homotopy/sphere.hlean index fcc08220d..7c2f6699b 100644 --- a/hott/homotopy/sphere.hlean +++ b/hott/homotopy/sphere.hlean @@ -255,29 +255,29 @@ namespace sphere namespace ops abbreviation S := sphere - notation `S.` := psphere + 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_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 := + : 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 [constructor] (n : ℕ) : S. n →* Ω (S. (succ n)) := - loop_susp_unit (S. n) + definition equator [constructor] (n : ℕ) : S* n →* Ω (S* (succ n)) := + loop_susp_unit (S* n) - definition surf {n : ℕ} : Ω[n] S. n := + definition surf {n : ℕ} : Ω[n] (S* n) := begin induction n with n s, { exact @base 0}, - { exact (loop_space_succ_in (S. (succ n)) n)⁻¹ᵉ* (apn n (equator n) s), } + { exact (loopn_succ_in (S* (succ n)) n)⁻¹ᵉ* (apn n (equator n) s), } end definition bool_of_sphere [unfold 1] : S 0 → bool := @@ -293,24 +293,24 @@ namespace sphere (λb, match b with | tt := idp | ff := idp end) (λx, proof susp.rec_on x idp idp (empty.rec _) qed) - definition psphere_pequiv_pbool : S. 0 ≃* pbool := + definition psphere_pequiv_pbool : S* 0 ≃* pbool := pequiv_of_equiv sphere_equiv_bool idp definition sphere_eq_bool : S 0 = bool := ua sphere_equiv_bool - definition sphere_eq_pbool : S. 0 = pbool := + 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" (the next def also) -- TODO2: we could make this a pointed equivalence - definition pmap_sphere (A : Type*) (n : ℕ) : (S. n →* A) ≃ Ω[n] A := + definition psphere_pmap_equiv (A : Type*) (n : ℕ) : (S* n →* A) ≃ Ω[n] A := begin -- fapply equiv_change_fun, -- { revert A, induction n with n IH: intro A, - { refine _ ⬝e !pmap_bool_equiv, exact equiv_ppcompose_right psphere_pequiv_pbool⁻¹ᵉ*}, - { refine susp_adjoint_loop (S. n) A ⬝e !IH ⬝e !loop_space_succ_in⁻¹ᵉ* } + { refine _ ⬝e !pmap_bool_equiv, exact pequiv_ppcompose_right psphere_pequiv_pbool⁻¹ᵉ*}, + { refine susp_adjoint_loop (S* n) A ⬝e !IH ⬝e !loopn_succ_in⁻¹ᵉ* } -- }, -- { intro f, exact apn n f surf}, -- { revert A, induction n with n IH: intro A f, @@ -318,25 +318,25 @@ namespace sphere -- { exact sorry}} end - -- definition pmap_sphere' (A : Type*) (n : ℕ) : (S. n →* A) ≃ Ω[n] A := + -- definition psphere_pmap_equiv' (A : Type*) (n : ℕ) : (S* n →* A) ≃ Ω[n] A := -- begin -- fapply equiv.MK, -- { intro f, exact apn n f surf }, -- { revert A, induction n with n IH: intro A p, -- { exact !pmap_bool_equiv⁻¹ᵉ p ∘* psphere_pequiv_pbool }, - -- { refine (susp_adjoint_loop (S. n) A)⁻¹ᵉ (IH (Ω A) _), - -- exact loop_space_succ_in A n p }}, + -- { refine (susp_adjoint_loop (S* n) A)⁻¹ᵉ (IH (Ω A) _), + -- exact loopn_succ_in A n p }}, -- { exact sorry}, -- { exact sorry} -- end - protected definition elim {n : ℕ} {P : Type*} (p : Ω[n] P) : S. n →* P := - to_inv !pmap_sphere p + protected definition elim {n : ℕ} {P : Type*} (p : Ω[n] P) : S* n →* P := + to_inv !psphere_pmap_equiv 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}, + -- { esimp [apn,surf,sphere.elim,psphere_pmap_equiv], apply sorry}, -- { apply sorry} -- end @@ -354,7 +354,7 @@ namespace sphere apply is_conn_susp } end - theorem is_conn_psphere [instance] (n : ℕ) : is_conn (n.-1) (S. n) := + 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 @@ -364,12 +364,12 @@ 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 : S. n →* pointed.Mk a) (x : S n), f x = f base) : is_trunc (n.-2.+1) A := + definition is_trunc_of_psphere_pmap_equiv_constant + (H : Π(a : A) (f : 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, + apply is_trunc_equiv_closed, apply psphere_pmap_equiv, fapply is_contr.mk, { exact pmap.mk (λx, a) idp}, { intro f, fapply pmap_eq, @@ -380,27 +380,27 @@ namespace is_trunc 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, + apply is_trunc_of_psphere_pmap_equiv_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 : S. n →* pointed.Mk a) (x : S n) : f x = f base := + definition psphere_pmap_equiv_constant_of_is_trunc' [H : is_trunc (n.-2.+1) A] + (a : A) (f : 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', + note H'' := @is_trunc_equiv_closed_rev _ _ _ !psphere_pmap_equiv 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 : 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 psphere_pmap_equiv_constant_of_is_trunc [H : is_trunc (n.-2.+1) A] + (a : A) (f : S* n →* pointed.Mk a) (x y : S n) : f x = f y := + let H := psphere_pmap_equiv_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 + psphere_pmap_equiv_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 := diff --git a/hott/homotopy/sphere2.hlean b/hott/homotopy/sphere2.hlean index 487f19ac7..3c15db76d 100644 --- a/hott/homotopy/sphere2.hlean +++ b/hott/homotopy/sphere2.hlean @@ -20,7 +20,7 @@ namespace sphere /- Corollaries of the complex hopf fibration combined with the LES of homotopy groups -/ open sphere sphere.ops int circle hopf - definition π2S2 : πg[1+1] (S. 2) ≃g gℤ := + definition π2S2 : πg[1+1] (S* 2) ≃g gℤ := begin refine _ ⬝g fundamental_group_of_circle, refine _ ⬝g homotopy_group_isomorphism_of_pequiv _ pfiber_complex_phopf, @@ -47,7 +47,7 @@ namespace sphere end open circle - definition πnS3_eq_πnS2 (n : ℕ) : πg[n+2 +1] (S. 3) ≃g πg[n+2 +1] (S. 2) := + definition πnS3_eq_πnS2 (n : ℕ) : πg[n+2 +1] (S* 3) ≃g πg[n+2 +1] (S* 2) := begin fapply isomorphism_of_equiv, { fapply equiv.mk, @@ -75,15 +75,15 @@ namespace sphere end definition sphere_stability_pequiv (k n : ℕ) (H : k + 2 ≤ 2 * n) : - π*[k + 1] (S. (n+1)) ≃* π*[k] (S. n) := + π[k + 1] (S* (n+1)) ≃* π[k] (S* n) := begin rewrite [+ psphere_eq_iterate_susp], exact iterate_susp_stability_pequiv empty H end definition stability_isomorphism (k n : ℕ) (H : k + 3 ≤ 2 * n) - : πg[k+1 +1] (S. (n+1)) ≃g πg[k+1] (S. n) := + : πg[k+1 +1] (S* (n+1)) ≃g πg[k+1] (S* n) := begin rewrite [+ psphere_eq_iterate_susp], exact iterate_susp_stability_isomorphism empty H end open int circle hopf - definition πnSn (n : ℕ) : πg[n+1] (S. (succ n)) ≃g gℤ := + definition πnSn (n : ℕ) : πg[n+1] (S* (succ n)) ≃g gℤ := begin cases n with n IH, { exact fundamental_group_of_circle}, @@ -93,10 +93,10 @@ namespace sphere rexact add_mul_le_mul_add n 1 2}} end - theorem not_is_trunc_sphere (n : ℕ) : ¬is_trunc n (S. (succ n)) := + theorem not_is_trunc_sphere (n : ℕ) : ¬is_trunc n (S* (succ n)) := begin intro H, - note H2 := trivial_ghomotopy_group_of_is_trunc (S. (succ n)) n n !le.refl, + note H2 := trivial_ghomotopy_group_of_is_trunc (S* (succ n)) n n !le.refl, have H3 : is_contr ℤ, from is_trunc_equiv_closed _ (equiv_of_isomorphism (πnSn n)), have H4 : (0 : ℤ) ≠ (1 : ℤ), from dec_star, apply H4, @@ -120,7 +120,7 @@ namespace sphere end - definition π3S2 : πg[2+1] (S. 2) ≃g gℤ := + definition π3S2 : πg[2+1] (S* 2) ≃g gℤ := (πnS3_eq_πnS2 0)⁻¹ᵍ ⬝g πnSn 2 end sphere diff --git a/hott/homotopy/susp.hlean b/hott/homotopy/susp.hlean index 8db9fb116..97c0f9c84 100644 --- a/hott/homotopy/susp.hlean +++ b/hott/homotopy/susp.hlean @@ -321,19 +321,19 @@ namespace susp { intro f, exact ap1 f ∘* loop_susp_unit X}, { intro g, exact loop_susp_counit Y ∘* psusp_functor g}, { intro g, apply eq_of_phomotopy, esimp, - refine !pwhisker_right !ap1_compose ⬝* _, + refine !pwhisker_right !ap1_pcompose ⬝* _, refine !passoc ⬝* _, refine !pwhisker_left !loop_susp_unit_natural⁻¹* ⬝* _, refine !passoc⁻¹* ⬝* _, refine !pwhisker_right !loop_susp_counit_unit ⬝* _, - apply pid_comp}, + apply pid_pcompose}, { intro f, apply eq_of_phomotopy, esimp, refine !pwhisker_left !psusp_functor_compose ⬝* _, refine !passoc⁻¹* ⬝* _, refine !pwhisker_right !loop_susp_counit_natural⁻¹* ⬝* _, refine !passoc ⬝* _, refine !pwhisker_left !loop_susp_unit_counit ⬝* _, - apply comp_pid}, + apply pcompose_pid}, end definition susp_adjoint_loop_nat_right (f : psusp X →* Y) (g : Y →* Z) @@ -342,7 +342,7 @@ namespace susp esimp [susp_adjoint_loop], refine _ ⬝* !passoc, apply pwhisker_right, - apply ap1_compose + apply ap1_pcompose end definition susp_adjoint_loop_nat_left (f : Y →* Ω Z) (g : X →* Y) diff --git a/hott/naming_conventions.md b/hott/naming_conventions.md new file mode 100644 index 000000000..37ab0c89b --- /dev/null +++ b/hott/naming_conventions.md @@ -0,0 +1,14 @@ +HoTT Naming Conventions +======================= + + +[generic naming conventions go here] + +Pointed Types +------------- + +We use a prefix `p` to specify that an operation/construction is pointed. For example `pequiv` is +pointed equivalences and `phomotopy` are pointed homotopies. Only if a construction only works for +pointed types and has no unpointed equivalent we omit the `p` (examples: `loop` `loopn` +`homotopy_group`). A lemma about pointed constructions repeats the `p` for every name, for example +`psusp_pequiv_psusp` or `pid_pcompose`. For notation we append `*` for the pointed version, like `Type*` (this is the universe of pointed types, not the universe considered as a pointed type), `S*` or `bool*`. For notations which only make sense pointed we don't add the star, like `Ω[n]` or `π[k]`. \ No newline at end of file diff --git a/hott/types/pointed.hlean b/hott/types/pointed.hlean index 5f6b417a4..985df4f8f 100644 --- a/hott/types/pointed.hlean +++ b/hott/types/pointed.hlean @@ -19,15 +19,15 @@ namespace pointed definition pointed_fun_closed [constructor] (f : A → B) [H : pointed A] : pointed B := pointed.mk (f pt) - definition ploop_space [reducible] [constructor] (A : Type*) : Type* := + definition loop [reducible] [constructor] (A : Type*) : Type* := pointed.mk' (point A = point A) - definition iterated_ploop_space [reducible] : ℕ → Type* → Type* - | iterated_ploop_space 0 X := X - | iterated_ploop_space (n+1) X := ploop_space (iterated_ploop_space n X) + definition loopn [reducible] : ℕ → Type* → Type* + | loopn 0 X := X + | loopn (n+1) X := loop (loopn n X) - notation `Ω` := ploop_space - notation `Ω[`:95 n:0 `] `:0 A:95 := iterated_ploop_space n A + notation `Ω` := loop + notation `Ω[`:95 n:0 `]`:0 := loopn n namespace ops -- this is in a separate namespace because it caused type class inference to loop in some places @@ -40,17 +40,17 @@ namespace pointed (n : ℕ₋₂) [H : is_trunc (n.+1) A] : is_trunc n (Ω A) := !is_trunc_eq - definition iterated_ploop_space_zero [unfold_full] (A : Type*) + definition loopn_zero_eq [unfold_full] (A : Type*) : Ω[0] A = A := rfl - definition iterated_ploop_space_succ [unfold_full] (k : ℕ) (A : Type*) - : Ω[succ k] A = Ω Ω[k] A := rfl + definition loopn_succ_eq [unfold_full] (k : ℕ) (A : Type*) + : Ω[succ k] A = Ω (Ω[k] A) := rfl definition rfln [constructor] [reducible] {n : ℕ} {A : Type*} : Ω[n] A := pt definition refln [constructor] [reducible] (n : ℕ) (A : Type*) : Ω[n] A := pt definition refln_eq_refl [unfold_full] (A : Type*) (n : ℕ) : rfln = rfl :> Ω[succ n] A := rfl - definition iterated_loop_space [unfold 3] (A : Type) [H : pointed A] (n : ℕ) : Type := + definition loopn_space [unfold 3] (A : Type) [H : pointed A] (n : ℕ) : Type := Ω[n] (pointed.mk' A) definition loop_mul {k : ℕ} {A : Type*} (mul : A → A → A) : Ω[k] A → Ω[k] A → Ω[k] A := @@ -131,14 +131,14 @@ namespace pointed induction pf, induction pg, induction ph, reflexivity end - definition pid_comp [constructor] (f : A →* B) : pid B ∘* f ~* f := + definition pid_pcompose [constructor] (f : A →* B) : pid B ∘* f ~* f := begin fconstructor, { intro a, reflexivity}, { reflexivity} end - definition comp_pid [constructor] (f : A →* B) : f ∘* pid A ~* f := + definition pcompose_pid [constructor] (f : A →* B) : f ∘* pid A ~* f := begin fconstructor, { intro a, reflexivity}, @@ -223,7 +223,7 @@ namespace pointed begin induction n with n IH, { exact f}, - { esimp [iterated_ploop_space], exact ap1 IH} + { esimp [loopn], exact ap1 IH} end prefix `Ω→`:(max+5) := ap1 @@ -279,7 +279,7 @@ namespace pointed definition is_equiv_pcast [instance] {A B : Type*} (p : A = B) : is_equiv (pcast p) := !is_equiv_cast - definition ap1_id [constructor] {A : Type*} : ap1 (pid A) ~* pid (Ω A) := + definition ap1_pid [constructor] {A : Type*} : ap1 (pid A) ~* pid (Ω A) := begin fapply phomotopy.mk, { intro p, esimp, refine !idp_con ⬝ !ap_id}, @@ -293,7 +293,7 @@ namespace pointed { reflexivity} end - definition ap1_compose (g : B →* C) (f : A →* B) : ap1 (g ∘* f) ~* ap1 g ∘* ap1 f := + definition ap1_pcompose (g : B →* C) (f : A →* B) : ap1 (g ∘* f) ~* ap1 g ∘* ap1 f := begin induction B, induction C, induction g with g pg, induction f with f pf, esimp at *, induction pg, induction pf, @@ -302,7 +302,7 @@ namespace pointed { reflexivity} end - definition ap1_compose_pinverse (f : A →* B) : ap1 f ∘* pinverse ~* pinverse ∘* ap1 f := + definition ap1_pcompose_pinverse (f : A →* B) : ap1 f ∘* pinverse ~* pinverse ∘* ap1 f := begin fconstructor, { intro p, esimp, refine !con.assoc ⬝ _ ⬝ !con_inv⁻¹, apply whisker_left, @@ -321,12 +321,6 @@ namespace pointed rewrite [▸*,ap_inv, +con_inv, inv_inv, +con.assoc], repeat apply whisker_left end - definition pcast_ap_loop_space {A B : Type*} (p : A = B) - : pcast (ap ploop_space p) ~* Ω→ (pcast p) := - begin - induction p, exact !ap1_id⁻¹* - end - definition pinverse_con [constructor] {X : Type*} (p q : Ω X) : pinverse (p ⬝ q) = pinverse q ⬝ pinverse p := !con_inv @@ -411,18 +405,18 @@ namespace pointed { exact ap1_phomotopy IH} end - definition apn_compose (n : ℕ) (g : B →* C) (f : A →* B) : apn n (g ∘* f) ~* apn n g ∘* apn n f := + definition apn_pcompose (n : ℕ) (g : B →* C) (f : A →* B) : apn n (g ∘* f) ~* apn n g ∘* apn n f := begin induction n with n IH, { reflexivity}, - { refine ap1_phomotopy IH ⬝* _, apply ap1_compose} + { refine ap1_phomotopy IH ⬝* _, apply ap1_pcompose} end definition apn_pid [constructor] {A : Type*} (n : ℕ) : apn n (pid A) ~* pid (Ω[n] A) := begin induction n with n IH, { reflexivity}, - { exact ap1_phomotopy IH ⬝* ap1_id} + { exact ap1_phomotopy IH ⬝* ap1_pid} end theorem apn_con (n : ℕ) (f : A →* B) (p q : Ω[n+1] A) @@ -439,7 +433,7 @@ namespace pointed { reflexivity} end - definition pcast_loop_space [constructor] {A B : Type*} (p : A = B) : + definition pcast_ap_loop [constructor] {A B : Type*} (p : A = B) : pcast (ap Ω p) ~* ap1 (pcast p) := begin fapply phomotopy.mk, @@ -589,7 +583,7 @@ namespace pointed refine _⁻¹* ⬝* pwhisker_left f⁻¹ᵉ* p ⬝* _: refine !passoc⁻¹* ⬝* _: refine pwhisker_right _ (pleft_inv f) ⬝* _: - apply pid_comp + apply pid_pcompose end definition pcancel_right (f : A ≃* B) {g h : B →* C} (p : g ∘* f ~* h ∘* f) : g ~* h := @@ -597,7 +591,7 @@ namespace pointed refine _⁻¹* ⬝* pwhisker_right f⁻¹ᵉ* p ⬝* _: refine !passoc ⬝* _: refine pwhisker_left _ (pright_inv f) ⬝* _: - apply comp_pid + apply pcompose_pid end definition phomotopy_pinv_right_of_phomotopy {f : A ≃* B} {g : B →* C} {h : A →* C} @@ -606,7 +600,7 @@ namespace pointed refine _ ⬝* pwhisker_right _ p, symmetry, refine !passoc ⬝* _, refine pwhisker_left _ (pright_inv f) ⬝* _, - apply comp_pid + apply pcompose_pid end definition phomotopy_of_pinv_right_phomotopy {f : B ≃* A} {g : B →* C} {h : A →* C} @@ -615,7 +609,7 @@ namespace pointed refine _ ⬝* pwhisker_right _ p, symmetry, refine !passoc ⬝* _, refine pwhisker_left _ (pleft_inv f) ⬝* _, - apply comp_pid + apply pcompose_pid end definition pinv_right_phomotopy_of_phomotopy {f : A ≃* B} {g : B →* C} {h : A →* C} @@ -632,7 +626,7 @@ namespace pointed refine _ ⬝* pwhisker_left _ p, symmetry, refine !passoc⁻¹* ⬝* _, refine pwhisker_right _ (pleft_inv f) ⬝* _, - apply pid_comp + apply pid_pcompose end definition phomotopy_of_pinv_left_phomotopy {f : C ≃* B} {g : A →* B} {h : A →* C} @@ -641,7 +635,7 @@ namespace pointed refine _ ⬝* pwhisker_left _ p, symmetry, refine !passoc⁻¹* ⬝* _, refine pwhisker_right _ (pright_inv f) ⬝* _, - apply pid_comp + apply pid_pcompose end definition pinv_left_phomotopy_of_phomotopy {f : B ≃* C} {g : A →* B} {h : A →* C} @@ -661,18 +655,18 @@ namespace pointed { apply pleft_inv}, { replace nat.succ n with n + 1, rewrite [+apn_succ], - refine !ap1_compose⁻¹* ⬝* _, + refine !ap1_pcompose⁻¹* ⬝* _, refine ap1_phomotopy IH ⬝* _, - apply ap1_id} + apply ap1_pid} end end abstract begin induction n with n IH, { apply pright_inv}, { replace nat.succ n with n + 1, rewrite [+apn_succ], - refine !ap1_compose⁻¹* ⬝* _, + refine !ap1_pcompose⁻¹* ⬝* _, refine ap1_phomotopy IH ⬝* _, - apply ap1_id} + apply ap1_pid} end end definition loop_pequiv_loop [constructor] (f : A ≃* B) : Ω A ≃* Ω B := @@ -753,31 +747,31 @@ namespace pointed /- properties of iterated loop space -/ variable (A) - definition loop_space_succ_in (n : ℕ) : Ω[succ n] A ≃* Ω[n] (Ω A) := + definition loopn_succ_in (n : ℕ) : Ω[succ n] A ≃* Ω[n] (Ω A) := begin induction n with n IH, { reflexivity}, { exact loop_pequiv_loop IH} end - definition loop_space_add (n m : ℕ) : Ω[n] (Ω[m] A) ≃* Ω[m+n] (A) := + definition loopn_add (n m : ℕ) : Ω[n] (Ω[m] A) ≃* Ω[m+n] (A) := begin induction n with n IH, { reflexivity}, { exact loop_pequiv_loop IH} end - definition loop_space_succ_eq_out (n : ℕ) : Ω[succ n] A ≃* Ω(Ω[n] A) := + definition loopn_succ_out (n : ℕ) : Ω[succ n] A ≃* Ω(Ω[n] A) := by reflexivity variable {A} - theorem loop_space_succ_in_con {n : ℕ} (p q : Ω[succ (succ n)] A) : - loop_space_succ_in A (succ n) (p ⬝ q) = - loop_space_succ_in A (succ n) p ⬝ loop_space_succ_in A (succ n) q := + theorem loopn_succ_in_con {n : ℕ} (p q : Ω[succ (succ n)] A) : + loopn_succ_in A (succ n) (p ⬝ q) = + loopn_succ_in A (succ n) p ⬝ loopn_succ_in A (succ n) q := !loop_pequiv_loop_con - definition loop_space_loop_irrel (p : point A = point A) : Ω(pointed.Mk p) = Ω[2] A := + definition loopn_loop_irrel (p : point A = point A) : Ω(pointed.Mk p) = Ω[2] A := begin intros, fapply pType_eq, { esimp, transitivity _, @@ -786,26 +780,26 @@ namespace pointed { esimp, apply con.left_inv} end - definition iterated_loop_space_loop_irrel (n : ℕ) (p : point A = point A) + definition loopn_space_loop_irrel (n : ℕ) (p : point A = point A) : Ω[succ n](pointed.Mk p) = Ω[succ (succ n)] A :> pType := calc - Ω[succ n](pointed.Mk p) = Ω[n](Ω (pointed.Mk p)) : eq_of_pequiv !loop_space_succ_in - ... = Ω[n] (Ω[2] A) : loop_space_loop_irrel - ... = Ω[2+n] A : eq_of_pequiv !loop_space_add + Ω[succ n](pointed.Mk p) = Ω[n](Ω (pointed.Mk p)) : eq_of_pequiv !loopn_succ_in + ... = Ω[n] (Ω[2] A) : loopn_loop_irrel + ... = Ω[2+n] A : eq_of_pequiv !loopn_add ... = Ω[n+2] A : by rewrite [algebra.add.comm] definition apn_succ_phomotopy_in (n : ℕ) (f : A →* B) : - loop_space_succ_in B n ∘* Ω→[n + 1] f ~* Ω→[n] (Ω→ f) ∘* loop_space_succ_in A n := + loopn_succ_in B n ∘* Ω→[n + 1] f ~* Ω→[n] (Ω→ f) ∘* loopn_succ_in A n := begin induction n with n IH, { reflexivity}, - { exact !ap1_compose⁻¹* ⬝* ap1_phomotopy IH ⬝* !ap1_compose} + { exact !ap1_pcompose⁻¹* ⬝* ap1_phomotopy IH ⬝* !ap1_pcompose} end definition ppcompose_left [constructor] (g : B →* C) : ppmap A B →* ppmap A C := pmap.mk (pcompose g) (eq_of_phomotopy (phomotopy.mk (λa, respect_pt g) (idp_con _)⁻¹)) - definition is_equiv_ppcompose_left [instance] [constructor] (g : B →* C) [H : is_equiv g] : + definition is_pequiv_ppcompose_left [instance] [constructor] (g : B →* C) [H : is_equiv g] : is_equiv (@ppcompose_left A B C g) := begin fapply is_equiv.adjointify, @@ -813,13 +807,13 @@ namespace pointed all_goals (intros f; esimp; apply eq_of_phomotopy), { exact calc g ∘* ((pequiv_of_pmap g H)⁻¹ᵉ* ∘* f) ~* (g ∘* (pequiv_of_pmap g H)⁻¹ᵉ*) ∘* f : passoc ... ~* pid _ ∘* f : pwhisker_right f (pright_inv (pequiv_of_pmap g H)) - ... ~* f : pid_comp f }, + ... ~* f : pid_pcompose f }, { exact calc (pequiv_of_pmap g H)⁻¹ᵉ* ∘* (g ∘* f) ~* ((pequiv_of_pmap g H)⁻¹ᵉ* ∘* g) ∘* f : passoc ... ~* pid _ ∘* f : pwhisker_right f (pleft_inv (pequiv_of_pmap g H)) - ... ~* f : pid_comp f } + ... ~* f : pid_pcompose f } end - definition equiv_ppcompose_left [constructor] (g : B ≃* C) : ppmap A B ≃* ppmap A C := + definition pequiv_ppcompose_left [constructor] (g : B ≃* C) : ppmap A B ≃* ppmap A C := pequiv_of_pmap (ppcompose_left g) _ definition pcompose_pconst [constructor] (f : B →* C) : f ∘* pconst A B ~* pconst A C := @@ -835,15 +829,15 @@ namespace pointed { apply eq_of_phomotopy, esimp, apply pconst_pcompose } end - definition equiv_ppcompose_right [constructor] (f : A ≃* B) : ppmap B C ≃* ppmap A C := + definition pequiv_ppcompose_right [constructor] (f : A ≃* B) : ppmap B C ≃* ppmap A C := begin fapply pequiv.MK, { exact ppcompose_right f }, { exact ppcompose_right f⁻¹ᵉ* }, { intro g, apply eq_of_phomotopy, refine !passoc ⬝* _, - refine pwhisker_left g !pright_inv ⬝* !comp_pid, }, + refine pwhisker_left g !pright_inv ⬝* !pcompose_pid, }, { intro g, apply eq_of_phomotopy, refine !passoc ⬝* _, - refine pwhisker_left g !pleft_inv ⬝* !comp_pid, }, + refine pwhisker_left g !pleft_inv ⬝* !pcompose_pid, }, end diff --git a/hott/types/trunc.hlean b/hott/types/trunc.hlean index 255d5b265..ce877e579 100644 --- a/hott/types/trunc.hlean +++ b/hott/types/trunc.hlean @@ -420,15 +420,15 @@ namespace is_trunc : is_trunc n A ↔ Π(a : A), is_contr (Ω[succ n](pointed.Mk a)) := begin revert A, induction n with n IH, - { intro A, esimp [iterated_ploop_space], transitivity _, + { intro A, esimp [loopn], transitivity _, { apply is_trunc_succ_iff_is_trunc_loop, apply le.refl}, { apply pi_iff_pi, intro a, esimp, apply is_prop_iff_is_contr, reflexivity}}, - { intro A, esimp [iterated_ploop_space], + { intro A, esimp [loopn], transitivity _, { apply @is_trunc_succ_iff_is_trunc_loop @n, esimp, apply minus_one_le_succ}, apply pi_iff_pi, intro a, transitivity _, apply IH, transitivity _, apply pi_iff_pi, intro p, - rewrite [iterated_loop_space_loop_irrel n p], apply iff.refl, esimp, + rewrite [loopn_space_loop_irrel n p], apply iff.refl, esimp, apply imp_iff, reflexivity} end @@ -437,7 +437,7 @@ namespace is_trunc : is_trunc (n.-2.+1) A ↔ (Π(a : A), is_contr (Ω[n](pointed.Mk a))) := begin induction n with n, - { esimp [sub_two,iterated_ploop_space], apply iff.intro, + { esimp [sub_two,loopn], apply iff.intro, intro H a, exact is_contr_of_inhabited_prop a, intro H, apply is_prop_of_imp_is_contr, exact H}, { apply is_trunc_iff_is_contr_loop_succ}, @@ -718,34 +718,34 @@ namespace trunc encode_con p q -- rename - definition iterated_loop_ptrunc_pequiv (n : ℕ₋₂) (k : ℕ) (A : Type*) : + definition loopn_ptrunc_pequiv (n : ℕ₋₂) (k : ℕ) (A : Type*) : Ω[k] (ptrunc (n+k) A) ≃* ptrunc n (Ω[k] A) := begin revert n, induction k with k IH: intro n, { reflexivity}, { refine _ ⬝e* loop_ptrunc_pequiv n (Ω[k] A), - rewrite [iterated_ploop_space_succ], apply loop_pequiv_loop, + rewrite [loopn_succ_eq], apply loop_pequiv_loop, refine _ ⬝e* IH (n.+1), rewrite succ_add_nat} end - definition iterated_loop_ptrunc_pequiv_con {n : ℕ₋₂} {k : ℕ} {A : Type*} + definition loopn_ptrunc_pequiv_con {n : ℕ₋₂} {k : ℕ} {A : Type*} (p q : Ω[succ k] (ptrunc (n+succ k) A)) : - iterated_loop_ptrunc_pequiv n (succ k) A (p ⬝ q) = - tconcat (iterated_loop_ptrunc_pequiv n (succ k) A p) - (iterated_loop_ptrunc_pequiv n (succ k) A q) := + loopn_ptrunc_pequiv n (succ k) A (p ⬝ q) = + tconcat (loopn_ptrunc_pequiv n (succ k) A p) + (loopn_ptrunc_pequiv n (succ k) A q) := begin refine _ ⬝ loop_ptrunc_pequiv_con _ _, exact ap !loop_ptrunc_pequiv !loop_pequiv_loop_con end - definition iterated_loop_ptrunc_pequiv_inv_con {n : ℕ₋₂} {k : ℕ} {A : Type*} + definition loopn_ptrunc_pequiv_inv_con {n : ℕ₋₂} {k : ℕ} {A : Type*} (p q : ptrunc n (Ω[succ k] A)) : - (iterated_loop_ptrunc_pequiv n (succ k) A)⁻¹ᵉ* (tconcat p q) = - (iterated_loop_ptrunc_pequiv n (succ k) A)⁻¹ᵉ* p ⬝ - (iterated_loop_ptrunc_pequiv n (succ k) A)⁻¹ᵉ* q := - equiv.inv_preserve_binary (iterated_loop_ptrunc_pequiv n (succ k) A) concat tconcat - (@iterated_loop_ptrunc_pequiv_con n k A) p q + (loopn_ptrunc_pequiv n (succ k) A)⁻¹ᵉ* (tconcat p q) = + (loopn_ptrunc_pequiv n (succ k) A)⁻¹ᵉ* p ⬝ + (loopn_ptrunc_pequiv n (succ k) A)⁻¹ᵉ* q := + equiv.inv_preserve_binary (loopn_ptrunc_pequiv n (succ k) A) concat tconcat + (@loopn_ptrunc_pequiv_con n k A) p q definition ptrunc_functor_pcompose [constructor] {X Y Z : Type*} (n : ℕ₋₂) (g : Y →* Z) (f : X →* Y) : ptrunc_functor n (g ∘* f) ~* ptrunc_functor n g ∘* ptrunc_functor n f :=