diff --git a/group_theory/constructions.hlean b/algebra/group_constructions.hlean similarity index 99% rename from group_theory/constructions.hlean rename to algebra/group_constructions.hlean index 2f679b1..b5ec4f0 100644 --- a/group_theory/constructions.hlean +++ b/algebra/group_constructions.hlean @@ -3,10 +3,10 @@ Copyright (c) 2015 Floris van Doorn. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Floris van Doorn -Constructions of groups +Constructions with groups -/ -import .basic hit.set_quotient types.sigma types.list types.sum +import algebra.group_theory hit.set_quotient types.sigma types.list types.sum open eq algebra is_trunc set_quotient relation sigma sigma.ops prod prod.ops sum list trunc function equiv diff --git a/group_theory/basic.hlean b/group_theory/basic.hlean deleted file mode 100644 index 73a0590..0000000 --- a/group_theory/basic.hlean +++ /dev/null @@ -1,202 +0,0 @@ -/- -Copyright (c) 2015 Floris van Doorn. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Floris van Doorn - -Basic group theory --/ - - -/- - Groups are defined in the HoTT library in algebra/group, as part of the algebraic hierarchy. - However, there is currently no group theory. - The only relevant defintions are the trivial group (in types/unit) and some files in algebra/ --/ - -import types.pointed types.pi algebra.bundled algebra.category.category - -open eq algebra pointed function is_trunc pi category equiv is_equiv -set_option class.force_new true - -namespace group - - definition pointed_Group [instance] (G : Group) : pointed G := pointed.mk one - definition pType_of_Group [reducible] (G : Group) : Type* := pointed.mk' G - definition Set_of_Group (G : Group) : Set := trunctype.mk G _ - - definition Group_of_CommGroup [coercion] [constructor] (G : CommGroup) : Group := - Group.mk G _ - - definition comm_group_Group_of_CommGroup [instance] [constructor] (G : CommGroup) - : comm_group (Group_of_CommGroup G) := - begin esimp, exact _ end - - definition group_pType_of_Group [instance] (G : Group) : group (pType_of_Group G) := - Group.struct G - - /- group homomorphisms -/ - - definition is_homomorphism [class] [reducible] - {G₁ G₂ : Type} [group G₁] [group G₂] (φ : G₁ → G₂) : Type := - Π(g h : G₁), φ (g * h) = φ g * φ h - - section - variables {G G₁ G₂ G₃ : Type} {g h : G₁} (ψ : G₂ → G₃) {φ₁ φ₂ : G₁ → G₂} (φ : G₁ → G₂) - [group G] [group G₁] [group G₂] [group G₃] - [is_homomorphism ψ] [is_homomorphism φ₁] [is_homomorphism φ₂] [is_homomorphism φ] - - definition respect_mul /- φ -/ : Π(g h : G₁), φ (g * h) = φ g * φ h := - by assumption - - theorem respect_one /- φ -/ : φ 1 = 1 := - mul.right_cancel - (calc - φ 1 * φ 1 = φ (1 * 1) : respect_mul φ - ... = φ 1 : ap φ !one_mul - ... = 1 * φ 1 : one_mul) - - theorem respect_inv /- φ -/ (g : G₁) : φ g⁻¹ = (φ g)⁻¹ := - eq_inv_of_mul_eq_one (!respect_mul⁻¹ ⬝ ap φ !mul.left_inv ⬝ !respect_one) - - definition is_embedding_homomorphism /- φ -/ (H : Π{g}, φ g = 1 → g = 1) : is_embedding φ := - begin - apply function.is_embedding_of_is_injective, - intro g g' p, - apply eq_of_mul_inv_eq_one, - apply H, - refine !respect_mul ⬝ _, - rewrite [respect_inv φ, p], - apply mul.right_inv - end - - definition is_homomorphism_compose {ψ : G₂ → G₃} {φ : G₁ → G₂} - (H1 : is_homomorphism ψ) (H2 : is_homomorphism φ) : is_homomorphism (ψ ∘ φ) := - λg h, ap ψ !respect_mul ⬝ !respect_mul - - definition is_homomorphism_id (G : Type) [group G] : is_homomorphism (@id G) := - λg h, idp - - end - - structure homomorphism (G₁ G₂ : Group) : Type := - (φ : G₁ → G₂) - (p : is_homomorphism φ) - - infix ` →g `:55 := homomorphism - - definition group_fun [unfold 3] [coercion] := @homomorphism.φ - definition homomorphism.struct [instance] [priority 2000] {G₁ G₂ : Group} (φ : G₁ →g G₂) - : is_homomorphism φ := - homomorphism.p φ - - variables {G G₁ G₂ G₃ : Group} {g h : G₁} {ψ : G₂ →g G₃} {φ₁ φ₂ : G₁ →g G₂} (φ : G₁ →g G₂) - - definition to_respect_mul /- φ -/ (g h : G₁) : φ (g * h) = φ g * φ h := - respect_mul φ g h - - theorem to_respect_one /- φ -/ : φ 1 = 1 := - respect_one φ - - theorem to_respect_inv /- φ -/ (g : G₁) : φ g⁻¹ = (φ g)⁻¹ := - respect_inv φ g - - definition to_is_embedding_homomorphism /- φ -/ (H : Π{g}, φ g = 1 → g = 1) : is_embedding φ := - is_embedding_homomorphism φ @H - - definition is_set_homomorphism [instance] (G₁ G₂ : Group) : is_set (G₁ →g G₂) := - begin - have H : G₁ →g G₂ ≃ Σ(f : G₁ → G₂), Π(g₁ g₂ : G₁), f (g₁ * g₂) = f g₁ * f g₂, - begin - fapply equiv.MK, - { intro φ, induction φ, constructor, assumption}, - { intro v, induction v, constructor, assumption}, - { intro v, induction v, reflexivity}, - { intro φ, induction φ, reflexivity} - end, - apply is_trunc_equiv_closed_rev, exact H - end - - local attribute group_pType_of_Group pointed.mk' [reducible] - definition pmap_of_homomorphism [constructor] /- φ -/ : pType_of_Group G₁ →* pType_of_Group G₂ := - pmap.mk φ (respect_one φ) - - definition homomorphism_eq (p : group_fun φ₁ ~ group_fun φ₂) : φ₁ = φ₂ := - begin - induction φ₁ with φ₁ q₁, induction φ₂ with φ₂ q₂, esimp at p, induction p, - exact ap (homomorphism.mk φ₁) !is_prop.elim - end - - /- categorical structure of groups + homomorphisms -/ - - definition homomorphism_compose [constructor] (ψ : G₂ →g G₃) (φ : G₁ →g G₂) : G₁ →g G₃ := - homomorphism.mk (ψ ∘ φ) (is_homomorphism_compose _ _) - - definition homomorphism_id [constructor] (G : Group) : G →g G := - homomorphism.mk (@id G) (is_homomorphism_id G) - - infixr ` ∘g `:75 := homomorphism_compose - notation 1 := homomorphism_id _ - - structure isomorphism (A B : Group) := - (to_hom : A →g B) - (is_equiv_to_hom : is_equiv to_hom) - - infix ` ≃g `:25 := isomorphism - attribute isomorphism.to_hom [coercion] - attribute isomorphism.is_equiv_to_hom [instance] - - definition equiv_of_isomorphism [constructor] (φ : G₁ ≃g G₂) : G₁ ≃ G₂ := - equiv.mk φ _ - - definition to_ginv [constructor] (φ : G₁ ≃g G₂) : G₂ →g G₁ := - homomorphism.mk φ⁻¹ - abstract begin - intro g₁ g₂, apply eq_of_fn_eq_fn' φ, - rewrite [respect_mul φ, +right_inv φ] - end end - - definition isomorphism.refl [refl] [constructor] (G : Group) : G ≃g G := - isomorphism.mk 1 !is_equiv_id - - definition isomorphism.symm [symm] [constructor] (φ : G₁ ≃g G₂) : G₂ ≃g G₁ := - isomorphism.mk (to_ginv φ) !is_equiv_inv - - definition isomorphism.trans [trans] [constructor] (φ : G₁ ≃g G₂) (ψ : G₂ ≃g G₃) - : G₁ ≃g G₃ := - isomorphism.mk (ψ ∘g φ) !is_equiv_compose - - postfix `⁻¹ᵍ`:(max + 1) := isomorphism.symm - infixl ` ⬝g `:75 := isomorphism.trans - - -- TODO - -- definition Group_univalence (G₁ G₂ : Group) : (G₁ ≃g G₂) ≃ (G₁ = G₂) := - -- begin - -- fapply equiv.MK, - -- { intro φ, fapply Group_eq, apply equiv_of_isomorphism φ, apply respect_mul}, - -- { intro p, apply transport _ p, reflexivity}, - -- { intro p, induction p, esimp, }, - -- { } - -- end - - /- category of groups -/ - - definition precategory_group [constructor] : precategory Group := - precategory.mk homomorphism - @homomorphism_compose - @homomorphism_id - (λG₁ G₂ G₃ G₄ φ₃ φ₂ φ₁, homomorphism_eq (λg, idp)) - (λG₁ G₂ φ, homomorphism_eq (λg, idp)) - (λG₁ G₂ φ, homomorphism_eq (λg, idp)) - - -- TODO - -- definition category_group : category Group := - -- category.mk precategory_group - -- begin - -- intro G₁ G₂, - -- fapply adjointify, - -- { intro φ, fapply Group_eq, }, - -- { }, - -- { } - -- end - -end group diff --git a/homotopy/LES_applications.hlean b/homotopy/LES_applications.hlean deleted file mode 100644 index fa19ba7..0000000 --- a/homotopy/LES_applications.hlean +++ /dev/null @@ -1,365 +0,0 @@ -/- -Copyright (c) 2016 Floris van Doorn. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Floris van Doorn --/ - -import .LES_of_homotopy_groups homotopy.connectedness homotopy.homotopy_group homotopy.join - homotopy.complex_hopf types.lift -open eq is_trunc pointed is_conn is_equiv fiber equiv trunc nat chain_complex fin algebra - group trunc_index function join pushout prod sigma sigma.ops - -namespace nat - open sigma sum - definition eq_even_or_eq_odd (n : ℕ) : (Σk, 2 * k = n) ⊎ (Σk, 2 * k + 1 = n) := - begin - induction n with n IH, - { exact inl ⟨0, idp⟩}, - { induction IH with H H: induction H with k p: induction p, - { exact inr ⟨k, idp⟩}, - { refine inl ⟨k+1, idp⟩}} - end - - definition rec_on_even_odd {P : ℕ → Type} (n : ℕ) (H : Πk, P (2 * k)) (H2 : Πk, P (2 * k + 1)) - : P n := - begin - cases eq_even_or_eq_odd n with v v: induction v with k p: induction p, - { exact H k}, - { exact H2 k} - end - -end nat -open nat - -namespace pointed - - definition apn_phomotopy {A B : Type*} {f g : A →* B} (n : ℕ) (p : f ~* g) - : apn n f ~* apn n g := - begin - induction n with n IH, - { exact p}, - { exact ap1_phomotopy IH} - end - -end pointed open pointed - -namespace chain_complex - section - universe variable u - parameters {F X Y : pType.{u}} (f : X →* Y) (g : F →* X) (e : pfiber f ≃* F) - (p : ppoint f ~* g ∘* e) - include f p - open succ_str - definition fibration_sequence_car [reducible] : +3ℕ → Type* - | (n, fin.mk 0 H) := Ω[n] Y - | (n, fin.mk 1 H) := Ω[n] X - | (n, fin.mk k H) := Ω[n] F - - definition fibration_sequence_fun - : Π(n : +3ℕ), fibration_sequence_car (S n) →* fibration_sequence_car n - | (n, fin.mk 0 H) := proof Ω→[n] f qed - | (n, fin.mk 1 H) := proof Ω→[n] g qed - | (n, fin.mk 2 H) := proof Ω→[n] (e ∘* boundary_map f) ∘* pcast (loop_space_succ_eq_in Y n) qed - | (n, fin.mk (k+3) H) := begin exfalso, apply lt_le_antisymm H, apply le_add_left end - - definition fibration_sequence_pequiv : Π(x : +3ℕ), - loop_spaces2 f x ≃* fibration_sequence_car x - | (n, fin.mk 0 H) := by reflexivity - | (n, fin.mk 1 H) := by reflexivity - | (n, fin.mk 2 H) := loopn_pequiv_loopn n e - | (n, fin.mk (k+3) H) := begin exfalso, apply lt_le_antisymm H, apply le_add_left end - - definition fibration_sequence_fun_phomotopy : Π(x : +3ℕ), - fibration_sequence_pequiv x ∘* loop_spaces_fun2 f x ~* - (fibration_sequence_fun x ∘* fibration_sequence_pequiv (S x)) - | (n, fin.mk 0 H) := by reflexivity - | (n, fin.mk 1 H) := - begin refine !pid_comp ⬝* _, refine apn_phomotopy n p ⬝* _, - refine !apn_compose ⬝* _, reflexivity end - | (n, fin.mk 2 H) := begin refine !passoc⁻¹* ⬝* _ ⬝* !comp_pid⁻¹*, apply pwhisker_right, - refine _ ⬝* !apn_compose⁻¹*, reflexivity end - | (n, fin.mk (k+3) H) := begin exfalso, apply lt_le_antisymm H, apply le_add_left end - - definition type_fibration_sequence [constructor] : type_chain_complex +3ℕ := - transfer_type_chain_complex - (LES_of_loop_spaces2 f) - fibration_sequence_fun - fibration_sequence_pequiv - fibration_sequence_fun_phomotopy - - definition is_exact_type_fibration_sequence : is_exact_t type_fibration_sequence := - begin - intro n, - apply is_exact_at_t_transfer, - apply is_exact_LES_of_loop_spaces2 - end - - definition fibration_sequence [constructor] : chain_complex +3ℕ := - trunc_chain_complex type_fibration_sequence - - end -end chain_complex - -namespace lift - - definition pup [constructor] {A : Type*} : A →* plift A := - pmap.mk up idp - - definition pdown [constructor] {A : Type*} : plift A →* A := - pmap.mk down idp - - definition plift_functor_phomotopy [constructor] {A B : Type*} (f : A →* B) - : pdown ∘* plift_functor f ∘* pup ~* f := - begin - fapply phomotopy.mk, - { reflexivity}, - { esimp, refine !idp_con ⬝ _, refine _ ⬝ ap02 down !idp_con⁻¹, - refine _ ⬝ !ap_compose, exact !ap_id⁻¹} - end - - definition equiv_lift [constructor] (A : Type) : A ≃ lift A := - equiv.MK up down up_down down_up - - definition pequiv_plift [constructor] (A : Type*) : A ≃* plift A := - pequiv_of_equiv (equiv_lift A) idp - -end lift open lift - -namespace is_conn - - local attribute comm_group.to_group [coercion] - local attribute is_equiv_tinverse [instance] - - -- TODO: generalize this to arbitrary maps using lifts, - -- using that up : A → lift A and down : lift A → A are equivalences - theorem is_equiv_π_of_is_connected'.{u} {A B : pType.{u}} {n k : ℕ} (f : A →* B) - (H2 : k ≤ n) [H : is_conn_fun n f] : is_equiv (π→[k] f) := - begin - cases k with k, - { /- k = 0 -/ - change (is_equiv (trunc_functor 0 f)), apply is_equiv_trunc_functor_of_is_conn_fun, - refine is_conn_fun_of_le f (zero_le_of_nat n)}, - { /- k > 0 -/ - have H2' : k ≤ n, from le.trans !self_le_succ H2, - exact - @is_equiv_of_trivial _ - (LES_of_homotopy_groups f) _ - (is_exact_LES_of_homotopy_groups f (k, 2)) - (is_exact_LES_of_homotopy_groups f (succ k, 0)) - (@is_contr_HG_fiber_of_is_connected A B k n f H H2') - (@is_contr_HG_fiber_of_is_connected A B (succ k) n f H H2) - (@pgroup_of_group _ (group_LES_of_homotopy_groups f k 0) idp) - (@pgroup_of_group _ (group_LES_of_homotopy_groups f k 1) idp) - (homomorphism.struct (homomorphism_LES_of_homotopy_groups_fun f (k, 0)))}, - end - - -- MOVE - -- Remark: ⁻¹ʰ conflicts with the inverse of a homomorphism - infix ` ⬝h `:75 := homotopy.trans - postfix `⁻¹ʰ`:(max+1) := homotopy.symm - - -- MOVE - definition trunc_functor_homotopy [unfold 7] {X Y : Type} (n : ℕ₋₂) {f g : X → Y} - (p : f ~ g) (x : trunc n X) : trunc_functor n f x = trunc_functor n g x := - begin - induction x with x, esimp, exact ap tr (p x) - end - - -- MOVE - definition ptrunc_functor_phomotopy [constructor] {X Y : Type*} (n : ℕ₋₂) {f g : X →* Y} - (p : f ~* g) : ptrunc_functor n f ~* ptrunc_functor n g := - begin - fapply phomotopy.mk, - { exact trunc_functor_homotopy n p}, - { esimp, refine !ap_con⁻¹ ⬝ _, exact ap02 tr !to_homotopy_pt}, - end - - -- MOVE - definition phomotopy_group_functor_phomotopy [constructor] (n : ℕ) {A B : Type*} {f g : A →* B} - (p : f ~* g) : π→*[n] f ~* π→*[n] g := - ptrunc_functor_phomotopy 0 (apn_phomotopy n p) - - -- MOVE - definition phomotopy_group_functor_compose [constructor] (n : ℕ) {A B C : Type*} (g : B →* C) - (f : A →* B) : π→*[n] (g ∘* f) ~* π→*[n] g ∘* π→*[n] f := - ptrunc_functor_phomotopy 0 !apn_compose ⬝* !ptrunc_functor_pcompose - - -- MOVE - definition is_equiv_homotopy_group_functor [constructor] (n : ℕ) {A B : Type*} (f : A →* B) - [is_equiv f] : is_equiv (π→[n] f) := - @(is_equiv_trunc_functor 0 _) !is_equiv_apn - - -- MOVE this to init.equiv, and incorporate it in `is_equiv_ap` - theorem eq_of_fn_eq_fn'_ap {A B : Type} (f : A → B) [is_equiv f] {x y : A} (q : x = y) - : eq_of_fn_eq_fn' f (ap f q) = q := - by induction q; apply con.left_inv - - -- MOVE - definition fiber_lift_functor {A B : Type} (f : A → B) (b : B) : - fiber (lift_functor f) (up b) ≃ fiber f b := - begin - fapply equiv.MK: intro v; cases v with a p, - { cases a with a, exact fiber.mk a (eq_of_fn_eq_fn' up p)}, - { exact fiber.mk (up a) (ap up p)}, - { esimp, apply ap (fiber.mk a), apply eq_of_fn_eq_fn'_ap}, - { cases a with a, esimp, apply ap (fiber.mk (up a)), apply ap_eq_of_fn_eq_fn'} - end - - -- MOVE - definition is_conn_fun_lift_functor (n : ℕ₋₂) {A B : Type} (f : A → B) [is_conn_fun n f] : - is_conn_fun n (lift_functor f) := - begin - intro b, cases b with b, apply is_trunc_equiv_closed_rev, - { apply trunc_equiv_trunc, apply fiber_lift_functor} - end - - theorem is_equiv_π_of_is_connected.{u v} {A : pType.{u}} {B : pType.{v}} {n k : ℕ} (f : A →* B) - (H2 : k ≤ n) [H : is_conn_fun n f] : is_equiv (π→[k] f) := - begin - have π→*[k] pdown.{v u} ∘* π→*[k] (plift_functor f) ∘* π→*[k] pup.{u v} ~* π→*[k] f, - begin - refine pwhisker_left _ !phomotopy_group_functor_compose⁻¹* ⬝* _, - refine !phomotopy_group_functor_compose⁻¹* ⬝* _, - apply phomotopy_group_functor_phomotopy, apply plift_functor_phomotopy - end, - have π→[k] pdown.{v u} ∘ π→[k] (plift_functor f) ∘ π→[k] pup.{u v} ~ π→[k] f, from this, - apply is_equiv.homotopy_closed, rotate 1, - { exact this}, - { do 2 apply is_equiv_compose, - { apply is_equiv_homotopy_group_functor, apply to_is_equiv !equiv_lift}, - { refine @(is_equiv_π_of_is_connected' _ H2) _, apply is_conn_fun_lift_functor}, - { apply is_equiv_homotopy_group_functor, apply to_is_equiv !equiv_lift⁻¹ᵉ}} - end - - theorem is_surjective_π_of_is_connected.{u} {A B : pType.{u}} (n : ℕ) (f : A →* B) - [H : is_conn_fun n f] : is_surjective (π→[n + 1] f) := - @is_surjective_of_trivial _ - (LES_of_homotopy_groups f) _ - (is_exact_LES_of_homotopy_groups f (n, 2)) - (@is_contr_HG_fiber_of_is_connected A B n n f H !le.refl) - - -- TODO: move and rename? - definition natural_square2 {A B X : Type} {f : A → X} {g : B → X} (h : Πa b, f a = g b) - {a a' : A} {b b' : B} (p : a = a') (q : b = b') - : square (ap f p) (ap g q) (h a b) (h a' b') := - by induction p; induction q; exact hrfl - -end is_conn - -namespace sigma - definition ppr1 [constructor] {A : Type*} {B : A → Type*} : (Σ*(x : A), B x) →* A := - pmap.mk pr1 idp - - definition ppr2 [unfold_full] {A : Type*} (B : A → Type*) (v : (Σ*(x : A), B x)) : B (ppr1 v) := - pr2 v -end sigma - -namespace hopf - - open sphere.ops susp circle sphere_index - - attribute hopf [unfold 4] - - -- maybe define this as a composition of pointed maps? - definition complex_phopf [constructor] : S. 3 →* S. 2 := - proof pmap.mk complex_hopf idp qed - - definition fiber_pr1_fun {A : Type} {B : A → Type} {a : A} (b : B a) - : fiber_pr1 B a (fiber.mk ⟨a, b⟩ idp) = b := - idp - - --TODO: in fiber.equiv_precompose, make f explicit - open sphere sphere.ops - - definition add_plus_one_of_nat (n m : ℕ) : (n +1+ m) = sphere_index.of_nat (n + m + 1) := - begin - induction m with m IH, - { reflexivity }, - { exact ap succ IH} - end - - -- definition pjoin_pspheres (n m : ℕ) : join (S. n) (S. m) ≃ (S. (n + m + 1)) := - -- join.spheres n m ⬝e begin esimp, apply equiv_of_eq, apply ap S, apply add_plus_one_of_nat end - - definition part_of_complex_hopf : S (of_nat 3) → sigma (hopf S¹) := - begin - intro x, apply inv (hopf.total S¹), apply inv (join.spheres 1 1), exact x - end - - definition part_of_complex_hopf_base2 - : (part_of_complex_hopf (@sphere.base 3)).2 = circle.base := - begin - exact sorry - end - - definition pfiber_complex_phopf : pfiber complex_phopf ≃* S. 1 := - begin - fapply pequiv_of_equiv, - { esimp, unfold [complex_hopf], - refine @fiber.equiv_precompose _ _ (sigma.pr1 ∘ (hopf.total S¹)⁻¹ᵉ) _ _ - (join.spheres 1 1)⁻¹ᵉ _ ⬝e _, - refine fiber.equiv_precompose (hopf.total S¹)⁻¹ᵉ ⬝e _, - apply fiber_pr1}, - { esimp, refine _ ⬝ part_of_complex_hopf_base2, apply fiber_pr1_fun} - end - - open int - - definition one_le_succ (n : ℕ) : 1 ≤ succ n := - nat.succ_le_succ !zero_le - - definition π2S2 : πg[1+1] (S. 2) = gℤ := - begin - refine _ ⬝ fundamental_group_of_circle, - refine _ ⬝ ap (λx, π₁ x) (eq_of_pequiv pfiber_complex_phopf), - fapply Group_eq, - { fapply equiv.mk, - { exact cc_to_fn (LES_of_homotopy_groups complex_phopf) (1, 2)}, - { refine @is_equiv_of_trivial _ - _ _ - (is_exact_LES_of_homotopy_groups _ (1, 1)) - (is_exact_LES_of_homotopy_groups _ (1, 2)) - _ - _ - (@pgroup_of_group _ (group_LES_of_homotopy_groups complex_phopf _ _) idp) - (@pgroup_of_group _ (group_LES_of_homotopy_groups complex_phopf _ _) idp) - _, - { rewrite [LES_of_homotopy_groups_1, ▸*], - have H : 1 ≤[ℕ] 2, from !one_le_succ, - apply trivial_homotopy_group_of_is_conn, exact H, rexact is_conn_psphere 3}, - { refine tr_rev (λx, is_contr (ptrunctype._trans_of_to_pType x)) - (LES_of_homotopy_groups_1 complex_phopf 2) _, - apply trivial_homotopy_group_of_is_conn, apply le.refl, rexact is_conn_psphere 3}, - { exact homomorphism.struct (homomorphism_LES_of_homotopy_groups_fun _ (0, 2))}}}, - { exact homomorphism.struct (homomorphism_LES_of_homotopy_groups_fun _ (0, 2))} - end - - open circle - definition πnS3_eq_πnS2 (n : ℕ) : πg[n+2 +1] (S. 3) = πg[n+2 +1] (S. 2) := - begin - fapply Group_eq, - { fapply equiv.mk, - { exact cc_to_fn (LES_of_homotopy_groups complex_phopf) (n+3, 0)}, - { have H : is_trunc 1 (pfiber complex_phopf), - from @(is_trunc_equiv_closed_rev _ pfiber_complex_phopf) is_trunc_circle, - refine @is_equiv_of_trivial _ - _ _ - (is_exact_LES_of_homotopy_groups _ (n+2, 2)) - (is_exact_LES_of_homotopy_groups _ (n+3, 0)) - _ - _ - (@pgroup_of_group _ (group_LES_of_homotopy_groups complex_phopf _ _) idp) - (@pgroup_of_group _ (group_LES_of_homotopy_groups complex_phopf _ _) idp) - _, - { rewrite [▸*, LES_of_homotopy_groups_2 _ (n +[ℕ] 2)], - have H : 1 ≤[ℕ] n + 1, from !one_le_succ, - apply trivial_homotopy_group_of_is_trunc _ _ _ H}, - { refine tr_rev (λx, is_contr (ptrunctype._trans_of_to_pType x)) - (LES_of_homotopy_groups_2 complex_phopf _) _, - have H : 1 ≤[ℕ] n + 2, from !one_le_succ, - apply trivial_homotopy_group_of_is_trunc _ _ _ H}, - { exact homomorphism.struct (homomorphism_LES_of_homotopy_groups_fun _ (n+2, 0))}}}, - { exact homomorphism.struct (homomorphism_LES_of_homotopy_groups_fun _ (n+2, 0))} - end - -end hopf diff --git a/homotopy/LES_of_homotopy_groups.hlean b/homotopy/LES_of_homotopy_groups.hlean deleted file mode 100644 index 10eb19a..0000000 --- a/homotopy/LES_of_homotopy_groups.hlean +++ /dev/null @@ -1,807 +0,0 @@ -/- -Copyright (c) 2016 Floris van Doorn. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Floris van Doorn - -We define the fiber sequence of a pointed map f : X →* Y. We mostly follow the proof in section 8.4 -of the book. - -PART 1: -We define a sequence fiber_sequence as in Definition 8.4.3. -It has types X(n) : Type* -X(0) := Y, -X(1) := X, -X(n+1) := fiber (f(n)) -with functions f(n) : X(n+1) →* X(n) -f(0) := f -f(n+1) := point (f(n)) [this is the first projection] -We prove that this is an exact sequence. -Then we prove Lemma 8.4.3, by showing that X(n+3) ≃* Ω(X(n)) and that this equivalence sends -the pointed map f(n+3) to -Ω(f(n)), i.e. the composition of Ω(f(n)) with path inversion. -Using this equivalence we get a boundary_map : Ω(Y) → pfiber f. - -PART 2: -Now we can define a new fiber sequence X'(n) : Type*, and here we slightly diverge from the book. -We define it as -X'(0) := Y, -X'(1) := X, -X'(2) := fiber f -X'(n+3) := Ω(X'(n)) -with maps f'(n) : X'(n+1) →* X'(n) -f'(0) := f -f'(1) := point f -f'(2) := boundary_map -f'(n+3) := Ω(f'(n)) - -This sequence is not equivalent to the previous sequence. The difference is in the signs. -The sequence f has negative signs (i.e. is composed with the inverse maps) for n ≡ 3, 4, 5 mod 6. -This sign information is captured by e : X'(n) ≃* X'(n) such that -e(k) := 1 for k = 0,1,2,3 -e(k+3) := Ω(e(k)) ∘ (-)⁻¹ for k > 0 - -Now the sequence (X', f' ∘ e) is equivalent to (X, f), Hence (X', f' ∘ e) is an exact sequence. -We then prove that (X', f') is an exact sequence by using that there are other equivalences -eₗ and eᵣ such that -f' = eᵣ ∘ f' ∘ e -f' ∘ eₗ = e ∘ f'. -(this fact is type_chain_complex_cancel_aut and is_exact_at_t_cancel_aut in the file chain_complex) -eₗ and eᵣ are almost the same as e, except that the places where the inverse is taken is -slightly shifted: -eᵣ = (-)⁻¹ for n ≡ 3, 4, 5 mod 6 and eᵣ = 1 otherwise -e = (-)⁻¹ for n ≡ 4, 5, 6 mod 6 (except for n = 0) and e = 1 otherwise -eₗ = (-)⁻¹ for n ≡ 5, 6, 7 mod 6 (except for n = 0, 1) and eₗ = 1 otherwise - -PART 3: -We change the type over which the sequence of types and maps are indexed from ℕ to ℕ × 3 -(where 3 is the finite type with 3 elements). The reason is that we have that X'(3n) = Ωⁿ(Y), but -this equality is not definitionally true. Hence we cannot even state whether f'(3n) = Ωⁿ(f) without -using transports. This gets ugly. However, if we use as index type ℕ × 3, we can do this. We can -define -Y : ℕ × 3 → Type* as -Y(n, 0) := Ωⁿ(Y) -Y(n, 1) := Ωⁿ(X) -Y(n, 2) := Ωⁿ(fiber f) -with maps g(n) : Y(S n) →* Y(n) (where the successor is defined in the obvious way) -g(n, 0) := Ωⁿ(f) -g(n, 1) := Ωⁿ(point f) -g(n, 2) := Ωⁿ(boundary_map) ∘ cast - -Here "cast" is the transport over the equality Ωⁿ⁺¹(Y) = Ωⁿ(Ω(Y)). We show that the sequence -(ℕ, X', f') is equivalent to (ℕ × 3, Y, g). - -PART 4: -We get the long exact sequence of homotopy groups by taking the set-truncation of (Y, g). --/ - -import .chain_complex algebra.homotopy_group - -open eq pointed sigma fiber equiv is_equiv sigma.ops is_trunc nat trunc algebra function sum - -section MOVE - -- TODO: MOVE - open group chain_complex - definition pinverse_pinverse (A : Type*) : pinverse ∘* pinverse ~* pid (Ω A) := - begin - fapply phomotopy.mk, - { apply inv_inv}, - { reflexivity} - end - - definition to_pmap_pequiv_of_pmap {A B : Type*} (f : A →* B) (H : is_equiv f) - : pequiv.to_pmap (pequiv_of_pmap f H) = f := - by cases f; reflexivity - - definition to_pmap_pequiv_trans {A B C : Type*} (f : A ≃* B) (g : B ≃* C) - : pequiv.to_pmap (f ⬝e* g) = g ∘* f := - !to_pmap_pequiv_of_pmap - - definition pequiv_pinverse (A : Type*) : Ω A ≃* Ω A := - pequiv_of_pmap pinverse !is_equiv_eq_inverse - - definition tr_mul_tr {A : Type*} (n : ℕ) (p q : Ω[n + 1] A) : - tr p *[πg[n+1] A] tr q = tr (p ⬝ q) := - by reflexivity - - definition is_homomorphism_cast_loop_space_succ_eq_in {A : Type*} (n : ℕ) : - is_homomorphism - (cast (ap (trunc 0 ∘ pointed.carrier) (loop_space_succ_eq_in A (succ n))) - : πg[n+1+1] A → πg[n+1] Ω A) := - begin - intro g h, induction g with g, induction h with h, - xrewrite [tr_mul_tr, - + fn_cast_eq_cast_fn _ (λn, tr), tr_mul_tr, ↑cast, -tr_compose, - loop_space_succ_eq_in_concat, - + tr_compose], - end - - definition is_homomorphism_inverse (A : Type*) (n : ℕ) - : is_homomorphism (λp, p⁻¹ : πag[n+2] A → πag[n+2] A) := - begin - intro g h, rewrite mul.comm, - induction g with g, induction h with h, - exact ap tr !con_inv - end - -end MOVE - -/-------------- - PART 1 - --------------/ - -namespace chain_complex - - definition fiber_sequence_helper [constructor] (v : Σ(X Y : Type*), X →* Y) - : Σ(Z X : Type*), Z →* X := - ⟨pfiber v.2.2, v.1, ppoint v.2.2⟩ - - definition fiber_sequence_helpern (v : Σ(X Y : Type*), X →* Y) (n : ℕ) - : Σ(Z X : Type*), Z →* X := - iterate fiber_sequence_helper n v - - section - universe variable u - parameters {X Y : pType.{u}} (f : X →* Y) - include f - - definition fiber_sequence_carrier (n : ℕ) : Type* := - (fiber_sequence_helpern ⟨X, Y, f⟩ n).2.1 - - definition fiber_sequence_fun (n : ℕ) - : fiber_sequence_carrier (n + 1) →* fiber_sequence_carrier n := - (fiber_sequence_helpern ⟨X, Y, f⟩ n).2.2 - - /- Definition 8.4.3 -/ - definition fiber_sequence : type_chain_complex.{0 u} +ℕ := - begin - fconstructor, - { exact fiber_sequence_carrier}, - { exact fiber_sequence_fun}, - { intro n x, cases n with n, - { exact point_eq x}, - { exact point_eq x}} - end - - definition is_exact_fiber_sequence : is_exact_t fiber_sequence := - λn x p, fiber.mk (fiber.mk x p) rfl - - /- (generalization of) Lemma 8.4.4(i)(ii) -/ - definition fiber_sequence_carrier_equiv (n : ℕ) - : fiber_sequence_carrier (n+3) ≃ Ω(fiber_sequence_carrier n) := - calc - fiber_sequence_carrier (n+3) ≃ fiber (fiber_sequence_fun (n+1)) pt : erfl - ... ≃ Σ(x : fiber_sequence_carrier _), fiber_sequence_fun (n+1) x = pt - : fiber.sigma_char - ... ≃ Σ(x : fiber (fiber_sequence_fun n) pt), fiber_sequence_fun _ x = pt - : erfl - ... ≃ Σ(v : Σ(x : fiber_sequence_carrier _), fiber_sequence_fun _ x = pt), - fiber_sequence_fun _ (fiber.mk v.1 v.2) = pt - : by exact sigma_equiv_sigma !fiber.sigma_char (λa, erfl) - ... ≃ Σ(v : Σ(x : fiber_sequence_carrier _), fiber_sequence_fun _ x = pt), - v.1 = pt - : erfl - ... ≃ Σ(v : Σ(x : fiber_sequence_carrier _), x = pt), - fiber_sequence_fun _ v.1 = pt - : sigma_assoc_comm_equiv - ... ≃ fiber_sequence_fun _ !center.1 = pt - : @(sigma_equiv_of_is_contr_left _) !is_contr_sigma_eq' - ... ≃ fiber_sequence_fun _ pt = pt - : erfl - ... ≃ pt = pt - : by exact !equiv_eq_closed_left !respect_pt - ... ≃ Ω(fiber_sequence_carrier n) : erfl - - /- computation rule -/ - definition fiber_sequence_carrier_equiv_eq (n : ℕ) - (x : fiber_sequence_carrier (n+1)) (p : fiber_sequence_fun n x = pt) - (q : fiber_sequence_fun (n+1) (fiber.mk x p) = pt) - : fiber_sequence_carrier_equiv n (fiber.mk (fiber.mk x p) q) - = !respect_pt⁻¹ ⬝ ap (fiber_sequence_fun n) q⁻¹ ⬝ p := - begin - refine _ ⬝ !con.assoc⁻¹, - apply whisker_left, - refine transport_eq_Fl _ _ ⬝ _, - apply whisker_right, - refine inverse2 !ap_inv ⬝ !inv_inv ⬝ _, - refine ap_compose (fiber_sequence_fun n) pr₁ _ ⬝ - ap02 (fiber_sequence_fun n) !ap_pr1_center_eq_sigma_eq', - end - - definition fiber_sequence_carrier_equiv_inv_eq (n : ℕ) - (p : Ω(fiber_sequence_carrier n)) : (fiber_sequence_carrier_equiv n)⁻¹ᵉ p = - fiber.mk (fiber.mk pt (respect_pt (fiber_sequence_fun n) ⬝ p)) idp := - begin - apply inv_eq_of_eq, - refine _ ⬝ !fiber_sequence_carrier_equiv_eq⁻¹, esimp, - exact !inv_con_cancel_left⁻¹ - end - - definition fiber_sequence_carrier_pequiv (n : ℕ) - : fiber_sequence_carrier (n+3) ≃* Ω(fiber_sequence_carrier n) := - pequiv_of_equiv (fiber_sequence_carrier_equiv n) - begin - esimp, - apply con.left_inv - end - - definition fiber_sequence_carrier_pequiv_eq (n : ℕ) - (x : fiber_sequence_carrier (n+1)) (p : fiber_sequence_fun n x = pt) - (q : fiber_sequence_fun (n+1) (fiber.mk x p) = pt) - : fiber_sequence_carrier_pequiv n (fiber.mk (fiber.mk x p) q) - = !respect_pt⁻¹ ⬝ ap (fiber_sequence_fun n) q⁻¹ ⬝ p := - fiber_sequence_carrier_equiv_eq n x p q - - definition fiber_sequence_carrier_pequiv_inv_eq (n : ℕ) - (p : Ω(fiber_sequence_carrier n)) : (fiber_sequence_carrier_pequiv n)⁻¹ᵉ* p = - fiber.mk (fiber.mk pt (respect_pt (fiber_sequence_fun n) ⬝ p)) idp := - by rexact fiber_sequence_carrier_equiv_inv_eq n p - - /- Lemma 8.4.4(iii) -/ - definition fiber_sequence_fun_eq_helper (n : ℕ) - (p : Ω(fiber_sequence_carrier (n + 1))) : - fiber_sequence_carrier_pequiv n - (fiber_sequence_fun (n + 3) - ((fiber_sequence_carrier_pequiv (n + 1))⁻¹ᵉ* p)) = - ap1 (fiber_sequence_fun n) p⁻¹ := - begin - refine ap (λx, fiber_sequence_carrier_pequiv n (fiber_sequence_fun (n + 3) x)) - (fiber_sequence_carrier_pequiv_inv_eq (n+1) p) ⬝ _, - /- the following three lines are rewriting some reflexivities: -/ - -- replace (n + 3) with (n + 2 + 1), - -- refine ap (fiber_sequence_carrier_pequiv n) - -- (fiber_sequence_fun_eq1 (n+2) _ idp) ⬝ _, - refine fiber_sequence_carrier_pequiv_eq n pt (respect_pt (fiber_sequence_fun n)) _ ⬝ _, - esimp, - apply whisker_right, - apply whisker_left, - apply ap02, apply inverse2, apply idp_con, - end - - theorem fiber_sequence_carrier_pequiv_eq_point_eq_idp (n : ℕ) : - fiber_sequence_carrier_pequiv_eq n - (Point (fiber_sequence_carrier (n+1))) - (respect_pt (fiber_sequence_fun n)) - (respect_pt (fiber_sequence_fun (n + 1))) = idp := - begin - apply con_inv_eq_idp, - refine ap (λx, whisker_left _ (_ ⬝ x)) _ ⬝ _, - { reflexivity}, - { reflexivity}, - refine ap (whisker_left _) - (transport_eq_Fl_idp_left (fiber_sequence_fun n) - (respect_pt (fiber_sequence_fun n))) ⬝ _, - apply whisker_left_idp_con_eq_assoc - end - - theorem fiber_sequence_fun_phomotopy_helper (n : ℕ) : - (fiber_sequence_carrier_pequiv n ∘* - fiber_sequence_fun (n + 3)) ∘* - (fiber_sequence_carrier_pequiv (n + 1))⁻¹ᵉ* ~* - ap1 (fiber_sequence_fun n) ∘* pinverse := - begin - fapply phomotopy.mk, - { exact chain_complex.fiber_sequence_fun_eq_helper f n}, - { esimp, rewrite [idp_con], refine _ ⬝ whisker_left _ !idp_con⁻¹, - apply whisker_right, - apply whisker_left, - exact chain_complex.fiber_sequence_carrier_pequiv_eq_point_eq_idp f n} - end - - theorem fiber_sequence_fun_eq (n : ℕ) : Π(x : fiber_sequence_carrier (n + 4)), - fiber_sequence_carrier_pequiv n (fiber_sequence_fun (n + 3) x) = - ap1 (fiber_sequence_fun n) (fiber_sequence_carrier_pequiv (n + 1) x)⁻¹ := - begin - apply homotopy_of_inv_homotopy_pre (fiber_sequence_carrier_pequiv (n + 1)), - apply fiber_sequence_fun_eq_helper n - end - - theorem fiber_sequence_fun_phomotopy (n : ℕ) : - fiber_sequence_carrier_pequiv n ∘* - fiber_sequence_fun (n + 3) ~* - (ap1 (fiber_sequence_fun n) ∘* pinverse) ∘* fiber_sequence_carrier_pequiv (n + 1) := - begin - apply phomotopy_of_pinv_right_phomotopy, - apply fiber_sequence_fun_phomotopy_helper - end - - definition boundary_map : Ω Y →* pfiber f := - fiber_sequence_fun 2 ∘* (fiber_sequence_carrier_pequiv 0)⁻¹ᵉ* - -/-------------- - PART 2 - --------------/ - - /- Now we are ready to define the long exact sequence of homotopy groups. - First we define its carrier -/ - definition loop_spaces : ℕ → Type* - | 0 := Y - | 1 := X - | 2 := pfiber f - | (k+3) := Ω (loop_spaces k) - - /- The maps between the homotopy groups -/ - definition loop_spaces_fun - : Π(n : ℕ), loop_spaces (n+1) →* loop_spaces n - | 0 := proof f qed - | 1 := proof ppoint f qed - | 2 := proof boundary_map qed - | (k+3) := proof ap1 (loop_spaces_fun k) qed - - definition loop_spaces_fun_add3 [unfold_full] (n : ℕ) : - loop_spaces_fun (n + 3) = ap1 (loop_spaces_fun n) := - proof idp qed - - definition fiber_sequence_pequiv_loop_spaces : - Πn, fiber_sequence_carrier n ≃* loop_spaces n - | 0 := by reflexivity - | 1 := by reflexivity - | 2 := by reflexivity - | (k+3) := - begin - refine fiber_sequence_carrier_pequiv k ⬝e* _, - apply loop_pequiv_loop, - exact fiber_sequence_pequiv_loop_spaces k - end - - definition fiber_sequence_pequiv_loop_spaces_add3 (n : ℕ) - : fiber_sequence_pequiv_loop_spaces (n + 3) = - ap1 (fiber_sequence_pequiv_loop_spaces n) ∘* fiber_sequence_carrier_pequiv n := - by reflexivity - - definition fiber_sequence_pequiv_loop_spaces_3_phomotopy - : fiber_sequence_pequiv_loop_spaces 3 ~* proof fiber_sequence_carrier_pequiv nat.zero qed := - begin - refine pwhisker_right _ ap1_id ⬝* _, - apply pid_comp - end - - definition pid_or_pinverse : Π(n : ℕ), loop_spaces n ≃* loop_spaces n - | 0 := pequiv.rfl - | 1 := pequiv.rfl - | 2 := pequiv.rfl - | 3 := pequiv.rfl - | (k+4) := !pequiv_pinverse ⬝e* loop_pequiv_loop (pid_or_pinverse (k+1)) - - definition pid_or_pinverse_add4 (n : ℕ) - : pid_or_pinverse (n + 4) = !pequiv_pinverse ⬝e* loop_pequiv_loop (pid_or_pinverse (n + 1)) := - by reflexivity - - definition pid_or_pinverse_add4_rev : Π(n : ℕ), - pid_or_pinverse (n + 4) ~* pinverse ∘* Ω→(pid_or_pinverse (n + 1)) - | 0 := begin rewrite [pid_or_pinverse_add4, + to_pmap_pequiv_trans], - replace pid_or_pinverse (0 + 1) with pequiv.refl X, - rewrite [loop_pequiv_loop_rfl, ▸*], refine !pid_comp ⬝* _, - exact !comp_pid⁻¹* ⬝* pwhisker_left _ !ap1_id⁻¹* end - | 1 := begin rewrite [pid_or_pinverse_add4, + to_pmap_pequiv_trans], - replace pid_or_pinverse (1 + 1) with pequiv.refl (pfiber f), - rewrite [loop_pequiv_loop_rfl, ▸*], refine !pid_comp ⬝* _, - exact !comp_pid⁻¹* ⬝* pwhisker_left _ !ap1_id⁻¹* end - | 2 := begin rewrite [pid_or_pinverse_add4, + to_pmap_pequiv_trans], - replace pid_or_pinverse (2 + 1) with pequiv.refl (Ω Y), - rewrite [loop_pequiv_loop_rfl, ▸*], refine !pid_comp ⬝* _, - exact !comp_pid⁻¹* ⬝* pwhisker_left _ !ap1_id⁻¹* end - | (k+3) := - begin - replace (k + 3 + 1) with (k + 4), - rewrite [+ pid_or_pinverse_add4, + to_pmap_pequiv_trans], - refine _ ⬝* pwhisker_left _ !ap1_compose⁻¹*, - refine _ ⬝* !passoc, - apply pconcat2, - { refine ap1_phomotopy (pid_or_pinverse_add4_rev k) ⬝* _, - refine !ap1_compose ⬝* _, apply pwhisker_right, apply ap1_pinverse}, - { refine !ap1_pinverse⁻¹*} - end - - theorem fiber_sequence_phomotopy_loop_spaces : Π(n : ℕ), - fiber_sequence_pequiv_loop_spaces n ∘* fiber_sequence_fun n ~* - (loop_spaces_fun n ∘* pid_or_pinverse (n + 1)) ∘* fiber_sequence_pequiv_loop_spaces (n + 1) - | 0 := proof proof phomotopy.rfl qed ⬝* pwhisker_right _ !comp_pid⁻¹* qed - | 1 := by reflexivity - | 2 := - begin - refine !pid_comp ⬝* _, - replace loop_spaces_fun 2 with boundary_map, - refine _ ⬝* pwhisker_left _ fiber_sequence_pequiv_loop_spaces_3_phomotopy⁻¹*, - apply phomotopy_of_pinv_right_phomotopy, - exact !pid_comp⁻¹* - end - | (k+3) := - begin - replace (k + 3 + 1) with (k + 1 + 3), - rewrite [fiber_sequence_pequiv_loop_spaces_add3 k, - fiber_sequence_pequiv_loop_spaces_add3 (k+1)], - refine !passoc ⬝* _, - refine pwhisker_left _ (fiber_sequence_fun_phomotopy k) ⬝* _, - refine !passoc⁻¹* ⬝* _ ⬝* !passoc, - apply pwhisker_right, - replace (k + 1 + 3) with (k + 4), - xrewrite [loop_spaces_fun_add3, pid_or_pinverse_add4, to_pmap_pequiv_trans], - refine _ ⬝* !passoc⁻¹*, - refine _ ⬝* pwhisker_left _ !passoc⁻¹*, - refine _ ⬝* pwhisker_left _ (pwhisker_left _ !ap1_compose_pinverse), - refine !passoc⁻¹* ⬝* _ ⬝* !passoc ⬝* !passoc, - apply pwhisker_right, - refine !ap1_compose⁻¹* ⬝* _ ⬝* !ap1_compose ⬝* pwhisker_right _ !ap1_compose, - apply ap1_phomotopy, - exact fiber_sequence_phomotopy_loop_spaces k - end - - definition pid_or_pinverse_right : Π(n : ℕ), loop_spaces n →* loop_spaces n - | 0 := !pid - | 1 := !pid - | 2 := !pid - | (k+3) := Ω→(pid_or_pinverse_right k) ∘* pinverse - - definition pid_or_pinverse_left : Π(n : ℕ), loop_spaces n →* loop_spaces n - | 0 := pequiv.rfl - | 1 := pequiv.rfl - | 2 := pequiv.rfl - | 3 := pequiv.rfl - | 4 := pequiv.rfl - | (k+5) := Ω→(pid_or_pinverse_left (k+2)) ∘* pinverse - - definition pid_or_pinverse_right_add3 (n : ℕ) - : pid_or_pinverse_right (n + 3) = Ω→(pid_or_pinverse_right n) ∘* pinverse := - by reflexivity - - definition pid_or_pinverse_left_add5 (n : ℕ) - : pid_or_pinverse_left (n + 5) = Ω→(pid_or_pinverse_left (n+2)) ∘* pinverse := - by reflexivity - - theorem pid_or_pinverse_commute_right : Π(n : ℕ), - loop_spaces_fun n ~* pid_or_pinverse_right n ∘* loop_spaces_fun n ∘* pid_or_pinverse (n + 1) - | 0 := proof !comp_pid⁻¹* ⬝* !pid_comp⁻¹* qed - | 1 := proof !comp_pid⁻¹* ⬝* !pid_comp⁻¹* qed - | 2 := proof !comp_pid⁻¹* ⬝* !pid_comp⁻¹* qed - | (k+3) := - begin - replace (k + 3 + 1) with (k + 4), - rewrite [pid_or_pinverse_right_add3, loop_spaces_fun_add3], - refine _ ⬝* pwhisker_left _ (pwhisker_left _ !pid_or_pinverse_add4_rev⁻¹*), - refine ap1_phomotopy (pid_or_pinverse_commute_right k) ⬝* _, - refine !ap1_compose ⬝* _ ⬝* !passoc⁻¹*, - apply pwhisker_left, - refine !ap1_compose ⬝* _ ⬝* !passoc ⬝* !passoc, - apply pwhisker_right, - refine _ ⬝* pwhisker_right _ !ap1_compose_pinverse, - refine _ ⬝* !passoc⁻¹*, - refine !comp_pid⁻¹* ⬝* pwhisker_left _ _, - symmetry, apply pinverse_pinverse - end - - theorem pid_or_pinverse_commute_left : Π(n : ℕ), - loop_spaces_fun n ∘* pid_or_pinverse_left (n + 1) ~* pid_or_pinverse n ∘* loop_spaces_fun n - | 0 := proof !comp_pid ⬝* !pid_comp⁻¹* qed - | 1 := proof !comp_pid ⬝* !pid_comp⁻¹* qed - | 2 := proof !comp_pid ⬝* !pid_comp⁻¹* qed - | 3 := proof !comp_pid ⬝* !pid_comp⁻¹* qed - | (k+4) := - begin - replace (k + 4 + 1) with (k + 5), - rewrite [pid_or_pinverse_left_add5, pid_or_pinverse_add4, to_pmap_pequiv_trans], - replace (k + 4) with (k + 1 + 3), - rewrite [loop_spaces_fun_add3], - refine !passoc⁻¹* ⬝* _ ⬝* !passoc⁻¹*, - refine _ ⬝* pwhisker_left _ !ap1_compose_pinverse, - refine _ ⬝* !passoc, - apply pwhisker_right, - refine !ap1_compose⁻¹* ⬝* _ ⬝* !ap1_compose, - exact ap1_phomotopy (pid_or_pinverse_commute_left (k+1)) - end - - definition LES_of_loop_spaces' [constructor] : type_chain_complex +ℕ := - transfer_type_chain_complex - fiber_sequence - (λn, loop_spaces_fun n ∘* pid_or_pinverse (n + 1)) - fiber_sequence_pequiv_loop_spaces - fiber_sequence_phomotopy_loop_spaces - - definition LES_of_loop_spaces [constructor] : type_chain_complex +ℕ := - type_chain_complex_cancel_aut - LES_of_loop_spaces' - loop_spaces_fun - pid_or_pinverse - pid_or_pinverse_right - (λn x, idp) - pid_or_pinverse_commute_right - - definition is_exact_LES_of_loop_spaces : is_exact_t LES_of_loop_spaces := - begin - intro n, - refine is_exact_at_t_cancel_aut n pid_or_pinverse_left _ _ pid_or_pinverse_commute_left _, - apply is_exact_at_t_transfer, - apply is_exact_fiber_sequence - end - - open prod succ_str fin - - /-------------- - PART 3 - --------------/ - - definition loop_spaces2 [reducible] : +3ℕ → Type* - | (n, fin.mk 0 H) := Ω[n] Y - | (n, fin.mk 1 H) := Ω[n] X - | (n, fin.mk k H) := Ω[n] (pfiber f) - - definition loop_spaces2_add1 (n : ℕ) : Π(x : fin 3), - loop_spaces2 (n+1, x) = Ω (loop_spaces2 (n, x)) - | (fin.mk 0 H) := by reflexivity - | (fin.mk 1 H) := by reflexivity - | (fin.mk 2 H) := by reflexivity - | (fin.mk (k+3) H) := begin exfalso, apply lt_le_antisymm H, apply le_add_left end - - definition loop_spaces_fun2 : Π(n : +3ℕ), loop_spaces2 (S n) →* loop_spaces2 n - | (n, fin.mk 0 H) := proof Ω→[n] f qed - | (n, fin.mk 1 H) := proof Ω→[n] (ppoint f) qed - | (n, fin.mk 2 H) := proof Ω→[n] boundary_map ∘* pcast (loop_space_succ_eq_in Y n) qed - | (n, fin.mk (k+3) H) := begin exfalso, apply lt_le_antisymm H, apply le_add_left end - - definition loop_spaces_fun2_add1_0 (n : ℕ) (H : 0 < succ 2) - : loop_spaces_fun2 (n+1, fin.mk 0 H) ~* - cast proof idp qed ap1 (loop_spaces_fun2 (n, fin.mk 0 H)) := - by reflexivity - - definition loop_spaces_fun2_add1_1 (n : ℕ) (H : 1 < succ 2) - : loop_spaces_fun2 (n+1, fin.mk 1 H) ~* - cast proof idp qed ap1 (loop_spaces_fun2 (n, fin.mk 1 H)) := - by reflexivity - - definition loop_spaces_fun2_add1_2 (n : ℕ) (H : 2 < succ 2) - : loop_spaces_fun2 (n+1, fin.mk 2 H) ~* - cast proof idp qed ap1 (loop_spaces_fun2 (n, fin.mk 2 H)) := - begin - esimp, - refine _ ⬝* !ap1_compose⁻¹*, - apply pwhisker_left, - apply pcast_ap_loop_space - end - - definition nat_of_str [unfold 2] [reducible] {n : ℕ} : ℕ × fin (succ n) → ℕ := - λx, succ n * pr1 x + val (pr2 x) - - definition str_of_nat {n : ℕ} : ℕ → ℕ × fin (succ n) := - λm, (m / (succ n), mk_mod n m) - - definition nat_of_str_3S [unfold 2] [reducible] - : Π(x : stratified +ℕ 2), nat_of_str x + 1 = nat_of_str (@S (stratified +ℕ 2) x) - | (n, fin.mk 0 H) := by reflexivity - | (n, fin.mk 1 H) := by reflexivity - | (n, fin.mk 2 H) := by reflexivity - | (n, fin.mk (k+3) H) := begin exfalso, apply lt_le_antisymm H, apply le_add_left end - - definition fin_prod_nat_equiv_nat [constructor] (n : ℕ) : ℕ × fin (succ n) ≃ ℕ := - equiv.MK nat_of_str str_of_nat - abstract begin - intro m, unfold [nat_of_str, str_of_nat, mk_mod], - refine _ ⬝ (eq_div_mul_add_mod m (succ n))⁻¹, - rewrite [mul.comm] - end end - abstract begin - intro x, cases x with m k, - cases k with k H, - apply prod_eq: esimp [str_of_nat], - { rewrite [add.comm, add_mul_div_self_left _ _ (!zero_lt_succ), ▸*, - div_eq_zero_of_lt H, zero_add]}, - { apply eq_of_veq, esimp [mk_mod], - rewrite [add.comm, add_mul_mod_self_left, ▸*, mod_eq_of_lt H]} - end end - - /- - note: in the following theorem the (n+1) case is 3 times the same, - so maybe this can be simplified - -/ - definition loop_spaces2_pequiv' : Π(n : ℕ) (x : fin (nat.succ 2)), - loop_spaces (nat_of_str (n, x)) ≃* loop_spaces2 (n, x) - | 0 (fin.mk 0 H) := by reflexivity - | 0 (fin.mk 1 H) := by reflexivity - | 0 (fin.mk 2 H) := by reflexivity - | (n+1) (fin.mk 0 H) := - begin - apply loop_pequiv_loop, - rexact loop_spaces2_pequiv' n (fin.mk 0 H) - end - | (n+1) (fin.mk 1 H) := - begin - apply loop_pequiv_loop, - rexact loop_spaces2_pequiv' n (fin.mk 1 H) - end - | (n+1) (fin.mk 2 H) := - begin - apply loop_pequiv_loop, - rexact loop_spaces2_pequiv' n (fin.mk 2 H) - end - | n (fin.mk (k+3) H) := begin exfalso, apply lt_le_antisymm H, apply le_add_left end - - definition loop_spaces2_pequiv : Π(x : +3ℕ), - loop_spaces (nat_of_str x) ≃* loop_spaces2 x - | (n, x) := loop_spaces2_pequiv' n x - - local attribute loop_pequiv_loop [reducible] - - /- all cases where n>0 are basically the same -/ - definition loop_spaces_fun2_phomotopy (x : +3ℕ) : - loop_spaces2_pequiv x ∘* loop_spaces_fun (nat_of_str x) ~* - (loop_spaces_fun2 x ∘* loop_spaces2_pequiv (S x)) - ∘* pcast (ap (loop_spaces) (nat_of_str_3S x)) := - begin - cases x with n x, cases x with k H, - do 3 (cases k with k; rotate 1), - { /-k≥3-/ exfalso, apply lt_le_antisymm H, apply le_add_left}, - { /-k=0-/ - induction n with n IH, - { refine !pid_comp ⬝* _ ⬝* !comp_pid⁻¹* ⬝* !comp_pid⁻¹*, - reflexivity}, - { refine _ ⬝* !comp_pid⁻¹*, - refine _ ⬝* pwhisker_right _ !loop_spaces_fun2_add1_0⁻¹*, - refine !ap1_compose⁻¹* ⬝* _ ⬝* !ap1_compose, apply ap1_phomotopy, - exact IH ⬝* !comp_pid}}, - { /-k=1-/ - induction n with n IH, - { refine !pid_comp ⬝* _ ⬝* !comp_pid⁻¹* ⬝* !comp_pid⁻¹*, - reflexivity}, - { refine _ ⬝* !comp_pid⁻¹*, - refine _ ⬝* pwhisker_right _ !loop_spaces_fun2_add1_1⁻¹*, - refine !ap1_compose⁻¹* ⬝* _ ⬝* !ap1_compose, apply ap1_phomotopy, - exact IH ⬝* !comp_pid}}, - { /-k=2-/ - induction n with n IH, - { refine !pid_comp ⬝* _ ⬝* !comp_pid⁻¹*, - refine !comp_pid⁻¹* ⬝* pconcat2 _ _, - { exact (comp_pid (chain_complex.boundary_map f))⁻¹*}, - { refine cast (ap (λx, _ ~* x) !loop_pequiv_loop_rfl)⁻¹ _, reflexivity}}, - { refine _ ⬝* !comp_pid⁻¹*, - refine _ ⬝* pwhisker_right _ !loop_spaces_fun2_add1_2⁻¹*, - refine !ap1_compose⁻¹* ⬝* _ ⬝* !ap1_compose, apply ap1_phomotopy, - exact IH ⬝* !comp_pid}}, - end - - definition LES_of_loop_spaces2 [constructor] : type_chain_complex +3ℕ := - transfer_type_chain_complex2 - LES_of_loop_spaces - !fin_prod_nat_equiv_nat - nat_of_str_3S - @loop_spaces_fun2 - @loop_spaces2_pequiv - begin - intro m x, - refine loop_spaces_fun2_phomotopy m x ⬝ _, - apply ap (loop_spaces_fun2 m), apply ap (loop_spaces2_pequiv (S m)), - esimp, exact ap010 cast !ap_compose⁻¹ x - end - - definition is_exact_LES_of_loop_spaces2 : is_exact_t LES_of_loop_spaces2 := - begin - intro n, - apply is_exact_at_t_transfer2, - apply is_exact_LES_of_loop_spaces - end - - definition LES_of_homotopy_groups' [constructor] : chain_complex +3ℕ := - trunc_chain_complex LES_of_loop_spaces2 - -/-------------- - PART 4 - --------------/ - - definition homotopy_groups [reducible] : +3ℕ → Set* - | (n, fin.mk 0 H) := π*[n] Y - | (n, fin.mk 1 H) := π*[n] X - | (n, fin.mk k H) := π*[n] (pfiber f) - - definition homotopy_groups_pequiv_loop_spaces2 [reducible] - : Π(n : +3ℕ), ptrunc 0 (loop_spaces2 n) ≃* homotopy_groups n - | (n, fin.mk 0 H) := by reflexivity - | (n, fin.mk 1 H) := by reflexivity - | (n, fin.mk 2 H) := by reflexivity - | (n, fin.mk (k+3) H) := begin exfalso, apply lt_le_antisymm H, apply le_add_left end - - definition homotopy_groups_fun : Π(n : +3ℕ), homotopy_groups (S n) →* homotopy_groups n - | (n, fin.mk 0 H) := proof π→*[n] f qed - | (n, fin.mk 1 H) := proof π→*[n] (ppoint f) qed - | (n, fin.mk 2 H) := - proof π→*[n] boundary_map ∘* pcast (ap (ptrunc 0) (loop_space_succ_eq_in Y n)) qed - | (n, fin.mk (k+3) H) := begin exfalso, apply lt_le_antisymm H, apply le_add_left end - - definition homotopy_groups_fun_phomotopy_loop_spaces_fun2 [reducible] - : Π(n : +3ℕ), homotopy_groups_pequiv_loop_spaces2 n ∘* ptrunc_functor 0 (loop_spaces_fun2 n) ~* - homotopy_groups_fun n ∘* homotopy_groups_pequiv_loop_spaces2 (S n) - | (n, fin.mk 0 H) := by reflexivity - | (n, fin.mk 1 H) := by reflexivity - | (n, fin.mk 2 H) := - begin - refine !pid_comp ⬝* _ ⬝* !comp_pid⁻¹*, - refine !ptrunc_functor_pcompose ⬝* _, - apply pwhisker_left, apply ptrunc_functor_pcast, - end - | (n, fin.mk (k+3) H) := begin exfalso, apply lt_le_antisymm H, apply le_add_left end - - definition LES_of_homotopy_groups [constructor] : chain_complex +3ℕ := - transfer_chain_complex - LES_of_homotopy_groups' - homotopy_groups_fun - homotopy_groups_pequiv_loop_spaces2 - homotopy_groups_fun_phomotopy_loop_spaces_fun2 - - definition is_exact_LES_of_homotopy_groups : is_exact LES_of_homotopy_groups := - begin - intro n, - apply is_exact_at_transfer, - apply is_exact_at_trunc, - apply is_exact_LES_of_loop_spaces2 - end - - variable (n : ℕ) - - /- the carrier of the fiber sequence is definitionally what we want (as pointed sets) -/ - example : LES_of_homotopy_groups (str_of_nat 6) = π*[2] Y :> Set* := by reflexivity - example : LES_of_homotopy_groups (str_of_nat 7) = π*[2] X :> Set* := by reflexivity - example : LES_of_homotopy_groups (str_of_nat 8) = π*[2] (pfiber f) :> Set* := by reflexivity - example : LES_of_homotopy_groups (str_of_nat 9) = π*[3] Y :> Set* := by reflexivity - example : LES_of_homotopy_groups (str_of_nat 10) = π*[3] X :> Set* := by reflexivity - example : LES_of_homotopy_groups (str_of_nat 11) = π*[3] (pfiber f) :> Set* := by reflexivity - - definition LES_of_homotopy_groups_0 : LES_of_homotopy_groups (n, 0) = π*[n] Y := - by reflexivity - definition LES_of_homotopy_groups_1 : LES_of_homotopy_groups (n, 1) = π*[n] X := - by reflexivity - definition LES_of_homotopy_groups_2 : LES_of_homotopy_groups (n, 2) = π*[n] (pfiber f) := - by reflexivity - - /- - the functions of the fiber sequence is definitionally what we want (as pointed function). - -/ - - definition LES_of_homotopy_groups_fun_0 : - cc_to_fn LES_of_homotopy_groups (n, 0) = π→*[n] f := - by reflexivity - definition LES_of_homotopy_groups_fun_1 : - cc_to_fn LES_of_homotopy_groups (n, 1) = π→*[n] (ppoint f) := - by reflexivity - definition LES_of_homotopy_groups_fun_2 : cc_to_fn LES_of_homotopy_groups (n, 2) = - π→*[n] boundary_map ∘* pcast (ap (ptrunc 0) (loop_space_succ_eq_in Y n)) := - by reflexivity - - open group - - definition group_LES_of_homotopy_groups (n : ℕ) : Π(x : fin (succ 2)), - group (LES_of_homotopy_groups (n + 1, x)) - | (fin.mk 0 H) := begin rexact group_homotopy_group n Y end - | (fin.mk 1 H) := begin rexact group_homotopy_group n X end - | (fin.mk 2 H) := begin rexact group_homotopy_group n (pfiber f) end - | (fin.mk (k+3) H) := begin exfalso, apply lt_le_antisymm H, apply le_add_left end - - definition comm_group_LES_of_homotopy_groups (n : ℕ) : Π(x : fin (succ 2)), - comm_group (LES_of_homotopy_groups (n + 2, x)) - | (fin.mk 0 H) := proof comm_group_homotopy_group n Y qed - | (fin.mk 1 H) := proof comm_group_homotopy_group n X qed - | (fin.mk 2 H) := proof comm_group_homotopy_group n (pfiber f) qed - | (fin.mk (k+3) H) := begin exfalso, apply lt_le_antisymm H, apply le_add_left end - - definition Group_LES_of_homotopy_groups (x : +3ℕ) : Group.{u} := - Group.mk (LES_of_homotopy_groups (nat.succ (pr1 x), pr2 x)) - (group_LES_of_homotopy_groups (pr1 x) (pr2 x)) - - definition CommGroup_LES_of_homotopy_groups (n : +3ℕ) : CommGroup.{u} := - CommGroup.mk (LES_of_homotopy_groups (pr1 n + 2, pr2 n)) - (comm_group_LES_of_homotopy_groups (pr1 n) (pr2 n)) - - definition homomorphism_LES_of_homotopy_groups_fun : Π(k : +3ℕ), - Group_LES_of_homotopy_groups (S k) →g Group_LES_of_homotopy_groups k - | (k, fin.mk 0 H) := - proof homomorphism.mk (cc_to_fn LES_of_homotopy_groups (k + 1, 0)) - (phomotopy_group_functor_mul _ _) qed - | (k, fin.mk 1 H) := - proof homomorphism.mk (cc_to_fn LES_of_homotopy_groups (k + 1, 1)) - (phomotopy_group_functor_mul _ _) qed - | (k, fin.mk 2 H) := - begin - apply homomorphism.mk (cc_to_fn LES_of_homotopy_groups (k + 1, 2)), - exact abstract begin rewrite [LES_of_homotopy_groups_fun_2], - refine @is_homomorphism_compose _ _ _ _ _ _ (π→*[k + 1] boundary_map) _ _ _, - { apply group_homotopy_group k}, - { apply phomotopy_group_functor_mul}, - { rewrite [▸*, -ap_compose', ▸*], - apply is_homomorphism_cast_loop_space_succ_eq_in} end end - end - | (k, fin.mk (l+3) H) := begin exfalso, apply lt_le_antisymm H, apply le_add_left end - - end -end chain_complex diff --git a/homotopy/LES_of_homotopy_groups_old.hlean b/homotopy/LES_of_homotopy_groups_old.hlean index 7b3f19e..2e6b31a 100644 --- a/homotopy/LES_of_homotopy_groups_old.hlean +++ b/homotopy/LES_of_homotopy_groups_old.hlean @@ -7,12 +7,12 @@ The old formalization of the LES of homotopy groups, where all the odd levels ha with negation -/ -import .LES_of_homotopy_groups +import homotopy.LES_of_homotopy_groups open eq pointed sigma fiber equiv is_equiv sigma.ops is_trunc nat trunc algebra function /-------------- - PART 1 + PART 1 is the same as the new formalization --------------/ namespace chain_complex @@ -721,7 +721,7 @@ namespace chain_complex namespace old begin apply homomorphism.mk (cc_to_fn (LES_of_homotopy_groups3 f) (k + 1, 2)), exact abstract begin rewrite [LES_of_homotopy_groups_fun3_2], - refine @is_homomorphism_compose _ _ _ _ _ _ (π→*[2 * (k + 1)] boundary_map f) _ _ _, + refine @is_homomorphism_compose _ _ _ _ _ _ (π→*[2 * (k + 1)] (boundary_map f)) _ _ _, { apply group_homotopy_group ((2 * k) + 1)}, { apply phomotopy_group_functor_mul}, { rewrite [▸*, -ap_compose', ▸*], diff --git a/homotopy/chain_complex.hlean b/homotopy/chain_complex.hlean deleted file mode 100644 index b6271fd..0000000 --- a/homotopy/chain_complex.hlean +++ /dev/null @@ -1,561 +0,0 @@ -/- -Copyright (c) 2016 Floris van Doorn. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Floris van Doorn - --/ - -import types.int types.pointed types.trunc algebra.hott ..group_theory.basic .fin - -open eq pointed int unit is_equiv equiv is_trunc trunc function algebra group sigma.ops - sum prod nat bool fin -namespace eq - definition transport_eq_Fl_idp_left {A B : Type} {a : A} {b : B} (f : A → B) (q : f a = b) - : transport_eq_Fl idp q = !idp_con⁻¹ := - by induction q; reflexivity - - definition whisker_left_idp_con_eq_assoc - {A : Type} {a₁ a₂ a₃ : A} (p : a₁ = a₂) (q : a₂ = a₃) - : whisker_left p (idp_con q)⁻¹ = con.assoc p idp q := - by induction q; reflexivity - -end eq open eq - -structure succ_str : Type := - (carrier : Type) - (succ : carrier → carrier) - -attribute succ_str.carrier [coercion] - -definition succ_str.S {X : succ_str} : X → X := succ_str.succ X - -open succ_str - -definition snat [reducible] [constructor] : succ_str := succ_str.mk ℕ nat.succ -definition snat' [reducible] [constructor] : succ_str := succ_str.mk ℕ nat.pred -definition sint [reducible] [constructor] : succ_str := succ_str.mk ℤ int.succ -definition sint' [reducible] [constructor] : succ_str := succ_str.mk ℤ int.pred - -notation `+ℕ` := snat -notation `-ℕ` := snat' -notation `+ℤ` := sint -notation `-ℤ` := sint' - -definition stratified_type [reducible] (N : succ_str) (n : ℕ) : Type₀ := N × fin (succ n) - -definition stratified_succ {N : succ_str} {n : ℕ} (x : stratified_type N n) - : stratified_type N n := -(if val (pr2 x) = n then S (pr1 x) else pr1 x, my_succ (pr2 x)) - -definition stratified [reducible] [constructor] (N : succ_str) (n : ℕ) : succ_str := -succ_str.mk (stratified_type N n) stratified_succ - -notation `+3ℕ` := stratified +ℕ 2 -notation `-3ℕ` := stratified -ℕ 2 -notation `+3ℤ` := stratified +ℤ 2 -notation `-3ℤ` := stratified -ℤ 2 -notation `+6ℕ` := stratified +ℕ 5 -notation `-6ℕ` := stratified -ℕ 5 -notation `+6ℤ` := stratified +ℤ 5 -notation `-6ℤ` := stratified -ℤ 5 - -namespace chain_complex - - -- are chain complexes with the "set"-requirement removed interesting? - structure type_chain_complex (N : succ_str) : Type := - (car : N → Type*) - (fn : Π(n : N), car (S n) →* car n) - (is_chain_complex : Π(n : N) (x : car (S (S n))), fn n (fn (S n) x) = pt) - - section - variables {N : succ_str} (X : type_chain_complex N) (n : N) - - definition tcc_to_car [unfold 2] [coercion] := @type_chain_complex.car - definition tcc_to_fn [unfold 2] : X (S n) →* X n := type_chain_complex.fn X n - definition tcc_is_chain_complex [unfold 2] - : Π(x : X (S (S n))), tcc_to_fn X n (tcc_to_fn X (S n) x) = pt := - type_chain_complex.is_chain_complex X n - - -- important: these notions are shifted by one! (this is to avoid transports) - definition is_exact_at_t [reducible] /- X n -/ : Type := - Π(x : X (S n)), tcc_to_fn X n x = pt → fiber (tcc_to_fn X (S n)) x - - definition is_exact_t [reducible] /- X -/ : Type := - Π(n : N), is_exact_at_t X n - - -- definition type_chain_complex_from_left (X : type_chain_complex) : type_chain_complex := - -- type_chain_complex.mk (int.rec X (λn, punit)) - -- begin - -- intro n, fconstructor, - -- { induction n with n n, - -- { exact @ltcc_to_fn X n}, - -- { esimp, intro x, exact star}}, - -- { induction n with n n, - -- { apply respect_pt}, - -- { reflexivity}} - -- end - -- begin - -- intro n, induction n with n n, - -- { exact ltcc_is_chain_complex X}, - -- { esimp, intro x, reflexivity} - -- end - - -- definition is_exact_t_from_left {X : type_chain_complex} {n : ℕ} (H : is_exact_at_lt X n) - -- : is_exact_at_t (type_chain_complex_from_left X) n := - -- H - - definition transfer_type_chain_complex [constructor] /- X -/ - {Y : N → Type*} (g : Π{n : N}, Y (S n) →* Y n) (e : Π{n}, X n ≃* Y n) - (p : Π{n} (x : X (S n)), e (tcc_to_fn X n x) = g (e x)) : type_chain_complex N := - type_chain_complex.mk Y @g - abstract begin - intro n, apply equiv_rect (equiv_of_pequiv e), intro x, - refine ap g (p x)⁻¹ ⬝ _, - refine (p _)⁻¹ ⬝ _, - refine ap e (tcc_is_chain_complex X n _) ⬝ _, - apply respect_pt - end end - - theorem is_exact_at_t_transfer {X : type_chain_complex N} {Y : N → Type*} - {g : Π{n : N}, Y (S n) →* Y n} (e : Π{n}, X n ≃* Y n) - (p : Π{n} (x : X (S n)), e (tcc_to_fn X n x) = g (e x)) {n : N} - (H : is_exact_at_t X n) : is_exact_at_t (transfer_type_chain_complex X @g @e @p) n := - begin - intro y q, esimp at *, - have H2 : tcc_to_fn X n (e⁻¹ᵉ* y) = pt, - begin - refine (inv_commute (λn, equiv_of_pequiv e) _ _ @p _)⁻¹ᵖ ⬝ _, - refine ap _ q ⬝ _, - exact respect_pt e⁻¹ᵉ* - end, - cases (H _ H2) with x r, - refine fiber.mk (e x) _, - refine (p x)⁻¹ ⬝ _, - refine ap e r ⬝ _, - apply right_inv - end - - -- cancel automorphisms inside a long exact sequence - definition type_chain_complex_cancel_aut [constructor] /- X -/ - (g : Π{n : N}, X (S n) →* X n) (e : Π{n}, X n ≃* X n) - (r : Π{n}, X n →* X n) - (p : Π{n : N} (x : X (S n)), g (e x) = tcc_to_fn X n x) - (pr : Π{n : N} (x : X (S n)), g x = r (g (e x))) : type_chain_complex N := - type_chain_complex.mk X @g - abstract begin - have p' : Π{n : N} (x : X (S n)), g x = tcc_to_fn X n (e⁻¹ x), - from λn, homotopy_inv_of_homotopy_pre e _ _ p, - intro n x, - refine ap g !p' ⬝ !pr ⬝ _, - refine ap r !p ⬝ _, - refine ap r (tcc_is_chain_complex X n _) ⬝ _, - apply respect_pt - end end - - theorem is_exact_at_t_cancel_aut {X : type_chain_complex N} - {g : Π{n : N}, X (S n) →* X n} {e : Π{n}, X n ≃* X n} - {r : Π{n}, X n →* X n} (l : Π{n}, X n →* X n) - (p : Π{n : N} (x : X (S n)), g (e x) = tcc_to_fn X n x) - (pr : Π{n : N} (x : X (S n)), g x = r (g (e x))) - (pl : Π{n : N} (x : X (S n)), g (l x) = e (g x)) - (H : is_exact_at_t X n) : is_exact_at_t (type_chain_complex_cancel_aut X @g @e @r @p @pr) n := - begin - intro y q, esimp at *, - have H2 : tcc_to_fn X n (e⁻¹ y) = pt, - from (homotopy_inv_of_homotopy_pre e _ _ p _)⁻¹ ⬝ q, - cases (H _ H2) with x s, - refine fiber.mk (l (e x)) _, - refine !pl ⬝ _, - refine ap e (!p ⬝ s) ⬝ _, - apply right_inv - end - - -- move to init.equiv. This is inv_commute for A ≡ unit - definition inv_commute1' {B C : Type} (f : B → C) [is_equiv f] (h : B → B) (h' : C → C) - (p : Π(b : B), f (h b) = h' (f b)) (c : C) : f⁻¹ (h' c) = h (f⁻¹ c) := - eq_of_fn_eq_fn' f (right_inv f (h' c) ⬝ ap h' (right_inv f c)⁻¹ ⬝ (p (f⁻¹ c))⁻¹) - - definition inv_commute1 {B C : Type} (f : B ≃ C) (h : B → B) (h' : C → C) - (p : Π(b : B), f (h b) = h' (f b)) (c : C) : f⁻¹ (h' c) = h (f⁻¹ c) := - inv_commute1' (to_fun f) h h' p c - - -- move - definition fn_cast_eq_cast_fn {A : Type} {P Q : A → Type} {x y : A} (p : x = y) - (f : Πx, P x → Q x) (z : P x) : f y (cast (ap P p) z) = cast (ap Q p) (f x z) := - by induction p; reflexivity - - definition cast_cast_inv {A : Type} {P : A → Type} {x y : A} (p : x = y) (z : P y) : - cast (ap P p) (cast (ap P p⁻¹) z) = z := - by induction p; reflexivity - - definition cast_inv_cast {A : Type} {P : A → Type} {x y : A} (p : x = y) (z : P x) : - cast (ap P p⁻¹) (cast (ap P p) z) = z := - by induction p; reflexivity - - -- more general transfer, where the base type can also change by an equivalence. - definition transfer_type_chain_complex2 [constructor] {M : succ_str} {Y : M → Type*} - (f : M ≃ N) (c : Π(m : M), S (f m) = f (S m)) - (g : Π{m : M}, Y (S m) →* Y m) (e : Π{m}, X (f m) ≃* Y m) - (p : Π{m} (x : X (S (f m))), e (tcc_to_fn X (f m) x) = g (e (cast (ap (λx, X x) (c m)) x))) - : type_chain_complex M := - type_chain_complex.mk Y @g - begin - intro m, - apply equiv_rect (equiv_of_pequiv e), - apply equiv_rect (equiv_of_eq (ap (λx, X x) (c (S m)))), esimp, - apply equiv_rect (equiv_of_eq (ap (λx, X (S x)) (c m))), esimp, - intro x, refine ap g (p _)⁻¹ ⬝ _, - refine ap g (ap e (fn_cast_eq_cast_fn (c m) (tcc_to_fn X) x)) ⬝ _, - refine (p _)⁻¹ ⬝ _, - refine ap e (tcc_is_chain_complex X (f m) _) ⬝ _, - apply respect_pt - end - - definition is_exact_at_t_transfer2 {X : type_chain_complex N} {M : succ_str} {Y : M → Type*} - (f : M ≃ N) (c : Π(m : M), S (f m) = f (S m)) - (g : Π{m : M}, Y (S m) →* Y m) (e : Π{m}, X (f m) ≃* Y m) - (p : Π{m} (x : X (S (f m))), e (tcc_to_fn X (f m) x) = g (e (cast (ap (λx, X x) (c m)) x))) - {m : M} (H : is_exact_at_t X (f m)) - : is_exact_at_t (transfer_type_chain_complex2 X f c @g @e @p) m := - begin - intro y q, esimp at *, - have H2 : tcc_to_fn X (f m) ((equiv_of_eq (ap (λx, X x) (c m)))⁻¹ᵉ (e⁻¹ y)) = pt, - begin - refine _ ⬝ ap e⁻¹ᵉ* q ⬝ (respect_pt (e⁻¹ᵉ*)), apply eq_inv_of_eq, clear q, revert y, - apply inv_homotopy_of_homotopy_pre e, - apply inv_homotopy_of_homotopy_pre, apply p - end, - induction (H _ H2) with x r, - refine fiber.mk (e (cast (ap (λx, X x) (c (S m))) (cast (ap (λx, X (S x)) (c m)) x))) _, - refine (p _)⁻¹ ⬝ _, - refine ap e (fn_cast_eq_cast_fn (c m) (tcc_to_fn X) x) ⬝ _, - refine ap (λx, e (cast _ x)) r ⬝ _, - esimp [equiv.symm], rewrite [-ap_inv], - refine ap e !cast_cast_inv ⬝ _, - apply right_inv - end - - -- definition trunc_type_chain_complex [constructor] (X : type_chain_complex N) - -- (k : trunc_index) : type_chain_complex N := - -- type_chain_complex.mk - -- (λn, ptrunc k (X n)) - -- (λn, ptrunc_functor k (tcc_to_fn X n)) - -- begin - -- intro n x, esimp at *, - -- refine trunc.rec _ x, -- why doesn't induction work here? - -- clear x, intro x, esimp, - -- exact ap tr (tcc_is_chain_complex X n x) - -- end - end - - /- actual (set) chain complexes -/ - structure chain_complex (N : succ_str) : Type := - (car : N → Set*) - (fn : Π(n : N), car (S n) →* car n) - (is_chain_complex : Π(n : N) (x : car (S (S n))), fn n (fn (S n) x) = pt) - - section - variables {N : succ_str} (X : chain_complex N) (n : N) - - definition cc_to_car [unfold 2] [coercion] := @chain_complex.car - definition cc_to_fn [unfold 2] : X (S n) →* X n := @chain_complex.fn N X n - definition cc_is_chain_complex [unfold 2] - : Π(x : X (S (S n))), cc_to_fn X n (cc_to_fn X (S n) x) = pt := - @chain_complex.is_chain_complex N X n - - -- important: these notions are shifted by one! (this is to avoid transports) - definition is_exact_at [reducible] /- X n -/ : Type := - Π(x : X (S n)), cc_to_fn X n x = pt → image (cc_to_fn X (S n)) x - - definition is_exact [reducible] /- X -/ : Type := Π(n : N), is_exact_at X n - - -- definition chain_complex_from_left (X : chain_complex) : chain_complex := - -- chain_complex.mk (int.rec X (λn, punit)) - -- begin - -- intro n, fconstructor, - -- { induction n with n n, - -- { exact @lcc_to_fn X n}, - -- { esimp, intro x, exact star}}, - -- { induction n with n n, - -- { apply respect_pt}, - -- { reflexivity}} - -- end - -- begin - -- intro n, induction n with n n, - -- { exact lcc_is_chain_complex X}, - -- { esimp, intro x, reflexivity} - -- end - - -- definition is_exact_from_left {X : chain_complex} {n : ℕ} (H : is_exact_at_l X n) - -- : is_exact_at (chain_complex_from_left X) n := - -- H - - definition transfer_chain_complex [constructor] {Y : N → Set*} - (g : Π{n : N}, Y (S n) →* Y n) (e : Π{n}, X n ≃* Y n) - (p : Π{n} (x : X (S n)), e (cc_to_fn X n x) = g (e x)) : chain_complex N := - chain_complex.mk Y @g - abstract begin - intro n, apply equiv_rect (equiv_of_pequiv e), intro x, - refine ap g (p x)⁻¹ ⬝ _, - refine (p _)⁻¹ ⬝ _, - refine ap e (cc_is_chain_complex X n _) ⬝ _, - apply respect_pt - end end - - theorem is_exact_at_transfer {X : chain_complex N} {Y : N → Set*} - (g : Π{n : N}, Y (S n) →* Y n) (e : Π{n}, X n ≃* Y n) - (p : Π{n} (x : X (S n)), e (cc_to_fn X n x) = g (e x)) - {n : N} (H : is_exact_at X n) : is_exact_at (transfer_chain_complex X @g @e @p) n := - begin - intro y q, esimp at *, - have H2 : cc_to_fn X n (e⁻¹ᵉ* y) = pt, - begin - refine (inv_commute (λn, equiv_of_pequiv e) _ _ @p _)⁻¹ᵖ ⬝ _, - refine ap _ q ⬝ _, - exact respect_pt e⁻¹ᵉ* - end, - induction (H _ H2) with x, - induction x with x r, - refine image.mk (e x) _, - refine (p x)⁻¹ ⬝ _, - refine ap e r ⬝ _, - apply right_inv - end - - definition trunc_chain_complex [constructor] (X : type_chain_complex N) - : chain_complex N := - chain_complex.mk - (λn, ptrunc 0 (X n)) - (λn, ptrunc_functor 0 (tcc_to_fn X n)) - begin - intro n x, esimp at *, - refine @trunc.rec _ _ _ (λH, !is_trunc_eq) _ x, - clear x, intro x, esimp, - exact ap tr (tcc_is_chain_complex X n x) - end - - definition is_exact_at_trunc (X : type_chain_complex N) {n : N} - (H : is_exact_at_t X n) : is_exact_at (trunc_chain_complex X) n := - begin - intro x p, esimp at *, - induction x with x, esimp at *, - note q := !tr_eq_tr_equiv p, - induction q with q, - induction H x q with y r, - refine image.mk (tr y) _, - esimp, exact ap tr r - end - - definition transfer_chain_complex2' [constructor] {M : succ_str} {Y : M → Set*} - (f : N ≃ M) (c : Π(n : N), f (S n) = S (f n)) - (g : Π{m : M}, Y (S m) →* Y m) (e : Π{n}, X n ≃* Y (f n)) - (p : Π{n} (x : X (S n)), e (cc_to_fn X n x) = g (c n ▸ e x)) : chain_complex M := - chain_complex.mk Y @g - begin - refine equiv_rect f _ _, intro n, - have H : Π (x : Y (f (S (S n)))), g (c n ▸ g (c (S n) ▸ x)) = pt, - begin - apply equiv_rect (equiv_of_pequiv e), intro x, - refine ap (λx, g (c n ▸ x)) (@p (S n) x)⁻¹ᵖ ⬝ _, - refine (p _)⁻¹ ⬝ _, - refine ap e (cc_is_chain_complex X n _) ⬝ _, - apply respect_pt - end, - refine pi.pi_functor _ _ H, - { intro x, exact (c (S n))⁻¹ ▸ (c n)⁻¹ ▸ x}, -- with implicit arguments, this is: - -- transport (λx, Y x) (c (S n))⁻¹ (transport (λx, Y (S x)) (c n)⁻¹ x) - { intro x, intro p, refine _ ⬝ p, rewrite [tr_inv_tr, fn_tr_eq_tr_fn (c n)⁻¹ @g, tr_inv_tr]} - end - - definition is_exact_at_transfer2' {X : chain_complex N} {M : succ_str} {Y : M → Set*} - (f : N ≃ M) (c : Π(n : N), f (S n) = S (f n)) - (g : Π{m : M}, Y (S m) →* Y m) (e : Π{n}, X n ≃* Y (f n)) - (p : Π{n} (x : X (S n)), e (cc_to_fn X n x) = g (c n ▸ e x)) - {n : N} (H : is_exact_at X n) : is_exact_at (transfer_chain_complex2' X f c @g @e @p) (f n) := - begin - intro y q, esimp at *, - have H2 : cc_to_fn X n (e⁻¹ᵉ* ((c n)⁻¹ ▸ y)) = pt, - begin - refine (inv_commute (λn, equiv_of_pequiv e) _ _ @p _)⁻¹ᵖ ⬝ _, - rewrite [tr_inv_tr, q], - exact respect_pt e⁻¹ᵉ* - end, - induction (H _ H2) with x, - induction x with x r, - refine image.mk (c n ▸ c (S n) ▸ e x) _, - rewrite [fn_tr_eq_tr_fn (c n) @g], - refine ap (λx, c n ▸ x) (p x)⁻¹ ⬝ _, - refine ap (λx, c n ▸ e x) r ⬝ _, - refine ap (λx, c n ▸ x) !right_inv ⬝ _, - apply tr_inv_tr, - end - - -- structure group_chain_complex : Type := - -- (car : N → Group) - -- (fn : Π(n : N), car (S n) →g car n) - -- (is_chain_complex : Π{n : N} (x : car ((S n) + 1)), fn n (fn (S n) x) = 1) - - -- structure group_chain_complex : Type := -- chain complex on the naturals with maps going down - -- (car : N → Group) - -- (fn : Π(n : N), car (S n) →g car n) - -- (is_chain_complex : Π{n : N} (x : car ((S n) + 1)), fn n (fn (S n) x) = 1) - - -- structure right_group_chain_complex : Type := -- chain complex on the naturals with maps going up - -- (car : N → Group) - -- (fn : Π(n : N), car n →g car (S n)) - -- (is_chain_complex : Π{n : N} (x : car n), fn (S n) (fn n x) = 1) - - -- definition gcc_to_car [unfold 1] [coercion] := @group_chain_complex.car - -- definition gcc_to_fn [unfold 1] := @group_chain_complex.fn - -- definition gcc_is_chain_complex [unfold 1] := @group_chain_complex.is_chain_complex - -- definition lgcc_to_car [unfold 1] [coercion] := @left_group_chain_complex.car - -- definition lgcc_to_fn [unfold 1] := @left_group_chain_complex.fn - -- definition lgcc_is_chain_complex [unfold 1] := @left_group_chain_complex.is_chain_complex - -- definition rgcc_to_car [unfold 1] [coercion] := @right_group_chain_complex.car - -- definition rgcc_to_fn [unfold 1] := @right_group_chain_complex.fn - -- definition rgcc_is_chain_complex [unfold 1] := @right_group_chain_complex.is_chain_complex - - -- -- important: these notions are shifted by one! (this is to avoid transports) - -- definition is_exact_at_g [reducible] (X : group_chain_complex) (n : N) : Type := - -- Π(x : X (S n)), gcc_to_fn X n x = 1 → image (gcc_to_fn X (S n)) x - -- definition is_exact_at_lg [reducible] (X : left_group_chain_complex) (n : N) : Type := - -- Π(x : X (S n)), lgcc_to_fn X n x = 1 → image (lgcc_to_fn X (S n)) x - -- definition is_exact_at_rg [reducible] (X : right_group_chain_complex) (n : N) : Type := - -- Π(x : X (S n)), rgcc_to_fn X (S n) x = 1 → image (rgcc_to_fn X n) x - - -- definition is_exact_g [reducible] (X : group_chain_complex) : Type := - -- Π(n : N), is_exact_at_g X n - -- definition is_exact_lg [reducible] (X : left_group_chain_complex) : Type := - -- Π(n : N), is_exact_at_lg X n - -- definition is_exact_rg [reducible] (X : right_group_chain_complex) : Type := - -- Π(n : N), is_exact_at_rg X n - - -- definition group_chain_complex_from_left (X : left_group_chain_complex) : group_chain_complex := - -- group_chain_complex.mk (int.rec X (λn, G0)) - -- begin - -- intro n, fconstructor, - -- { induction n with n n, - -- { exact @lgcc_to_fn X n}, - -- { esimp, intro x, exact star}}, - -- { induction n with n n, - -- { apply respect_mul}, - -- { intro g h, reflexivity}} - -- end - -- begin - -- intro n, induction n with n n, - -- { exact lgcc_is_chain_complex X}, - -- { esimp, intro x, reflexivity} - -- end - - -- definition is_exact_g_from_left {X : left_group_chain_complex} {n : N} (H : is_exact_at_lg X n) - -- : is_exact_at_g (group_chain_complex_from_left X) n := - -- H - - -- definition transfer_left_group_chain_complex [constructor] (X : left_group_chain_complex) - -- {Y : N → Group} (g : Π{n : N}, Y (S n) →g Y n) (e : Π{n}, X n ≃* Y n) - -- (p : Π{n} (x : X (S n)), e (lgcc_to_fn X n x) = g (e x)) : left_group_chain_complex := - -- left_group_chain_complex.mk Y @g - -- begin - -- intro n, apply equiv_rect (pequiv_of_equiv e), intro x, - -- refine ap g (p x)⁻¹ ⬝ _, - -- refine (p _)⁻¹ ⬝ _, - -- refine ap e (lgcc_is_chain_complex X _) ⬝ _, - -- exact respect_pt - -- end - - -- definition is_exact_at_t_transfer {X : left_group_chain_complex} {Y : N → Type*} - -- {g : Π{n : N}, Y (S n) →* Y n} (e : Π{n}, X n ≃* Y n) - -- (p : Π{n} (x : X (S n)), e (lgcc_to_fn X n x) = g (e x)) {n : N} - -- (H : is_exact_at_lg X n) : is_exact_at_lg (transfer_left_group_chain_complex X @g @e @p) n := - -- begin - -- intro y q, esimp at *, - -- have H2 : lgcc_to_fn X n (e⁻¹ᵉ* y) = pt, - -- begin - -- refine (inv_commute (λn, equiv_of_pequiv e) _ _ @p _)⁻¹ᵖ ⬝ _, - -- refine ap _ q ⬝ _, - -- exact respect_pt e⁻¹ᵉ* - -- end, - -- cases (H _ H2) with x r, - -- refine image.mk (e x) _, - -- refine (p x)⁻¹ ⬝ _, - -- refine ap e r ⬝ _, - -- apply right_inv - -- end - - -- TODO: move - definition is_trunc_ptrunctype [instance] {n : trunc_index} (X : ptrunctype n) - : is_trunc n (ptrunctype.to_pType X) := - trunctype.struct X - - /- - A group where the point in the pointed type corresponds with 1 in the group. - We need this structure because a chain complex is a sequence of pointed types, and we need - to assume for some of the theorems below that some of these pointed types are groups, where the - unit for multiplication is the point. - -/ - structure pgroup [class] (X : Type*) extends semigroup X, has_inv X := - (pt_mul : Πa, mul pt a = a) - (mul_pt : Πa, mul a pt = a) - (mul_left_inv_pt : Πa, mul (inv a) a = pt) - - definition group_of_pgroup [reducible] [instance] (X : Type*) [H : pgroup X] - : group X := - ⦃group, H, - one := pt, - one_mul := pgroup.pt_mul , - mul_one := pgroup.mul_pt, - mul_left_inv := pgroup.mul_left_inv_pt⦄ - - definition pgroup_of_group (X : Type*) [H : group X] (p : one = pt :> X) : pgroup X := - begin - cases X with X x, esimp at *, induction p, - exact ⦃pgroup, H, - pt_mul := one_mul, - mul_pt := mul_one, - mul_left_inv_pt := mul.left_inv⦄ - end - - /- - The following theorems state that in a chain complex, if certain types are contractible, and - the chain complex is exact at the right spots, a map in the chain complex is an - embedding/surjection/equivalence. For the first and third we also need to assume that - the map is a group homomorphism (and hence that the two types around it are groups). - -/ - - definition is_embedding_of_trivial (X : chain_complex N) {n : N} - (H : is_exact_at X n) [HX : is_contr (X (S (S n)))] - [pgroup (X n)] [pgroup (X (S n))] [is_homomorphism (cc_to_fn X n)] - : is_embedding (cc_to_fn X n) := - begin - apply is_embedding_homomorphism, - intro g p, - induction H g p with v, - induction v with x q, - have r : pt = x, from !is_prop.elim, - induction r, - refine q⁻¹ ⬝ _, - apply respect_pt - end - - definition is_surjective_of_trivial (X : chain_complex N) {n : N} - (H : is_exact_at X n) [HX : is_contr (X n)] : is_surjective (cc_to_fn X (S n)) := - begin - intro g, - refine trunc.elim _ (H g !is_prop.elim), - apply tr - end - - definition is_equiv_of_trivial (X : chain_complex N) {n : N} - (H1 : is_exact_at X n) (H2 : is_exact_at X (S n)) - [HX1 : is_contr (X n)] [HX2 : is_contr (X (S (S (S n))))] - [pgroup (X (S n))] [pgroup (X (S (S n)))] [is_homomorphism (cc_to_fn X (S n))] - : is_equiv (cc_to_fn X (S n)) := - begin - apply is_equiv_of_is_surjective_of_is_embedding, - { apply is_embedding_of_trivial X, apply H2}, - { apply is_surjective_of_trivial X, apply H1}, - end - - end - -end chain_complex diff --git a/homotopy/fin.hlean b/homotopy/fin.hlean deleted file mode 100644 index 990e01d..0000000 --- a/homotopy/fin.hlean +++ /dev/null @@ -1,59 +0,0 @@ -/- -Copyright (c) 2016 Floris van Doorn. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Floris van Doorn - -Finite ordinal types. --/ - -import types.fin - -open eq nat fin algebra - -inductive is_succ [class] : ℕ → Type := -| mk : Πn, is_succ (succ n) - -attribute is_succ.mk [instance] - -definition is_succ_add_right [instance] (n m : ℕ) [H : is_succ m] : is_succ (n+m) := -by induction H with m; constructor - -definition is_succ_add_left (n m : ℕ) [H : is_succ n] : is_succ (n+m) := -by induction H with n; cases m with m: constructor - -definition is_succ_bit0 [instance] (n : ℕ) [H : is_succ n] : is_succ (bit0 n) := -by induction H with n; constructor - - -namespace fin - - definition my_succ {n : ℕ} (x : fin n) : fin n := - begin - cases n with n, - { exfalso, apply not_lt_zero _ (is_lt x)}, - { exact - if H : val x = n - then fin.mk 0 !zero_lt_succ - else fin.mk (nat.succ (val x)) (succ_lt_succ (lt_of_le_of_ne (le_of_lt_succ (is_lt x)) H))} - end - - protected definition add {n : ℕ} (x y : fin n) : fin n := - iterate my_succ (val y) x - - definition has_zero_fin [instance] (n : ℕ) [H : is_succ n] : has_zero (fin n) := - by induction H with n; exact has_zero.mk (fin.zero n) - - definition has_one_fin [instance] (n : ℕ) [H : is_succ n] : has_one (fin n) := - by induction H with n; exact has_one.mk (my_succ (fin.zero n)) - - definition has_add_fin [instance] (n : ℕ) : has_add (fin n) := - has_add.mk fin.add - - -- definition my_succ_eq_zero {n : ℕ} (x : fin (nat.succ n)) (p : val x = n) : my_succ x = 0 := - -- if H : val x = n - -- then fin.mk 0 !zero_lt_succ - -- else fin.mk (nat.succ (val x)) (succ_lt_succ (lt_of_le_of_ne (le_of_lt_succ (is_lt x)) H)) - - - -end fin diff --git a/homotopy/homotopy_groups.hlean b/homotopy/homotopy_groups.hlean deleted file mode 100644 index 2ac4d87..0000000 --- a/homotopy/homotopy_groups.hlean +++ /dev/null @@ -1,97 +0,0 @@ -/- -Copyright (c) 2016 Floris van Doorn. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Floris van Doorn - --/ - --- to be moved to algebra/homotopy_group in the Lean library - -import group_theory.basic algebra.homotopy_group - -open eq algebra pointed group trunc is_trunc nat algebra equiv is_equiv - -namespace my - - section - variables {A B C : Type*} - definition apn_compose (n : ℕ) (g : B →* C) (f : A →* B) : apn n (g ∘* f) ~* apn n g ∘* apn n f := - begin - induction n with n IH, - { reflexivity}, - { refine ap1_phomotopy IH ⬝* _, apply ap1_compose} - end - - theorem ap1_con (f : A →* B) (p q : Ω A) : ap1 f (p ⬝ q) = ap1 f p ⬝ ap1 f q := - begin - rewrite [▸*, ap_con, +con.assoc, con_inv_cancel_left] - end - - definition apn_con {n : ℕ} (f : A →* B) (p q : Ω[n + 1] A) - : apn (n+1) f (p ⬝ q) = apn (n+1) f p ⬝ apn (n+1) f q := - ap1_con (apn n f) p q - - definition tr_mul {n : ℕ} (p q : Ω[n + 1] A) : @mul (πg[n+1] A) _ (tr p ) (tr q) = tr (p ⬝ q) := - by reflexivity - end - - section - - parameters {A B : Type} (f : A ≃ B) [group A] - - definition group_equiv_mul (b b' : B) : B := f (f⁻¹ᶠ b * f⁻¹ᶠ b') - - definition group_equiv_one : B := f one - - definition group_equiv_inv (b : B) : B := f (f⁻¹ᶠ b)⁻¹ - - local infix * := my.group_equiv_mul f - local postfix ^ := my.group_equiv_inv f - local notation 1 := my.group_equiv_one f - - theorem group_equiv_mul_assoc (b₁ b₂ b₃ : B) : (b₁ * b₂) * b₃ = b₁ * (b₂ * b₃) := - by rewrite [↑group_equiv_mul, +left_inv f, mul.assoc] - - theorem group_equiv_one_mul (b : B) : 1 * b = b := - by rewrite [↑group_equiv_mul, ↑group_equiv_one, left_inv f, one_mul, right_inv f] - - theorem group_equiv_mul_one (b : B) : b * 1 = b := - by rewrite [↑group_equiv_mul, ↑group_equiv_one, left_inv f, mul_one, right_inv f] - - theorem group_equiv_mul_left_inv (b : B) : b^ * b = 1 := - by rewrite [↑group_equiv_mul, ↑group_equiv_one, ↑group_equiv_inv, - +left_inv f, mul.left_inv] - - definition group_equiv_closed : group B := - ⦃group, - mul := group_equiv_mul, - mul_assoc := group_equiv_mul_assoc, - one := group_equiv_one, - one_mul := group_equiv_one_mul, - mul_one := group_equiv_mul_one, - inv := group_equiv_inv, - mul_left_inv := group_equiv_mul_left_inv, - is_set_carrier := is_trunc_equiv_closed 0 f⦄ - - end - -end my open my - -namespace eq - - local attribute mul [unfold 2] - definition homotopy_group_homomorphism [constructor] (n : ℕ) {A B : Type*} (f : A →* B) - : πg[n+1] A →g πg[n+1] B := - begin - fconstructor, - { exact phomotopy_group_functor (n+1) f}, - { intro g, - refine @trunc.rec _ _ _ (λx, !is_trunc_eq) _, intro h, - refine @trunc.rec _ _ _ (λx, !is_trunc_eq) _ g, clear g, intro g, - rewrite [tr_mul, ▸*], - apply ap tr, apply apn_con} - end - - notation `π→g[`:95 n:0 ` +1] `:0 f:95 := homotopy_group_homomorphism n f - -end eq diff --git a/homotopy/sec86.hlean b/homotopy/sec86.hlean deleted file mode 100644 index 914b592..0000000 --- a/homotopy/sec86.hlean +++ /dev/null @@ -1,425 +0,0 @@ -/- -Copyright (c) 2016 Floris van Doorn. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Floris van Doorn --/ - -import homotopy.wedge homotopy.homotopy_group homotopy.circle .LES_applications - -open eq is_conn is_trunc pointed susp nat pi equiv is_equiv trunc fiber trunc_index - - -- definition iterated_loop_ptrunc_pequiv_con' (n : ℕ₋₂) (k : ℕ) (A : Type*) - -- (p q : Ω[k](ptrunc (n+k) (Ω A))) : - -- iterated_loop_ptrunc_pequiv n k (Ω A) (loop_mul trunc_concat p q) = - -- trunc_functor2 (loop_mul concat) (iterated_loop_ptrunc_pequiv n k (Ω A) p) - -- (iterated_loop_ptrunc_pequiv n k (Ω A) q) := - -- begin - -- revert n p q, induction k with k IH: intro n p q, - -- { reflexivity}, - -- { exact sorry} - -- end - - theorem elim_type_merid_inv {A : Type} (PN : Type) (PS : Type) (Pm : A → PN ≃ PS) - (a : A) : transport (susp.elim_type PN PS Pm) (merid a)⁻¹ = to_inv (Pm a) := - by rewrite [tr_eq_cast_ap_fn,↑susp.elim_type,ap_inv,elim_merid]; apply cast_ua_inv_fn - - definition is_conn_trunc (A : Type) (n k : ℕ₋₂) [H : is_conn n A] - : is_conn n (trunc k A) := - begin - apply is_trunc_equiv_closed, apply trunc_trunc_equiv_trunc_trunc - end - - section open sphere sphere.ops - definition psphere_succ [unfold_full] (n : ℕ) : S. (n + 1) = psusp (S. n) := idp - end - -namespace freudenthal section - - /- The Freudenthal Suspension Theorem -/ - parameters {A : Type*} {n : ℕ} [is_conn n A] - - /- - This proof is ported from Agda - This is the 95% version of the Freudenthal Suspension Theorem, which means that we don't - prove that loop_susp_unit : A →* Ω(psusp A) is 2n-connected (if A is n-connected), - but instead we only prove that it induces an equivalence on the first 2n homotopy groups. - -/ - - definition up (a : A) : north = north :> susp A := - loop_susp_unit A a - - definition code_merid : A → ptrunc (n + n) A → ptrunc (n + n) A := - begin - have is_conn n (ptrunc (n + n) A), from !is_conn_trunc, - refine wedge_extension.ext n n (λ x y, ttrunc (n + n) A) _ _ _, - { exact tr}, - { exact id}, - { reflexivity} - end - - definition code_merid_β_left (a : A) : code_merid a pt = tr a := - by apply wedge_extension.β_left - - definition code_merid_β_right (b : ptrunc (n + n) A) : code_merid pt b = b := - by apply wedge_extension.β_right - - definition code_merid_coh : code_merid_β_left pt = code_merid_β_right pt := - begin - symmetry, apply eq_of_inv_con_eq_idp, apply wedge_extension.coh - end - - definition is_equiv_code_merid (a : A) : is_equiv (code_merid a) := - begin - have Πa, is_trunc n.-2.+1 (is_equiv (code_merid a)), - from λa, is_trunc_of_le _ !minus_one_le_succ, - refine is_conn.elim (n.-1) _ _ a, - { esimp, exact homotopy_closed id (homotopy.symm (code_merid_β_right))} - end - - definition code_merid_equiv [constructor] (a : A) : trunc (n + n) A ≃ trunc (n + n) A := - equiv.mk _ (is_equiv_code_merid a) - - definition code_merid_inv_pt (x : trunc (n + n) A) : (code_merid_equiv pt)⁻¹ x = x := - begin - refine ap010 @(is_equiv.inv _) _ x ⬝ _, - { exact homotopy_closed id (homotopy.symm code_merid_β_right)}, - { apply is_conn.elim_β}, - { reflexivity} - end - - definition code [unfold 4] : susp A → Type := - susp.elim_type (trunc (n + n) A) (trunc (n + n) A) code_merid_equiv - - definition is_trunc_code (x : susp A) : is_trunc (n + n) (code x) := - begin - induction x with a: esimp, - { exact _}, - { exact _}, - { apply is_prop.elimo} - end - local attribute is_trunc_code [instance] - - definition decode_north [unfold 4] : code north → trunc (n + n) (north = north :> susp A) := - trunc_functor (n + n) up - - definition decode_north_pt : decode_north (tr pt) = tr idp := - ap tr !con.right_inv - - definition decode_south [unfold 4] : code south → trunc (n + n) (north = south :> susp A) := - trunc_functor (n + n) merid - - definition encode' {x : susp A} (p : north = x) : code x := - transport code p (tr pt) - - definition encode [unfold 5] {x : susp A} (p : trunc (n + n) (north = x)) : code x := - begin - induction p with p, - exact transport code p (tr pt) - end - - theorem encode_decode_north (c : code north) : encode (decode_north c) = c := - begin - have H : Πc, is_trunc (n + n) (encode (decode_north c) = c), from _, - esimp at *, - induction c with a, - rewrite [↑[encode, decode_north, up, code], con_tr, elim_type_merid, ▸*, - code_merid_β_left, elim_type_merid_inv, ▸*, code_merid_inv_pt] - end - - definition decode_coh_f (a : A) : tr (up pt) =[merid a] decode_south (code_merid a (tr pt)) := - begin - refine _ ⬝op ap decode_south (code_merid_β_left a)⁻¹, - apply trunc_pathover, - apply eq_pathover_constant_left_id_right, - apply square_of_eq, - exact whisker_right !con.right_inv (merid a) - end - - definition decode_coh_g (a' : A) : tr (up a') =[merid pt] decode_south (code_merid pt (tr a')) := - begin - refine _ ⬝op ap decode_south (code_merid_β_right (tr a'))⁻¹, - apply trunc_pathover, - apply eq_pathover_constant_left_id_right, - apply square_of_eq, refine !inv_con_cancel_right ⬝ !idp_con⁻¹ - end - - definition decode_coh_lem {A : Type} {a a' : A} (p : a = a') - : whisker_right (con.right_inv p) p = inv_con_cancel_right p p ⬝ (idp_con p)⁻¹ := - by induction p; reflexivity - - theorem decode_coh (a : A) : decode_north =[merid a] decode_south := - begin - apply arrow_pathover_left, intro c, esimp at *, - induction c with a', - rewrite [↑code, elim_type_merid, ▸*], - refine wedge_extension.ext n n _ _ _ _ a a', - { exact decode_coh_f}, - { exact decode_coh_g}, - { clear a a', unfold [decode_coh_f, decode_coh_g], refine ap011 concato_eq _ _, - { refine ap (λp, trunc_pathover (eq_pathover_constant_left_id_right (square_of_eq p))) _, - apply decode_coh_lem}, - { apply ap (λp, ap decode_south p⁻¹), apply code_merid_coh}} - end - - definition decode [unfold 4] {x : susp A} (c : code x) : trunc (n + n) (north = x) := - begin - induction x with a, - { exact decode_north c}, - { exact decode_south c}, - { exact decode_coh a} - end - - theorem decode_encode {x : susp A} (p : trunc (n + n) (north = x)) : decode (encode p) = p := - begin - induction p with p, induction p, esimp, apply decode_north_pt - end - - parameters (A n) - definition equiv' : trunc (n + n) A ≃ trunc (n + n) (Ω (psusp A)) := - equiv.MK decode_north encode decode_encode encode_decode_north - - definition pequiv' : ptrunc (n + n) A ≃* ptrunc (n + n) (Ω (psusp A)) := - pequiv_of_equiv equiv' decode_north_pt - - -- We don't prove this: - -- theorem freudenthal_suspension : is_conn_fun (n+n) (loop_susp_unit A) := - -end end freudenthal - -open algebra -definition freudenthal_pequiv (A : Type*) {n k : ℕ} [is_conn n A] (H : k ≤ 2 * n) - : ptrunc k A ≃* ptrunc k (Ω (psusp A)) := -have H' : k ≤[ℕ₋₂] n + n, - by rewrite [mul.comm at H, -algebra.zero_add n at {1}]; exact of_nat_le_of_nat H, -ptrunc_pequiv_ptrunc_of_le H' (freudenthal.pequiv' A n) - -definition freudenthal_equiv {A : Type*} {n k : ℕ} [is_conn n A] (H : k ≤ 2 * n) - : trunc k A ≃ trunc k (Ω (psusp A)) := -freudenthal_pequiv A H - -namespace sphere - open ops algebra pointed function - - -- replace with definition in algebra.homotopy_group - definition phomotopy_group_succ_in2 (A : Type*) (n : ℕ) : π*[n + 1] A = π*[n] Ω A :> Type* := - ap (ptrunc 0) (loop_space_succ_eq_in A n) - - definition stability_pequiv_helper (k n : ℕ) (H : k + 2 ≤ 2 * n) - : ptrunc k (Ω(psusp (S. n))) ≃* ptrunc k (S. n) := - begin - have H' : k ≤ 2 * pred n, - begin - rewrite [mul_pred_right], change pred (pred (k + 2)) ≤ pred (pred (2 * n)), - apply pred_le_pred, apply pred_le_pred, exact H - end, - have is_conn (of_nat (pred n)) (S. n), - begin - cases n with n, - { exfalso, exact not_succ_le_zero _ H}, - { esimp, apply is_conn_psphere} - end, - symmetry, exact freudenthal_pequiv (S. n) H' - end - - definition stability_pequiv (k n : ℕ) (H : k + 2 ≤ 2 * n) : π*[k + 1] (S. (n+1)) ≃* π*[k] (S. n) := - begin - refine pequiv_of_eq (phomotopy_group_succ_in2 (S. (n+1)) k) ⬝e* _, - rewrite psphere_succ, - refine !phomotopy_group_pequiv_loop_ptrunc ⬝e* _, - refine loopn_pequiv_loopn k (stability_pequiv_helper k n H) ⬝e* _, - exact !phomotopy_group_pequiv_loop_ptrunc⁻¹ᵉ*, - end - - -- change some "+1"'s intro succ's to avoid this definition (or vice versa) - definition group_homotopy_group2 [instance] (k : ℕ) (A : Type*) : - group (carrier (ptrunctype.to_pType (π*[k + 1] A))) := - group_homotopy_group k A - - definition loop_pequiv_loop_con {A B : Type*} (f : A ≃* B) (p q : Ω A) - : loop_pequiv_loop f (p ⬝ q) = loop_pequiv_loop f p ⬝ loop_pequiv_loop f q := - loopn_pequiv_loopn_con 0 f p q - - definition iterated_loop_ptrunc_pequiv_con {n : ℕ₋₂} {k : ℕ} {A : Type*} - (p q : Ω[succ k] (ptrunc (n+succ k) A)) : - iterated_loop_ptrunc_pequiv n (succ k) A (p ⬝ q) = - trunc_concat (iterated_loop_ptrunc_pequiv n (succ k) A p) - (iterated_loop_ptrunc_pequiv n (succ k) A q) := - begin - refine _ ⬝ loop_ptrunc_pequiv_con _ _, - exact ap !loop_ptrunc_pequiv !loop_pequiv_loop_con - end - - theorem inv_respect_binary_operation {A B : Type} (f : A ≃ B) (mA : A → A → A) (mB : B → B → B) - (p : Πa₁ a₂, f (mA a₁ a₂) = mB (f a₁) (f a₂)) (b₁ b₂ : B) : - f⁻¹ (mB b₁ b₂) = mA (f⁻¹ b₁) (f⁻¹ b₂) := - begin - refine is_equiv_rect' f⁻¹ _ _ b₁, refine is_equiv_rect' f⁻¹ _ _ b₂, - intros a₂ a₁, apply inv_eq_of_eq, symmetry, exact p a₁ a₂ - end - - definition iterated_loop_ptrunc_pequiv_inv_con {n : ℕ₋₂} {k : ℕ} {A : Type*} - (p q : ptrunc n (Ω[succ k] A)) : - (iterated_loop_ptrunc_pequiv n (succ k) A)⁻¹ᵉ* (trunc_concat p q) = - (iterated_loop_ptrunc_pequiv n (succ k) A)⁻¹ᵉ* p ⬝ - (iterated_loop_ptrunc_pequiv n (succ k) A)⁻¹ᵉ* q := - inv_respect_binary_operation (iterated_loop_ptrunc_pequiv n (succ k) A) concat trunc_concat - (@iterated_loop_ptrunc_pequiv_con n k A) p q - - definition phomotopy_group_pequiv_loop_ptrunc_con {k : ℕ} {A : Type*} (p q : πg[k +1] A) : - phomotopy_group_pequiv_loop_ptrunc (succ k) A (p * q) = - phomotopy_group_pequiv_loop_ptrunc (succ k) A p ⬝ - phomotopy_group_pequiv_loop_ptrunc (succ k) A q := - begin - refine _ ⬝ !loopn_pequiv_loopn_con, - exact ap (loopn_pequiv_loopn _ _) !iterated_loop_ptrunc_pequiv_inv_con - end - - definition phomotopy_group_pequiv_loop_ptrunc_inv_con {k : ℕ} {A : Type*} - (p q : Ω[succ k] (ptrunc (succ k) A)) : - (phomotopy_group_pequiv_loop_ptrunc (succ k) A)⁻¹ᵉ* (p ⬝ q) = - (phomotopy_group_pequiv_loop_ptrunc (succ k) A)⁻¹ᵉ* p * - (phomotopy_group_pequiv_loop_ptrunc (succ k) A)⁻¹ᵉ* q := - inv_respect_binary_operation (phomotopy_group_pequiv_loop_ptrunc (succ k) A) mul concat - (@phomotopy_group_pequiv_loop_ptrunc_con k A) p q - - definition tcast [constructor] {n : ℕ₋₂} {A B : n-Type*} (p : A = B) : A →* B := - pcast (ap ptrunctype.to_pType p) - - definition tr_mul_tr {n : ℕ} {A : Type*} (p q : Ω[succ n] A) - : tr p *[π[n + 1] A] tr q = tr (p ⬝ q) := - idp - - -- use this in proof for ghomotopy_group_succ_in - definition phomotopy_group_succ_in2_con {A : Type*} {n : ℕ} (g h : πg[succ n +1] A) : - pcast (phomotopy_group_succ_in2 A (succ n)) (g * h) = - pcast (phomotopy_group_succ_in2 A (succ n)) g * pcast (phomotopy_group_succ_in2 A (succ n)) h := - begin - induction g with p, induction h with q, esimp, - rewrite [-+ tr_eq_cast_ap, ↑phomotopy_group_succ_in2, -+ tr_compose], - refine ap (transport _ _) !tr_mul_tr ⬝ _, - rewrite [+ trunc_transport], - apply ap tr, apply loop_space_succ_eq_in_concat, - end - - definition stability_eq (k n : ℕ) (H : k + 3 ≤ 2 * n) : πg[k+1 +1] (S. (n+1)) = πg[k+1] (S. n) := - begin - fapply Group_eq, - { exact equiv_of_pequiv (stability_pequiv (succ k) n H)}, - { intro g h, - refine _ ⬝ !phomotopy_group_pequiv_loop_ptrunc_inv_con, - apply ap !phomotopy_group_pequiv_loop_ptrunc⁻¹ᵉ*, - refine ap (loopn_pequiv_loopn _ _) _ ⬝ !loopn_pequiv_loopn_con, - refine ap !phomotopy_group_pequiv_loop_ptrunc _ ⬝ !phomotopy_group_pequiv_loop_ptrunc_con, - apply phomotopy_group_succ_in2_con - } - end - - theorem mul_two {A : Type} [semiring A] (a : A) : a * 2 = a + a := - by rewrite [-one_add_one_eq_two, left_distrib, +mul_one] - - theorem two_mul {A : Type} [semiring A] (a : A) : 2 * a = a + a := - by rewrite [-one_add_one_eq_two, right_distrib, +one_mul] - - definition two_le_succ_succ (n : ℕ) : 2 ≤ succ (succ n) := - nat.succ_le_succ (nat.succ_le_succ !zero_le) - - open int circle hopf - definition πnSn (n : ℕ) : πg[n+1] (S. (succ n)) = gℤ := - begin - cases n with n IH, - { exact fundamental_group_of_circle}, - { induction n with n IH, - { exact π2S2}, - { refine _ ⬝ IH, apply stability_eq, - calc - succ n + 3 = succ (succ n) + 2 : !succ_add⁻¹ - ... ≤ succ (succ n) + (succ (succ n)) : add_le_add_left !two_le_succ_succ - ... = 2 * (succ (succ n)) : !two_mul⁻¹ }} - end - - - attribute group_integers [constructor] - theorem not_is_trunc_sphere (n : ℕ) : ¬is_trunc n (S. (succ n)) := - begin - intro H, - note H2 := trivial_homotopy_group_of_is_trunc (S. (succ n)) n n !le.refl, - rewrite [πnSn at H2, ▸* at H2], - have H3 : (0 : ℤ) ≠ (1 : ℤ), from dec_star, - apply H3, - apply is_prop.elim, - end - - definition transport11 {A B : Type} (P : A → B → Type) {a a' : A} {b b' : B} - (p : a = a') (q : b = b') (z : P a b) : P a' b' := - transport (P a') q (p ▸ z) - - section - open sphere_index - - definition add_plus_one_minus_one (n : ℕ₋₁) : n +1+ -1 = n := idp - definition add_plus_one_succ (n m : ℕ₋₁) : n +1+ (m.+1) = (n +1+ m).+1 := idp - definition minus_one_add_plus_one (n : ℕ₋₁) : -1 +1+ n = n := - begin induction n with n IH, reflexivity, exact ap succ IH end - definition succ_add_plus_one (n m : ℕ₋₁) : (n.+1) +1+ m = (n +1+ m).+1 := - begin induction m with m IH, reflexivity, exact ap succ IH end - - definition nat_of_sphere_index : ℕ₋₁ → ℕ := - sphere_index.rec 0 (λx, succ) - - definition trunc_index_of_nat_of_sphere_index (n : ℕ₋₁) - : trunc_index.of_nat (nat_of_sphere_index n) = (of_sphere_index n).+1 := - begin - induction n with n IH, - { reflexivity}, - { exact ap succ IH} - end - - definition sphere_index_of_nat_of_sphere_index (n : ℕ₋₁) - : sphere_index.of_nat (nat_of_sphere_index n) = n.+1 := - begin - induction n with n IH, - { reflexivity}, - { exact ap succ IH} - end - - definition of_sphere_index_succ (n : ℕ₋₁) - : of_sphere_index (n.+1) = (of_sphere_index n).+1 := - begin - induction n with n IH, - { reflexivity}, - { exact ap succ IH} - end - - definition sphere_index.of_nat_succ (n : ℕ) - : sphere_index.of_nat (succ n) = (sphere_index.of_nat n).+1 := - begin - induction n with n IH, - { reflexivity}, - { exact ap succ IH} - end - - definition nat_of_sphere_index_succ (n : ℕ₋₁) - : nat_of_sphere_index (n.+1) = succ (nat_of_sphere_index n) := - begin - induction n with n IH, - { reflexivity}, - { exact ap succ IH} - end - - definition not_is_trunc_sphere' (n : ℕ₋₁) : ¬is_trunc n (S (n.+1)) := - begin - cases n with n, - { esimp [sphere.ops.S, sphere], intro H, - have H2 : is_prop bool, from @(is_trunc_equiv_closed -1 sphere_equiv_bool) H, - have H3 : bool.tt ≠ bool.ff, from dec_star, apply H3, apply is_prop.elim}, - { intro H, apply not_is_trunc_sphere (nat_of_sphere_index n), - rewrite [▸*, trunc_index_of_nat_of_sphere_index, -nat_of_sphere_index_succ, - sphere_index_of_nat_of_sphere_index], - exact H} - end - end - - definition π3S2 : πg[2+1] (S. 2) = gℤ := - (πnS3_eq_πnS2 0)⁻¹ ⬝ πnSn 2 - -end sphere diff --git a/homotopy/spectrum.hlean b/homotopy/spectrum.hlean index 5408f80..0197517 100644 --- a/homotopy/spectrum.hlean +++ b/homotopy/spectrum.hlean @@ -5,7 +5,7 @@ Authors: Michael Shulman -/ -import types.int types.pointed types.trunc homotopy.susp algebra.homotopy_group .chain_complex cubical +import types.int types.pointed types.trunc homotopy.susp algebra.homotopy_group homotopy.chain_complex cubical open eq nat int susp pointed pmap sigma is_equiv equiv fiber algebra trunc trunc_index pi /----------------------------------------- @@ -109,7 +109,7 @@ namespace pointed definition pfiber_loop_space {A B : Type*} (f : A →* B) : pfiber (Ω→ f) ≃* Ω (pfiber f) := pequiv_of_equiv - (calc pfiber (Ω→ f) ≃ Σ(p : Point A = Point A), ap1 f p = rfl : (fiber.sigma_char (ap1 f) (Point Ω B)) + (calc pfiber (Ω→ f) ≃ Σ(p : Point A = Point A), ap1 f p = rfl : (fiber.sigma_char (ap1 f) (Point (Ω B))) ... ≃ Σ(p : Point A = Point A), (respect_pt f) = ap f p ⬝ (respect_pt f) : (sigma_equiv_sigma_right (λp, calc (ap1 f p = rfl) ≃ !respect_pt⁻¹ ⬝ (ap f p ⬝ !respect_pt) = rfl : equiv_eq_closed_left _ (con.assoc _ _ _) ... ≃ ap f p ⬝ (respect_pt f) = (respect_pt f) : eq_equiv_inv_con_eq_idp @@ -137,15 +137,15 @@ namespace pointed definition pequiv_postcompose {A B B' : Type*} (f : A →* B) (g : B ≃* B') : pfiber (g ∘* f) ≃* pfiber f := begin fapply pequiv_of_equiv, esimp, - refine ((transport_fiber_equiv (g ∘* f) (respect_pt g)⁻¹) ⬝e (@fiber.equiv_postcompose A B f (Point B) B' g _)), - esimp, apply (ap (fiber.mk (Point A))), rewrite con.assoc, apply inv_con_eq_of_eq_con, + refine transport_fiber_equiv (g ∘* f) (respect_pt g)⁻¹ ⬝e fiber.equiv_postcompose f g (Point B), + esimp, apply (ap (fiber.mk (Point A))), refine !con.assoc ⬝ _, apply inv_con_eq_of_eq_con, rewrite [con.assoc, con.right_inv, con_idp, -ap_compose'], apply ap_con_eq_con end definition pequiv_precompose {A A' B : Type*} (f : A →* B) (g : A' ≃* A) : pfiber (f ∘* g) ≃* pfiber f := begin fapply pequiv_of_equiv, esimp, - refine (@fiber.equiv_precompose A B f (Point B) A' g _), + refine fiber.equiv_precompose f g (Point B), esimp, apply (eq_of_fn_eq_fn (fiber.sigma_char _ _)), fapply sigma_eq: esimp, { apply respect_pt g }, { apply pathover_eq_Fl' } @@ -291,7 +291,7 @@ namespace spectrum definition sid {N : succ_str} (E : gen_spectrum N) : E →ₛ E := smap.mk (λn, pid (E n)) (λn, calc glue E n ∘* pid (E n) ~* glue E n : comp_pid - ... ~* pid Ω(E (S n)) ∘* glue E n : pid_comp + ... ~* pid (Ω(E (S n))) ∘* glue E n : pid_comp ... ~* Ω→(pid (E (S n))) ∘* glue E n : pwhisker_right (glue E n) ap1_id⁻¹*) definition scompose {N : succ_str} {X Y Z : gen_prespectrum N} (g : Y →ₛ Z) (f : X →ₛ Y) : X →ₛ Z :=