diff --git a/algebra/arrow_group.hlean b/algebra/arrow_group.hlean index ac16067..539c227 100644 --- a/algebra/arrow_group.hlean +++ b/algebra/arrow_group.hlean @@ -38,6 +38,7 @@ namespace group { intro a, exact con.left_inv (f a) }, { exact !con_left_inv_idp }}, end + -- inf_pgroup_pequiv_closed (loop_pppi_pequiv B) _ definition inf_group_ppi [constructor] {A : Type*} (B : A → Type*) : inf_group (Π*a, Ω (B a)) := @inf_group_of_inf_pgroup _ (inf_pgroup_pppi B) @@ -128,6 +129,10 @@ namespace group gtrunc (gloop (Π*(a : A), B a)) ≃g gtrunc (gppi_loop B) := proof trunc_ppi_loop_isomorphism_gen (ppi_const B) qed + definition gppi_loop_homomorphism_right [constructor] {A : Type*} {B B' : A → Type*} + (g : Πa, B a →* B' a) : gppi_loop B →∞g gppi_loop B' := + gloop_ppi_isomorphism B' ∘∞g Ωg→ (pppi_compose_left g) ∘∞g (gloop_ppi_isomorphism B)⁻¹ᵍ⁸ + /- We first define the group structure on A →* Ω B (except for truncatedness). Instead of Ω B, we could also choose any infinity group. However, we need various 2-coherences, @@ -183,12 +188,30 @@ namespace group definition gpmap_loop [reducible] [constructor] (A B : Type*) : InfGroup := InfGroup.mk (A →* Ω B) !inf_group_ppi + definition gpmap_loopn [constructor] (n : ℕ) [H : is_succ n] (A B : Type*) : InfGroup := + InfGroup.mk (A →** Ω[n] B) (by induction H with n; exact inf_group_ppi (λa, Ω[n] B)) + + definition gloop_pmap_isomorphism (A B : Type*) : Ωg (A →** B) ≃∞g gpmap_loop A B := + gloop_ppi_isomorphism _ + + definition gloopn_pmap_isomorphism (n : ℕ) [H : is_succ n] (A B : Type*) : + Ωg[n] (A →** B) ≃∞g gpmap_loopn n A B := + begin + induction H with n, induction n with n IH, + { exact gloop_pmap_isomorphism A B }, + { rexact Ωg≃ (pequiv_of_inf_isomorphism IH) ⬝∞g gloop_pmap_isomorphism A (Ω[succ n] B) } + end + definition gpmap_loop' [reducible] [constructor] (A : Type*) {B C : Type*} (e : Ω C ≃* B) : InfGroup := InfGroup.mk (A →* B) (@inf_group_of_inf_pgroup _ (inf_pgroup_pequiv_closed (ppmap_pequiv_ppmap_right e) !inf_pgroup_pppi)) + definition gpmap_loop_homomorphism_right [constructor] (A : Type*) {B B' : Type*} + (g : B →* B') : gpmap_loop A B →∞g gpmap_loop A B' := + gppi_loop_homomorphism_right (λa, g) + definition Group_trunc_pmap [reducible] [constructor] (A B : Type*) : Group := Group.mk (trunc 0 (A →* Ω B)) (@group_trunc _ !inf_group_ppi) diff --git a/cohomology/serre.hlean b/cohomology/serre.hlean index 8822393..8e271df 100644 --- a/cohomology/serre.hlean +++ b/cohomology/serre.hlean @@ -85,8 +85,6 @@ begin exact pfiber_postnikov_map A n end - -set_option formatter.hide_full_terms false definition pfiber_postnikov_map_pred' (A : spectrum) (n k l : ℤ) (p : n + k = l) : pfiber (postnikov_map_pred (A k) (maxm2 l)) ≃* EM_spectrum (πₛ[n] A) l := begin diff --git a/homotopy/EM.hlean b/homotopy/EM.hlean index ee2fa6a..fe19189 100644 --- a/homotopy/EM.hlean +++ b/homotopy/EM.hlean @@ -156,7 +156,7 @@ namespace EM (ptrunc_pequiv (n+1+1) (EMadd1 G (n+1)))⁻¹ᵉ* := by reflexivity - definition ap1_EMadd1_natural {G H : AbGroup} (φ : G →g H) (n : ℕ) : + definition loop_EMadd1_natural {G H : AbGroup} (φ : G →g H) (n : ℕ) : psquare (loop_EMadd1 G n) (loop_EMadd1 H n) (EMadd1_functor φ n) (Ω→ (EMadd1_functor φ (succ n))) := begin @@ -181,7 +181,7 @@ namespace EM { refine pwhisker_left _ !loopn_EMadd1_pequiv_EM1_succ ⬝* _, refine _ ⬝* pwhisker_right _ !loopn_EMadd1_pequiv_EM1_succ⁻¹*, refine _ ⬝h* !loopn_succ_in_inv_natural, - exact IH ⬝h* (apn_psquare n !ap1_EMadd1_natural) } + exact IH ⬝h* (apn_psquare n !loop_EMadd1_natural) } end definition homotopy_group_functor_EMadd1_functor {G H : AbGroup} (φ : G →g H) (n : ℕ) : @@ -301,15 +301,18 @@ namespace EM proof λa, idp qed definition EMadd1_pmap_equiv (n : ℕ) (X Y : Type*) [is_conn (n+1) X] [is_trunc (n+1+1) X] - [is_conn (n+1) Y] [is_trunc (n+1+1) Y] : (X →* Y) ≃ πag[n+2] X →g πag[n+2] Y := + [H4 : is_trunc (n+1+1) Y] : (X →* Y) ≃ πag[n+2] X →g πag[n+2] Y := begin + have H4' : is_trunc ((n+1).+1) Y, from H4, + have is_set (Ωg[succ (n+1)] Y), from is_set_loopn (n+1+1) Y, fapply equiv.MK, { exact π→g[n+2] }, - { exact λφ, (EMadd1_pequiv_type Y n ∘* EMadd1_functor φ (n+1)) ∘* (EMadd1_pequiv_type X n)⁻¹ᵉ* }, + { intro φ, refine (_ ∘* EMadd1_functor φ (n+1)) ∘* (EMadd1_pequiv_type X n)⁻¹ᵉ*, + exact EMadd1_pmap (n+1) (gtrunc_isomorphism (Ωg[succ (n+1)] Y)) }, { intro φ, apply homomorphism_eq, refine homotopy_group_functor_pcompose (n+2) _ _ ⬝hty _, exact sorry }, -- easy but tedious { intro f, apply eq_of_phomotopy, refine (phomotopy_pinv_right_of_phomotopy _)⁻¹*, - apply EMadd1_pequiv_type_natural } + exact sorry /-apply EMadd1_pequiv_type_natural-/ } end definition EM1_functor_trivial_homomorphism [constructor] (G H : Group) : @@ -343,19 +346,39 @@ namespace EM { refine !loopn_succ_in ⬝e* Ω≃[n] (loop_EMadd1 G (m + n))⁻¹ᵉ* ⬝e* e } end + definition loopn_EMadd1_add_of_eq (G : AbGroup) {n m k : ℕ} (p : m + n = k) : Ω[n] (EMadd1 G k) ≃* EMadd1 G m := + by induction p; exact loopn_EMadd1_add G n m + + definition EM1_phomotopy {G : Group} {X : Type*} [is_trunc 1 X] {f g : EM1 G →* X} (h : Ω→ f ~ Ω→ g) : + f ~* g := + begin + fapply phomotopy.mk, + { intro x, induction x using EM.set_rec with a, + { exact respect_pt f ⬝ (respect_pt g)⁻¹ }, + { apply eq_pathover, apply move_top_of_right, apply move_bot_of_right, + apply move_top_of_left', apply move_bot_of_left, apply hdeg_square, exact h (pth a) }}, + { apply inv_con_cancel_right } + end + /- properties about EM -/ + definition deloopable_EM [instance] [constructor] (G : AbGroup) (n : ℕ) : deloopable (EM G n) := + deloopable.mk (EMadd1 G n) (loop_EM G n) + definition gEM (G : AbGroup) (n : ℕ) : InfGroup := - InfGroup_equiv_closed (Ωg (EMadd1 G n)) (loop_EM G n) + InfGroup_of_deloopable (EM G n) definition gloop_EM1 [constructor] (G : Group) : Ωg (EM1 G) ≃∞g InfGroup_of_Group G := inf_isomorphism_of_equiv (EM.base_eq_base_equiv G) groupoid_quotient.encode_con + definition gloop_EMadd1 [constructor] (G : AbGroup) (n : ℕ) : Ωg (EMadd1 G n) ≃∞g gEM G n := + deloop_isomorphism (EM G n) + definition gEM0_isomorphism (G : AbGroup) : gEM G 0 ≃∞g InfGroup_of_Group G := - !InfGroup_equiv_closed_isomorphism⁻¹ᵍ⁸ ⬝∞g gloop_EM1 G + (gloop_EMadd1 G 0)⁻¹ᵍ⁸ ⬝∞g gloop_EM1 G definition gEM_functor {G H : AbGroup} (φ : G →g H) (n : ℕ) : gEM G n →∞g gEM H n := - inf_homomorphism.mk (EM_functor φ n) sorry + gloop_EMadd1 H n ∘∞g Ωg→ (EMadd1_functor φ n) ∘∞g (gloop_EMadd1 G n)⁻¹ᵍ⁸ definition EM_pmap [unfold 8] {G : AbGroup} (X : InfGroup) (n : ℕ) (e : AbInfGroup_of_AbGroup G →∞g Ωg'[n] X) [H : is_trunc n X] : EM G n →* X := @@ -366,9 +389,35 @@ namespace EM end definition EM_homomorphism_gloop [unfold 8] {G : AbGroup} (X : Type*) (n : ℕ) - (e : AbInfGroup_of_AbGroup G →∞g Ωg[succ n] X) [H : is_trunc n X] : gEM G n →∞g Ωg X := + (e : AbInfGroup_of_AbGroup G →∞g Ωg[succ n] X) [H : is_trunc (n+1) X] : gEM G n →∞g Ωg X := Ωg→ (EMadd1_pmap n e) ∘∞g !InfGroup_equiv_closed_isomorphism⁻¹ᵍ⁸ + definition gloopn_succ_in' (n : ℕ) (A : Type*) : Ωg[succ n] A ≃∞g Ωg'[n] (Ωg A) := + inf_isomorphism_of_equiv (loopn_succ_in n A) + (by cases n with n; apply is_mul_hom_id; exact loopn_succ_in_con) + + definition EM_homomorphism_deloopable [unfold 8] {G : AbGroup} (X : Type*) (H : deloopable X) (n : ℕ) + (e : AbInfGroup_of_AbGroup G →∞g Ωg'[n] (InfGroup_of_deloopable X)) (H : is_trunc (n+1) (deloop X)) : + gEM G n →∞g InfGroup_of_deloopable X := + deloop_isomorphism X ∘∞g + EM_homomorphism_gloop (deloop X) n + ((gloopn_succ_in' n (deloop X))⁻¹ᵍ⁸ ∘∞g Ωg'→[n] (deloop_isomorphism X)⁻¹ᵍ⁸ ∘∞g e) + + definition is_mul_hom_EM_functor [constructor] (G H : AbGroup) (n : ℕ) : + is_mul_hom (λ(φ : G →gg H), EM_functor φ n) := + begin + intro φ ψ, + apply eq_of_phomotopy, + exact sorry + -- exact sorry, exact sorry, exact sorry +-- refine idpath (φ 0 * ψ 0) ⬝ _, + end + + /- an enriched homomorphism -/ + definition EM_ehomomorphism [constructor] (G H : AbGroup) (n : ℕ) : + InfGroup_of_Group (G →gg H) →∞g InfGroup_of_deloopable (EM G n →** EM H n) := + inf_homomorphism.mk (λφ, EM_functor φ n) (is_mul_hom_EM_functor G H n) + -- definition EM_homomorphism [unfold 8] {G : AbGroup} {X : Type*} (Y : Type*) (e : Ω Y ≃* X) (n : ℕ) -- (e : AbInfGroup_of_AbGroup G →∞g Ωg[succ n] X) [H : is_trunc n X] : gEM G n →∞g X := -- _ diff --git a/homotopy/EMRing.hlean b/homotopy/EMRing.hlean index a69ea67..9093f1c 100644 --- a/homotopy/EMRing.hlean +++ b/homotopy/EMRing.hlean @@ -2,9 +2,11 @@ import .EM .smash_adjoint ..algebra.ring ..algebra.arrow_group -open algebra eq EM is_equiv equiv is_trunc is_conn pointed trunc susp smash group nat +open algebra eq EM is_equiv equiv is_trunc is_conn pointed trunc susp smash group nat function + namespace EM + definition EM1product_adj {R : Ring} : EM1 (AbGroup_of_Ring R) →* ppmap (EM1 (AbGroup_of_Ring R)) (EMadd1 (AbGroup_of_Ring R) 1) := begin @@ -25,6 +27,7 @@ definition EM0EMadd1product {A B C : AbGroup} (φ : A →g B →gg C) (n : ℕ) A →* EMadd1 B n →** EMadd1 C n := EMadd1_pfunctor B C n ∘* pmap_of_homomorphism φ +-- TODO: simplify definition EMadd1product {A B C : AbGroup} (φ : A →g B →gg C) (n m : ℕ) : EMadd1 A n →* EMadd1 B m →** EMadd1 C (m + succ n) := begin @@ -32,10 +35,12 @@ begin { refine is_trunc_pmap_of_is_conn _ (m.-1) !is_conn_EMadd1 _ _ _ _ !is_trunc_EMadd1, exact le_of_eq (trunc_index.of_nat_add_plus_two_of_nat m n)⁻¹ᵖ }, apply EMadd1_pmap, - exact sorry - /- the underlying pointed map is: -/ - -- refine (loopn_ppmap_pequiv _ _ _)⁻¹ᵉ* ∘* ppcompose_left !loopn_EMadd1_add⁻¹ᵉ* ∘* - -- EM0EMadd1product φ m + refine (gloopn_pmap_isomorphism (succ n) _ _)⁻¹ᵍ⁸ ∘∞g + gpmap_loop_homomorphism_right (EMadd1 B m) (loopn_EMadd1_add_of_eq C !succ_add)⁻¹ᵉ* ∘∞g + gloop_pmap_isomorphism _ _ ∘∞g + (deloop_isomorphism _)⁻¹ᵍ⁸ ∘∞g + EM_ehomomorphism B C (succ m) ∘∞g + inf_homomorphism_of_homomorphism φ end definition EMproduct1 {A B C : AbGroup} (φ : A →g B →gg C) (n m : ℕ) : @@ -51,8 +56,9 @@ begin { exact ppcompose_left (ptransport (EMadd1 C) !succ_add⁻¹) ∘* EMadd1product φ n m }} end + definition EMproduct2 {A B C : AbGroup} (φ : A →g B →gg C) (n m : ℕ) : - EM A n →* EM B m →** EM C (m + n) := + EM A n →* (EM B m →** EM C (m + n)) := begin assert H1 : is_trunc n (gpmap_loop' (EM B m) (loop_EM C (m + n))), { exact is_trunc_pmap_of_is_conn_nat _ m !is_conn_EM _ _ _ !le.refl !is_trunc_EM }, @@ -72,6 +78,44 @@ begin -- --(gmap_loop' (EM B m) (loop_EM C (m + n))) n, -- exact _ /- (loopn_ppmap_pequiv _ _ _)⁻¹ᵉ* -/ ∘∞g _ /-ppcompose_left !loopn_EMadd1_add⁻¹ᵉ*-/ ∘∞g -- _ ∘∞g inf_homomorphism_of_homomorphism φ + exact sorry +end + +definition EMproduct4 {A B C : AbGroup} (φ : A →g B →gg C) (n m : ℕ) : + gEM A n →∞g Ωg (EM B m →** EM C (m + n + 1)) := +begin + assert H1 : is_trunc (n+1) (EM B m →** EM C (m + n + 1)), + { exact is_trunc_pmap_of_is_conn_nat _ m !is_conn_EM _ _ _ !le.refl !is_trunc_EM }, + apply EM_homomorphism_gloop, + refine (gloopn_pmap_isomorphism _ _ _)⁻¹ᵍ⁸ ∘∞g _ ∘∞g inf_homomorphism_of_homomorphism φ, + +-- exact _ /- (loopn_ppmap_pequiv _ _ _)⁻¹ᵉ* -/ ∘∞g _ /-ppcompose_left !loopn_EMadd1_add⁻¹ᵉ*-/ ∘∞g +-- _ ∘∞g inf_homomorphism_of_homomorphism φ + exact sorry +end + +definition EMproduct5 {A B C : AbGroup} (φ : A →g B →gg C) (n m : ℕ) : + InfGroup_of_deloopable (EM A n) →∞g InfGroup_of_deloopable (EM B m →** EM C (m + n)) := +begin + assert H1 : is_trunc (n + 1) (deloop (EM B m →** EM C (m + n))), + { exact is_trunc_pmap_of_is_conn_nat _ m !is_conn_EM _ _ _ !le.refl !is_trunc_EM }, + refine EM_homomorphism_deloopable _ _ _ _ _, + + -- exact _ /- (loopn_ppmap_pequiv _ _ _)⁻¹ᵉ* -/ ∘∞g _ /-ppcompose_left !loopn_EMadd1_add⁻¹ᵉ*-/ ∘∞g + -- _ ∘∞g inf_homomorphism_of_homomorphism φ + exact sorry +end + +definition EMadd1product2 {A B C : AbGroup} (φ : A →g B →gg C) (n m : ℕ) : + gEM A (n+1) →∞g Ωg[succ n] (EMadd1 B m →** EMadd1 C m) := +begin + assert H1 : is_trunc (n+1) (Ω[n] (EMadd1 B m →** EMadd1 C m)), + { apply is_trunc_loopn, exact sorry }, +-- refine EM_homomorphism_gloop (Ω[n] (EMadd1 B m →** EMadd1 C m)) _ _, + /- the underlying pointed map is: -/ +-- exact sorry + -- refine (loopn_ppmap_pequiv _ _ _)⁻¹ᵉ* ∘* ppcompose_left !loopn_EMadd1_add⁻¹ᵉ* ∘* + -- EM0EMadd1product φ m exact sorry end diff --git a/pointed.hlean b/pointed.hlean index 9a9d76e..513ac8f 100644 --- a/pointed.hlean +++ b/pointed.hlean @@ -611,5 +611,29 @@ begin fapply phomotopy.mk, exact homotopy.rfl, refine whisker_left idp (ap_id p)⁻¹ end +structure deloopable.{u} [class] (A : pType.{u}) : Type.{u+1} := + (deloop : pType.{u}) + (deloop_pequiv : Ω deloop ≃* A) + +abbreviation deloop [unfold 2] := deloopable.deloop +abbreviation deloop_pequiv [unfold 2] := deloopable.deloop_pequiv + +definition deloopable_loop [instance] [constructor] (A : Type*) : deloopable (Ω A) := +deloopable.mk A pequiv.rfl + +definition deloopable_loopn [instance] [priority 500] (n : ℕ) [H : is_succ n] (A : Type*) : + deloopable (Ω[n] A) := +by induction H with n; exact deloopable.mk (Ω[n] A) pequiv.rfl + +definition inf_group_of_deloopable (A : Type*) [deloopable A] : inf_group A := +inf_group_equiv_closed (deloop_pequiv A) _ + +definition InfGroup_of_deloopable (A : Type*) [deloopable A] : InfGroup := +InfGroup.mk A (inf_group_of_deloopable A) + +definition deloop_isomorphism [constructor] (A : Type*) [deloopable A] : + Ωg (deloop A) ≃∞g InfGroup_of_deloopable A := +InfGroup_equiv_closed_isomorphism (Ωg (deloop A)) (deloop_pequiv A) + end pointed diff --git a/pointed_pi.hlean b/pointed_pi.hlean index cb3524e..c8d8b83 100644 --- a/pointed_pi.hlean +++ b/pointed_pi.hlean @@ -938,6 +938,15 @@ namespace pointed (Π*(a : A), Ω (B a)) ≃* Ω (Π*a, B a) := (loop_pppi_pequiv B)⁻¹ᵉ* +definition deloopable_pppi [instance] [constructor] {A : Type*} (B : A → Type*) [Πa, deloopable (B a)] : + deloopable (Π*a, B a) := +deloopable.mk (Π*a, deloop (B a)) + (loop_pppi_pequiv (λa, deloop (B a)) ⬝e* ppi_pequiv_right (λa, deloop_pequiv (B a))) + +definition deloopable_ppmap [instance] [constructor] (A B : Type*) [deloopable B] : + deloopable (A →** B) := +deloopable_pppi (λa, B) + /- below is an alternate proof strategy for the naturality of loop_pppi_pequiv_natural, where we define loop_pppi_pequiv as composite of pointed equivalences, and proved the