From a22ac8af289f8fe6838c8b59a83cac0ebb23c946 Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Fri, 19 Jan 2018 10:07:28 -0500 Subject: [PATCH] work on connectification of a type --- higher_groups.hlean | 66 ++++++++++++++++++++++------- move_to_lib.hlean | 100 ++++++++++++++++++++++++++++++++++++++++---- 2 files changed, 143 insertions(+), 23 deletions(-) diff --git a/higher_groups.hlean b/higher_groups.hlean index 794712c..5d75bed 100644 --- a/higher_groups.hlean +++ b/higher_groups.hlean @@ -10,17 +10,18 @@ import .move_to_lib open eq is_conn pointed is_trunc trunc equiv is_equiv trunc_index susp nat algebra prod.ops sigma sigma.ops namespace higher_group set_option pp.binder_types true +universe variable u /- We require that the carrier has a point (preserved by the equivalence) -/ -structure Grp.{u} (n k : ℕ) : Type.{u+1} := /- (n,k)Grp, denoted here as [n;k]Grp -/ +structure Grp (n k : ℕ) : Type := /- (n,k)Grp, denoted here as [n;k]Grp -/ (car : ptrunctype.{u} n) - (B : pconntype.{u} (k.-1)) + (B : pconntype.{u} (k.-1)) /- this is Bᵏ -/ (e : car ≃* Ω[k] B) -structure InfGrp.{u} (k : ℕ) : Type.{u+1} := /- (∞,k)Grp, denoted here as [∞;k]Grp -/ +structure InfGrp (k : ℕ) : Type := /- (∞,k)Grp, denoted here as [∞;k]Grp -/ (car : pType.{u}) - (B : pconntype.{u} (k.-1)) + (B : pconntype.{u} (k.-1)) /- this is Bᵏ -/ (e : car ≃* Ω[k] B) structure ωGrp (n : ℕ) := /- (n,ω)Grp, denoted here as [n;ω]Grp -/ @@ -51,12 +52,24 @@ transport (λm, is_trunc m (B G)) (add.comm k n) (is_trunc_B' G) local attribute [instance] is_trunc_B +/- some equivalences -/ +--set_option pp.all true +definition Grp.sigma_char (n k : ℕ) : + Grp.{u} n k ≃ Σ(B : pconntype.{u} (k.-1)), Σ(X : ptrunctype.{u} n), X ≃* Ω[k] B := +begin + fapply equiv.MK, + { intro G, exact ⟨B G, G, e G⟩ }, + { intro v, exact Grp.mk v.2.1 v.1 v.2.2 }, + { intro v, induction v with v₁ v₂, induction v₂, reflexivity }, + { intro G, induction G, reflexivity }, +end + definition Grp_equiv (n k : ℕ) : [n;k]Grp ≃ (n+k)-Type*[k.-1] := let f : Π(B : Type*[k.-1]) (H : Σ(X : n-Type*), X ≃* Ω[k] B), (n+k)-Type*[k.-1] := λB' H, ptruncconntype.mk B' (is_trunc_B (Grp.mk H.1 B' H.2)) pt _ in calc - [n;k]Grp ≃ Σ(B : Type*[k.-1]), Σ(X : n-Type*), X ≃* Ω[k] B : sorry + [n;k]Grp ≃ Σ(B : Type*[k.-1]), Σ(X : n-Type*), X ≃* Ω[k] B : Grp.sigma_char n k ... ≃ Σ(B : (n+k)-Type*[k.-1]), Σ(X : n-Type*), X ≃* Ω[k] B : @sigma_equiv_of_is_embedding_left _ _ _ sorry ptruncconntype.to_pconntype sorry (λB' H, fiber.mk (f B' H) sorry) @@ -65,9 +78,13 @@ calc sigma_equiv_sigma_right (λB, sigma_equiv_sigma_right (λX, sorry)) ... ≃ (n+k)-Type*[k.-1] : sigma_equiv_of_is_contr_right -definition Grp_eq_equiv {n k : ℕ} (G H : [n;k]Grp) : (G = H) ≃ (B G ≃* B H) := +definition Grp_equiv_pequiv {n k : ℕ} (G : [n;k]Grp) : Grp_equiv n k G ≃* B G := sorry +definition Grp_eq_equiv {n k : ℕ} (G H : [n;k]Grp) : (G = H) ≃ (B G ≃* B H) := +eq_equiv_fn_eq_of_equiv (Grp_equiv n k) _ _ ⬝e +sorry -- use Grp_equiv_homotopy and equality in ptruncconntype + definition Grp_eq {n k : ℕ} {G H : [n;k]Grp} (e : B G ≃* B H) : G = H := (Grp_eq_equiv G H)⁻¹ᵉ e @@ -81,7 +98,7 @@ definition Decat (G : [n+1;k]Grp) : [n;k]Grp := Grp.mk (ptrunctype.mk (ptrunc n G) _ pt) (pconntype.mk (ptrunc (n + k) (B G)) _ pt) abstract begin refine ptrunc_pequiv_ptrunc n (e G) ⬝e* _, - symmetry, exact sorry --!loopn_ptrunc_pequiv + symmetry, exact !loopn_ptrunc_pequiv_nat end end definition Disc (G : [n;k]Grp) : [n+1;k]Grp := @@ -119,12 +136,7 @@ pmap_ptrunc_pequiv (n + k) (iB G) (B H) /- To do: naturality -/ definition InfDecat_InfDisc (G : [n;k]Grp) : InfDecat n (InfDisc n G) = G := -sorry - -definition Loop (G : [n+1;k]Grp) : [n;k+1]Grp := -Grp.mk (ptrunctype.mk (Ω G) !is_trunc_loop_nat pt) - (connconnect k (B G)) - (loop_pequiv_loop (e G) ⬝e* (loopn_connect k (B G))⁻¹ᵉ*) +Grp_eq !ptrunc_pequiv definition Deloop (G : [n;k+1]Grp) : [n+1;k]Grp := have is_conn k (B G), from is_conn_pconntype (B G), @@ -134,6 +146,18 @@ Grp.mk (ptrunctype.mk (Ω[k] (B G)) !is_trunc_loopn_nat pt) (pconntype.mk (B G) !is_conn_of_is_conn_succ pt) (pequiv_of_equiv erfl idp) +definition Loop (G : [n+1;k]Grp) : [n;k+1]Grp := +Grp.mk (ptrunctype.mk (Ω G) !is_trunc_loop_nat pt) + (connconnect k (B G)) + (loop_pequiv_loop (e G) ⬝e* (loopn_connect k (B G))⁻¹ᵉ*) + +definition Deloop_adjoint_Loop (G : [n;k+1]Grp) (H : [n+1;k]Grp) : + ppmap (B (Deloop G)) (B H) ≃* ppmap (B G) (B (Loop H)) := +(connect_intro_pequiv _ !is_conn_pconntype)⁻¹ᵉ* /- still a sorry here -/ + +definition Loop_Deloop (G : [n;k+1]Grp) : Loop (Deloop G) = G := +Grp_eq (connect_pequiv (is_conn_pconntype (B G))) + /- to do: adjunction, and Loop ∘ Deloop = id -/ definition Forget (G : [n;k+1]Grp) : [n;k]Grp := @@ -162,20 +186,30 @@ have is_trunc (n +[ℕ₋₂] k) (oB G k), from transport (λn, is_trunc n _) !o have is_trunc n (Ω[k] (oB G k)), from !is_trunc_loopn, Grp.mk (ptrunctype.mk (Ω[k] (oB G k)) _ pt) (oB G k) (pequiv_of_equiv erfl idp) -definition nStabilize.{u} (H : k ≤ l) (G : Grp.{u} n k) : Grp.{u} n l := +definition nStabilize (H : k ≤ l) (G : Grp.{u} n k) : Grp.{u} n l := begin induction H with l H IH, exact G, exact Stabilize IH end +lemma Stabilize_pequiv (H : k ≥ n + 2) (G : [n;k]Grp) : B G ≃* Ω (B (Stabilize G)) := +sorry + theorem stabilization (H : k ≥ n + 2) : is_equiv (@Stabilize n k) := sorry -definition ωStabilize_of_le (H : k ≥ n + 2) (G : [n;k]Grp) : [n;ω]Grp := -ωGrp.mk (λl, sorry) (λl, sorry) +definition ωGrp.mk_le {n : ℕ} (k₀ : ℕ) + (B : Π⦃k : ℕ⦄, k₀ ≤ k → (n+k)-Type*[k.-1]) + (e : Π⦃k : ℕ⦄ (H : k₀ ≤ k), B H ≃* Ω (B (le.step H))) : [n;ω]Grp := +sorry /- for l ≤ k we want to define it as Ω[k-l] (B G), for H : l ≥ k we want to define it as nStabilize H G -/ +definition ωStabilize_of_le (H : k ≥ n + 2) (G : [n;k]Grp) : [n;ω]Grp := +ωGrp.mk_le k (λl H', Grp_equiv n l (nStabilize H' G)) + (λl H', !Grp_equiv_pequiv ⬝e* Stabilize_pequiv (le.trans H H') (nStabilize H' G) ⬝e* + loop_pequiv_loop (!Grp_equiv_pequiv⁻¹ᵉ*)) + definition ωStabilize (G : [n;k]Grp) : [n;ω]Grp := ωStabilize_of_le !le_max_left (nStabilize !le_max_right G) diff --git a/move_to_lib.hlean b/move_to_lib.hlean index b294f00..bcc0a07 100644 --- a/move_to_lib.hlean +++ b/move_to_lib.hlean @@ -568,6 +568,21 @@ end lift namespace trunc open trunc_index +/- replace trunc_trunc_equiv_left by this -/ +definition trunc_trunc_equiv_left' [constructor] (A : Type) {n m : ℕ₋₂} (H : n ≤ m) + : trunc n (trunc m A) ≃ trunc n A := +begin + note H2 := is_trunc_of_le (trunc n A) H, + fapply equiv.MK, + { intro x, induction x with x, induction x with x, exact tr x }, + { exact trunc_functor n tr }, + { intro x, induction x with x, reflexivity}, + { intro x, induction x with x, induction x with x, reflexivity} +end + +definition is_equiv_ptrunc_functor_ptr [constructor] (A : Type*) {n m : ℕ₋₂} (H : n ≤ m) + : is_equiv (ptrunc_functor n (ptr m A)) := +to_is_equiv (trunc_trunc_equiv_left' A H)⁻¹ᵉ definition Prop_eq {P Q : Prop} (H : P ↔ Q) : P = Q := tua (equiv_of_is_prop (iff.mp H) (iff.mpr H)) @@ -682,7 +697,7 @@ 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 +end trunc open trunc namespace is_trunc @@ -937,7 +952,12 @@ end end group open group namespace fiber - open pointed sigma + open pointed sigma sigma.ops + +definition fiber_eq_equiv' [constructor] {A B : Type} {f : A → B} {b : B} (x y : fiber f b) + : (x = y) ≃ (Σ(p : point x = point y), point_eq x = ap f p ⬝ point_eq y) := +@equiv_change_inv _ _ (fiber_eq_equiv x y) (λpq, fiber_eq pq.1 pq.2) + begin intro pq, cases pq, reflexivity end definition is_contr_pfiber_pid (A : Type*) : is_contr (pfiber (pid A)) := is_contr.mk pt begin intro x, induction x with a p, esimp at p, cases p, reflexivity end @@ -1001,7 +1021,7 @@ definition is_conn_fun_compose (k : ℕ₋₂) {A B C : Type} {g : B → C} {f : (Hg : is_conn_fun k g) (Hf : is_conn_fun k f) : is_conn_fun k (g ∘ f) := λc, is_conn_equiv_closed_rev k (fiber_compose g f c) _ -end fiber +end fiber open fiber namespace fin @@ -1018,6 +1038,10 @@ namespace function (HB : is_set B) : is_contr B := is_contr.mk (f !center) begin intro b, induction H b, exact ap f !is_prop.elim ⬝ p end + definition is_surjective_of_is_contr [constructor] (f : A → B) (a : A) (H : is_contr B) : + is_surjective f := + λb, image.mk a !eq_of_is_contr + definition is_contr_of_is_embedding (f : A → B) (H : is_embedding f) (HB : is_prop B) (a₀ : A) : is_contr A := is_contr.mk a₀ (λa, is_injective_of_is_embedding (is_prop.elim (f a₀) (f a))) @@ -1057,23 +1081,84 @@ namespace is_conn definition is_conn_zero_pointed' {A : Type*} (p : Πa : A, ∥ a = pt ∥) : is_conn 0 A := is_conn_zero_pointed (λa a', tconcat (p a) (tinverse (p a'))) - definition is_conn_fiber (n : ℕ₋₂) {A B : Type} (f : A → B) (b : B) [is_conn n A] [is_conn (n.+1) B] : - is_conn n (fiber f b) := + definition is_conn_fiber (n : ℕ₋₂) {A B : Type} (f : A → B) (b : B) [is_conn n A] + [is_conn (n.+1) B] : is_conn n (fiber f b) := is_conn_equiv_closed_rev _ !fiber.sigma_char _ definition is_conn_fun_compose {n : ℕ₋₂} {A B C : Type} (g : B → C) (f : A → B) (H : is_conn_fun n g) (K : is_conn_fun n f) : is_conn_fun n (g ∘ f) := sorry +-- definition is_conn_pfiber_of_equiv_on_homotopy_groups (n : ℕ) {A B : pType.{u}} (f : A →* B) +-- [H : is_conn 0 A] +-- (H1 : Πk, k ≤ n → is_equiv (π→[k] f)) +-- (H2 : is_surjective (π→[succ n] f)) : +-- is_conn n (pfiber f) := +-- _ + +-- definition is_conn_pelim [constructor] {k : ℕ} {X : Type*} (Y : Type*) (H : is_conn k X) : +-- (X →* connect k Y) ≃ (X →* Y) := + /- the k-connectification of X, the fiber of the map X → ∥X∥ₖ. -/ definition connect (k : ℕ) (X : Type*) : Type* := pfiber (ptr k X) definition is_conn_connect (k : ℕ) (X : Type*) : is_conn k (connect k X) := -sorry +is_conn_fun_tr k X (tr pt) definition connconnect [constructor] (k : ℕ) (X : Type*) : Type*[k] := -pconntype.mk (connect k X) (is_conn_connect k X) pt +pconntype.mk (connect k X) (is_conn_connect k X) pt. + +definition connect_intro [constructor] {k : ℕ} {X : Type*} {Y : Type*} (H : is_conn k X) + (f : X →* Y) : X →* connect k Y := +pmap.mk (λx, fiber.mk (f x) (is_conn.elim (k.-1) _ (ap tr (respect_pt f)) x)) + begin + fapply fiber_eq, exact respect_pt f, apply is_conn.elim_β + end + +definition ppoint_connect_intro [constructor] {k : ℕ} {X : Type*} {Y : Type*} (H : is_conn k X) + (f : X →* Y) : ppoint (ptr k Y) ∘* connect_intro H f ~* f := +begin + induction f with f f₀, induction Y with Y y₀, esimp at (f,f₀), induction f₀, + fapply phomotopy.mk, + { intro x, reflexivity }, + { symmetry, esimp, apply point_fiber_eq } +end + +definition connect_intro_ppoint [constructor] {k : ℕ} {X : Type*} {Y : Type*} (H : is_conn k X) + (f : X →* connect k Y) : connect_intro H (ppoint (ptr k Y) ∘* f) ~* f := +begin + -- induction f with f f₀, --induction Y with Y y₀, esimp, + -- revert f₀, refine equiv_rect (fiber_eq_equiv' _ _)⁻¹ᵉ _ _, + -- intro pq, induction pq with p q, esimp, + fapply phomotopy.mk, + { intro x, fapply fiber_eq, reflexivity, + refine _ ⬝ !idp_con⁻¹, + refine @is_conn.elim (k.-1) _ _ _ (λx', !is_trunc_eq) _ x, + refine !is_conn.elim_β ⬝ _, + cases f with f f₀, esimp, + revert f₀, generalize f (Point X), + intro x p, cases p, reflexivity }, + { esimp, exact sorry } +end + +definition connect_intro_equiv [constructor] {k : ℕ} {X : Type*} (Y : Type*) (H : is_conn k X) : + (X →* connect k Y) ≃ (X →* Y) := +begin + fapply equiv.MK, + { intro f, exact ppoint (ptr k Y) ∘* f }, + { intro g, exact connect_intro H g }, + { intro g, apply eq_of_phomotopy, exact ppoint_connect_intro H g }, + { intro f, apply eq_of_phomotopy, exact connect_intro_ppoint H f } +end + +definition connect_intro_pequiv [constructor] {k : ℕ} {X : Type*} (Y : Type*) (H : is_conn k X) : + ppmap X (connect k Y) ≃* ppmap X Y := +pequiv_of_equiv (connect_intro_equiv Y H) (eq_of_phomotopy !pcompose_pconst) + + +definition connect_pequiv {k : ℕ} {X : Type*} (H : is_conn k X) : connect k X ≃* X := +sorry definition loopn_connect (k : ℕ) (X : Type*) : Ω[k+1] (connect k X) ≃* Ω[k+1] X := sorry @@ -1088,6 +1173,7 @@ namespace misc open sigma.ops pointed trunc_index + /- this is equivalent to pfiber (A → ∥A∥₀) ≡ connect 0 A -/ definition component [constructor] (A : Type*) : Type* := pType.mk (Σ(a : A), merely (pt = a)) ⟨pt, tr idp⟩