From 73a34e9edf8f949ac6ac7479a65e0be8250a3780 Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Sun, 21 May 2017 00:39:30 -0400 Subject: [PATCH] finish construction of exact couple from a sequence of spectrum maps --- algebra/arrow_group.hlean | 6 - algebra/cogroup.hlean | 41 ----- algebra/graded.hlean | 47 ----- algebra/is_short_exact.hlean | 22 ++- algebra/module_exact_couple.hlean | 113 +++--------- homotopy/spectrum.hlean | 4 +- move_to_lib.hlean | 287 ++++++++++++++++++++++++++++-- pointed.hlean | 4 +- 8 files changed, 313 insertions(+), 211 deletions(-) diff --git a/algebra/arrow_group.hlean b/algebra/arrow_group.hlean index e73784a..7cfa23d 100644 --- a/algebra/arrow_group.hlean +++ b/algebra/arrow_group.hlean @@ -3,12 +3,6 @@ open pi pointed algebra group eq equiv is_trunc trunc namespace group - -- definition pmap_mul [constructor] {A B : Type*} [inf_pgroup B] (f g : A →* B) : A →* B := - -- pmap.mk (λa, f a * g a) (ap011 mul (respect_pt f) (respect_pt g) ⬝ !one_mul) - - -- definition pmap_inv [constructor] {A B : Type*} [inf_pgroup B] (f : A →* B) : A →* B := - -- pmap.mk (λa, (f a)⁻¹) (ap inv (respect_pt f) ⬝ !one_inv) - definition pmap_mul [constructor] {A B : Type*} (f g : A →* Ω B) : A →* Ω B := pmap.mk (λa, f a ⬝ g a) (respect_pt f ◾ respect_pt g ⬝ !idp_con) diff --git a/algebra/cogroup.hlean b/algebra/cogroup.hlean index d500a3c..c1256b6 100644 --- a/algebra/cogroup.hlean +++ b/algebra/cogroup.hlean @@ -3,46 +3,6 @@ import algebra.group_theory ..pointed ..homotopy.smash open eq pointed algebra group eq equiv is_trunc is_conn prod prod.ops smash susp unit pushout trunc prod --- should be in pushout -section -parameters {TL BL TR : Type} (f : TL → BL) (g : TL → TR) - -protected theorem pushout.elim_inl {P : Type} (Pinl : BL → P) (Pinr : TR → P) - (Pglue : Π(x : TL), Pinl (f x) = Pinr (g x)) {b b' : BL} (p : b = b') - : ap (pushout.elim Pinl Pinr Pglue) (ap inl p) = ap Pinl p := -by cases p; reflexivity - -protected theorem pushout.elim_inr {P : Type} (Pinl : BL → P) (Pinr : TR → P) - (Pglue : Π(x : TL), Pinl (f x) = Pinr (g x)) {b b' : TR} (p : b = b') - : ap (pushout.elim Pinl Pinr Pglue) (ap inr p) = ap Pinr p := -by cases p; reflexivity - -end - --- should be in prod -definition prod.pair_eq_eta {A B : Type} {u v : A × B} - (p : u = v) : pair_eq (p..1) (p..2) = prod.eta u ⬝ p ⬝ (prod.eta v)⁻¹ := -by induction p; induction u; reflexivity - -definition prod.prod_eq_eq {A B : Type} {u v : A × B} - {p₁ q₁ : u.1 = v.1} {p₂ q₂ : u.2 = v.2} (α₁ : p₁ = q₁) (α₂ : p₂ = q₂) - : prod_eq p₁ p₂ = prod_eq q₁ q₂ := -by cases α₁; cases α₂; reflexivity - -definition prod.prod_eq_assemble {A B : Type} {u v : A × B} - {p q : u = v} (α₁ : p..1 = q..1) (α₂ : p..2 = q..2) : p = q := -(prod_eq_eta p)⁻¹ ⬝ prod.prod_eq_eq α₁ α₂ ⬝ prod_eq_eta q - -definition prod.eq_pr1_concat {A B : Type} {u v w : A × B} - (p : u = v) (q : v = w) - : (p ⬝ q)..1 = p..1 ⬝ q..1 := -by cases q; reflexivity - -definition prod.eq_pr2_concat {A B : Type} {u v w : A × B} - (p : u = v) (q : v = w) - : (p ⬝ q)..2 = p..2 ⬝ q..2 := -by cases q; reflexivity - section variables {A B C : Type*} @@ -258,4 +218,3 @@ end -/ end group - diff --git a/algebra/graded.hlean b/algebra/graded.hlean index f0939a3..40df902 100644 --- a/algebra/graded.hlean +++ b/algebra/graded.hlean @@ -6,53 +6,6 @@ import .left_module .direct_sum .submodule --..heq open is_trunc algebra eq left_module pointed function equiv is_equiv prod group sigma nat --- move - lemma le_sub_of_add_le {n m k : ℕ} (h : n + m ≤ k) : n ≤ k - m := - begin - induction h with k h IH, - { exact le_of_eq !nat.add_sub_cancel⁻¹ }, - { exact le.trans IH (nat.sub_le_sub_right !self_le_succ _) } - end - - lemma iterate_sub {A : Type} (f : A ≃ A) {n m : ℕ} (h : n ≥ m) (a : A) : - iterate f (n - m) a = iterate f n (iterate f⁻¹ m a) := - begin - revert n h, induction m with m p: intro n h, - { reflexivity }, - { cases n with n, exfalso, apply not_succ_le_zero _ h, - rewrite [succ_sub_succ], refine p n (le_of_succ_le_succ h) ⬝ _, - refine ap (_^[n]) _ ⬝ !iterate_succ⁻¹, exact !to_right_inv⁻¹ } - end - - definition iterate_commute {A : Type} {f g : A → A} (n : ℕ) (h : f ∘ g ~ g ∘ f) : - iterate f n ∘ g ~ g ∘ iterate f n := - by induction n with n IH; reflexivity; exact λx, ap f (IH x) ⬝ !h - - -- definition iterate_left_inv {A : Type} (f : A ≃ A) (n : ℕ) : Πa, f⁻¹ᵉ^[n] (f^[n] a) = a := - -- begin - -- induction n with n p: intro a, - -- reflexivity, - -- exact ap f⁻¹ᵉ (ap (f⁻¹ᵉ^[n]) (iterate_succ f n a) ⬝ p (f a)) ⬝ left_inv f a, - -- end - - definition iterate_equiv {A : Type} (f : A ≃ A) (n : ℕ) : A ≃ A := - equiv.mk (iterate f n) - (by induction n with n IH; apply is_equiv_id; exact is_equiv_compose f (iterate f n)) - - definition iterate_inv {A : Type} (f : A ≃ A) (n : ℕ) : - (iterate_equiv f n)⁻¹ ~ iterate f⁻¹ n := - begin - induction n with n p: intro a, - reflexivity, - exact p (f⁻¹ a) ⬝ !iterate_succ⁻¹ - end - - definition iterate_left_inv {A : Type} (f : A ≃ A) (n : ℕ) (a : A) : f⁻¹ᵉ^[n] (f^[n] a) = a := - (iterate_inv f n (f^[n] a))⁻¹ ⬝ to_left_inv (iterate_equiv f n) a - - definition iterate_right_inv {A : Type} (f : A ≃ A) (n : ℕ) (a : A) : f^[n] (f⁻¹ᵉ^[n] a) = a := - ap (f^[n]) (iterate_inv f n a)⁻¹ ⬝ to_right_inv (iterate_equiv f n) a - namespace left_module definition graded [reducible] (str : Type) (I : Type) : Type := I → str diff --git a/algebra/is_short_exact.hlean b/algebra/is_short_exact.hlean index 88f2608..d9f7950 100644 --- a/algebra/is_short_exact.hlean +++ b/algebra/is_short_exact.hlean @@ -21,7 +21,7 @@ structure is_short_exact_t {A B : Type} {C : Type*} (f : A → B) (g : B → C) (ker_in_im : Π(b:B), (g b = pt) → fiber f b) (is_surj : is_split_surjective g) -definition is_short_exact_of_is_exact {X A B C Y : Group} +lemma is_short_exact_of_is_exact {X A B C Y : Group} (k : X →g A) (f : A →g B) (g : B →g C) (l : C →g Y) (hX : is_contr X) (hY : is_contr Y) (kf : is_exact k f) (fg : is_exact f g) (gl : is_exact g l) : is_short_exact f g := @@ -35,15 +35,23 @@ begin { intro c, exact is_exact.ker_in_im gl c !is_prop.elim }, end -definition is_short_exact_equiv {A B A' B' : Type} {C C' : Type*} +lemma is_short_exact_equiv {A B A' B' : Type} {C C' : Type*} {f' : A' → B'} {g' : B' → C'} (f : A → B) (g : B → C) (eA : A ≃ A') (eB : B ≃ B') (eC : C ≃* C') - (h : hsquare f f' eA eB) (h : hsquare g g' eB eC) + (h₁ : hsquare f f' eA eB) (h₂ : hsquare g g' eB eC) (H : is_short_exact f' g') : is_short_exact f g := begin constructor, - { exact sorry }, - { exact sorry }, - { exact sorry }, - { exact sorry } + { apply is_embedding_homotopy_closed_rev (homotopy_top_of_hsquare h₁), + apply is_embedding_compose, apply is_embedding_of_is_equiv, + apply is_embedding_compose, apply is_short_exact.is_emb H, apply is_embedding_of_is_equiv }, + { intro a, refine homotopy_top_of_hsquare' (hhconcat h₁ h₂) a ⬝ _, + refine ap eC⁻¹ _ ⬝ respect_pt eC⁻¹ᵉ*, exact is_short_exact.im_in_ker H (eA a) }, + { intro b p, note q := eq_of_inv_eq ((homotopy_top_of_hsquare' h₂ b)⁻¹ ⬝ p) ⬝ respect_pt eC, + induction is_short_exact.ker_in_im H (eB b) q with a' r, + apply image.mk (eA⁻¹ a'), + exact eq_of_fn_eq_fn eB ((homotopy_top_of_hsquare h₁⁻¹ʰᵗʸᵛ a')⁻¹ ⬝ r) }, + { apply is_surjective_homotopy_closed_rev (homotopy_top_of_hsquare' h₂), + apply is_surjective_compose, apply is_surjective_of_is_equiv, + apply is_surjective_compose, apply is_short_exact.is_surj H, apply is_surjective_of_is_equiv } end diff --git a/algebra/module_exact_couple.hlean b/algebra/module_exact_couple.hlean index 3a04c8b..257b57e 100644 --- a/algebra/module_exact_couple.hlean +++ b/algebra/module_exact_couple.hlean @@ -6,83 +6,6 @@ import .graded ..homotopy.spectrum .product_group open algebra is_trunc left_module is_equiv equiv eq function nat --- move -section - open group int chain_complex pointed succ_str - - definition is_exact_of_is_exact_at {N : succ_str} {A : chain_complex N} {n : N} - (H : is_exact_at A n) : is_exact (cc_to_fn A (S n)) (cc_to_fn A n) := - is_exact.mk (cc_is_chain_complex A n) H - - definition is_equiv_mul_right [constructor] {A : Group} (a : A) : is_equiv (λb, b * a) := - adjointify _ (λb : A, b * a⁻¹) (λb, !inv_mul_cancel_right) (λb, !mul_inv_cancel_right) - - definition right_action [constructor] {A : Group} (a : A) : A ≃ A := - equiv.mk _ (is_equiv_mul_right a) - - definition is_equiv_add_right [constructor] {A : AddGroup} (a : A) : is_equiv (λb, b + a) := - adjointify _ (λb : A, b - a) (λb, !neg_add_cancel_right) (λb, !add_neg_cancel_right) - - definition add_right_action [constructor] {A : AddGroup} (a : A) : A ≃ A := - equiv.mk _ (is_equiv_add_right a) - - - section - variables {A B : Type} (f : A ≃ B) [ab_group A] - - -- to group - definition group_equiv_mul_comm (b b' : B) : group_equiv_mul f b b' = group_equiv_mul f b' b := - by rewrite [↑group_equiv_mul, mul.comm] - - definition ab_group_equiv_closed : ab_group B := - ⦃ab_group, group_equiv_closed f, - mul_comm := group_equiv_mul_comm f⦄ - end - - definition ab_group_of_is_contr (A : Type) [is_contr A] : ab_group A := - have ab_group unit, from ab_group_unit, - ab_group_equiv_closed (equiv_unit_of_is_contr A)⁻¹ᵉ - - definition group_of_is_contr (A : Type) [is_contr A] : group A := - have ab_group A, from ab_group_of_is_contr A, by apply _ - - definition ab_group_lift_unit : ab_group (lift unit) := - ab_group_of_is_contr (lift unit) - - definition trivial_ab_group_lift : AbGroup := - AbGroup.mk _ ab_group_lift_unit - - definition homomorphism_of_is_contr_right (A : Group) {B : Type} (H : is_contr B) : - A →g Group.mk B (group_of_is_contr B) := - group.homomorphism.mk (λa, center _) (λa a', !is_prop.elim) - - open trunc pointed is_conn - definition ab_group_homotopy_group_of_is_conn (n : ℕ) (A : Type*) [H : is_conn 1 A] : ab_group (π[n] A) := - begin - have is_conn 0 A, from !is_conn_of_is_conn_succ, - cases n with n, - { unfold [homotopy_group, ptrunc], apply ab_group_of_is_contr }, - cases n with n, - { unfold [homotopy_group, ptrunc], apply ab_group_of_is_contr }, - exact ab_group_homotopy_group n A - end - -end - -namespace int /- move to int-/ - definition max0 : ℤ → ℕ - | (of_nat n) := n - | (-[1+ n]) := 0 - - lemma le_max0 : Π(n : ℤ), n ≤ of_nat (max0 n) - | (of_nat n) := proof le.refl n qed - | (-[1+ n]) := proof unit.star qed - - lemma le_of_max0_le {n : ℤ} {m : ℕ} (h : max0 n ≤ m) : n ≤ of_nat m := - le.trans (le_max0 n) (of_nat_le_of_nat_of_le h) - -end int - /- exact couples -/ namespace left_module @@ -403,7 +326,7 @@ namespace left_module lemma rb0 (n : ℕ) : r n ≥ n + 1 := ge.trans !le_max_left (ge.trans !le_max_left !le_add_left) lemma rb1 (n : ℕ) : B (deg (j X) (deg (k X) x)) ≤ r n - (n + 1) := - le_sub_of_add_le (le.trans !le_max_left !le_max_left) + nat.le_sub_of_add_le (le.trans !le_max_left !le_max_left) lemma rb2 (n : ℕ) : B3 ((deg (i X))^[n] x) ≤ r n := le.trans !le_max_right !le_max_left lemma rb3 (n : ℕ) : B' (deg (k X) ((deg (i X))^[n] x)) ≤ r n := @@ -471,7 +394,7 @@ namespace pointed | (of_nat n) A := homotopy_group_conn_nat n A | (-[1+ n]) A := trivial_ab_group_lift - notation `πag'[`:95 n:0 `]`:0 := homotopy_group_conn n + notation `πc[`:95 n:0 `]`:0 := homotopy_group_conn n definition homotopy_group_conn_nat_functor (n : ℕ) {A B : Type*[1]} (f : A →* B) : homotopy_group_conn_nat n A →g homotopy_group_conn_nat n B := @@ -481,7 +404,7 @@ namespace pointed exact π→g[n+2] f end - definition homotopy_group_conn_functor : Π(n : ℤ) {A B : Type*[1]} (f : A →* B), πag'[n] A →g πag'[n] B + definition homotopy_group_conn_functor : Π(n : ℤ) {A B : Type*[1]} (f : A →* B), πc[n] A →g πc[n] B | (of_nat n) A B f := homotopy_group_conn_nat_functor n f | (-[1+ n]) A B f := homomorphism_of_is_contr_right _ _ @@ -494,10 +417,10 @@ namespace pointed definition I [constructor] : Set := trunctype.mk (ℤ × ℤ) !is_trunc_prod definition D_sequence : graded_module rℤ I := - λv, LeftModule_int_of_AbGroup (πag'[v.2] (A (v.1))) + λv, LeftModule_int_of_AbGroup (πc[v.2] (A (v.1))) definition E_sequence : graded_module rℤ I := - λv, LeftModule_int_of_AbGroup (πag'[v.2] (pconntype.mk (pfiber (f (v.1))) !Hf pt)) + λv, LeftModule_int_of_AbGroup (πc[v.2] (pconntype.mk (pfiber (f (v.1))) !Hf pt)) -- definition exact_couple_sequence : exact_couple rℤ I := -- exact_couple.mk D_sequence E_sequence sorry sorry sorry sorry sorry sorry @@ -530,15 +453,20 @@ namespace spectrum exact πₛ→[v.1] (f v.2) end - definition j_sequence : D_sequence →gm E_sequence := + definition deg_j_seq_inv [constructor] : I ≃ I := + prod_equiv_prod (add_right_action 1) (add_right_action (- 1)) + + definition fn_j_sequence [unfold 3] (x : I) : + D_sequence (deg_j_seq_inv x) →lm E_sequence x := begin - fapply graded_hom.mk_out', - exact (prod_equiv_prod (add_right_action 1) (add_right_action (- 1))), - intro v, induction v with n s, + induction x with n s, apply lm_hom_int.mk, esimp, rexact shomotopy_groups_fun (f s) (n, 2) end + definition j_sequence : D_sequence →gm E_sequence := + graded_hom.mk_out deg_j_seq_inv⁻¹ᵉ fn_j_sequence + definition k_sequence : E_sequence →gm D_sequence := begin fapply graded_hom.mk erfl, @@ -558,7 +486,7 @@ namespace spectrum revert t q, refine eq.rec_equiv (add_right_action (- 1)) _, induction p using eq.rec_symm, apply is_exact_homotopy homotopy.rfl, - { symmetry, intro, apply graded_hom_mk_out'_left_inv }, + { symmetry, intro m, exact graded_hom_mk_out_right_inv deg_j_seq_inv⁻¹ᵉ fn_j_sequence m }, rexact is_exact_of_is_exact_at (is_exact_LES_of_shomotopy_groups (f s) (m, 2)), end @@ -568,7 +496,7 @@ namespace spectrum revert x y p, refine eq.rec_right_inv (deg j_sequence) _, intro x, induction x with n s, apply is_exact_homotopy, - { symmetry, intro, apply graded_hom_mk_out'_left_inv }, + { symmetry, intro m, exact graded_hom_mk_out_right_inv deg_j_seq_inv⁻¹ᵉ fn_j_sequence m }, { reflexivity }, rexact is_exact_of_is_exact_at (is_exact_LES_of_shomotopy_groups (f s) (n, 1)), end @@ -651,4 +579,13 @@ namespace spectrum end +-- Uncomment the next line to see that the proof uses univalence, but that there are no holes +--('sorry') in the proof: + +-- print axioms is_bounded_sequence + +-- I think it depends on univalence in an essential way. The reason is that the long exact sequence +-- of homotopy groups already depends on univalence. Namely, in that proof we need to show that if f +-- : A → B and g : B → C are exact at B, then ∥A∥₀ → ∥B∥₀ → ∥C∥₀ is exact at ∥B∥₀. For this we need +-- that the equality |b|₀ = |b'|₀ is equivalent to ∥b = b'∥₋₁, which requires univalence. end spectrum diff --git a/homotopy/spectrum.hlean b/homotopy/spectrum.hlean index 3236768..9e84cfa 100644 --- a/homotopy/spectrum.hlean +++ b/homotopy/spectrum.hlean @@ -243,7 +243,7 @@ namespace spectrum definition sfiber {N : succ_str} {X Y : gen_spectrum N} (f : X →ₛ Y) : gen_spectrum N := spectrum.MK (λn, pfiber (f n)) - (λn, pfiber_loop_space (f (S n)) ∘*ᵉ pfiber_equiv_of_square _ _ (sglue_square f n)) + (λn, (loop_pfiber (f (S n)))⁻¹ᵉ* ∘*ᵉ pfiber_equiv_of_square _ _ (sglue_square f n)) /- the map from the fiber to the domain -/ definition spoint {N : succ_str} {X Y : gen_spectrum N} (f : X →ₛ Y) : sfiber f →ₛ X := @@ -251,7 +251,7 @@ namespace spectrum begin intro n, refine _ ⬝* !passoc, - refine _ ⬝* pwhisker_right _ !ap1_ppoint_phomotopy⁻¹*, + refine _ ⬝* pwhisker_right _ !ppoint_loop_pfiber_inv⁻¹*, rexact (pfiber_equiv_of_square_ppoint (equiv_glue X n) (equiv_glue Y n) (sglue_square f n))⁻¹* end diff --git a/move_to_lib.hlean b/move_to_lib.hlean index fb23564..608d047 100644 --- a/move_to_lib.hlean +++ b/move_to_lib.hlean @@ -10,6 +10,7 @@ attribute is_prop.elim_set [unfold 6] definition add_comm_right {A : Type} [add_comm_semigroup A] (n m k : A) : n + m + k = n + k + m := !add.assoc ⬝ ap (add n) !add.comm ⬝ !add.assoc⁻¹ +-- move to chain_complex (or another file). rename chain_complex.is_exact structure is_exact_t {A B : Type} {C : Type*} (f : A → B) (g : B → C) := ( im_in_ker : Π(a:A), g (f a) = pt) ( ker_in_im : Π(b:B), (g b = pt) → fiber f b) @@ -50,6 +51,13 @@ definition is_surjective_of_is_exact_of_is_contr {A B : Type} {C : Type*} {f : A (H : is_exact f g) [is_contr C] : is_surjective f := λb, is_exact.ker_in_im H b !is_prop.elim +section chain_complex +open succ_str chain_complex +definition is_exact_of_is_exact_at {N : succ_str} {A : chain_complex N} {n : N} + (H : is_exact_at A n) : is_exact (cc_to_fn A (S n)) (cc_to_fn A n) := +is_exact.mk (cc_is_chain_complex A n) H +end chain_complex + namespace algebra definition ab_group_unit [constructor] : ab_group unit := ⦃ab_group, trivial_group, mul_comm := λx y, idp⦄ @@ -109,16 +117,12 @@ namespace eq intro a₀ p, exact eq.rec_to (right_inv f a₀) (H a₀) p, end - definition eq.rec_equiv {A B : Type} {a₀ : A} (f : A ≃ B) {P : Π⦃a₁⦄, f a₀ = f a₁ → Type} + definition eq.rec_equiv {A B : Type} {a₀ : A} (f : A ≃ B) {P : Π{a₁}, f a₀ = f a₁ → Type} (H : P (idpath (f a₀))) ⦃a₁ : A⦄ (p : f a₀ = f a₁) : P p := begin --- induction f using equiv.rec_on_ua_idp, esimp at *, induction p, exact H - revert a₁ p, refine equiv_rect f⁻¹ᵉ _ _, intro b p, - refine transport (@P _) (!con_inv_cancel_right) _, - exact b, exact right_inv f b, - generalize p ⬝ right_inv f b, - clear p, intro q, induction q, - exact sorry + assert qr : Σ(q : a₀ = a₁), ap f q = p, + { exact ⟨eq_of_fn_eq_fn f p, ap_eq_of_fn_eq_fn' f p⟩ }, + cases qr with q r, apply transport P r, induction q, exact H end definition eq.rec_symm {A : Type} {a₀ : A} {P : Π⦃a₁⦄, a₁ = a₀ → Type} @@ -404,6 +408,14 @@ end definition homotopy_of_hsquare (p : hsquare f₁₀ f₁₂ f₀₁ f₂₁) : f₂₁ ∘ f₁₀ ~ f₁₂ ∘ f₀₁ := p + definition homotopy_top_of_hsquare {f₂₁ : A₂₀ ≃ A₂₂} (p : hsquare f₁₀ f₁₂ f₀₁ f₂₁) : + f₁₀ ~ f₂₁⁻¹ ∘ f₁₂ ∘ f₀₁ := + homotopy_inv_of_homotopy_post _ _ _ p + + definition homotopy_top_of_hsquare' [is_equiv f₂₁] (p : hsquare f₁₀ f₁₂ f₀₁ f₂₁) : + f₁₀ ~ f₂₁⁻¹ ∘ f₁₂ ∘ f₀₁ := + homotopy_inv_of_homotopy_post _ _ _ p + definition hhconcat (p : hsquare f₁₀ f₁₂ f₀₁ f₂₁) (q : hsquare f₃₀ f₃₂ f₂₁ f₄₁) : hsquare (f₃₀ ∘ f₁₀) (f₃₂ ∘ f₁₂) f₀₁ f₄₁ := hwhisker_right f₁₀ q ⬝hty hwhisker_left f₃₂ p @@ -456,6 +468,46 @@ namespace wedge end wedge +namespace nat + + definition iterate_succ {A : Type} (f : A → A) (n : ℕ) (x : A) : + f^[succ n] x = f^[n] (f x) := + by induction n with n p; reflexivity; exact ap f p + + lemma iterate_sub {A : Type} (f : A ≃ A) {n m : ℕ} (h : n ≥ m) (a : A) : + iterate f (n - m) a = iterate f n (iterate f⁻¹ m a) := + begin + revert n h, induction m with m p: intro n h, + { reflexivity }, + { cases n with n, exfalso, apply not_succ_le_zero _ h, + rewrite [succ_sub_succ], refine p n (le_of_succ_le_succ h) ⬝ _, + refine ap (f^[n]) _ ⬝ !iterate_succ⁻¹, exact !to_right_inv⁻¹ } + end + + definition iterate_commute {A : Type} {f g : A → A} (n : ℕ) (h : f ∘ g ~ g ∘ f) : + iterate f n ∘ g ~ g ∘ iterate f n := + by induction n with n IH; reflexivity; exact λx, ap f (IH x) ⬝ !h + + definition iterate_equiv {A : Type} (f : A ≃ A) (n : ℕ) : A ≃ A := + equiv.mk (iterate f n) + (by induction n with n IH; apply is_equiv_id; exact is_equiv_compose f (iterate f n)) + + definition iterate_inv {A : Type} (f : A ≃ A) (n : ℕ) : + (iterate_equiv f n)⁻¹ ~ iterate f⁻¹ n := + begin + induction n with n p: intro a, + reflexivity, + exact p (f⁻¹ a) ⬝ !iterate_succ⁻¹ + end + + definition iterate_left_inv {A : Type} (f : A ≃ A) (n : ℕ) (a : A) : f⁻¹ᵉ^[n] (f^[n] a) = a := + (iterate_inv f n (f^[n] a))⁻¹ ⬝ to_left_inv (iterate_equiv f n) a + + definition iterate_right_inv {A : Type} (f : A ≃ A) (n : ℕ) (a : A) : f^[n] (f⁻¹ᵉ^[n] a) = a := + ap (f^[n]) (iterate_inv f n a)⁻¹ ⬝ to_right_inv (iterate_equiv f n) a + +end nat + namespace pi definition is_contr_pi_of_neg {A : Type} (B : A → Type) (H : ¬ A) : is_contr (Πa, B a) := @@ -682,6 +734,57 @@ namespace group apply is_trunc_equiv_closed_rev, exact H end + definition is_equiv_mul_right [constructor] {A : Group} (a : A) : is_equiv (λb, b * a) := + adjointify _ (λb : A, b * a⁻¹) (λb, !inv_mul_cancel_right) (λb, !mul_inv_cancel_right) + + definition right_action [constructor] {A : Group} (a : A) : A ≃ A := + equiv.mk _ (is_equiv_mul_right a) + + definition is_equiv_add_right [constructor] {A : AddGroup} (a : A) : is_equiv (λb, b + a) := + adjointify _ (λb : A, b - a) (λb, !neg_add_cancel_right) (λb, !add_neg_cancel_right) + + definition add_right_action [constructor] {A : AddGroup} (a : A) : A ≃ A := + equiv.mk _ (is_equiv_add_right a) + + section + variables {A B : Type} (f : A ≃ B) [ab_group A] + definition group_equiv_mul_comm (b b' : B) : group_equiv_mul f b b' = group_equiv_mul f b' b := + by rewrite [↑group_equiv_mul, mul.comm] + + definition ab_group_equiv_closed : ab_group B := + ⦃ab_group, group_equiv_closed f, + mul_comm := group_equiv_mul_comm f⦄ + end + + definition ab_group_of_is_contr (A : Type) [is_contr A] : ab_group A := + have ab_group unit, from ab_group_unit, + ab_group_equiv_closed (equiv_unit_of_is_contr A)⁻¹ᵉ + + definition group_of_is_contr (A : Type) [is_contr A] : group A := + have ab_group A, from ab_group_of_is_contr A, by apply _ + + definition ab_group_lift_unit : ab_group (lift unit) := + ab_group_of_is_contr (lift unit) + + definition trivial_ab_group_lift : AbGroup := + AbGroup.mk _ ab_group_lift_unit + + definition homomorphism_of_is_contr_right (A : Group) {B : Type} (H : is_contr B) : + A →g Group.mk B (group_of_is_contr B) := + group.homomorphism.mk (λa, center _) (λa a', !is_prop.elim) + + open trunc pointed is_conn + definition ab_group_homotopy_group_of_is_conn (n : ℕ) (A : Type*) [H : is_conn 1 A] : + ab_group (π[n] A) := + begin + have is_conn 0 A, from !is_conn_of_is_conn_succ, + cases n with n, + { unfold [homotopy_group, ptrunc], apply ab_group_of_is_contr }, + cases n with n, + { unfold [homotopy_group, ptrunc], apply ab_group_of_is_contr }, + exact ab_group_homotopy_group n A + end + -- definition is_equiv_isomorphism @@ -703,7 +806,32 @@ namespace group end group open group +namespace function + variables {A B : Type} {f f' : A → B} + definition is_embedding_homotopy_closed (p : f ~ f') (H : is_embedding f) : is_embedding f' := + begin + intro a a', fapply is_equiv_of_equiv_of_homotopy, + exact equiv.mk (ap f) _ ⬝e equiv_eq_closed_left _ (p a) ⬝e equiv_eq_closed_right _ (p a'), + intro q, esimp, exact (eq_bot_of_square (transpose (natural_square p q)))⁻¹ + end + + definition is_embedding_homotopy_closed_rev (p : f' ~ f) (H : is_embedding f) : is_embedding f' := + is_embedding_homotopy_closed p⁻¹ʰᵗʸ H + + definition is_surjective_homotopy_closed (p : f ~ f') (H : is_surjective f) : is_surjective f' := + begin + intro b, induction H b with a q, + exact image.mk a ((p a)⁻¹ ⬝ q) + end + + definition is_surjective_homotopy_closed_rev (p : f' ~ f) (H : is_surjective f) : + is_surjective f' := + is_surjective_homotopy_closed p⁻¹ʰᵗʸ H + +end function + namespace fiber + open pointed definition pcompose_ppoint {A B : Type*} (f : A →* B) : f ∘* ppoint f ~* pconst (pfiber f) B := begin @@ -712,16 +840,91 @@ namespace fiber { exact !idp_con⁻¹ } end - definition ap1_ppoint_phomotopy {A B : Type*} (f : A →* B) - : Ω→ (ppoint f) ∘* pfiber_loop_space f ~* ppoint (Ω→ f) := + definition point_fiber_eq {A B : Type} {f : A → B} {b : B} {x y : fiber f b} + (p : point x = point y) (q : point_eq x = ap f p ⬝ point_eq y) : + ap point (fiber_eq p q) = p := begin - exact sorry + induction x with a r, induction y with a' s, esimp at *, induction p, + induction q using eq.rec_symm, induction s, reflexivity + end + + definition fiber_eq_equiv_fiber {A B : Type} {f : A → B} {b : B} (x y : fiber f b) : + x = y ≃ fiber (ap1_gen f (point_eq x) (point_eq y)) (idpath b) := + calc + x = y ≃ fiber.sigma_char f b x = fiber.sigma_char f b y : + eq_equiv_fn_eq_of_equiv (fiber.sigma_char f b) x y + ... ≃ Σ(p : point x = point y), point_eq x =[p] point_eq y : sigma_eq_equiv + ... ≃ Σ(p : point x = point y), (point_eq x)⁻¹ ⬝ ap f p ⬝ point_eq y = idp : + sigma_equiv_sigma_right (λp, + calc point_eq x =[p] point_eq y ≃ point_eq x = ap f p ⬝ point_eq y : eq_pathover_equiv_Fl + ... ≃ ap f p ⬝ point_eq y = point_eq x : eq_equiv_eq_symm + ... ≃ (point_eq x)⁻¹ ⬝ (ap f p ⬝ point_eq y) = idp : eq_equiv_inv_con_eq_idp + ... ≃ (point_eq x)⁻¹ ⬝ ap f p ⬝ point_eq y = idp : equiv_eq_closed_left _ !con.assoc⁻¹) + ... ≃ fiber (ap1_gen f (point_eq x) (point_eq y)) (idpath b) : fiber.sigma_char + + definition loop_pfiber [constructor] {A B : Type*} (f : A →* B) : Ω (pfiber f) ≃* pfiber (Ω→ f) := + pequiv_of_equiv (fiber_eq_equiv_fiber pt pt) + begin + induction f with f f₀, induction B with B b₀, esimp at (f,f₀), induction f₀, reflexivity + end + + definition point_fiber_eq_equiv_fiber {A B : Type} {f : A → B} {b : B} {x y : fiber f b} + (p : x = y) : point (fiber_eq_equiv_fiber x y p) = ap1_gen point idp idp p := + by induction p; reflexivity + + lemma ppoint_loop_pfiber {A B : Type*} (f : A →* B) : + ppoint (Ω→ f) ∘* loop_pfiber f ~* Ω→ (ppoint f) := + phomotopy.mk (point_fiber_eq_equiv_fiber) + begin + induction f with f f₀, induction B with B b₀, esimp at (f,f₀), induction f₀, reflexivity + end + + lemma ppoint_loop_pfiber_inv {A B : Type*} (f : A →* B) : + Ω→ (ppoint f) ∘* (loop_pfiber f)⁻¹ᵉ* ~* ppoint (Ω→ f) := + (phomotopy_pinv_right_of_phomotopy (ppoint_loop_pfiber f))⁻¹* + + lemma pfiber_equiv_of_phomotopy_ppoint {A B : Type*} {f g : A →* B} (h : f ~* g) + : ppoint g ∘* pfiber_equiv_of_phomotopy h ~* ppoint f := + begin + induction f with f f₀, induction g with g g₀, induction h with h h₀, induction B with B b₀, + esimp at *, induction h₀, induction g₀, + fapply phomotopy.mk, + { reflexivity }, + { esimp [pfiber_equiv_of_phomotopy], exact !point_fiber_eq⁻¹ } + end + + lemma pequiv_postcompose_ppoint {A B B' : Type*} (f : A →* B) (g : B ≃* B') + : ppoint f ∘* fiber.pequiv_postcompose f g ~* ppoint (g ∘* f) := + begin + induction f with f f₀, induction g with g hg g₀, induction B with B b₀, + induction B' with B' b₀', esimp at *, induction g₀, induction f₀, + fapply phomotopy.mk, + { reflexivity }, + { esimp [pequiv_postcompose], symmetry, + refine !ap_compose⁻¹ ⬝ _, apply ap_constant } + end + + lemma pequiv_precompose_ppoint {A A' B : Type*} (f : A →* B) (g : A' ≃* A) + : ppoint f ∘* fiber.pequiv_precompose f g ~* g ∘* ppoint (f ∘* g) := + begin + induction f with f f₀, induction g with g hg g₀, induction B with B b₀, + induction A with A a₀', esimp at *, induction g₀, induction f₀, + reflexivity, end definition pfiber_equiv_of_square_ppoint {A B C D : Type*} {f : A →* B} {g : C →* D} (h : A ≃* C) (k : B ≃* D) (s : k ∘* f ~* g ∘* h) : ppoint g ∘* pfiber_equiv_of_square h k s ~* h ∘* ppoint f := - sorry + begin + refine !passoc⁻¹* ⬝* _, + refine pwhisker_right _ !pequiv_precompose_ppoint ⬝* _, + refine !passoc ⬝* _, + apply pwhisker_left, + refine !passoc⁻¹* ⬝* _, + refine pwhisker_right _ !pfiber_equiv_of_phomotopy_ppoint ⬝* _, + apply pinv_right_phomotopy_of_phomotopy, + refine !pequiv_postcompose_ppoint⁻¹*, + end end fiber @@ -1222,11 +1425,6 @@ section show a = 0, from is_injective_of_is_embedding this end -definition iterate_succ {A : Type} (f : A → A) (n : ℕ) (x : A) : - f^[succ n] x = f^[n] (f x) := -by induction n with n p; reflexivity; exact ap f p - - /- put somewhere in algebra -/ structure Ring := @@ -1242,6 +1440,17 @@ namespace int notation `rℤ` := ring_int + definition max0 : ℤ → ℕ + | (of_nat n) := n + | (-[1+ n]) := 0 + + lemma le_max0 : Π(n : ℤ), n ≤ of_nat (max0 n) + | (of_nat n) := proof le.refl n qed + | (-[1+ n]) := proof unit.star qed + + lemma le_of_max0_le {n : ℤ} {m : ℕ} (h : max0 n ≤ m) : n ≤ of_nat m := + le.trans (le_max0 n) (of_nat_le_of_nat_of_le h) + end int namespace set_quotient @@ -1275,3 +1484,47 @@ namespace set_quotient equiv.mk _ (is_equiv_class_of R p) end set_quotient + +-- should be in pushout +namespace pushout +variables {TL BL TR : Type} (f : TL → BL) (g : TL → TR) + +protected theorem elim_inl {P : Type} (Pinl : BL → P) (Pinr : TR → P) + (Pglue : Π(x : TL), Pinl (f x) = Pinr (g x)) {b b' : BL} (p : b = b') + : ap (pushout.elim Pinl Pinr Pglue) (ap inl p) = ap Pinl p := +by cases p; reflexivity + +protected theorem elim_inr {P : Type} (Pinl : BL → P) (Pinr : TR → P) + (Pglue : Π(x : TL), Pinl (f x) = Pinr (g x)) {b b' : TR} (p : b = b') + : ap (pushout.elim Pinl Pinr Pglue) (ap inr p) = ap Pinr p := +by cases p; reflexivity + +end pushout + +-- should be in prod +namespace prod +open prod.ops +definition pair_eq_eta {A B : Type} {u v : A × B} + (p : u = v) : pair_eq (p..1) (p..2) = prod.eta u ⬝ p ⬝ (prod.eta v)⁻¹ := +by induction p; induction u; reflexivity + +definition prod_eq_eq {A B : Type} {u v : A × B} + {p₁ q₁ : u.1 = v.1} {p₂ q₂ : u.2 = v.2} (α₁ : p₁ = q₁) (α₂ : p₂ = q₂) + : prod_eq p₁ p₂ = prod_eq q₁ q₂ := +by cases α₁; cases α₂; reflexivity + +definition prod_eq_assemble {A B : Type} {u v : A × B} + {p q : u = v} (α₁ : p..1 = q..1) (α₂ : p..2 = q..2) : p = q := +(prod_eq_eta p)⁻¹ ⬝ prod.prod_eq_eq α₁ α₂ ⬝ prod_eq_eta q + +definition eq_pr1_concat {A B : Type} {u v w : A × B} + (p : u = v) (q : v = w) + : (p ⬝ q)..1 = p..1 ⬝ q..1 := +by cases q; reflexivity + +definition eq_pr2_concat {A B : Type} {u v w : A × B} + (p : u = v) (q : v = w) + : (p ⬝ q)..2 = p..2 ⬝ q..2 := +by cases q; reflexivity + +end prod diff --git a/pointed.hlean b/pointed.hlean index 9faf663..c749a82 100644 --- a/pointed.hlean +++ b/pointed.hlean @@ -1,9 +1,7 @@ -/- equalities between pointed homotopies -/ +/- equalities between pointed homotopies and other facts about pointed types/functions/homotopies -/ -- Author: Floris van Doorn ---import .pointed_pi - import .move_to_lib open pointed eq equiv function is_equiv unit is_trunc trunc nat algebra group sigma