From e1d2392a138ea644195f4e165e6d1b76d0dcc096 Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Tue, 4 Sep 2018 11:54:26 +0200 Subject: [PATCH] move more stuff --- homotopy/degree.hlean | 4 + move_to_lib.hlean | 307 +++++++++++------------------------------- 2 files changed, 80 insertions(+), 231 deletions(-) diff --git a/homotopy/degree.hlean b/homotopy/degree.hlean index 7a69dbe..9f4ece2 100644 --- a/homotopy/degree.hlean +++ b/homotopy/degree.hlean @@ -59,6 +59,10 @@ namespace sphere attribute untrunc_of_is_trunc [unfold 4] definition surf_eq_loop : @surf 1 = circle.loop := sorry +/- + Favonia had a good idea, which he got from Ulrik: use the cogroup structure on the suspension to construct a group structure on ΣX →* Y, from which you can easily show that deg(id) = 1. See in the Agda library the files cogroup, cohspace and Group/LoopSuspAdjoint (or something) +-/ + -- definition π2S2_surf : π2S2 (tr surf) = 1 :> ℤ := -- begin diff --git a/move_to_lib.hlean b/move_to_lib.hlean index 5e7e23f..6c65c6c 100644 --- a/move_to_lib.hlean +++ b/move_to_lib.hlean @@ -19,6 +19,10 @@ le_step_left > le_of_succ_le pmap.eta > pmap_eta pType.sigma_char' > pType.sigma_char cghomotopy_group to aghomotopy_group +is_trunc_loop_of_is_trunc > is_trunc_loopn_of_is_trunc + + +first two arguments reordered in is_trunc_loopn_nat -/ namespace eq @@ -94,224 +98,11 @@ namespace trunc { exact sorry } end - definition ptrunctype.sigma_char [constructor] (n : ℕ₋₂) : - n-Type* ≃ Σ(X : Type*), is_trunc n X := - equiv.MK (λX, ⟨ptrunctype.to_pType X, _⟩) - (λX, ptrunctype.mk (carrier X.1) X.2 pt) - begin intro X, induction X with X HX, induction X, reflexivity end - begin intro X, induction X, reflexivity end - - definition is_embedding_ptrunctype_to_pType (n : ℕ₋₂) : is_embedding (@ptrunctype.to_pType n) := - begin - intro X Y, fapply is_equiv_of_equiv_of_homotopy, - { exact eq_equiv_fn_eq (ptrunctype.sigma_char n) _ _ ⬝e subtype_eq_equiv _ _ }, - intro p, induction p, reflexivity - end - - definition ptrunctype_eq_equiv {n : ℕ₋₂} (X Y : n-Type*) : (X = Y) ≃ (X ≃* Y) := - equiv.mk _ (is_embedding_ptrunctype_to_pType n X Y) ⬝e pType_eq_equiv X Y - - definition Prop_eq {P Q : Prop} (H : P ↔ Q) : P = Q := - tua (equiv_of_is_prop (iff.mp H) (iff.mpr H)) - - definition is_trunc_ptrunc_of_is_trunc [instance] [priority 500] (A : Type*) - (n m : ℕ₋₂) [H : is_trunc n A] : is_trunc n (ptrunc m A) := - is_trunc_trunc_of_is_trunc A n m - - definition ptrunc_pequiv_ptrunc_of_is_trunc {n m k : ℕ₋₂} {A : Type*} - (H1 : n ≤ m) (H2 : n ≤ k) (H : is_trunc n A) : ptrunc m A ≃* ptrunc k A := - have is_trunc m A, from is_trunc_of_le A H1, - have is_trunc k A, from is_trunc_of_le A H2, - pequiv.MK (ptrunc.elim _ (ptr k A)) (ptrunc.elim _ (ptr m A)) - abstract begin - refine !ptrunc_elim_pcompose⁻¹* ⬝* _, - exact ptrunc_elim_phomotopy _ !ptrunc_elim_ptr ⬝* !ptrunc_elim_ptr_phomotopy_pid, - end end - abstract begin - refine !ptrunc_elim_pcompose⁻¹* ⬝* _, - exact ptrunc_elim_phomotopy _ !ptrunc_elim_ptr ⬝* !ptrunc_elim_ptr_phomotopy_pid, - end end - - definition ptrunc_change_index {k l : ℕ₋₂} (p : k = l) (X : Type*) - : ptrunc k X ≃* ptrunc l X := - pequiv_ap (λ n, ptrunc n X) p - - definition ptrunc_functor_le {k l : ℕ₋₂} (p : l ≤ k) (X : Type*) - : ptrunc k X →* ptrunc l X := - have is_trunc k (ptrunc l X), from is_trunc_of_le _ p, - ptrunc.elim _ (ptr l X) - - definition trunc_index.pred [unfold 1] (n : ℕ₋₂) : ℕ₋₂ := - begin cases n with n, exact -2, exact n end - - /- A more general version of ptrunc_elim_phomotopy, where the proofs of truncatedness might be different -/ - definition ptrunc_elim_phomotopy2 [constructor] (k : ℕ₋₂) {A B : Type*} {f g : A →* B} (H₁ : is_trunc k B) - (H₂ : is_trunc k B) (p : f ~* g) : @ptrunc.elim k A B H₁ f ~* @ptrunc.elim k A B H₂ g := - begin - fapply phomotopy.mk, - { intro x, induction x with a, exact p a }, - { exact to_homotopy_pt p } - end - - definition pmap_ptrunc_equiv [constructor] (n : ℕ₋₂) (A B : Type*) [H : is_trunc n B] : - (ptrunc n A →* B) ≃ (A →* B) := - begin - fapply equiv.MK, - { intro g, exact g ∘* ptr n A }, - { exact ptrunc.elim n }, - { intro f, apply eq_of_phomotopy, apply ptrunc_elim_ptr }, - { intro g, apply eq_of_phomotopy, - exact ptrunc_elim_pcompose n g (ptr n A) ⬝* pwhisker_left g (ptrunc_elim_ptr_phomotopy_pid n A) ⬝* - pcompose_pid g } - end - - definition pmap_ptrunc_pequiv [constructor] (n : ℕ₋₂) (A B : Type*) [H : is_trunc n B] : - ppmap (ptrunc n A) B ≃* ppmap A B := - pequiv_of_equiv (pmap_ptrunc_equiv n A B) (eq_of_phomotopy (pconst_pcompose (ptr n A))) - - definition loopn_ptrunc_pequiv_nat (n : ℕ) (k : ℕ) (A : Type*) : - Ω[k] (ptrunc (n+k) A) ≃* ptrunc n (Ω[k] A) := - loopn_pequiv_loopn k (ptrunc_change_index (of_nat_add_of_nat n k)⁻¹ A) ⬝e* loopn_ptrunc_pequiv n k A - end trunc open trunc -namespace is_trunc - open trunc_index is_conn - - lemma is_trunc_loopn_nat (m n : ℕ) (A : Type*) [H : is_trunc (n + m) A] : - is_trunc n (Ω[m] A) := - @is_trunc_loopn n m A (transport (λk, is_trunc k _) (of_nat_add_of_nat n m)⁻¹ H) - - lemma is_trunc_loop_nat (n : ℕ) (A : Type*) [H : is_trunc (n + 1) A] : - is_trunc n (Ω A) := - is_trunc_loop A n - - definition is_trunc_of_eq {n m : ℕ₋₂} (p : n = m) {A : Type} (H : is_trunc n A) : is_trunc m A := - transport (λk, is_trunc k A) p H - - definition is_trunc_succ_succ_of_is_trunc_loop (n : ℕ₋₂) (A : Type*) (H : is_trunc (n.+1) (Ω A)) - (H2 : is_conn 0 A) : is_trunc (n.+2) A := - begin - apply is_trunc_succ_of_is_trunc_loop, apply minus_one_le_succ, - refine is_conn.elim -1 _ _, exact H - end - - lemma is_trunc_of_is_trunc_loopn (m n : ℕ) (A : Type*) (H : is_trunc n (Ω[m] A)) - (H2 : is_conn (m.-1) A) : is_trunc (m + n) A := - begin - revert A H H2; induction m with m IH: intro A H H2, - { rewrite [nat.zero_add], exact H }, - rewrite [succ_add], - apply is_trunc_succ_succ_of_is_trunc_loop, - { apply IH, - { apply is_trunc_equiv_closed _ !loopn_succ_in }, - apply is_conn_loop }, - exact is_conn_of_le _ (zero_le_of_nat m) - end - - lemma is_trunc_of_is_set_loopn (m : ℕ) (A : Type*) (H : is_set (Ω[m] A)) - (H2 : is_conn (m.-1) A) : is_trunc m A := - is_trunc_of_is_trunc_loopn m 0 A H H2 - - definition is_trunc_of_trivial_homotopy {n : ℕ} {m : ℕ₋₂} {A : Type} (H : is_trunc m A) - (H2 : Πk a, k > n → is_contr (π[k] (pointed.MK A a))) : is_trunc n A := - begin - fapply is_trunc_is_equiv_closed_rev, { exact @tr n A }, - apply whitehead_principle m, - { apply is_equiv_trunc_functor_of_is_conn_fun, - note z := is_conn_fun_tr n A, - apply is_conn_fun_of_le _ (of_nat_le_of_nat (zero_le n)), }, - intro a k, - apply @nat.lt_ge_by_cases n (k+1), - { intro H3, apply @is_equiv_of_is_contr, exact H2 _ _ H3, - refine @trivial_homotopy_group_of_is_trunc _ _ _ _ H3, apply is_trunc_trunc }, - { intro H3, apply @(is_equiv_π_of_is_connected _ H3), apply is_conn_fun_tr } - end - - definition is_trunc_of_trivial_homotopy_pointed {n : ℕ} {m : ℕ₋₂} {A : Type*} (H : is_trunc m A) - (Hconn : is_conn 0 A) (H2 : Πk, k > n → is_contr (π[k] A)) : is_trunc n A := - begin - apply is_trunc_of_trivial_homotopy H, - intro k a H3, revert a, apply is_conn.elim -1, - cases A with A a₀, exact H2 k H3 - end - - definition is_trunc_of_is_trunc_succ {n : ℕ} {A : Type} (H : is_trunc (n.+1) A) - (H2 : Πa, is_contr (π[n+1] (pointed.MK A a))) : is_trunc n A := - begin - apply is_trunc_of_trivial_homotopy H, - intro k a H3, induction H3 with k H3 IH, exact H2 a, - apply @trivial_homotopy_group_of_is_trunc _ (n+1) _ H, exact succ_le_succ H3 - end - - definition is_trunc_of_is_trunc_succ_pointed {n : ℕ} {A : Type*} (H : is_trunc (n.+1) A) - (Hconn : is_conn 0 A) (H2 : is_contr (π[n+1] A)) : is_trunc n A := - begin - apply is_trunc_of_trivial_homotopy_pointed H Hconn, - intro k H3, induction H3 with k H3 IH, exact H2, - apply @trivial_homotopy_group_of_is_trunc _ (n+1) _ H, exact succ_le_succ H3 - end - -end is_trunc namespace sigma open sigma.ops - -definition sigma_functor2 [constructor] {A₁ A₂ A₃ : Type} - {B₁ : A₁ → Type} {B₂ : A₂ → Type} {B₃ : A₃ → Type} - (f : A₁ → A₂ → A₃) (g : Π⦃a₁ a₂⦄, B₁ a₁ → B₂ a₂ → B₃ (f a₁ a₂)) - (x₁ : Σa₁, B₁ a₁) (x₂ : Σa₂, B₂ a₂) : Σa₃, B₃ a₃ := -⟨f x₁.1 x₂.1, g x₁.2 x₂.2⟩ - -definition eq.rec_sigma {A : Type} {B : A → Type} {a : A} {b : B a} - (P : Π⦃a'⦄ {b' : B a'}, ⟨a, b⟩ = ⟨a', b'⟩ → Type) - (IH : P idp) ⦃a' : A⦄ {b' : B a'} (p : ⟨a, b⟩ = ⟨a', b'⟩) : P p := -begin - apply transport (λp, P p) (to_left_inv !sigma_eq_equiv p), - generalize !sigma_eq_equiv p, esimp, intro q, - induction q with q₁ q₂, induction q₂, exact IH -end - - definition ap_dpair_eq_dpair_pr {A A' : Type} {B : A → Type} {a a' : A} {b : B a} {b' : B a'} (f : Πa, B a → A') (p : a = a') (q : b =[p] b') - : ap (λx, f x.1 x.2) (dpair_eq_dpair p q) = apd011 f p q := - by induction q; reflexivity - - definition sigma_eq_equiv_of_is_prop_right [constructor] {A : Type} {B : A → Type} (u v : Σa, B a) - [H : Π a, is_prop (B a)] : u = v ≃ u.1 = v.1 := - !sigma_eq_equiv ⬝e !sigma_equiv_of_is_contr_right - - definition ap_sigma_pr1 {A B : Type} {C : B → Type} {a₁ a₂ : A} (f : A → B) (g : Πa, C (f a)) - (p : a₁ = a₂) : (ap (λa, ⟨f a, g a⟩) p)..1 = ap f p := - by induction p; reflexivity - - definition ap_sigma_pr2 {A B : Type} {C : B → Type} {a₁ a₂ : A} (f : A → B) (g : Πa, C (f a)) - (p : a₁ = a₂) : (ap (λa, ⟨f a, g a⟩) p)..2 = - change_path (ap_sigma_pr1 f g p)⁻¹ (pathover_ap C f (apd g p)) := - by induction p; reflexivity - -definition ap_sigma_functor_sigma_eq {A A' : Type} {B : A → Type} {B' : A' → Type} - {a a' : A} {b : B a} {b' : B a'} (f : A → A') (g : Πa, B a → B' (f a)) (p : a = a') (q : b =[p] b') : - ap (sigma_functor f g) (sigma_eq p q) = sigma_eq (ap f p) (pathover_ap B' f (apo g q)) := -by induction q; reflexivity - -definition ap_sigma_functor_id_sigma_eq {A : Type} {B B' : A → Type} - {a a' : A} {b : B a} {b' : B a'} (g : Πa, B a → B' a) (p : a = a') (q : b =[p] b') : - ap (sigma_functor id g) (sigma_eq p q) = sigma_eq p (apo g q) := -by induction q; reflexivity - -definition sigma_eq_pr2_constant {A B : Type} {a a' : A} {b b' : B} (p : a = a') - (q : b =[p] b') : ap pr2 (sigma_eq p q) = (eq_of_pathover q) := -by induction q; reflexivity - -definition sigma_eq_pr2_constant2 {A B : Type} {a a' : A} {b b' : B} (p : a = a') - (q : b = b') : ap pr2 (sigma_eq p (pathover_of_eq p q)) = q := -by induction p; induction q; reflexivity - -definition sigma_eq_concato_eq {A : Type} {B : A → Type} {a a' : A} {b : B a} {b₁ b₂ : B a'} - (p : a = a') (q : b =[p] b₁) (q' : b₁ = b₂) : sigma_eq p (q ⬝op q') = sigma_eq p q ⬝ ap (dpair a') q' := -by induction q'; reflexivity - - -- open sigma.ops -- definition eq.rec_sigma {A : Type} {B : A → Type} {a₀ : A} {b₀ : B a₀} -- {P : Π(a : A) (b : B a), ⟨a₀, b₀⟩ = ⟨a, b⟩ → Type} (H : P a₀ b₀ idp) {a : A} {b : B a} @@ -332,6 +123,60 @@ by induction q'; reflexivity -- end --rexact @(ap pathover_pr1) _ idpo _, + definition sigma_functor2 [constructor] {A₁ A₂ A₃ : Type} + {B₁ : A₁ → Type} {B₂ : A₂ → Type} {B₃ : A₃ → Type} + (f : A₁ → A₂ → A₃) (g : Π⦃a₁ a₂⦄, B₁ a₁ → B₂ a₂ → B₃ (f a₁ a₂)) + (x₁ : Σa₁, B₁ a₁) (x₂ : Σa₂, B₂ a₂) : Σa₃, B₃ a₃ := + ⟨f x₁.1 x₂.1, g x₁.2 x₂.2⟩ + + definition eq.rec_sigma {A : Type} {B : A → Type} {a : A} {b : B a} + (P : Π⦃a'⦄ {b' : B a'}, ⟨a, b⟩ = ⟨a', b'⟩ → Type) + (IH : P idp) ⦃a' : A⦄ {b' : B a'} (p : ⟨a, b⟩ = ⟨a', b'⟩) : P p := + begin + apply transport (λp, P p) (to_left_inv !sigma_eq_equiv p), + generalize !sigma_eq_equiv p, esimp, intro q, + induction q with q₁ q₂, induction q₂, exact IH + end + + definition ap_dpair_eq_dpair_pr {A A' : Type} {B : A → Type} {a a' : A} {b : B a} {b' : B a'} (f : Πa, B a → A') (p : a = a') (q : b =[p] b') + : ap (λx, f x.1 x.2) (dpair_eq_dpair p q) = apd011 f p q := + by induction q; reflexivity + + definition sigma_eq_equiv_of_is_prop_right [constructor] {A : Type} {B : A → Type} (u v : Σa, B a) + [H : Π a, is_prop (B a)] : u = v ≃ u.1 = v.1 := + !sigma_eq_equiv ⬝e !sigma_equiv_of_is_contr_right + + definition ap_sigma_pr1 {A B : Type} {C : B → Type} {a₁ a₂ : A} (f : A → B) (g : Πa, C (f a)) + (p : a₁ = a₂) : (ap (λa, ⟨f a, g a⟩) p)..1 = ap f p := + by induction p; reflexivity + + definition ap_sigma_pr2 {A B : Type} {C : B → Type} {a₁ a₂ : A} (f : A → B) (g : Πa, C (f a)) + (p : a₁ = a₂) : (ap (λa, ⟨f a, g a⟩) p)..2 = + change_path (ap_sigma_pr1 f g p)⁻¹ (pathover_ap C f (apd g p)) := + by induction p; reflexivity + + definition ap_sigma_functor_sigma_eq {A A' : Type} {B : A → Type} {B' : A' → Type} + {a a' : A} {b : B a} {b' : B a'} (f : A → A') (g : Πa, B a → B' (f a)) (p : a = a') (q : b =[p] b') : + ap (sigma_functor f g) (sigma_eq p q) = sigma_eq (ap f p) (pathover_ap B' f (apo g q)) := + by induction q; reflexivity + + definition ap_sigma_functor_id_sigma_eq {A : Type} {B B' : A → Type} + {a a' : A} {b : B a} {b' : B a'} (g : Πa, B a → B' a) (p : a = a') (q : b =[p] b') : + ap (sigma_functor id g) (sigma_eq p q) = sigma_eq p (apo g q) := + by induction q; reflexivity + + definition sigma_eq_pr2_constant {A B : Type} {a a' : A} {b b' : B} (p : a = a') + (q : b =[p] b') : ap pr2 (sigma_eq p q) = (eq_of_pathover q) := + by induction q; reflexivity + + definition sigma_eq_pr2_constant2 {A B : Type} {a a' : A} {b b' : B} (p : a = a') + (q : b = b') : ap pr2 (sigma_eq p (pathover_of_eq p q)) = q := + by induction p; induction q; reflexivity + + definition sigma_eq_concato_eq {A : Type} {B : A → Type} {a a' : A} {b : B a} {b₁ b₂ : B a'} + (p : a = a') (q : b =[p] b₁) (q' : b₁ = b₂) : sigma_eq p (q ⬝op q') = sigma_eq p q ⬝ ap (dpair a') q' := + by induction q'; reflexivity + definition sigma_functor_compose {A A' A'' : Type} {B : A → Type} {B' : A' → Type} {B'' : A'' → Type} {f' : A' → A''} {f : A → A'} (g' : Πa, B' a → B'' (f' a)) (g : Πa, B a → B' (f a)) (x : Σa, B a) : @@ -359,26 +204,26 @@ by induction q'; reflexivity sigma_functor_homotopy h k x ⬝ (sigma_functor_compose g₁₂ g₀₁ x)⁻¹ -definition sigma_equiv_of_is_embedding_left_fun [constructor] {X Y : Type} {P : Y → Type} - {f : X → Y} (H : Πy, P y → fiber f y) (v : Σy, P y) : Σx, P (f x) := -⟨fiber.point (H v.1 v.2), transport P (point_eq (H v.1 v.2))⁻¹ v.2⟩ + definition sigma_equiv_of_is_embedding_left_fun [constructor] {X Y : Type} {P : Y → Type} + {f : X → Y} (H : Πy, P y → fiber f y) (v : Σy, P y) : Σx, P (f x) := + ⟨fiber.point (H v.1 v.2), transport P (point_eq (H v.1 v.2))⁻¹ v.2⟩ -definition sigma_equiv_of_is_embedding_left_prop [constructor] {X Y : Type} {P : Y → Type} - (f : X → Y) (Hf : is_embedding f) (HP : Πx, is_prop (P (f x))) (H : Πy, P y → fiber f y) : - (Σy, P y) ≃ Σx, P (f x) := -begin - apply equiv.MK (sigma_equiv_of_is_embedding_left_fun H) (sigma_functor f (λa, id)), - { intro v, induction v with x p, esimp [sigma_equiv_of_is_embedding_left_fun], - fapply sigma_eq, apply @is_injective_of_is_embedding _ _ f, exact point_eq (H (f x) p), - apply is_prop.elimo }, - { intro v, induction v with y p, esimp, fapply sigma_eq, exact point_eq (H y p), - apply tr_pathover } -end + definition sigma_equiv_of_is_embedding_left_prop [constructor] {X Y : Type} {P : Y → Type} + (f : X → Y) (Hf : is_embedding f) (HP : Πx, is_prop (P (f x))) (H : Πy, P y → fiber f y) : + (Σy, P y) ≃ Σx, P (f x) := + begin + apply equiv.MK (sigma_equiv_of_is_embedding_left_fun H) (sigma_functor f (λa, id)), + { intro v, induction v with x p, esimp [sigma_equiv_of_is_embedding_left_fun], + fapply sigma_eq, apply @is_injective_of_is_embedding _ _ f, exact point_eq (H (f x) p), + apply is_prop.elimo }, + { intro v, induction v with y p, esimp, fapply sigma_eq, exact point_eq (H y p), + apply tr_pathover } + end -definition sigma_equiv_of_is_embedding_left_contr [constructor] {X Y : Type} {P : Y → Type} - (f : X → Y) (Hf : is_embedding f) (HP : Πx, is_contr (P (f x))) (H : Πy, P y → fiber f y) : - (Σy, P y) ≃ X := -sigma_equiv_of_is_embedding_left_prop f Hf _ H ⬝e !sigma_equiv_of_is_contr_right + definition sigma_equiv_of_is_embedding_left_contr [constructor] {X Y : Type} {P : Y → Type} + (f : X → Y) (Hf : is_embedding f) (HP : Πx, is_contr (P (f x))) (H : Πy, P y → fiber f y) : + (Σy, P y) ≃ X := + sigma_equiv_of_is_embedding_left_prop f Hf _ H ⬝e !sigma_equiv_of_is_contr_right end sigma open sigma