diff --git a/algebra/direct_sum.hlean b/algebra/direct_sum.hlean index 0d1f6c1..e4fdeef 100644 --- a/algebra/direct_sum.hlean +++ b/algebra/direct_sum.hlean @@ -6,9 +6,9 @@ Authors: Floris van Doorn, Egbert Rijke Constructions with groups -/ -import .quotient_group .free_commutative_group +import .quotient_group .free_commutative_group .product_group -open eq algebra is_trunc set_quotient relation sigma prod sum list trunc function equiv sigma.ops +open eq is_equiv algebra is_trunc set_quotient relation sigma prod sum list trunc function equiv sigma.ops namespace group @@ -89,6 +89,35 @@ namespace group end + definition binary_dirsum (G H : AbGroup) : dirsum (bool.rec G H) ≃g G ×ag H := + let branch := bool.rec G H in + let to_hom := (dirsum_elim (bool.rec (product_inl G H) (product_inr G H)) + : dirsum (bool.rec G H) →g G ×ag H) in + let from_hom := (Group_sum_elim (dirsum (bool.rec G H)) + (dirsum_incl branch bool.ff) (dirsum_incl branch bool.tt) + : G ×g H →g dirsum branch) in + begin + fapply isomorphism.mk, + { exact dirsum_elim (bool.rec (product_inl G H) (product_inr G H)) }, + fapply adjointify, + { exact from_hom }, + { intro gh, induction gh with g h, + exact prod_eq (mul_one (1 * g) ⬝ one_mul g) (ap (λ o, o * h) (mul_one 1) ⬝ one_mul h) }, + { refine dirsum.rec _ _ _, + { intro b x, + refine ap from_hom (dirsum_elim_compute (bool.rec (product_inl G H) (product_inr G H)) b x) ⬝ _, + induction b, + { exact ap (λ y, dirsum_incl branch bool.ff x * y) (to_respect_one (dirsum_incl branch bool.tt)) ⬝ mul_one _ }, + { exact ap (λ y, y * dirsum_incl branch bool.tt x) (to_respect_one (dirsum_incl branch bool.ff)) ⬝ one_mul _ } + }, + { refine ap from_hom (to_respect_one to_hom) ⬝ to_respect_one from_hom }, + { intro g h gβ hβ, + refine ap from_hom (to_respect_mul to_hom _ _) ⬝ to_respect_mul from_hom _ _ ⬝ _, + exact ap011 mul gβ hβ + } + } + end + variables {I J : Set} {Y Y' Y'' : I → AbGroup} definition dirsum_functor [constructor] (f : Πi, Y i →g Y' i) : dirsum Y →g dirsum Y' := diff --git a/algebra/product_group.hlean b/algebra/product_group.hlean index 75c1d66..2bd56d1 100644 --- a/algebra/product_group.hlean +++ b/algebra/product_group.hlean @@ -8,7 +8,7 @@ Constructions with groups import algebra.group_theory hit.set_quotient types.list types.sum .subgroup .quotient_group -open eq algebra is_trunc set_quotient relation sigma sigma.ops prod prod.ops sum list trunc function +open eq algebra is_trunc set_quotient relation sigma prod prod.ops sum list trunc function equiv namespace group @@ -61,12 +61,19 @@ namespace group infix ` ×g `:60 := group.product infix ` ×ag `:60 := group.ab_product - definition product_inl (G H : Group) : G →g G ×g H := + definition product_inl [constructor] (G H : Group) : G →g G ×g H := homomorphism.mk (λx, (x, one)) (λx y, prod_eq !refl !one_mul⁻¹) - definition product_inr (G H : Group) : H →g G ×g H := + definition product_inr [constructor] (G H : Group) : H →g G ×g H := homomorphism.mk (λx, (one, x)) (λx y, prod_eq !one_mul⁻¹ !refl) + definition Group_sum_elim [constructor] {G H : Group} (I : AbGroup) (φ : G →g I) (ψ : H →g I) : G ×g H →g I := + homomorphism.mk (λx, φ x.1 * ψ x.2) abstract (λx y, calc + φ (x.1 * y.1) * ψ (x.2 * y.2) = (φ x.1 * φ y.1) * (ψ x.2 * ψ y.2) + : by exact ap011 mul (to_respect_mul φ x.1 y.1) (to_respect_mul ψ x.2 y.2) + ... = (φ x.1 * ψ x.2) * (φ y.1 * ψ y.2) + : by exact interchange I (φ x.1) (φ y.1) (ψ x.2) (ψ y.2)) end + definition product_functor [constructor] {G G' H H' : Group} (φ : G →g H) (ψ : G' →g H') : G ×g G' →g H ×g H' := homomorphism.mk (λx, (φ x.1, ψ x.2)) (λx y, prod_eq !to_respect_mul !to_respect_mul) @@ -79,4 +86,7 @@ namespace group infix ` ×≃g `:60 := group.product_isomorphism + definition product_group_mul_eq {G H : Group} (g h : G ×g H) : g * h = product_mul g h := + idp + end group diff --git a/colim.hlean b/colim.hlean index f1b5467..7619b49 100644 --- a/colim.hlean +++ b/colim.hlean @@ -251,7 +251,7 @@ namespace seq_colim definition pshift_equiv_pinclusion {A : ℕ → Type*} (f : Πn, A n →* A (succ n)) (n : ℕ) : psquare (pinclusion f n) (pinclusion (λn, f (n+1)) n) (f n) (pshift_equiv f) := - phomotopy.mk homotopy.rfl begin + phomotopy.mk homotopy.rfl begin refine !idp_con ⬝ _, esimp, induction n with n IH, { esimp[inclusion_pt], esimp[shift_diag], exact !idp_con⁻¹ }, @@ -259,7 +259,7 @@ namespace seq_colim rewrite ap_con, rewrite ap_con, refine _ ⬝ whisker_right _ !con.assoc, refine _ ⬝ (con.assoc (_ ⬝ _) _ _)⁻¹, - xrewrite [-IH], + xrewrite [-IH], esimp[shift_up], rewrite [elim_glue, ap_inv, -ap_compose'], esimp, rewrite [-+con.assoc], apply whisker_right, rewrite con.assoc, apply !eq_inv_con_of_con_eq, @@ -285,7 +285,6 @@ namespace seq_colim !elim_glue omit p - definition is_equiv_seq_colim_functor [constructor] [H : Πn, is_equiv (@g n)] : is_equiv (seq_colim_functor @g p) := adjointify _ (seq_colim_functor (λn, (@g _)⁻¹) (λn a, inv_commute' g f f' p a)) @@ -323,25 +322,34 @@ namespace seq_colim : Π(x : seq_colim f), P x := by induction v with Pincl Pglue; exact seq_colim.rec f Pincl Pglue - definition pseq_colim_pequiv [constructor] {A A' : ℕ → Type*} {f : Π{n}, A n →* A (n+1)} - {f' : Π{n}, A' n →* A' (n+1)} (g : Π{n}, A n ≃* A' n) - (p : Π⦃n⦄, g ∘* f ~ f' ∘* g) : pseq_colim @f ≃* pseq_colim @f' := - pequiv_of_equiv (seq_colim_equiv @g p) (ap (ι _) (respect_pt g)) + definition pseq_colim_pequiv' [constructor] {A A' : ℕ → Type*} {f : Πn, A n →* A (n+1)} + {f' : Πn, A' n →* A' (n+1)} (g : Πn, A n ≃* A' n) + (p : Π⦃n⦄, g (n+1) ∘* f n ~ f' n ∘* g n) : pseq_colim @f ≃* pseq_colim @f' := + pequiv_of_equiv (seq_colim_equiv g p) (ap (ι _) (respect_pt (g _))) + + definition pseq_colim_pequiv [constructor] {A A' : ℕ → Type*} {f : Πn, A n →* A (n+1)} + {f' : Πn, A' n →* A' (n+1)} (g : Πn, A n ≃* A' n) + (p : Πn, g (n+1) ∘* f n ~* f' n ∘* g n) : pseq_colim @f ≃* pseq_colim @f' := + pseq_colim_pequiv' g (λn, @p n) definition seq_colim_equiv_constant [constructor] {A : ℕ → Type*} {f f' : Π⦃n⦄, A n → A (n+1)} (p : Π⦃n⦄ (a : A n), f a = f' a) : seq_colim f ≃ seq_colim f' := seq_colim_equiv (λn, erfl) p - definition pseq_colim_equiv_constant [constructor] {A : ℕ → Type*} {f f' : Π{n}, A n →* A (n+1)} - (p : Π⦃n⦄, f ~ f') : pseq_colim @f ≃* pseq_colim @f' := - pseq_colim_pequiv (λn, pequiv.rfl) p + definition pseq_colim_equiv_constant' [constructor] {A : ℕ → Type*} {f f' : Πn, A n →* A (n+1)} + (p : Π⦃n⦄, f n ~ f' n) : pseq_colim @f ≃* pseq_colim @f' := + pseq_colim_pequiv' (λn, pequiv.rfl) p - definition pseq_colim_pequiv_pinclusion {A A' : ℕ → Type*} {f : Π(n), A n →* A (n+1)} - {f' : Π(n), A' n →* A' (n+1)} (g : Π(n), A n ≃* A' n) + definition pseq_colim_equiv_constant [constructor] {A : ℕ → Type*} {f f' : Πn, A n →* A (n+1)} + (p : Πn, f n ~* f' n) : pseq_colim @f ≃* pseq_colim @f' := + pseq_colim_pequiv (λn, pequiv.rfl) (λn, !pid_pcompose ⬝* p n ⬝* !pcompose_pid⁻¹*) + + definition pseq_colim_pequiv_pinclusion {A A' : ℕ → Type*} {f : Πn, A n →* A (n+1)} + {f' : Πn, A' n →* A' (n+1)} (g : Πn, A n ≃* A' n) (p : Π⦃n⦄, g (n+1) ∘* f n ~* f' n ∘* g n) (n : ℕ) : psquare (pinclusion f n) (pinclusion f' n) (g n) (pseq_colim_pequiv g p) := - phomotopy.mk homotopy.rfl begin - esimp, refine !idp_con ⬝ _, + phomotopy.mk homotopy.rfl begin + esimp, refine !idp_con ⬝ _, induction n with n IH, { esimp[inclusion_pt], exact !idp_con⁻¹ }, { esimp[inclusion_pt], rewrite [+ap_con, -+ap_inv, +con.assoc, +seq_colim_functor_glue], @@ -350,25 +358,24 @@ namespace seq_colim apply whisker_right, esimp, rewrite[(eq_con_inv_of_con_eq (!to_homotopy_pt))], rewrite[ap_con], esimp, - rewrite[-+con.assoc], - rewrite[ap_con], rewrite[-ap_compose'], - rewrite[+ap_inv], + rewrite[-+con.assoc, ap_con, -ap_compose', +ap_inv], rewrite[-+con.assoc], refine _ ⬝ whisker_right _ (whisker_right _ (whisker_right _ (whisker_right _ !con.left_inv⁻¹))), - rewrite[idp_con], - rewrite[+con.assoc], apply whisker_left, - rewrite[ap_con], rewrite[-ap_compose'], - rewrite[con_inv], - rewrite[+con.assoc], apply whisker_left, + rewrite[idp_con, +con.assoc], apply whisker_left, + rewrite[ap_con, -ap_compose', con_inv, +con.assoc], apply whisker_left, refine eq_inv_con_of_con_eq _, symmetry, exact eq_of_square !natural_square } end - definition seq_colim_equiv_constant_pinclusion {A : ℕ → Type*} {f f' : Π⦃n⦄, A n →* A (n+1)} - (p : Π⦃n⦄ (a : A n), f a = f' a) (n : ℕ) : + definition seq_colim_equiv_constant_pinclusion {A : ℕ → Type*} {f f' : Πn, A n →* A (n+1)} + (p : Πn, f n ~* f' n) (n : ℕ) : pseq_colim_equiv_constant p ∘* pinclusion f n ~* pinclusion f' n := - sorry + begin + transitivity pinclusion f' n ∘* !pid, + refine phomotopy_of_psquare !pseq_colim_pequiv_pinclusion, + exact !pcompose_pid + end definition is_equiv_seq_colim_rec (P : seq_colim f → Type) : is_equiv (seq_colim_rec_unc : @@ -392,7 +399,7 @@ namespace seq_colim equiv.mk _ !is_equiv_seq_colim_rec end functor - definition pseq_colim.elim [constructor] {A : ℕ → Type*} {B : Type*} {f : Π{n}, A n →* A (n+1)} + definition pseq_colim.elim' [constructor] {A : ℕ → Type*} {B : Type*} {f : Π{n}, A n →* A (n+1)} (g : Πn, A n →* B) (p : Πn, g (n+1) ∘* f ~ g n) : pseq_colim @f →* B := begin fapply pmap.mk, @@ -402,6 +409,10 @@ namespace seq_colim { esimp, apply respect_pt } end + definition pseq_colim.elim [constructor] {A : ℕ → Type*} {B : Type*} {f : Π{n}, A n →* A (n+1)} + (g : Πn, A n →* B) (p : Πn, g (n+1) ∘* f ~* g n) : pseq_colim @f →* B := + pseq_colim.elim' g p + definition prep0 [constructor] {A : ℕ → Type*} (f : pseq_diagram A) (k : ℕ) : A 0 →* A k := pmap.mk (rep0 (λn x, f x) k) begin induction k with k p, reflexivity, exact ap (@f k) p ⬝ !respect_pt end diff --git a/homology/homology.hlean b/homology/homology.hlean index 32e79f8..6fe727b 100644 --- a/homology/homology.hlean +++ b/homology/homology.hlean @@ -1,3 +1,11 @@ +/- +Copyright (c) 2017 Yuri Sulyma, Favonia +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Yuri Sulyma, Favonia + +Reduced homology theories +-/ + import ..homotopy.spectrum ..homotopy.EM ..algebra.arrow_group ..algebra.direct_sum ..homotopy.fwedge ..choice ..homotopy.pushout ..move_to_lib open eq spectrum int pointed group algebra sphere nat equiv susp is_trunc @@ -10,36 +18,39 @@ namespace homology structure homology_theory.{u} : Type.{u+1} := (HH : ℤ → pType.{u} → AbGroup.{u}) (Hh : Π(n : ℤ) {X Y : Type*} (f : X →* Y), HH n X →g HH n Y) - (Hid : Π(n : ℤ) {X : Type*} (x : HH n X), Hh n (pid X) x = x) - (Hcompose : Π(n : ℤ) {X Y Z : Type*} (f : Y →* Z) (g : X →* Y), + (Hpid : Π(n : ℤ) {X : Type*} (x : HH n X), Hh n (pid X) x = x) + (Hpcompose : Π(n : ℤ) {X Y Z : Type*} (f : Y →* Z) (g : X →* Y), Hh n (f ∘* g) ~ Hh n f ∘ Hh n g) - (Hsusp : Π(n : ℤ) (X : Type*), HH (succ n) (psusp X) ≃g HH n X) - (Hsusp_natural : Π(n : ℤ) {X Y : Type*} (f : X →* Y), - Hsusp n Y ∘ Hh (succ n) (psusp_functor f) ~ Hh n f ∘ Hsusp n X) + (Hpsusp : Π(n : ℤ) (X : Type*), HH (succ n) (psusp X) ≃g HH n X) + (Hpsusp_natural : Π(n : ℤ) {X Y : Type*} (f : X →* Y), + Hpsusp n Y ∘ Hh (succ n) (psusp_functor f) ~ Hh n f ∘ Hpsusp n X) (Hexact : Π(n : ℤ) {X Y : Type*} (f : X →* Y), is_exact_g (Hh n f) (Hh n (pcod f))) (Hadditive : Π(n : ℤ) {I : Set.{u}} (X : I → Type*), is_equiv (dirsum_elim (λi, Hh n (pinl i)) : dirsum (λi, HH n (X i)) → HH n (⋁ X))) + structure ordinary_homology_theory.{u} extends homology_theory.{u} : Type.{u+1} := + (Hdimension : Π(n : ℤ), n ≠ 0 → is_contr (HH n (plift (psphere 0)))) + section parameter (theory : homology_theory) open homology_theory theorem HH_base_indep (n : ℤ) {A : Type} (a b : A) : HH theory n (pType.mk A a) ≃g HH theory n (pType.mk A b) := - calc HH theory n (pType.mk A a) ≃g HH theory (int.succ n) (psusp A) : by exact (Hsusp theory n (pType.mk A a)) ⁻¹ᵍ - ... ≃g HH theory n (pType.mk A b) : by exact Hsusp theory n (pType.mk A b) + calc HH theory n (pType.mk A a) ≃g HH theory (int.succ n) (psusp A) : by exact (Hpsusp theory n (pType.mk A a)) ⁻¹ᵍ + ... ≃g HH theory n (pType.mk A b) : by exact Hpsusp theory n (pType.mk A b) theorem Hh_homotopy' (n : ℤ) {A B : Type*} (f : A → B) (p q : f pt = pt) : Hh theory n (pmap.mk f p) ~ Hh theory n (pmap.mk f q) := λ x, calc Hh theory n (pmap.mk f p) x - = Hh theory n (pmap.mk f p) (Hsusp theory n A ((Hsusp theory n A)⁻¹ᵍ x)) - : by exact ap (Hh theory n (pmap.mk f p)) (equiv.to_right_inv (equiv_of_isomorphism (Hsusp theory n A)) x)⁻¹ - ... = Hsusp theory n B (Hh theory (succ n) (pmap.mk (susp.functor f) !refl) ((Hsusp theory n A)⁻¹ x)) - : by exact (Hsusp_natural theory n (pmap.mk f p) ((Hsusp theory n A)⁻¹ᵍ x))⁻¹ - ... = Hh theory n (pmap.mk f q) (Hsusp theory n A ((Hsusp theory n A)⁻¹ x)) - : by exact Hsusp_natural theory n (pmap.mk f q) ((Hsusp theory n A)⁻¹ x) + = Hh theory n (pmap.mk f p) (Hpsusp theory n A ((Hpsusp theory n A)⁻¹ᵍ x)) + : by exact ap (Hh theory n (pmap.mk f p)) (equiv.to_right_inv (equiv_of_isomorphism (Hpsusp theory n A)) x)⁻¹ + ... = Hpsusp theory n B (Hh theory (succ n) (pmap.mk (susp.functor f) !refl) ((Hpsusp theory n A)⁻¹ x)) + : by exact (Hpsusp_natural theory n (pmap.mk f p) ((Hpsusp theory n A)⁻¹ᵍ x))⁻¹ + ... = Hh theory n (pmap.mk f q) (Hpsusp theory n A ((Hpsusp theory n A)⁻¹ x)) + : by exact Hpsusp_natural theory n (pmap.mk f q) ((Hpsusp theory n A)⁻¹ x) ... = Hh theory n (pmap.mk f q) x - : by exact ap (Hh theory n (pmap.mk f q)) (equiv.to_right_inv (equiv_of_isomorphism (Hsusp theory n A)) x) + : by exact ap (Hh theory n (pmap.mk f q)) (equiv.to_right_inv (equiv_of_isomorphism (Hpsusp theory n A)) x) theorem Hh_homotopy (n : ℤ) {A B : Type*} (f g : A →* B) (h : f ~ g) : Hh theory n f ~ Hh theory n g := λ x, calc Hh theory n f x @@ -56,18 +67,71 @@ namespace homology { exact Hh theory n e⁻¹ᵉ* }, { intro x, exact calc Hh theory n e (Hh theory n e⁻¹ᵉ* x) - = Hh theory n (e ∘* e⁻¹ᵉ*) x : by exact (Hcompose theory n e e⁻¹ᵉ* x)⁻¹ + = Hh theory n (e ∘* e⁻¹ᵉ*) x : by exact (Hpcompose theory n e e⁻¹ᵉ* x)⁻¹ ... = Hh theory n !pid x : by exact Hh_homotopy n (e ∘* e⁻¹ᵉ*) !pid (to_right_inv e) x - ... = x : by exact Hid theory n x + ... = x : by exact Hpid theory n x }, { intro x, exact calc Hh theory n e⁻¹ᵉ* (Hh theory n e x) - = Hh theory n (e⁻¹ᵉ* ∘* e) x : by exact (Hcompose theory n e⁻¹ᵉ* e x)⁻¹ + = Hh theory n (e⁻¹ᵉ* ∘* e) x : by exact (Hpcompose theory n e⁻¹ᵉ* e x)⁻¹ ... = Hh theory n !pid x : by exact Hh_homotopy n (e⁻¹ᵉ* ∘* e) !pid (to_left_inv e) x - ... = x : by exact Hid theory n x + ... = x : by exact Hpid theory n x } end end +/- homology theory associated to a spectrum -/ +definition homology (X : Type*) (E : spectrum) (n : ℤ) : AbGroup := +shomotopy_group n (smash_spectrum X E) + +definition parametrized_homology {X : Type*} (E : X → spectrum) (n : ℤ) : AbGroup := +sorry + +definition ordinary_homology [reducible] (X : Type*) (G : AbGroup) (n : ℤ) : AbGroup := +homology X (EM_spectrum G) n + +definition ordinary_homology_Z [reducible] (X : Type*) (n : ℤ) : AbGroup := +ordinary_homology X agℤ n + +notation `H_` n `[`:0 X:0 `, ` E:0 `]`:0 := homology X E n +notation `H_` n `[`:0 X:0 `]`:0 := ordinary_homology_Z X n +notation `pH_` n `[`:0 binders `, ` r:(scoped E, parametrized_homology E n) `]`:0 := r + +definition unpointed_homology (X : Type) (E : spectrum) (n : ℤ) : AbGroup := +H_ n[X₊, E] + +definition homology_functor [constructor] {X Y : Type*} {E F : spectrum} (f : X →* Y) (g : E →ₛ F) (n : ℤ) : homology X E n →g homology Y F n := +shomotopy_group_fun n (smash_spectrum_fun f g) + +definition homology_theory_spectrum.{u} [constructor] (E : spectrum.{u}) : homology_theory.{u} := +begin + refine homology_theory.mk _ _ _ _ _ _ _ _, + exact (λn X, H_ n[X, E]), + exact (λn X Y f, homology_functor f (sid E) n), + exact sorry, -- Hid is uninteresting but potentially very hard to prove + exact sorry, + exact sorry, + exact sorry, + exact sorry, + exact sorry + -- sorry + -- sorry + -- sorry + -- sorry + -- sorry + -- sorry +-- (λn A, H^n[A, Y]) +-- (λn A B f, cohomology_isomorphism f Y n) +-- (λn A, cohomology_isomorphism_refl A Y n) +-- (λn A B f, cohomology_functor f Y n) +-- (λn A B f g p, cohomology_functor_phomotopy p Y n) +-- (λn A B f x, cohomology_functor_phomotopy_refl f Y n x) +-- (λn A x, cohomology_functor_pid A Y n x) +-- (λn A B C g f x, cohomology_functor_pcompose g f Y n x) +-- (λn A, cohomology_psusp A Y n) +-- (λn A B f, cohomology_psusp_natural f Y n) +-- (λn A B f, cohomology_exact f Y n) +-- (λn I A H, spectrum_additive H A Y n) +end end homology diff --git a/homology/sphere.hlean b/homology/sphere.hlean index 6d9ed54..d6f789f 100644 --- a/homology/sphere.hlean +++ b/homology/sphere.hlean @@ -5,7 +5,6 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Kuen-Bang Hou (Favonia) -/ -import core import .homology open eq pointed group algebra circle sphere nat equiv susp @@ -18,7 +17,7 @@ section open homology_theory - theorem Hsphere : Π(n : ℤ)(m : ℕ), HH theory n (plift (psphere m)) ≃g HH theory (n - m) (plift (psphere 0)) := + theorem Hpsphere : Π(n : ℤ)(m : ℕ), HH theory n (plift (psphere m)) ≃g HH theory (n - m) (plift (psphere 0)) := begin intros n m, revert n, induction m with m, { exact λ n, isomorphism_ap (λ n, HH theory n (plift (psphere 0))) (sub_zero n)⁻¹ }, @@ -27,7 +26,7 @@ section ≃g HH theory n (psusp (plift (psphere m))) : by exact HH_isomorphism theory n (plift_psusp (psphere m)) ... ≃g HH theory (succ (pred n)) (psusp (plift (psphere m))) : by exact isomorphism_ap (λ n, HH theory n (psusp (plift (psphere m)))) (succ_pred n)⁻¹ - ... ≃g HH theory (pred n) (plift (psphere m)) : by exact Hsusp theory (pred n) (plift (psphere m)) + ... ≃g HH theory (pred n) (plift (psphere m)) : by exact Hpsusp theory (pred n) (plift (psphere m)) ... ≃g HH theory (pred n - m) (plift (psphere 0)) : by exact v_0 (pred n) ... ≃g HH theory (n - succ m) (plift (psphere 0)) : by exact isomorphism_ap (λ n, HH theory n (plift (psphere 0))) (sub_sub n 1 m ⬝ ap (λ m, n - m) (add.comm 1 m)) diff --git a/homotopy/cohomology.hlean b/homotopy/cohomology.hlean index 38a7e4c..8c25b70 100644 --- a/homotopy/cohomology.hlean +++ b/homotopy/cohomology.hlean @@ -189,7 +189,7 @@ structure cohomology_theory.{u} : Type.{u+1} := (Hadditive : Π(n : ℤ) {I : Type.{u}} (X : I → Type*), has_choice 0 I → is_equiv (Group_pi_intro (λi, Hh n (pinl i)) : HH n (⋁ X) → Πᵍ i, HH n (X i))) -structure ordinary_theory.{u} extends cohomology_theory.{u} : Type.{u+1} := +structure ordinary_cohomology_theory.{u} extends cohomology_theory.{u} : Type.{u+1} := (Hdimension : Π(n : ℤ), n ≠ 0 → is_contr (HH n (plift pbool))) attribute cohomology_theory.HH [coercion] @@ -270,7 +270,7 @@ cohomology_theory.mk -- print has_choice_lift -- print equiv_lift -- print has_choice_equiv_closed -definition ordinary_theory_EM [constructor] (G : AbGroup) : ordinary_theory := -⦃ordinary_theory, cohomology_theory_spectrum (EM_spectrum G), Hdimension := EM_dimension G ⦄ +definition ordinary_cohomology_theory_EM [constructor] (G : AbGroup) : ordinary_cohomology_theory := +⦃ordinary_cohomology_theory, cohomology_theory_spectrum (EM_spectrum G), Hdimension := EM_dimension G ⦄ end cohomology diff --git a/homotopy/spectrum.hlean b/homotopy/spectrum.hlean index 33dc6aa..7e4fdb2 100644 --- a/homotopy/spectrum.hlean +++ b/homotopy/spectrum.hlean @@ -146,7 +146,7 @@ namespace spectrum -- I guess this manual eta-expansion is necessary because structures lack definitional eta? := phomotopy.mk (glue_square f n) (to_homotopy_pt (glue_square f n)) - definition sid {N : succ_str} (E : gen_spectrum N) : E →ₛ E := + definition sid {N : succ_str} (E : gen_prespectrum N) : E →ₛ E := smap.mk (λn, pid (E n)) (λn, calc glue E n ∘* pid (E n) ~* glue E n : pcompose_pid ... ~* pid (Ω(E (S n))) ∘* glue E n : pid_pcompose @@ -373,13 +373,17 @@ namespace spectrum definition spectrify_type_term {N : succ_str} (X : gen_prespectrum N) (n : N) (k : ℕ) : Type* := Ω[k] (X (n +' k)) - definition spectrify_type_fun' {N : succ_str} (X : gen_prespectrum N) (k : ℕ) (n : N) : + definition spectrify_type_fun' {N : succ_str} (X : gen_prespectrum N) (n : N) (k : ℕ) : Ω[k] (X n) →* Ω[k+1] (X (S n)) := !loopn_succ_in⁻¹ᵉ* ∘* Ω→[k] (glue X n) definition spectrify_type_fun {N : succ_str} (X : gen_prespectrum N) (n : N) (k : ℕ) : spectrify_type_term X n k →* spectrify_type_term X n (k+1) := - spectrify_type_fun' X k (n +' k) + spectrify_type_fun' X (n +' k) k + + definition spectrify_type_fun_zero {N : succ_str} (X : gen_prespectrum N) (n : N) : + spectrify_type_fun X n 0 ~* glue X n := + !pid_pcompose definition spectrify_type {N : succ_str} (X : gen_prespectrum N) (n : N) : Type* := pseq_colim (spectrify_type_fun X n) @@ -393,20 +397,28 @@ namespace spectrum ... ≡ Y n -/ + definition spectrify_type_fun'_succ {N : succ_str} (X : gen_prespectrum N) (n : N) (k : ℕ) : + spectrify_type_fun' X n (succ k) ~* Ω→ (spectrify_type_fun' X n k) := + begin + refine _ ⬝* !ap1_pcompose⁻¹*, + apply !pwhisker_right, + refine !to_pinv_pequiv_MK2 + end + definition spectrify_pequiv {N : succ_str} (X : gen_prespectrum N) (n : N) : spectrify_type X n ≃* Ω (spectrify_type X (S n)) := begin refine !pshift_equiv ⬝e* _, - transitivity pseq_colim (λk, spectrify_type_fun' X (succ k) (S n +' k)), + transitivity pseq_colim (λk, spectrify_type_fun' X (S n +' k) (succ k)), fapply pseq_colim_pequiv, { intro n, apply loopn_pequiv_loopn, apply pequiv_ap X, apply succ_str.add_succ }, - { intro k, apply to_homotopy, + { exact abstract begin intro k, refine !passoc⁻¹* ⬝* _, refine pwhisker_right _ (loopn_succ_in_inv_natural (succ k) _) ⬝* _, refine !passoc ⬝* _ ⬝* !passoc⁻¹*, apply pwhisker_left, refine !apn_pcompose⁻¹* ⬝* _ ⬝* !apn_pcompose, apply apn_phomotopy, - exact !glue_ptransport⁻¹* }, + exact !glue_ptransport⁻¹* end end }, refine _ ⬝e* !pseq_colim_loop⁻¹ᵉ*, - refine pseq_colim_equiv_constant (λn, !ap1_pcompose⁻¹*), + exact pseq_colim_equiv_constant (λn, !spectrify_type_fun'_succ), end definition spectrify [constructor] {N : succ_str} (X : gen_prespectrum N) : gen_spectrum N := @@ -419,21 +431,31 @@ namespace spectrum -- note: the forward map is (currently) not definitionally equal to gluen. Is that a problem? definition equiv_gluen {N : succ_str} (X : gen_spectrum N) (n : N) (k : ℕ) : X n ≃* Ω[k] (X (n +' k)) := - by induction k with k f; reflexivity; exact f ⬝e* loopn_pequiv_loopn k (equiv_glue X (n +' k)) - ⬝e* !loopn_succ_in⁻¹ᵉ* + by induction k with k f; reflexivity; exact f ⬝e* (loopn_pequiv_loopn k (equiv_glue X (n +' k)) + ⬝e* !loopn_succ_in⁻¹ᵉ*) + + definition equiv_gluen_inv_succ {N : succ_str} (X : gen_spectrum N) (n : N) (k : ℕ) : + (equiv_gluen X n (k+1))⁻¹ᵉ* ~* + (equiv_gluen X n k)⁻¹ᵉ* ∘* Ω→[k] (equiv_glue X (n +' k))⁻¹ᵉ* ∘* !loopn_succ_in := + begin + refine !trans_pinv ⬝* pwhisker_left _ _, refine !trans_pinv ⬝* _, refine !to_pinv_pequiv_MK2 ◾* !pinv_pinv + end definition spectrify_map {N : succ_str} {X : gen_prespectrum N} : X →ₛ spectrify X := begin fapply smap.mk, { intro n, exact pinclusion _ 0 }, - { intro n, apply phomotopy_of_psquare, refine !pid_pcompose⁻¹* ⬝ph* _, + { intro n, apply phomotopy_of_psquare, refine !pid_pcompose⁻¹* ⬝ph* _, - --pshift_equiv_pinclusion (spectrify_type_fun X n) 0 - refine _ ⬝v* _, - rotate 1, exact pshift_equiv_pinclusion (spectrify_type_fun X n) 0, --- refine !passoc⁻¹* ⬝* pwhisker_left _ _ ⬝* _, - exact sorry -} + refine !passoc ⬝* pwhisker_left _ (pshift_equiv_pinclusion (spectrify_type_fun X n) 0) ⬝* _, + refine !passoc⁻¹* ⬝* _, + refine _ ◾* (spectrify_type_fun_zero X n ⬝* !pid_pcompose⁻¹*), + refine !passoc ⬝* pwhisker_left _ !pseq_colim_pequiv_pinclusion ⬝* _, + refine pwhisker_left _ (pwhisker_left _ (ap1_pid) ⬝* !pcompose_pid) ⬝* _, + refine !passoc ⬝* pwhisker_left _ !seq_colim_equiv_constant_pinclusion ⬝* _, + apply pinv_left_phomotopy_of_phomotopy, + exact !pseq_colim_loop_pinclusion⁻¹* + } end definition spectrify.elim {N : succ_str} {X : gen_prespectrum N} {Y : gen_spectrum N} @@ -442,10 +464,25 @@ namespace spectrum fapply smap.mk, { intro n, fapply pseq_colim.elim, { intro k, refine !equiv_gluen⁻¹ᵉ* ∘* apn k (f (n +' k)) }, - { intro k, apply to_homotopy, exact sorry }}, + { intro k, refine !passoc ⬝* pwhisker_right _ !equiv_gluen_inv_succ ⬝* _, + refine !passoc ⬝* _, apply pwhisker_left, + refine !passoc ⬝* _, + refine pwhisker_left _ ((passoc _ _ (_ ∘* _))⁻¹*) ⬝* _, + refine pwhisker_left _ !passoc⁻¹* ⬝* _, + refine pwhisker_left _ (pwhisker_right _ (phomotopy_pinv_right_of_phomotopy (!loopn_succ_in_natural)⁻¹*)⁻¹*) ⬝* _, + refine pwhisker_right _ !apn_pinv ⬝* _, + refine (phomotopy_pinv_left_of_phomotopy _)⁻¹*, + refine pwhisker_right _ !pmap_eta⁻¹* ⬝* _, + refine apn_psquare k _, + refine pwhisker_right _ _ ⬝* psquare_of_phomotopy !smap.glue_square, + exact !pmap_eta⁻¹* + }}, { intro n, exact sorry } end + definition spectrify_fun {N : succ_str} {X Y : gen_prespectrum N} (f : X →ₛ Y) : spectrify X →ₛ spectrify Y := + spectrify.elim ((@spectrify_map _ Y) ∘ₛ f) + /- Tensor by spaces -/ /- Smash product of spectra -/ @@ -461,6 +498,28 @@ prespectrum.mk (λ z, X ∧ Y z) begin exact !glue end +definition smash_prespectrum_fun {X X' : Type*} {Y Y' : prespectrum} (f : X →* X') (g : Y →ₛ Y') : smash_prespectrum X Y →ₛ smash_prespectrum X' Y' := +smap.mk (λn, smash_functor f (g n)) begin + intro n, + refine susp_to_loop_psquare _ _ _ _ _, + refine pvconcat (psquare_transpose (phinverse (smash_psusp_natural f (g n)))) _, + refine vconcat_phomotopy _ (smash_functor_split f (g (S n))), + refine phomotopy_vconcat (smash_functor_split f (psusp_functor (g n))) _, + refine phconcat _ _, + let glue_adjoint := psusp_pelim (Y n) (Y (S n)) (glue Y n), + exact pid X' ∧→ glue_adjoint, + exact smash_functor_psquare (pvrefl f) (phrefl glue_adjoint), + refine smash_functor_psquare (phrefl (pid X')) _, + refine loop_to_susp_square _ _ _ _ _, + exact smap.glue_square g n +end + +definition smash_spectrum (X : Type*) (Y : spectrum) : spectrum := +spectrify (smash_prespectrum X Y) + +definition smash_spectrum_fun {X X' : Type*} {Y Y' : spectrum} (f : X →* X') (g : Y →ₛ Y') : smash_spectrum X Y →ₛ smash_spectrum X' Y' := +spectrify_fun (smash_prespectrum_fun f g) + /- Cofibers and stability -/ /- The Eilenberg-MacLane spectrum -/ diff --git a/move_to_lib.hlean b/move_to_lib.hlean index c34b769..eb666c3 100644 --- a/move_to_lib.hlean +++ b/move_to_lib.hlean @@ -1,6 +1,6 @@ -- definitions, theorems and attributes which should be moved to files in the HoTT library -import homotopy.sphere2 homotopy.cofiber homotopy.wedge hit.prop_trunc hit.set_quotient eq2 +import homotopy.sphere2 homotopy.cofiber homotopy.wedge hit.prop_trunc hit.set_quotient eq2 types.pointed2 .homotopy.smash_adjoint open eq nat int susp pointed pmap sigma is_equiv equiv fiber algebra trunc trunc_index pi group is_trunc function sphere unit sum prod bool @@ -558,3 +558,32 @@ open trunc fiber image end end injective_surjective + +-- Yuri Sulyma's code from HoTT MRC + +notation `⅀→`:(max+5) := psusp_functor + +namespace pointed + variables {A₀₀ A₂₀ A₀₂ A₂₂ : Type*} + {f₁₀ : A₀₀ →* A₂₀} {f₁₂ : A₀₂ →* A₂₂} + {f₀₁ : A₀₀ →* A₀₂} {f₂₁ : A₂₀ →* A₂₂} + + definition psquare_transpose (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) : psquare f₀₁ f₂₁ f₁₀ f₁₂ := p⁻¹* + + definition suspend_psquare (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) : psquare (⅀→ f₁₀) (⅀→ f₁₂) (⅀→ f₀₁) (⅀→ f₂₁) := +sorry + + definition susp_to_loop_psquare (f₁₀ : A₀₀ →* A₂₀) (f₁₂ : A₀₂ →* A₂₂) (f₀₁ : psusp A₀₀ →* A₀₂) (f₂₁ : psusp A₂₀ →* A₂₂) : (psquare (⅀→ f₁₀) f₁₂ f₀₁ f₂₁) → (psquare f₁₀ (Ω→ f₁₂) ((loop_psusp_pintro A₀₀ A₀₂) f₀₁) ((loop_psusp_pintro A₂₀ A₂₂) f₂₁)) := + begin + intro p, + refine pvconcat _ (ap1_psquare p), + exact loop_psusp_unit_natural f₁₀ + end + + definition loop_to_susp_square (f₁₀ : A₀₀ →* A₂₀) (f₁₂ : A₀₂ →* A₂₂) (f₀₁ : A₀₀ →* Ω A₀₂) (f₂₁ : A₂₀ →* Ω A₂₂) : (psquare f₁₀ (Ω→ f₁₂) f₀₁ f₂₁) → (psquare (⅀→ f₁₀) f₁₂ ((psusp_pelim A₀₀ A₀₂) f₀₁) ((psusp_pelim A₂₀ A₂₂) f₂₁)) := + begin + intro p, + refine pvconcat (suspend_psquare p) _, + exact psquare_transpose (loop_psusp_counit_natural f₁₂) + end +end pointed diff --git a/pointed.hlean b/pointed.hlean index 8f1ea82..453a3cd 100644 --- a/pointed.hlean +++ b/pointed.hlean @@ -142,5 +142,13 @@ namespace pointed -- definition phomotopy_eq_equiv_phomotopy2 : p = q ≃ p ~*2 q := -- sorry +/- Homotopy between a function and its eta expansion -/ + + definition pmap_eta {X Y : Type*} (f : X →* Y) : f ~* pmap.mk f (pmap.resp_pt f) := + begin + fapply phomotopy.mk, + reflexivity, + esimp, exact !idp_con + end end pointed