diff --git a/hott/algebra/algebra.md b/hott/algebra/algebra.md index 03d2a88b9..355312659 100644 --- a/hott/algebra/algebra.md +++ b/hott/algebra/algebra.md @@ -16,9 +16,10 @@ The following files are [ported](../port.md) from the standard library. If anyth * [ordered_field](ordered_field.hlean) * [bundled](bundled.hlean) : bundled versions of the algebraic structures -Files which are HoTT specific: +Files which are not ported from the standard library: * [hott](hott.hlean) : Basic theorems about the algebraic hierarchy specific to HoTT +* [group_theory](group_theory.hlean) : Basic theorems about group homomorphisms and isomorphisms * [trunc_group](trunc_group.hlean) : truncate an infinity-group to a group * [homotopy_group](homotopy_group.hlean) : homotopy groups of a pointed type * [e_closure](e_closure.hlean) : the type of words formed by a relation diff --git a/hott/algebra/binary.hlean b/hott/algebra/binary.hlean index 18a5525cd..d11673f16 100644 --- a/hott/algebra/binary.hlean +++ b/hott/algebra/binary.hlean @@ -88,30 +88,30 @@ end binary open eq namespace is_equiv definition inv_preserve_binary {A B : Type} (f : A → B) [H : is_equiv f] - (mA : A → A → A) (mB : B → B → B) (H : Π(a a' : A), mB (f a) (f a') = f (mA a a')) + (mA : A → A → A) (mB : B → B → B) (H : Π(a a' : A), f (mA a a') = mB (f a) (f a')) (b b' : B) : f⁻¹ (mB b b') = mA (f⁻¹ b) (f⁻¹ b') := begin - have H2 : f⁻¹ (mB (f (f⁻¹ b)) (f (f⁻¹ b'))) = f⁻¹ (f (mA (f⁻¹ b) (f⁻¹ b'))), from ap f⁻¹ !H, + have H2 : f⁻¹ (mB (f (f⁻¹ b)) (f (f⁻¹ b'))) = f⁻¹ (f (mA (f⁻¹ b) (f⁻¹ b'))), from ap f⁻¹ !H⁻¹, rewrite [+right_inv f at H2,left_inv f at H2,▸* at H2,H2] end definition preserve_binary_of_inv_preserve {A B : Type} (f : A → B) [H : is_equiv f] - (mA : A → A → A) (mB : B → B → B) (H : Π(b b' : B), mA (f⁻¹ b) (f⁻¹ b') = f⁻¹ (mB b b')) + (mA : A → A → A) (mB : B → B → B) (H : Π(b b' : B), f⁻¹ (mB b b') = mA (f⁻¹ b) (f⁻¹ b')) (a a' : A) : f (mA a a') = mB (f a) (f a') := begin - have H2 : f (mA (f⁻¹ (f a)) (f⁻¹ (f a'))) = f (f⁻¹ (mB (f a) (f a'))), from ap f !H, + have H2 : f (mA (f⁻¹ (f a)) (f⁻¹ (f a'))) = f (f⁻¹ (mB (f a) (f a'))), from ap f !H⁻¹, rewrite [right_inv f at H2,+left_inv f at H2,▸* at H2,H2] end end is_equiv namespace equiv open is_equiv definition inv_preserve_binary {A B : Type} (f : A ≃ B) - (mA : A → A → A) (mB : B → B → B) (H : Π(a a' : A), mB (f a) (f a') = f (mA a a')) + (mA : A → A → A) (mB : B → B → B) (H : Π(a a' : A), f (mA a a') = mB (f a) (f a')) (b b' : B) : f⁻¹ (mB b b') = mA (f⁻¹ b) (f⁻¹ b') := inv_preserve_binary f mA mB H b b' definition preserve_binary_of_inv_preserve {A B : Type} (f : A ≃ B) - (mA : A → A → A) (mB : B → B → B) (H : Π(b b' : B), mA (f⁻¹ b) (f⁻¹ b') = f⁻¹ (mB b b')) + (mA : A → A → A) (mB : B → B → B) (H : Π(b b' : B), f⁻¹ (mB b b') = mA (f⁻¹ b) (f⁻¹ b')) (a a' : A) : f (mA a a') = mB (f a) (f a') := preserve_binary_of_inv_preserve f mA mB H a a' end equiv diff --git a/hott/algebra/group_theory.hlean b/hott/algebra/group_theory.hlean index cd742a1de..4f8bd88c8 100644 --- a/hott/algebra/group_theory.hlean +++ b/hott/algebra/group_theory.hlean @@ -144,6 +144,10 @@ namespace group definition equiv_of_isomorphism [constructor] (φ : G₁ ≃g G₂) : G₁ ≃ G₂ := equiv.mk φ _ + definition pequiv_of_isomorphism [constructor] (φ : G₁ ≃g G₂) : + pType_of_Group G₁ ≃* pType_of_Group G₂ := + pequiv.mk φ _ (respect_one φ) + definition isomorphism_of_equiv [constructor] (φ : G₁ ≃ G₂) (p : Πg₁ g₂, φ (g₁ * g₂) = φ g₁ * φ g₂) : G₁ ≃g G₂ := isomorphism.mk (homomorphism.mk φ p) !to_is_equiv @@ -171,8 +175,18 @@ namespace group definition isomorphism.trans [trans] [constructor] (φ : G₁ ≃g G₂) (ψ : G₂ ≃g G₃) : G₁ ≃g G₃ := isomorphism.mk (ψ ∘g φ) !is_equiv_compose + definition isomorphism.eq_trans [trans] [constructor] + {G₁ G₂ G₃ : Group} (φ : G₁ = G₂) (ψ : G₂ ≃g G₃) : G₁ ≃g G₃ := + proof isomorphism.trans (isomorphism_of_eq φ) ψ qed + + definition isomorphism.trans_eq [trans] [constructor] + {G₁ G₂ G₃ : Group} (φ : G₁ ≃g G₂) (ψ : G₂ = G₃) : G₁ ≃g G₃ := + isomorphism.trans φ (isomorphism_of_eq ψ) + postfix `⁻¹ᵍ`:(max + 1) := isomorphism.symm infixl ` ⬝g `:75 := isomorphism.trans + infixl ` ⬝gp `:75 := isomorphism.trans_eq + infixl ` ⬝pg `:75 := isomorphism.eq_trans -- TODO -- definition Group_univalence (G₁ G₂ : Group) : (G₁ ≃g G₂) ≃ (G₁ = G₂) := @@ -257,4 +271,31 @@ namespace group definition trivial_group_of_is_contr' (G : Group) [H : is_contr G] : G = G0 := eq_of_isomorphism (trivial_group_of_is_contr G) + /- + A group where the point in the pointed type corresponds with 1 in the group. + We need this structure when we are given a pointed type, and want to say that there is a group + structure on it which is compatible with the point. This is used in chain complexes. + -/ + 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 + end group diff --git a/hott/algebra/homotopy_group.hlean b/hott/algebra/homotopy_group.hlean index 067191599..62567143a 100644 --- a/hott/algebra/homotopy_group.hlean +++ b/hott/algebra/homotopy_group.hlean @@ -8,8 +8,9 @@ homotopy groups of a pointed space import .trunc_group types.trunc .group_theory -open nat eq pointed trunc is_trunc algebra group function equiv unit +open nat eq pointed trunc is_trunc algebra group function equiv unit is_equiv +-- TODO: consistently make n an argument before A namespace eq definition phomotopy_group [reducible] [constructor] (n : ℕ) (A : Type*) : Set* := @@ -25,6 +26,10 @@ namespace eq : group (π[succ n] A) := trunc_group concat inverse idp con.assoc idp_con con_idp con.left_inv + definition group_homotopy_group2 [instance] (k : ℕ) (A : Type*) : + group (carrier (ptrunctype.to_pType (π*[k + 1] A))) := + group_homotopy_group k A + definition comm_group_homotopy_group [constructor] [reducible] (n : ℕ) (A : Type*) : comm_group (π[succ (succ n)] A) := trunc_comm_group concat inverse idp con.assoc idp_con con_idp con.left_inv eckmann_hilton @@ -43,7 +48,7 @@ namespace eq notation `πg[`:95 n:0 ` +1] `:0 A:95 := ghomotopy_group n A notation `πag[`:95 n:0 ` +2] `:0 A:95 := cghomotopy_group n A - notation `π₁` := fundamental_group + notation `π₁` := fundamental_group -- should this be notation for the group or pointed type? definition tr_mul_tr {n : ℕ} {A : Type*} (p q : Ω[n + 1] A) : tr p *[πg[n+1] A] tr q = tr (p ⬝ q) := @@ -64,6 +69,15 @@ namespace eq exact loopn_pequiv_loopn k (pequiv_of_eq begin rewrite [trunc_index.zero_add] end) end + definition phomotopy_group_ptrunc [constructor] (k : ℕ) (A : Type*) : + π*[k] (ptrunc k A) ≃* π*[k] A := + calc + π*[k] (ptrunc k A) ≃* Ω[k] (ptrunc k (ptrunc k A)) + : phomotopy_group_pequiv_loop_ptrunc k (ptrunc k A) + ... ≃* Ω[k] (ptrunc k A) + : loopn_pequiv_loopn k (ptrunc_pequiv k (ptrunc k A) _) + ... ≃* π*[k] A : (phomotopy_group_pequiv_loop_ptrunc k A)⁻¹ᵉ* + theorem trivial_homotopy_of_is_set (A : Type*) [H : is_set A] (n : ℕ) : πg[n+1] A ≃g G0 := begin apply trivial_group_of_is_contr, @@ -74,11 +88,23 @@ namespace eq definition phomotopy_group_succ_out (A : Type*) (n : ℕ) : π*[n + 1] A = π₁ Ω[n] A := idp - definition phomotopy_group_succ_in (A : Type*) (n : ℕ) : π*[n + 1] A = π*[n] Ω A := + definition phomotopy_group_succ_in (A : Type*) (n : ℕ) : π*[n + 1] A = π*[n] (Ω A) :> Type* := ap (ptrunc 0) (loop_space_succ_eq_in A n) definition ghomotopy_group_succ_out (A : Type*) (n : ℕ) : πg[n +1] A = π₁ Ω[n] A := idp + definition phomotopy_group_succ_in_con {A : Type*} {n : ℕ} (g h : πg[succ n +1] A) : + pcast (phomotopy_group_succ_in A (succ n)) (g * h) = + pcast (phomotopy_group_succ_in A (succ n)) g * + pcast (phomotopy_group_succ_in A (succ n)) h := + begin + induction g with p, induction h with q, esimp, + rewrite [-+ tr_eq_cast_ap, ↑phomotopy_group_succ_in, -+ tr_compose], + refine ap (transport _ _) !tr_mul_tr' ⬝ _, + rewrite [+ trunc_transport], + apply ap tr, apply loop_space_succ_eq_in_concat, + end + definition ghomotopy_group_succ_in (A : Type*) (n : ℕ) : πg[succ n +1] A ≃g πg[n +1] Ω A := begin fapply isomorphism_of_equiv, @@ -98,6 +124,36 @@ namespace eq notation `π→*[`:95 n:0 `] `:0 := phomotopy_group_functor n notation `π→[`:95 n:0 `] `:0 := homotopy_group_functor n + 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) + + 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 + + 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 + + definition phomotopy_group_functor_succ_phomotopy_in (n : ℕ) {A B : Type*} (f : A →* B) : + pcast (phomotopy_group_succ_in B n) ∘* π→*[n + 1] f ~* + π→*[n] (Ω→ f) ∘* pcast (phomotopy_group_succ_in A n) := + begin + refine pwhisker_right _ (pcast_ptrunc 0 (loop_space_succ_eq_in B n)) ⬝* _, + refine _ ⬝* pwhisker_left _ (pcast_ptrunc 0 (loop_space_succ_eq_in A n))⁻¹*, + refine !ptrunc_functor_pcompose⁻¹* ⬝* _ ⬝* !ptrunc_functor_pcompose, + exact ptrunc_functor_phomotopy 0 (apn_succ_phomotopy_in n f) + end + + definition is_equiv_phomotopy_group_functor_ap1 (n : ℕ) {A B : Type*} (f : A →* B) + [is_equiv (π→*[n + 1] f)] : is_equiv (π→*[n] (Ω→ f)) := + have is_equiv (pcast (phomotopy_group_succ_in B n) ∘* π→*[n + 1] f), + begin apply @(is_equiv_compose (π→*[n + 1] f) _) end, + have is_equiv (π→*[n] (Ω→ f) ∘ pcast (phomotopy_group_succ_in A n)), + from is_equiv.homotopy_closed _ (phomotopy_group_functor_succ_phomotopy_in n f), + is_equiv.cancel_right (pcast (phomotopy_group_succ_in A n)) _ + definition tinverse [constructor] {X : Type*} : π*[1] X →* π*[1] X := ptrunc_functor 0 pinverse @@ -156,6 +212,36 @@ namespace eq isomorphism_of_eq (ap (λx, πg[x+1] A) (p⁻¹ ⬝ add.comm n k)) ⬝g trivial_homotopy_add_of_is_set_loop_space k H2 + 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_preserve_binary (phomotopy_group_pequiv_loop_ptrunc (succ k) A) mul concat + (@phomotopy_group_pequiv_loop_ptrunc_con k A) p q + + definition ghomotopy_group_ptrunc [constructor] (k : ℕ) (A : Type*) : + πg[k+1] (ptrunc (k+1) A) ≃g πg[k+1] A := + begin + fapply isomorphism_of_equiv, + { exact phomotopy_group_ptrunc (k+1) A}, + { intro g₁ g₂, esimp, + refine _ ⬝ !phomotopy_group_pequiv_loop_ptrunc_inv_con, + apply ap ((phomotopy_group_pequiv_loop_ptrunc (k+1) A)⁻¹ᵉ*), + refine _ ⬝ !loopn_pequiv_loopn_con , + apply ap (loopn_pequiv_loopn (k+1) _), + apply phomotopy_group_pequiv_loop_ptrunc_con} + end + /- some homomorphisms -/ definition is_homomorphism_cast_loop_space_succ_eq_in {A : Type*} (n : ℕ) : diff --git a/hott/function.hlean b/hott/function.hlean index 3dbfac836..48ccbe42d 100644 --- a/hott/function.hlean +++ b/hott/function.hlean @@ -13,9 +13,22 @@ open equiv sigma sigma.ops eq trunc is_trunc pi is_equiv fiber prod variables {A B : Type} (f : A → B) {b : B} +/- the image of a map is the (-1)-truncated fiber -/ +definition image' [constructor] (f : A → B) (b : B) : Type := ∥ fiber f b ∥ +definition is_prop_image' [instance] (f : A → B) (b : B) : is_prop (image' f b) := !is_trunc_trunc +definition image [constructor] (f : A → B) (b : B) : Prop := Prop.mk (image' f b) _ + +definition image.mk [constructor] {f : A → B} {b : B} (a : A) (p : f a = b) + : image f b := +tr (fiber.mk a p) + +protected definition image.rec [unfold 8] [recursor 8] {f : A → B} {b : B} {P : image' f b → Type} + [H : Πv, is_prop (P v)] (H : Π(a : A) (p : f a = b), P (image.mk a p)) (v : image' f b) : P v := +begin unfold [image'] at *, induction v with v, induction v with a p, exact H a p end + definition is_embedding [class] (f : A → B) := Π(a a' : A), is_equiv (ap f : a = a' → f a = f a') -definition is_surjective [class] (f : A → B) := Π(b : B), ∥ fiber f b ∥ +definition is_surjective [class] (f : A → B) := Π(b : B), image f b definition is_split_surjective [class] (f : A → B) := Π(b : B), fiber f b @@ -114,13 +127,13 @@ namespace function λb, tr (H b) definition is_prop_is_surjective [instance] : is_prop (is_surjective f) := - by unfold is_surjective; exact _ + begin unfold is_surjective, exact _ end definition is_surjective_cancel_right {A B C : Type} (g : B → C) (f : A → B) [H : is_surjective (g ∘ f)] : is_surjective g := begin intro c, - induction H c with v, induction v with a p, + induction H c with a p, exact tr (fiber.mk (f a) p) end diff --git a/hott/hit/groupoid_quotient.hlean b/hott/hit/groupoid_quotient.hlean new file mode 100644 index 000000000..b22bf2cc0 --- /dev/null +++ b/hott/hit/groupoid_quotient.hlean @@ -0,0 +1,245 @@ +/- +Copyright (c) 2015-16 Floris van Doorn. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Authors: Floris van Doorn + +The groupoid quotient. This is a 1-type which path spaces is the same as the morphisms +a given groupoid. We define it as the 1-truncation of a two quotient. +-/ + +import algebra.category.groupoid .two_quotient homotopy.connectedness + algebra.group_theory + +open trunc_two_quotient eq bool unit relation category e_closure iso is_trunc trunc equiv is_equiv + group + +namespace groupoid_quotient +section + parameter (G : Groupoid) + + inductive groupoid_quotient_R : G → G → Type := + | Rmk : Π{a b : G} (f : a ⟶ b), groupoid_quotient_R a b + + open groupoid_quotient_R + local abbreviation R := groupoid_quotient_R + + inductive groupoid_quotient_Q : Π⦃x y : G⦄, + e_closure groupoid_quotient_R x y → e_closure groupoid_quotient_R x y → Type := + | Qconcat : Π{a b c : G} (g : b ⟶ c) (f : a ⟶ b), + groupoid_quotient_Q [Rmk (g ∘ f)] ([Rmk f] ⬝r [Rmk g]) + + open groupoid_quotient_Q + local abbreviation Q := groupoid_quotient_Q + + definition groupoid_quotient := trunc_two_quotient 1 R Q + + local attribute groupoid_quotient [reducible] + definition is_trunc_groupoid_quotient [instance] : is_trunc 1 groupoid_quotient := _ + + parameter {G} + variables {a b c : G} + definition elt (a : G) : groupoid_quotient := incl0 a + definition pth (f : a ⟶ b) : elt a = elt b := incl1 (Rmk f) + definition resp_comp (g : b ⟶ c) (f : a ⟶ b) : pth (g ∘ f) = pth f ⬝ pth g := incl2 (Qconcat g f) + definition resp_id (a : G) : pth (ID a) = idp := + begin + apply cancel_right (pth (id)), refine _ ⬝ !idp_con⁻¹, + refine !resp_comp⁻¹ ⬝ _, + exact ap pth !id_id, + end + + definition resp_inv (f : a ⟶ b) : pth (f⁻¹) = (pth f)⁻¹ := + begin + apply eq_inv_of_con_eq_idp', + refine !resp_comp⁻¹ ⬝ _, + refine ap pth !right_inverse ⬝ _, + apply resp_id + end + + protected definition rec {P : groupoid_quotient → Type} [Πx, is_trunc 1 (P x)] + (Pe : Πg, P (elt g)) (Pp : Π⦃a b⦄ (f : a ⟶ b), Pe a =[pth f] Pe b) + (Pcomp : Π⦃a b c⦄ (g : b ⟶ c) (f : a ⟶ b), + change_path (resp_comp g f) (Pp (g ∘ f)) = Pp f ⬝o Pp g) + (x : groupoid_quotient) : P x := + begin + induction x, + { apply Pe}, + { induction s with a b f, apply Pp}, + { induction q with a b c g f, + apply Pcomp} + end + + protected definition rec_on {P : groupoid_quotient → Type} [Πx, is_trunc 1 (P x)] + (x : groupoid_quotient) + (Pe : Πg, P (elt g)) (Pp : Π⦃a b⦄ (f : a ⟶ b), Pe a =[pth f] Pe b) + (Pcomp : Π⦃a b c⦄ (g : b ⟶ c) (f : a ⟶ b), + change_path (resp_comp g f) (Pp (g ∘ f)) = Pp f ⬝o Pp g) : P x := + rec Pe Pp Pcomp x + + protected definition set_rec {P : groupoid_quotient → Type} [Πx, is_set (P x)] + (Pe : Πg, P (elt g)) (Pp : Π⦃a b⦄ (f : a ⟶ b), Pe a =[pth f] Pe b) + (x : groupoid_quotient) : P x := + rec Pe Pp !center x + + protected definition prop_rec {P : groupoid_quotient → Type} [Πx, is_prop (P x)] + (Pe : Πg, P (elt g)) (x : groupoid_quotient) : P x := + rec Pe !center !center x + + definition rec_pth {P : groupoid_quotient → Type} [Πx, is_trunc 1 (P x)] + {Pe : Πg, P (elt g)} {Pp : Π⦃a b⦄ (f : a ⟶ b), Pe a =[pth f] Pe b} + (Pcomp : Π⦃a b c⦄ (g : b ⟶ c) (f : a ⟶ b), + change_path (resp_comp g f) (Pp (g ∘ f)) = Pp f ⬝o Pp g) + {a b : G} (f : a ⟶ b) : apd (rec Pe Pp Pcomp) (pth f) = Pp f := + proof !rec_incl1 qed + + protected definition elim {P : Type} [is_trunc 1 P] (Pe : G → P) + (Pp : Π⦃a b⦄ (f : a ⟶ b), Pe a = Pe b) + (Pcomp : Π⦃a b c⦄ (g : b ⟶ c) (f : a ⟶ b), Pp (g ∘ f) = Pp f ⬝ Pp g) + (x : groupoid_quotient) : P := + begin + induction x, + { exact Pe a}, + { induction s with a b f, exact Pp f}, + { induction q with a b c g f, + exact Pcomp g f} + end + + protected definition elim_on [reducible] {P : Type} [is_trunc 1 P] (x : groupoid_quotient) + (Pe : G → P) (Pp : Π⦃a b⦄ (f : a ⟶ b), Pe a = Pe b) + (Pcomp : Π⦃a b c⦄ (g : b ⟶ c) (f : a ⟶ b), Pp (g ∘ f) = Pp f ⬝ Pp g) : P := + elim Pe Pp Pcomp x + + protected definition set_elim [reducible] {P : Type} [is_set P] (Pe : G → P) + (Pp : Π⦃a b⦄ (f : a ⟶ b), Pe a = Pe b) + (x : groupoid_quotient) : P := + elim Pe Pp !center x + + protected definition prop_elim [reducible] {P : Type} [is_prop P] (Pe : G → P) + (x : groupoid_quotient) : P := + elim Pe !center !center x + + definition elim_pth {P : Type} [is_trunc 1 P] {Pe : G → P} {Pp : Π⦃a b⦄ (f : a ⟶ b), Pe a = Pe b} + (Pcomp : Π⦃a b c⦄ (g : b ⟶ c) (f : a ⟶ b), Pp (g ∘ f) = Pp f ⬝ Pp g) {a b : G} (f : a ⟶ b) : + ap (elim Pe Pp Pcomp) (pth f) = Pp f := + !elim_incl1 + + -- The following rule is also true because P is a 1-type, and can be proven by `!is_set.elims` + -- The following is the canonical proofs which holds for any truncated two-quotient. + theorem elim_resp_comp {P : Type} [is_trunc 1 P] {Pe : G → P} + {Pp : Π⦃a b⦄ (f : a ⟶ b), Pe a = Pe b} + (Pcomp : Π⦃a b c⦄ (g : b ⟶ c) (f : a ⟶ b), Pp (g ∘ f) = Pp f ⬝ Pp g) + {a b c : G} (g : b ⟶ c) (f : a ⟶ b) + : square (ap02 (elim Pe Pp Pcomp) (resp_comp g f)) + (Pcomp g f) + (elim_pth Pcomp (g ∘ f)) + (!ap_con ⬝ (elim_pth Pcomp f ◾ elim_pth Pcomp g)) := + proof !elim_incl2 qed + + protected definition elim_set.{u} (Pe : G → Set.{u}) (Pp : Π⦃a b⦄ (f : a ⟶ b), Pe a ≃ Pe b) + (Pcomp : Π⦃a b c⦄ (g : b ⟶ c) (f : a ⟶ b) (x : Pe a), Pp (g ∘ f) x = Pp g (Pp f x)) + (x : groupoid_quotient) : Set.{u} := + elim Pe (λa b f, tua (Pp f)) (λa b c g f, ap tua (equiv_eq (Pcomp g f)) ⬝ !tua_trans) x + + theorem elim_set_pth {Pe : G → Set} {Pp : Π⦃a b⦄ (f : a ⟶ b), Pe a ≃ Pe b} + (Pcomp : Π⦃a b c⦄ (g : b ⟶ c) (f : a ⟶ b) (x : Pe a), Pp (g ∘ f) x = Pp g (Pp f x)) + {a b : G} (f : a ⟶ b) : + transport (elim_set Pe Pp Pcomp) (pth f) = Pp f := + by rewrite [tr_eq_cast_ap_fn, ↑elim_set, ▸*, ap_compose' trunctype.carrier, elim_pth]; + apply tcast_tua_fn + +end +end groupoid_quotient + +attribute groupoid_quotient.elt [constructor] +attribute groupoid_quotient.rec groupoid_quotient.elim [unfold 7] [recursor 7] +attribute groupoid_quotient.rec_on groupoid_quotient.elim_on [unfold 4] +attribute groupoid_quotient.set_rec groupoid_quotient.set_elim [unfold 6] +attribute groupoid_quotient.prop_rec groupoid_quotient.prop_elim + groupoid_quotient.elim_set [unfold 5] + + +open sigma pi is_conn function +namespace groupoid_quotient +section + universe variables u v + variables {G : Groupoid.{u v}} (a : G) {b c : G} + + include a + + protected definition code [unfold 3] (x : groupoid_quotient G) : Set.{v} := + begin + refine groupoid_quotient.elim_set _ _ _ x, + { intro b, exact homset a b}, + { intro b c g, exact equiv_postcompose g}, + { intro b c d h g f, esimp at *, apply assoc'} + end + + omit a + + local abbreviation code [unfold 3] := @groupoid_quotient.code G a + + variable {a} + protected definition encode [unfold 4] (x : groupoid_quotient G) (p : elt a = x) : code a x := + transport (code a) p (ID a) + + protected definition decode [unfold 3] (x : groupoid_quotient G) (z : code a x) : elt a = x := + begin + induction x using groupoid_quotient.set_rec with b b c g, + { esimp, exact pth z}, + { apply arrow_pathover_left, esimp, intro f, apply eq_pathover_constant_left_id_right, + apply square_of_eq, refine !resp_comp⁻¹ ⬝ _ ⬝ !idp_con⁻¹, rewrite elim_set_pth} + end + + local abbreviation encode [unfold_full] := @groupoid_quotient.encode G a + local abbreviation decode [unfold 3] := @groupoid_quotient.decode G a + + protected definition decode_encode (x : groupoid_quotient G) (p : elt a = x) : + decode x (encode x p) = p := + begin induction p, esimp, apply resp_id end + + protected definition encode_decode (x : groupoid_quotient G) (z : code a x) : + encode x (decode x z) = z := + begin + induction x using groupoid_quotient.prop_rec with b, + esimp, refine ap10 !elim_set_pth.{u v v} (ID a) ⬝ _, esimp, + apply id_right + end + + definition decode_comp (z : code a (elt b)) (z' : code b (elt c)) : + decode (elt c) (z' ∘ z) = decode (elt b) z ⬝ decode (elt c) z' := + !resp_comp + + variables (a b) + definition elt_eq_elt_equiv [constructor] : (elt a = elt b) ≃ (a ⟶ b) := + equiv.MK (encode (elt b)) (decode (elt b)) + (groupoid_quotient.encode_decode (elt b)) (groupoid_quotient.decode_encode (elt b)) + + variables {a b} + definition encode_con (p : elt a = elt b) + (q : elt b = elt c) : encode (elt c) (p ⬝ q) = encode (elt c) q ∘ encode (elt b) p := + begin + apply eq_of_fn_eq_fn (elt_eq_elt_equiv a c)⁻¹ᵉ, + refine !right_inv ⬝ _ ⬝ !decode_comp⁻¹, + apply concat2, do 2 exact (to_left_inv !elt_eq_elt_equiv _)⁻¹ + end + + variable (G) + definition is_conn_groupoid_quotient [H : is_conn 0 G] : is_conn 0 (groupoid_quotient G) := + begin + have g : trunc 0 G, from !center, + induction g with g, + have p : Πh, ∥ g = h ∥, + begin + intro h, refine !tr_eq_tr_equiv _, apply is_prop.elim + end, + fapply is_contr.mk, + { apply trunc_functor 0 elt (tr g)}, + { intro x, induction x with x, + induction x using groupoid_quotient.prop_rec with b, esimp, + induction p b with q, exact ap (tr ∘ elt) q} + end + +end + +end groupoid_quotient diff --git a/hott/hit/hit.md b/hott/hit/hit.md index c73e0dbd5..9babcd7c1 100644 --- a/hott/hit/hit.md +++ b/hott/hit/hit.md @@ -23,4 +23,5 @@ Files in this folder: The following hits have also 2-constructors. They are defined only using quotients. * [two_quotient](two_quotient.hlean): Quotients where you can also specify 2-paths. These are used for all hits which have 2-constructors, and they are almost fully general for such hits, as long as they are nonrecursive -* [refl_quotient](refl_quotient.hlean): Quotients where you can also specify 2-paths \ No newline at end of file +* [refl_quotient](refl_quotient.hlean): Quotients where you can also specify 2-paths +* [groupoid_quotient](groupoid_quotient.hlean): The realization or quotient of a groupoid. \ No newline at end of file diff --git a/hott/hit/pushout.hlean b/hott/hit/pushout.hlean index 1d29b0f1e..ccf1073f6 100644 --- a/hott/hit/pushout.hlean +++ b/hott/hit/pushout.hlean @@ -1,7 +1,7 @@ /- -Copyright (c) 2015 Floris van Doorn. All rights reserved. +Copyright (c) 2015-16 Floris van Doorn. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Floris van Doorn +Authors: Floris van Doorn, Ulrik Buchholtz Declaration and properties of the pushout -/ diff --git a/hott/hit/two_quotient.hlean b/hott/hit/two_quotient.hlean index f7da0347f..d3cda79fb 100644 --- a/hott/hit/two_quotient.hlean +++ b/hott/hit/two_quotient.hlean @@ -10,7 +10,7 @@ import homotopy.circle eq2 algebra.e_closure cubical.squareover cubical.cube cub open quotient eq circle sum sigma equiv function relation e_closure /- - This files defines a general class of nonrecursive HITs using just quotients. + This files defines a general class of nonrecursive 2-HITs using just quotients. We can define any HIT X which has - a single 0-constructor f : A → X (for some type A) @@ -27,6 +27,15 @@ open quotient eq circle sum sigma equiv function relation e_closure so an example 2-constructor could be (as long as it typechecks): ap f q' ⬝ ((e r)⁻¹ ⬝ ap f q)⁻¹ ⬝ e r' = idp + + We first define "simple two quotients" which have as requirement that the right hand side is idp + Then we define "two quotients" which can have an arbitrary path on the right hand side + Then we define "truncated two quotients", which is a two quotient followed by n-truncation, + and show that this satisfies the desired induction principle and computation rule. + + Caveat: for none of these constructions we show that the induction priniciple computes on + 2-paths. However, with truncated two quotients, if the truncation is a 1-truncation, then this + computation rule follows automatically, since the target is a 1-type. -/ namespace simple_two_quotient @@ -489,3 +498,160 @@ attribute two_quotient.rec two_quotient.elim [unfold 8] [recursor 8] --attribute two_quotient.elim_type [unfold 9] attribute two_quotient.rec_on two_quotient.elim_on [unfold 5] --attribute two_quotient.elim_type_on [unfold 6] + +open two_quotient is_trunc trunc + +namespace trunc_two_quotient + + section + parameters (n : ℕ₋₂) {A : Type} + (R : A → A → Type) + local abbreviation T := e_closure R -- the (type-valued) equivalence closure of R + parameter (Q : Π⦃a a'⦄, T a a' → T a a' → Type) + variables ⦃a a' a'' : A⦄ {s : R a a'} {t t' : T a a'} + + definition trunc_two_quotient := trunc n (two_quotient R Q) + + parameters {n R Q} + definition incl0 (a : A) : trunc_two_quotient := tr (!incl0 a) + definition incl1 (s : R a a') : incl0 a = incl0 a' := ap tr (!incl1 s) + definition incltw (t : T a a') : incl0 a = incl0 a' := ap tr (!inclt t) + definition inclt (t : T a a') : incl0 a = incl0 a' := e_closure.elim incl1 t + definition incl2w (q : Q t t') : incltw t = incltw t' := + ap02 tr (!incl2 q) + definition incl2 (q : Q t t') : inclt t = inclt t' := + !ap_e_closure_elim⁻¹ ⬝ ap02 tr (!incl2 q) ⬝ !ap_e_closure_elim + + local attribute trunc_two_quotient incl0 [reducible] + definition is_trunc_trunc_two_quotient [instance] : is_trunc n trunc_two_quotient := _ + + protected definition rec {P : trunc_two_quotient → Type} [H : Πx, is_trunc n (P x)] + (P0 : Π(a : A), P (incl0 a)) + (P1 : Π⦃a a' : A⦄ (s : R a a'), P0 a =[incl1 s] P0 a') + (P2 : Π⦃a a' : A⦄ ⦃t t' : T a a'⦄ (q : Q t t'), + change_path (incl2 q) (e_closure.elimo incl1 P1 t) = e_closure.elimo incl1 P1 t') + (x : trunc_two_quotient) : P x := + begin + induction x, + induction a, + { exact P0 a}, + { exact !pathover_of_pathover_ap (P1 s)}, + { exact abstract [irreducible] + by rewrite [+ e_closure_elimo_ap, ↓incl1, -P2 q, change_path_pathover_of_pathover_ap, + - + change_path_con, ↑incl2, con_inv_cancel_right] end} + end + + protected definition rec_on [reducible] {P : trunc_two_quotient → Type} [H : Πx, is_trunc n (P x)] + (x : trunc_two_quotient) + (P0 : Π(a : A), P (incl0 a)) + (P1 : Π⦃a a' : A⦄ (s : R a a'), P0 a =[incl1 s] P0 a') + (P2 : Π⦃a a' : A⦄ ⦃t t' : T a a'⦄ (q : Q t t'), + change_path (incl2 q) (e_closure.elimo incl1 P1 t) = e_closure.elimo incl1 P1 t') : P x := + rec P0 P1 P2 x + + theorem rec_incl1 {P : trunc_two_quotient → Type} [H : Πx, is_trunc n (P x)] + (P0 : Π(a : A), P (incl0 a)) + (P1 : Π⦃a a' : A⦄ (s : R a a'), P0 a =[incl1 s] P0 a') + (P2 : Π⦃a a' : A⦄ ⦃t t' : T a a'⦄ (q : Q t t'), + change_path (incl2 q) (e_closure.elimo incl1 P1 t) = e_closure.elimo incl1 P1 t') + ⦃a a' : A⦄ (s : R a a') : apd (rec P0 P1 P2) (incl1 s) = P1 s := + !apd_ap ⬝ ap !pathover_ap !rec_incl1 ⬝ to_right_inv !pathover_compose (P1 s) + + theorem rec_inclt {P : trunc_two_quotient → Type} [H : Πx, is_trunc n (P x)] + (P0 : Π(a : A), P (incl0 a)) + (P1 : Π⦃a a' : A⦄ (s : R a a'), P0 a =[incl1 s] P0 a') + (P2 : Π⦃a a' : A⦄ ⦃t t' : T a a'⦄ (q : Q t t'), + change_path (incl2 q) (e_closure.elimo incl1 P1 t) = e_closure.elimo incl1 P1 t') + ⦃a a' : A⦄ (t : T a a') : apd (rec P0 P1 P2) (inclt t) = e_closure.elimo incl1 P1 t := + ap_e_closure_elimo_h incl1 P1 (rec_incl1 P0 P1 P2) t + + protected definition elim {P : Type} (P0 : A → P) [H : is_trunc n P] + (P1 : Π⦃a a' : A⦄ (s : R a a'), P0 a = P0 a') + (P2 : Π⦃a a' : A⦄ ⦃t t' : T a a'⦄ (q : Q t t'), e_closure.elim P1 t = e_closure.elim P1 t') + (x : trunc_two_quotient) : P := + begin + induction x, + induction a, + { exact P0 a}, + { exact P1 s}, + { exact P2 q}, + end + local attribute elim [unfold 10] + + protected definition elim_on {P : Type} [H : is_trunc n P] (x : trunc_two_quotient) (P0 : A → P) + (P1 : Π⦃a a' : A⦄ (s : R a a'), P0 a = P0 a') + (P2 : Π⦃a a' : A⦄ ⦃t t' : T a a'⦄ (q : Q t t'), e_closure.elim P1 t = e_closure.elim P1 t') + : P := + elim P0 P1 P2 x + + definition elim_incl1 {P : Type} [H : is_trunc n P] {P0 : A → P} + {P1 : Π⦃a a' : A⦄ (s : R a a'), P0 a = P0 a'} + (P2 : Π⦃a a' : A⦄ ⦃t t' : T a a'⦄ (q : Q t t'), e_closure.elim P1 t = e_closure.elim P1 t') + ⦃a a' : A⦄ (s : R a a') : ap (elim P0 P1 P2) (incl1 s) = P1 s := + !ap_compose⁻¹ ⬝ !elim_incl1 + + definition elim_inclt {P : Type} [H : is_trunc n P] {P0 : A → P} + {P1 : Π⦃a a' : A⦄ (s : R a a'), P0 a = P0 a'} + (P2 : Π⦃a a' : A⦄ ⦃t t' : T a a'⦄ (q : Q t t'), e_closure.elim P1 t = e_closure.elim P1 t') + ⦃a a' : A⦄ (t : T a a') : ap (elim P0 P1 P2) (inclt t) = e_closure.elim P1 t := + ap_e_closure_elim_h incl1 (elim_incl1 P2) t + + open function + + theorem elim_incl2 {P : Type} [H : is_trunc n P] (P0 : A → P) + (P1 : Π⦃a a' : A⦄ (s : R a a'), P0 a = P0 a') + (P2 : Π⦃a a' : A⦄ ⦃t t' : T a a'⦄ (q : Q t t'), e_closure.elim P1 t = e_closure.elim P1 t') + ⦃a a' : A⦄ ⦃t t' : T a a'⦄ (q : Q t t') + : square (ap02 (elim P0 P1 P2) (incl2 q)) (P2 q) (elim_inclt P2 t) (elim_inclt P2 t') := + begin + note Ht' := ap_ap_e_closure_elim tr (elim P0 P1 P2) (two_quotient.incl1 R Q) t', + note Ht := ap_ap_e_closure_elim tr (elim P0 P1 P2) (two_quotient.incl1 R Q) t, + note Hn := natural_square (ap_compose (elim P0 P1 P2) tr) (two_quotient.incl2 R Q q), + note H7 := eq_top_of_square (Ht⁻¹ʰ ⬝h Hn⁻¹ᵛ ⬝h Ht'), clear [Hn, Ht, Ht'], + unfold [ap02,incl2], rewrite [+ap_con,ap_inv,-ap_compose (ap _)], + xrewrite [H7, ↑function.compose, eq_top_of_square (elim_incl2 P0 P1 P2 q)], clear [H7], + have H : Π(t : T a a'), + ap_e_closure_elim (elim P0 P1 P2) (λa a' (r : R a a'), ap tr (two_quotient.incl1 R Q r)) t ⬝ + (ap_e_closure_elim_h (two_quotient.incl1 R Q) + (λa a' (s : R a a'), ap_compose (elim P0 P1 P2) tr (two_quotient.incl1 R Q s)) t)⁻¹ ⬝ + two_quotient.elim_inclt P2 t = elim_inclt P2 t, from + ap_e_closure_elim_h_zigzag (elim P0 P1 P2) + (two_quotient.incl1 R Q) + (two_quotient.elim_incl1 P2), + rewrite [con.assoc5, con.assoc5, H t, -inv_con_inv_right, -con_inv], xrewrite [H t'], + apply top_deg_square + end + + definition elim_inclt_rel [unfold_full] {P : Type} [is_trunc n P] {P0 : A → P} + {P1 : Π⦃a a' : A⦄ (s : R a a'), P0 a = P0 a'} + (P2 : Π⦃a a' : A⦄ ⦃t t' : T a a'⦄ (q : Q t t'), e_closure.elim P1 t = e_closure.elim P1 t') + ⦃a a' : A⦄ (r : R a a') : elim_inclt P2 [r] = elim_incl1 P2 r := + idp + + definition elim_inclt_inv [unfold_full] {P : Type} [is_trunc n P] {P0 : A → P} + {P1 : Π⦃a a' : A⦄ (s : R a a'), P0 a = P0 a'} + (P2 : Π⦃a a' : A⦄ ⦃t t' : T a a'⦄ (q : Q t t'), e_closure.elim P1 t = e_closure.elim P1 t') + ⦃a a' : A⦄ (t : T a a') + : elim_inclt P2 t⁻¹ʳ = ap_inv (elim P0 P1 P2) (inclt t) ⬝ (elim_inclt P2 t)⁻² := + idp + + definition elim_inclt_con [unfold_full] {P : Type} [is_trunc n P] {P0 : A → P} + {P1 : Π⦃a a' : A⦄ (s : R a a'), P0 a = P0 a'} + (P2 : Π⦃a a' : A⦄ ⦃t t' : T a a'⦄ (q : Q t t'), e_closure.elim P1 t = e_closure.elim P1 t') + ⦃a a' a'' : A⦄ (t : T a a') (t': T a' a'') + : elim_inclt P2 (t ⬝r t') = + ap_con (elim P0 P1 P2) (inclt t) (inclt t') ⬝ (elim_inclt P2 t ◾ elim_inclt P2 t') := + idp + + definition inclt_rel [unfold_full] (r : R a a') : inclt [r] = incl1 r := idp + definition inclt_inv [unfold_full] (t : T a a') : inclt t⁻¹ʳ = (inclt t)⁻¹ := idp + definition inclt_con [unfold_full] (t : T a a') (t' : T a' a'') + : inclt (t ⬝r t') = inclt t ⬝ inclt t' := idp + + +end +end trunc_two_quotient + +attribute trunc_two_quotient.incl0 [constructor] +attribute trunc_two_quotient.rec trunc_two_quotient.elim [unfold 10] [recursor 10] +attribute trunc_two_quotient.rec_on trunc_two_quotient.elim_on [unfold 7] diff --git a/hott/homotopy/EM.hlean b/hott/homotopy/EM.hlean new file mode 100644 index 000000000..3b3c8f472 --- /dev/null +++ b/hott/homotopy/EM.hlean @@ -0,0 +1,259 @@ +/- +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 + +Eilenberg MacLane spaces +-/ + +import hit.groupoid_quotient .hopf .freudenthal .homotopy_group +open algebra pointed nat eq category group algebra is_trunc iso pointed unit trunc equiv is_conn + +namespace EM + open groupoid_quotient + + variable {G : Group} + definition EM1 (G : Group) : Type := + groupoid_quotient (Groupoid_of_Group G) + definition pEM1 [constructor] (G : Group) : Type* := + pointed.MK (EM1 G) (elt star) + + definition base : EM1 G := elt star + definition pth : G → base = base := pth + definition resp_mul (g h : G) : pth (g * h) = pth g ⬝ pth h := resp_comp h g + definition resp_one : pth (1 : G) = idp := + resp_id star + + definition resp_inv (g : G) : pth (g⁻¹) = (pth g)⁻¹ := + resp_inv g + + local attribute pointed.MK pointed.carrier pEM1 EM1 [reducible] + protected definition rec {P : EM1 G → Type} [H : Π(x : EM1 G), is_trunc 1 (P x)] + (Pb : P base) (Pp : Π(g : G), Pb =[pth g] Pb) + (Pmul : Π(g h : G), change_path (resp_mul g h) (Pp (g * h)) = Pp g ⬝o Pp h) (x : EM1 G) : P x := + begin + induction x, + { induction g, exact Pb}, + { induction a, induction b, exact Pp f}, + { induction a, induction b, induction c, exact Pmul f g} + end + + protected definition rec_on {P : EM1 G → Type} [H : Π(x : EM1 G), is_trunc 1 (P x)] + (x : EM1 G) (Pb : P base) (Pp : Π(g : G), Pb =[pth g] Pb) + (Pmul : Π(g h : G), change_path (resp_mul g h) (Pp (g * h)) = Pp g ⬝o Pp h) : P x := + EM.rec Pb Pp Pmul x + + protected definition set_rec {P : EM1 G → Type} [H : Π(x : EM1 G), is_set (P x)] + (Pb : P base) (Pp : Π(g : G), Pb =[pth g] Pb) (x : EM1 G) : P x := + EM.rec Pb Pp !center x + + protected definition prop_rec {P : EM1 G → Type} [H : Π(x : EM1 G), is_prop (P x)] + (Pb : P base) (x : EM1 G) : P x := + EM.rec Pb !center !center x + + definition rec_pth {P : EM1 G → Type} [H : Π(x : EM1 G), is_trunc 1 (P x)] + {Pb : P base} {Pp : Π(g : G), Pb =[pth g] Pb} + (Pmul : Π(g h : G), change_path (resp_mul g h) (Pp (g * h)) = Pp g ⬝o Pp h) + (g : G) : apd (EM.rec Pb Pp Pmul) (pth g) = Pp g := + proof !rec_pth qed + + protected definition elim {P : Type} [is_trunc 1 P] (Pb : P) (Pp : Π(g : G), Pb = Pb) + (Pmul : Π(g h : G), Pp (g * h) = Pp g ⬝ Pp h) (x : EM1 G) : P := + begin + induction x, + { exact Pb}, + { exact Pp f}, + { exact Pmul f g} + end + + protected definition elim_on [reducible] {P : Type} [is_trunc 1 P] (x : EM1 G) + (Pb : P) (Pp : G → Pb = Pb) (Pmul : Π(g h : G), Pp (g * h) = Pp g ⬝ Pp h) : P := + EM.elim Pb Pp Pmul x + + protected definition set_elim [reducible] {P : Type} [is_set P] (Pb : P) (Pp : G → Pb = Pb) + (x : EM1 G) : P := + EM.elim Pb Pp !center x + + protected definition prop_elim [reducible] {P : Type} [is_prop P] (Pb : P) (x : EM1 G) : P := + EM.elim Pb !center !center x + + definition elim_pth {P : Type} [is_trunc 1 P] {Pb : P} {Pp : G → Pb = Pb} + (Pmul : Π(g h : G), Pp (g * h) = Pp g ⬝ Pp h) (g : G) : ap (EM.elim Pb Pp Pmul) (pth g) = Pp g := + proof !elim_pth qed + + protected definition elim_set.{u} (Pb : Set.{u}) (Pp : Π(g : G), Pb ≃ Pb) + (Pmul : Π(g h : G) (x : Pb), Pp (g * h) x = Pp h (Pp g x)) (x : EM1 G) : Set.{u} := + groupoid_quotient.elim_set (λu, Pb) (λu v, Pp) (λu v w g h, proof Pmul h g qed) x + + theorem elim_set_pth {Pb : Set} {Pp : Π(g : G), Pb ≃ Pb} + (Pmul : Π(g h : G) (x : Pb), Pp (g * h) x = Pp h (Pp g x)) (g : G) : + transport (EM.elim_set Pb Pp Pmul) (pth g) = Pp g := + !elim_set_pth + +end EM + +-- attribute EM.rec EM.elim [recursor 7] +attribute EM.base [constructor] +attribute EM.rec EM.elim [unfold 7] [recursor 7] +attribute EM.rec_on EM.elim_on [unfold 4] +attribute EM.set_rec EM.set_elim [unfold 6] +attribute EM.prop_rec EM.prop_elim EM.elim_set [unfold 5] + +namespace EM + open groupoid_quotient + + definition base_eq_base_equiv [constructor] (G : Group) : (base = base :> pEM1 G) ≃ G := + !elt_eq_elt_equiv + + definition fundamental_group_pEM1 (G : Group) : π₁ (pEM1 G) ≃g G := + begin + fapply isomorphism_of_equiv, + { exact trunc_equiv_trunc 0 !base_eq_base_equiv ⬝e trunc_equiv 0 G}, + { intros g h, induction g with p, induction h with q, + exact encode_con p q} + end + + proposition is_trunc_pEM1 [instance] (G : Group) : is_trunc 1 (pEM1 G) := + !is_trunc_groupoid_quotient + + proposition is_trunc_EM1 [instance] (G : Group) : is_trunc 1 (EM1 G) := + !is_trunc_groupoid_quotient + + proposition is_conn_EM1 [instance] (G : Group) : is_conn 0 (EM1 G) := + by apply @is_conn_groupoid_quotient; esimp; exact _ + + proposition is_conn_pEM1 [instance] (G : Group) : is_conn 0 (pEM1 G) := + is_conn_EM1 G + + -- TODO: prove this using truncated Whitehead. + + definition EM1_map [unfold 7] {G : Group} {X : Type*} (e : Ω X ≃ G) + (r : Πp q, e (p ⬝ q) = e p * e q) [is_conn 0 X] [is_trunc 1 X] : EM1 G → X := + begin + intro x, induction x using EM.elim, + { exact Point X}, + { note p := e⁻¹ᵉ g, exact p}, + { exact inv_preserve_binary e concat mul r g h} + end + + -- TODO + -- definition EM1_equiv {G : Group} {X : Type*} (e : Ω X ≃ G) + -- (r : Πp q, e (p ⬝ q) = e p * e q) [is_conn 0 X] [is_trunc 1 X] : EM1 G ≃ X := + -- begin + -- apply equiv.mk (EM1_map e r), + -- apply whiteheads_principle 1, + -- { apply is_equiv_of_is_contr}, + -- { intro x n, cases n with n, + -- { exact sorry}, + -- { apply @is_equiv_of_is_contr, do 2 exact sorry}} + -- end + + -- definition pequiv_pEM1 {G : Group} {X : Type*} (e : π₁ X ≃g G) [is_conn 0 X] [is_trunc 1 X] + -- : X ≃* pEM1 G := + -- sorry + +end EM + +open hopf susp +namespace EM + -- The K(G,n+1): + variables (G : CommGroup) (n : ℕ) + + definition EM1_mul [unfold 2 3] {G : CommGroup} (x x' : EM1 G) : EM1 G := + begin + induction x, + { exact x'}, + { induction x' using EM.set_rec, + { exact pth g}, + { exact abstract begin apply loop_pathover, apply square_of_eq, + refine !resp_mul⁻¹ ⬝ _ ⬝ !resp_mul, + exact ap pth !mul.comm end end}}, + { refine EM.prop_rec _ x', esimp, apply resp_mul}, + end + + definition EM1_mul_one (G : CommGroup) (x : EM1 G) : EM1_mul x base = x := + begin + induction x using EM.set_rec, + { reflexivity}, + { apply eq_pathover_id_right, apply hdeg_square, refine EM.elim_pth _ g} + end + + definition h_space_EM1 [constructor] [instance] (G : CommGroup) : h_space (pEM1 G) := + begin + fapply h_space.mk, + { exact EM1_mul}, + { exact base}, + { intro x', reflexivity}, + { apply EM1_mul_one} + end + + /- K(G, n+1) -/ + definition EMadd1 (G : CommGroup) (n : ℕ) : Type* := + ptrunc (n+1) (iterate_psusp n (pEM1 G)) + + definition loop_EM2 (G : CommGroup) : Ω[1] (EMadd1 G 1) ≃* pEM1 G := + begin + apply hopf.delooping, reflexivity + end + + definition homotopy_group_EM2 (G : CommGroup) : πg[1+1] (EMadd1 G 1) ≃g G := + begin + refine ghomotopy_group_succ_in _ 0 ⬝g _, + refine homotopy_group_isomorphism_of_pequiv 0 (loop_EM2 G) ⬝g _, + apply fundamental_group_pEM1 + end + + definition homotopy_group_EMadd1 (G : CommGroup) (n : ℕ) : πg[n+1] (EMadd1 G n) ≃g G := + begin + cases n with n, + { refine homotopy_group_isomorphism_of_pequiv 0 _ ⬝g fundamental_group_pEM1 G, + apply ptrunc_pequiv, apply is_trunc_pEM1}, + induction n with n IH, + { apply homotopy_group_EM2 G}, + refine _ ⬝g IH, + refine !ghomotopy_group_ptrunc ⬝g _ ⬝g !ghomotopy_group_ptrunc⁻¹ᵍ, + apply iterate_psusp_stability_isomorphism, + rexact add_mul_le_mul_add n 1 1 + end + + local attribute EMadd1 [reducible] + definition is_conn_EMadd1 (G : CommGroup) (n : ℕ) : is_conn n (EMadd1 G n) := _ + + definition is_trunc_EMadd1 (G : CommGroup) (n : ℕ) : is_trunc (n+1) (EMadd1 G n) := _ + + /- K(G, n+1) -/ + definition EM (G : CommGroup) : ℕ → Type* + | 0 := pType_of_Group G + | (k+1) := EMadd1 G k + + definition phomotopy_group_EM (G : CommGroup) (n : ℕ) : π*[n] (EM G n) ≃* pType_of_Group G := + begin + cases n with n, + { rexact ptrunc_pequiv 0 (pType_of_Group G) _}, + { apply pequiv_of_isomorphism (homotopy_group_EMadd1 G n)} + end + + definition ghomotopy_group_EM (G : CommGroup) (n : ℕ) : πg[n+1] (EM G (n+1)) ≃g G := + homotopy_group_EMadd1 G n + + definition is_conn_EM [instance] (G : CommGroup) (n : ℕ) : is_conn (n.-1) (EM G n) := + begin + cases n with n, + { apply is_conn_minus_one, apply tr, unfold [EM], exact 1}, + { apply is_conn_EMadd1} + end + + definition is_conn_EM_succ [instance] (G : CommGroup) (n : ℕ) : is_conn n (EM G (succ n)) := + is_conn_EM G (succ n) + + definition is_trunc_EM [instance] (G : CommGroup) (n : ℕ) : is_trunc n (EM G n) := + begin + cases n with n, + { unfold [EM], apply semigroup.is_set_carrier}, + { apply is_trunc_EMadd1} + end + + + +end EM diff --git a/hott/homotopy/LES_of_homotopy_groups.hlean b/hott/homotopy/LES_of_homotopy_groups.hlean new file mode 100644 index 000000000..41844f951 --- /dev/null +++ b/hott/homotopy/LES_of_homotopy_groups.hlean @@ -0,0 +1,826 @@ +/- +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 eq2 + +open eq pointed sigma fiber equiv is_equiv sigma.ops is_trunc nat trunc algebra function sum + +/-------------- + 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 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 + + /- + Fibration sequences + + This is a similar construction, but with as input data two pointed maps, + and a pointed equivalence between the domain of the second map and the fiber of the first map, + and a pointed homotopy. + -/ + + 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 prod nat + 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 diff --git a/hott/homotopy/chain_complex.hlean b/hott/homotopy/chain_complex.hlean new file mode 100644 index 000000000..f77195bbe --- /dev/null +++ b/hott/homotopy/chain_complex.hlean @@ -0,0 +1,522 @@ +/- +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 + +Chain complexes. + +We define chain complexes in a general way as a sequence X of types indexes over an arbitrary type +N with a successor S. There are maps X (S n) → X n for n : N. We can vary N to have chain complexes +indexed by ℕ, ℤ, a finite type or something else, and for both ℕ and ℤ we can choose the maps to +go up or down. We also use the indexing ℕ × 3 for the LES of homotopy groups, because then it +computes better (see [LES_of_homotopy_groups]). + +We have two separate notions of +chain complexes: +- type_chain_complex: sequence of types, where exactness is formulated using pure existence. +- chain_complex: sequence of sets, where exactness is formulated using mere existence. + +-/ + +import types.int algebra.group_theory types.fin + +open eq pointed int unit is_equiv equiv is_trunc trunc function algebra group sigma.ops + sum prod nat bool fin + +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, cyclic_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 + + /- + We define "type chain complexes" which are chain complexes without the + "set"-requirement. Exactness is formulated without propositional truncation. + -/ + 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 + + -- A chain complex on +ℕ can be trivially extended to a chain complex on +ℤ + 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 tcc_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 tcc_is_chain_complex X n}, + { esimp, intro x, reflexivity} + end + + definition is_exact_t_from_left {X : type_chain_complex +ℕ} {n : ℕ} + (H : is_exact_at_t X n) + : is_exact_at_t (type_chain_complex_from_left X) (of_nat n) := + H + + /- + Given a natural isomorphism between a chain complex and any other sequence, + we can give the other sequence the structure of a chain complex, which is exact at the + positions where the original sequence is. + -/ + 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 + + /- + We want a theorem which states that if we have a chain complex, but with some + where the maps are composed by an equivalences, we want to remove this equivalence. + The following two theorems give sufficient conditions for when this is allowed. + We use this to transform the LES of homotopy groups where on the odd levels we have + maps -πₙ(...) into the LES of homotopy groups where we remove the minus signs (which + represents composition with path inversion). + -/ + 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 + + /- + A more general transfer theorem. + Here 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 + + 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 cc_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 cc_is_chain_complex X n}, + { esimp, intro x, reflexivity} + end + + definition is_exact_from_left {X : chain_complex +ℕ} {n : ℕ} (H : is_exact_at X n) + : is_exact_at (chain_complex_from_left X) (of_nat 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 r, + refine image.mk (e x) _, + refine (p x)⁻¹ ⬝ _, + refine ap e r ⬝ _, + apply right_inv + end + + /- A type chain complex can be set-truncated to a chain complex -/ + 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 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 + + /- + This is a start of a development of chain complexes consisting only on groups. + This might be useful to have in stable algebraic topology, but in the unstable case it's less + useful, since the smallest terms usually don't have a group structure. + We don't use it yet, so it's commented out for now + -/ + -- 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 + + /- + 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 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/hott/homotopy/circle.hlean b/hott/homotopy/circle.hlean index df8a14ce0..9fec818da 100644 --- a/hott/homotopy/circle.hlean +++ b/hott/homotopy/circle.hlean @@ -285,8 +285,8 @@ namespace circle definition base_eq_base_equiv [constructor] : base = base ≃ ℤ := circle_eq_equiv base - definition decode_add (a b : ℤ) : circle.decode a ⬝ circle.decode b = circle.decode (a +[ℤ] b) := - !power_con_power + definition decode_add (a b : ℤ) : circle.decode (a +[ℤ] b) = circle.decode a ⬝ circle.decode b := + !power_con_power⁻¹ definition encode_con (p q : base = base) : circle.encode (p ⬝ q) = circle.encode p +[ℤ] circle.encode q := diff --git a/hott/homotopy/cofiber.hlean b/hott/homotopy/cofiber.hlean index 7ff1801e0..68d857e27 100644 --- a/hott/homotopy/cofiber.hlean +++ b/hott/homotopy/cofiber.hlean @@ -5,7 +5,7 @@ Authors: Jakob von Raumer The Cofiber Type -/ -import hit.pointed_pushout function .susp +import hit.pointed_pushout function .susp types.unit open eq pushout unit pointed is_trunc is_equiv susp unit diff --git a/hott/homotopy/complex_hopf.hlean b/hott/homotopy/complex_hopf.hlean index 038695919..aff545afa 100644 --- a/hott/homotopy/complex_hopf.hlean +++ b/hott/homotopy/complex_hopf.hlean @@ -1,15 +1,15 @@ /- Copyright (c) 2016 Ulrik Buchholtz and Egbert Rijke. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Ulrik Buchholtz, Egbert Rijke +Authors: Ulrik Buchholtz, Egbert Rijke, Floris van Doorn The H-space structure on S¹ and the complex Hopf fibration (the standard one). -/ -import .hopf .circle +import .hopf .circle types.fin -open eq equiv is_equiv circle is_conn trunc is_trunc sphere_index sphere susp +open eq equiv is_equiv circle is_conn trunc is_trunc sphere susp pointed fiber sphere.ops function namespace hopf @@ -28,7 +28,7 @@ namespace hopf { apply is_prop.elimo, apply is_trunc_square } } end - open sphere.ops function + open sphere_index definition complex_hopf : S 3 → S 2 := begin @@ -36,4 +36,18 @@ namespace hopf apply inv (hopf.total S¹), apply inv (join.spheres 1 1), exact x end + definition complex_phopf [constructor] : S. 3 →* S. 2 := + proof pmap.mk complex_hopf idp qed + + 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 (of_nat 1) (of_nat 1))⁻¹ᵉ _ ⬝e _, + refine fiber.equiv_precompose _ (hopf.total S¹)⁻¹ᵉ _ ⬝e _, + apply fiber_pr1}, + { reflexivity} + end + end hopf diff --git a/hott/homotopy/connectedness.hlean b/hott/homotopy/connectedness.hlean index 222ef8616..8b53233c8 100644 --- a/hott/homotopy/connectedness.hlean +++ b/hott/homotopy/connectedness.hlean @@ -3,7 +3,7 @@ Copyright (c) 2015 Ulrik Buchholtz. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Ulrik Buchholtz, Floris van Doorn -/ -import types.trunc types.arrow_2 types.fiber +import types.trunc types.arrow_2 types.lift open eq is_trunc is_equiv nat equiv trunc function fiber funext pi @@ -199,7 +199,7 @@ namespace is_conn (fiber (λs x, s (Point A)) (λx, p)) (fiber (λs, s (Point A)) p) k - (equiv.symm (fiber.equiv_postcompose (to_fun (arrow_unit_left (P (Point A)))))) + (equiv.symm (fiber.equiv_postcompose _ (arrow_unit_left (P (Point A))) _)) (is_conn_fun.elim_general n k (is_conn_fun_from_unit n A (Point A)) P (λx, p)) end end is_conn @@ -251,6 +251,21 @@ namespace is_conn definition is_conn_minus_two (A : Type) : is_conn -2 A := _ + -- merely inhabited types are -1-connected + definition is_conn_minus_one (A : Type) (a : ∥ A ∥) : is_conn -1 A := + is_contr.mk a (is_prop.elim _) + + definition is_conn_trunc [instance] (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 + + open pointed + definition is_conn_ptrunc [instance] (A : Type*) (n k : ℕ₋₂) [H : is_conn n A] + : is_conn n (ptrunc k A) := + is_conn_trunc A n k + -- the following trivial cases are solved by type class inference definition is_conn_of_is_contr (k : ℕ₋₂) (A : Type) [is_contr A] : is_conn k A := _ definition is_conn_fun_of_is_equiv (k : ℕ₋₂) {A B : Type} (f : A → B) [is_equiv f] : @@ -301,4 +316,12 @@ namespace is_conn { exact is_conn_fun_trunc_functor_of_ge f H} end + open lift + 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 + end is_conn diff --git a/hott/homotopy/cylinder.hlean b/hott/homotopy/cylinder.hlean index e53d551bf..8916d09dd 100644 --- a/hott/homotopy/cylinder.hlean +++ b/hott/homotopy/cylinder.hlean @@ -117,6 +117,7 @@ namespace cylinder definition fseg (a : A) : fbase (f a) = ftop a := fiber_eq (seg a) !elim_seg⁻¹ +-- TODO: define the induction principle for "fcylinder" -- set_option pp.notation false -- -- The induction principle for the dependent mapping cylinder (TODO) -- protected definition frec {P : Π(b), fcylinder f b → Type} diff --git a/hott/homotopy/freudenthal.hlean b/hott/homotopy/freudenthal.hlean new file mode 100644 index 000000000..6e535f8a0 --- /dev/null +++ b/hott/homotopy/freudenthal.hlean @@ -0,0 +1,241 @@ +/- +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 + +The Freudenthal Suspension Theorem +-/ + +import homotopy.wedge homotopy.circle + +open eq is_conn is_trunc pointed susp nat pi equiv is_equiv trunc fiber trunc_index + +namespace freudenthal section + + 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. + -/ + + private 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) := sorry + +end end freudenthal + +open algebra group +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 + +definition freudenthal_homotopy_group_pequiv (A : Type*) {n k : ℕ} [is_conn n A] (H : k ≤ 2 * n) + : π*[k + 1] (psusp A) ≃* π*[k] A := +calc + π*[k + 1] (psusp A) ≃* π*[k] (Ω (psusp A)) : pequiv_of_eq (phomotopy_group_succ_in (psusp A) k) + ... ≃* Ω[k] (ptrunc k (Ω (psusp A))) : phomotopy_group_pequiv_loop_ptrunc k (Ω (psusp A)) + ... ≃* Ω[k] (ptrunc k A) : loopn_pequiv_loopn k (freudenthal_pequiv A H) + ... ≃* π*[k] A : (phomotopy_group_pequiv_loop_ptrunc k A)⁻¹ᵉ* + +definition freudenthal_homotopy_group_isomorphism (A : Type*) {n k : ℕ} [is_conn n A] + (H : k + 1 ≤ 2 * n) : πg[k+1 +1] (psusp A) ≃g πg[k+1] A := +begin + fapply isomorphism_of_equiv, + { exact equiv_of_pequiv (freudenthal_homotopy_group_pequiv A 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_in_con} +end + +namespace susp + + definition iterate_psusp_stability_pequiv (A : Type*) {k n : ℕ} [is_conn 0 A] + (H : k ≤ 2 * n) : π*[k + 1] (iterate_psusp (n + 1) A) ≃* π*[k] (iterate_psusp n A) := + have is_conn n (iterate_psusp n A), by rewrite [-zero_add n]; exact _, + freudenthal_homotopy_group_pequiv (iterate_psusp n A) H + + definition iterate_psusp_stability_isomorphism (A : Type*) {k n : ℕ} [is_conn 0 A] + (H : k + 1 ≤ 2 * n) : πg[k+1 +1] (iterate_psusp (n + 1) A) ≃g πg[k+1] (iterate_psusp n A) := + have is_conn n (iterate_psusp n A), by rewrite [-zero_add n]; exact _, + freudenthal_homotopy_group_isomorphism (iterate_psusp n A) H + + definition stability_helper1 {k n : ℕ} (H : k + 2 ≤ 2 * n) : 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 + + definition stability_helper2 (A : Type) {k n : ℕ} (H : k + 2 ≤ 2 * n) : + is_conn (pred n) (iterate_susp (n + 1) A) := + have Π(n : ℕ), n = -2 + (succ n + 1), + begin intro n, induction n with n IH, reflexivity, exact ap succ IH end, + begin + cases n with n, + { exfalso, exact not_succ_le_zero _ H}, + { esimp, rewrite [this n], apply is_conn_iterate_susp} + end + + definition iterate_susp_stability_pequiv (A : Type) {k n : ℕ} + (H : k + 2 ≤ 2 * n) : π*[k + 1] (pointed.MK (iterate_susp (n + 2) A) !north) ≃* + π*[k ] (pointed.MK (iterate_susp (n + 1) A) !north) := + have is_conn (pred n) (carrier (pointed.MK (iterate_susp (n + 1) A) !north)), from + stability_helper2 A H, + freudenthal_homotopy_group_pequiv (pointed.MK (iterate_susp (n + 1) A) !north) + (stability_helper1 H) + + definition iterate_susp_stability_isomorphism (A : Type) {k n : ℕ} + (H : k + 3 ≤ 2 * n) : πg[k+1 +1] (pointed.MK (iterate_susp (n + 2) A) !north) ≃g + πg[k+1] (pointed.MK (iterate_susp (n + 1) A) !north) := + have is_conn (pred n) (carrier (pointed.MK (iterate_susp (n + 1) A) !north)), from + @stability_helper2 A (k+1) n H, + freudenthal_homotopy_group_isomorphism (pointed.MK (iterate_susp (n + 1) A) !north) + (stability_helper1 H) + +end susp diff --git a/hott/homotopy/homotopy.md b/hott/homotopy/homotopy.md index 571991008..e0f48aac5 100644 --- a/hott/homotopy/homotopy.md +++ b/hott/homotopy/homotopy.md @@ -15,12 +15,16 @@ folder (sorted such that files only import previous files). * [cofiber](cofiber.hlean) * [wedge](wedge.hlean) * [smash](smash.hlean) -* [homotopy_group](homotopy_group.hlean) (theorems about homotopy groups. The definition and basic facts about homotopy groups is in [algebra/homotopy_group](../algebra/homotopy_group.hlean)). * [join](join.hlean) +* [freudenthal](freudenthal.hlean) (The Freudenthal Suspension Theorem) * [hopf](hopf.hlean) (the Hopf construction and delooping of coherent connected H-spaces) * [complex_hopf](complex_hopf.hlean) (the complex Hopf fibration) * [imaginaroid](imaginaroid.hlean) (imaginaroids as a variant of the Cayley-Dickson construction) * [quaternionic_hopf](quaternionic_hopf.hlean) (the quaternionic Hopf fibration) +* [chain_complex](chain_complex.hlean) +* [LES_of_homotopy_groups](LES_of_homotopy_groups.hlean) +* [homotopy_group](homotopy_group.hlean) (theorems about homotopy groups. The definition and basic facts about homotopy groups is in [algebra/homotopy_group](../algebra/homotopy_group.hlean)) +* [sphere2](sphere2.hlean) (calculation of the homotopy group of spheres) The following files depend on [hit.two_quotient](../hit/two_quotient.hlean) which on turn depends on @@ -28,3 +32,4 @@ The following files depend on * [red_susp](red_susp.hlean) (Reduced suspensions) * [torus](torus.hlean) (defined as a two-quotient) +* [EM](EM.hlean): Eilenberg MacLane spaces diff --git a/hott/homotopy/homotopy_group.hlean b/hott/homotopy/homotopy_group.hlean index 785ad87c1..6b768b405 100644 --- a/hott/homotopy/homotopy_group.hlean +++ b/hott/homotopy/homotopy_group.hlean @@ -5,7 +5,7 @@ Authors: Floris van Doorn, Clive Newstead -/ -import algebra.homotopy_group .sphere +import .LES_of_homotopy_groups .sphere .complex_hopf open eq is_trunc trunc_index pointed algebra trunc nat is_conn fiber pointed @@ -47,5 +47,105 @@ namespace is_trunc [H : is_conn_fun n f] (H2 : k ≤ n) : is_contr (π[k] (pfiber f)) := @(trivial_homotopy_group_of_is_conn (pfiber f) H2) (H pt) + /- Corollaries of the LES of homotopy groups -/ + local attribute comm_group.to_group [coercion] + local attribute is_equiv_tinverse [instance] + open prod chain_complex group fin equiv function is_equiv lift + + /- + Because of the construction of the LES this proof only gives us this result when + A and B live in the same universe (because Lean doesn't have universe cumulativity). + However, below we also proof that it holds for A and B in arbitrary universes. + -/ + 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 + + 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 + + definition π_equiv_π_of_is_connected {A B : Type*} {n k : ℕ} (f : A →* B) + (H2 : k ≤ n) [H : is_conn_fun n f] : π*[k] A ≃* π*[k] B := + pequiv_of_pmap (π→*[k] f) (is_equiv_π_of_is_connected f H2) + + -- TODO: prove this for A and B in different universe levels + 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) + + /- + Theorem 8.8.3: Whitehead's principle + -/ + definition whiteheads_principle (n : ℕ₋₂) {A B : Type} + [HA : is_trunc n A] [HB : is_trunc n B] (f : A → B) (H' : is_equiv (trunc_functor 0 f)) + (H : Πa k, is_equiv (π→*[k + 1] (pmap_of_map f a))) : is_equiv f := + begin + revert A B HA HB f H' H, induction n with n IH: intros, + { apply is_equiv_of_is_contr}, + have Πa, is_equiv (Ω→ (pmap_of_map f a)), + begin + intro a, + apply IH, do 2 (esimp; exact _), + { rexact H a 0}, + intro p k, + have is_equiv (π→*[k + 1] (Ω→(pmap_of_map f a))), + from is_equiv_phomotopy_group_functor_ap1 (k+1) (pmap_of_map f a), + have Π(b : A) (p : a = b), + is_equiv (pmap.to_fun (π→*[k + 1] (pmap_of_map (ap f) p))), + begin + intro b p, induction p, apply is_equiv.homotopy_closed, exact this, + refine phomotopy_group_functor_phomotopy _ _, + apply ap1_pmap_of_map + end, + have is_equiv (phomotopy_group_pequiv _ + (pequiv_of_eq_pt (!idp_con⁻¹ : ap f p = Ω→ (pmap_of_map f a) p)) ∘ + pmap.to_fun (π→*[k + 1] (pmap_of_map (ap f) p))), + begin + apply is_equiv_compose, exact this a p, + end, + apply is_equiv.homotopy_closed, exact this, + refine !phomotopy_group_functor_compose⁻¹* ⬝* _, + apply phomotopy_group_functor_phomotopy, + fapply phomotopy.mk, + { esimp, intro q, refine !idp_con⁻¹}, + { esimp, refine !idp_con⁻¹}, + end, + apply is_equiv_of_is_equiv_ap1_of_is_equiv_trunc + end end is_trunc diff --git a/hott/homotopy/hopf.hlean b/hott/homotopy/hopf.hlean index 017ae94b3..5300e9c3c 100644 --- a/hott/homotopy/hopf.hlean +++ b/hott/homotopy/hopf.hlean @@ -55,7 +55,7 @@ section variables [H : h_space A] [K : is_conn 0 A] include H K - definition hopf : susp A → Type := + definition hopf [unfold 4] : susp A → Type := susp.elim_type A A (λa, equiv.mk (λx, a * x) !is_equiv_mul_left) /- Lemma 8.5.7. The total space is A * A -/ @@ -185,11 +185,11 @@ section equiv.MK encode decode' encode_decode' decode_encode definition main_lemma_point - : pointed.MK (trunc 1 (Ω(psusp A))) (tr idp) ≃* pointed.MK A 1 := + : ptrunc 1 (Ω(psusp A)) ≃* pointed.MK A 1 := pointed.pequiv_of_equiv main_lemma idp - protected definition delooping : (tr north = tr north :> trunc 2 (susp A)) ≃ A := - (tr_eq_tr_equiv 1 north north) ⬝e main_lemma + protected definition delooping : Ω (ptrunc 2 (psusp A)) ≃* pointed.MK A 1 := + loop_ptrunc_pequiv 1 (psusp A) ⬝e* main_lemma_point end diff --git a/hott/homotopy/quaternionic_hopf.hlean b/hott/homotopy/quaternionic_hopf.hlean index 698a91a22..f4b235e59 100644 --- a/hott/homotopy/quaternionic_hopf.hlean +++ b/hott/homotopy/quaternionic_hopf.hlean @@ -18,10 +18,10 @@ namespace hopf ⦃ involutive_neg, neg := empty.elim, neg_neg := by intro a; induction a ⦄ definition involutive_neg_circle [instance] : involutive_neg circle := - involutive_neg_susp + by change involutive_neg (susp (susp empty)); exact _ definition has_star_circle [instance] : has_star circle := - has_star_susp + by change has_star (susp (susp empty)); exact _ -- this is the "natural" conjugation defined using the base-loop recursor definition circle_star [reducible] : S¹ → S¹ := @@ -80,7 +80,7 @@ namespace hopf induction x, { apply inverse, exact circle_mul_base (y*) }, { apply eq_pathover, induction y, - { exact natural_square_tr + { exact natural_square_tr (λa : S¹, ap (λb : S¹, b*) (circle_mul_base a)) loop }, { apply is_prop.elimo } } end diff --git a/hott/homotopy/red_susp.hlean b/hott/homotopy/red_susp.hlean index b46b65a3d..03b03595b 100644 --- a/hott/homotopy/red_susp.hlean +++ b/hott/homotopy/red_susp.hlean @@ -35,25 +35,23 @@ section definition merid_pt : merid pt = idp := incl2 R Q Qmk - -- protected definition rec {P : red_susp → Type} (Pb : P base) (Pm : Π(a : A), Pb =[merid a] Pb) - -- (Pe : Pm pt =[merid_pt] idpo) (x : red_susp) : P x := - -- begin - -- induction x, - -- end + protected definition rec {P : red_susp → Type} (Pb : P base) (Pm : Π(a : A), Pb =[merid a] Pb) + (Pe : change_path merid_pt (Pm pt) = idpo) (x : red_susp) : P x := + begin + induction x, + { induction a, exact Pb}, + { induction s, exact Pm a}, + { induction q, esimp, exact Pe} + end - -- protected definition rec_on [reducible] {P : red_susp → Type} (x : red_susp) (Pb : P base) - -- (Pm : Π(a : A), Pb =[merid a] Pb) (Pe : Pm pt =[merid_pt] idpo) : P x := - -- rec Pb Pm Pe x + protected definition rec_on [reducible] {P : red_susp → Type} (x : red_susp) (Pb : P base) + (Pm : Π(a : A), Pb =[merid a] Pb) (Pe : change_path merid_pt (Pm pt) = idpo) : P x := + red_susp.rec Pb Pm Pe x - -- definition rec_merid {P : red_susp → Type} (Pb : P base) (Pm : Π(a : A), Pb =[merid a] Pb) - -- (Pe : Pm pt =[merid_pt] idpo) (a : A) - -- : apd (rec Pb Pm Pe) (merid a) = Pm a := - -- !rec_incl1 - - -- theorem elim_merid_pt {P : red_susp → Type} (Pb : P base) (Pm : Π(a : A), Pb =[merid a] Pb) - -- (Pe : Pm pt =[merid_pt] idpo) - -- : square (ap02 (rec Pb Pm Pe) merid_pt) Pe (rec_merid Pe pt) idp := - -- !rec_incl2 + definition rec_merid {P : red_susp → Type} (Pb : P base) (Pm : Π(a : A), Pb =[merid a] Pb) + (Pe : change_path merid_pt (Pm pt) = idpo) (a : A) + : apd (rec Pb Pm Pe) (merid a) = Pm a := + !rec_incl1 protected definition elim {P : Type} (Pb : P) (Pm : Π(a : A), Pb = Pb) (Pe : Pm pt = idp) (x : red_susp) : P := @@ -81,7 +79,7 @@ end end red_susp attribute red_susp.base [constructor] -attribute /-red_susp.rec-/ red_susp.elim [unfold 6] [recursor 6] +attribute red_susp.rec red_susp.elim [unfold 6] [recursor 6] --attribute red_susp.elim_type [unfold 9] -attribute /-red_susp.rec_on-/ red_susp.elim_on [unfold 3] +attribute red_susp.rec_on red_susp.elim_on [unfold 3] --attribute red_susp.elim_type_on [unfold 6] diff --git a/hott/homotopy/sphere.hlean b/hott/homotopy/sphere.hlean index 573b8d08b..51c471885 100644 --- a/hott/homotopy/sphere.hlean +++ b/hott/homotopy/sphere.hlean @@ -75,15 +75,26 @@ namespace sphere_index definition has_le_sphere_index [instance] : has_le ℕ₋₁ := has_le.mk sphere_index.le - definition of_nat [coercion] [reducible] (n : ℕ) : ℕ₋₁ := - (nat.rec_on n -1 (λ n k, k.+1)).+1 - definition sub_one [reducible] (n : ℕ) : ℕ₋₁ := nat.rec_on n -1 (λ n k, k.+1) postfix `..-1`:(max+1) := sub_one + + definition of_nat [coercion] [reducible] (n : ℕ) : ℕ₋₁ := + n..-1.+1 + -- we use a double dot to distinguish with the notation .-1 in trunc_index (of type ℕ → ℕ₋₂) + definition add_one [reducible] (n : ℕ₋₁) : ℕ := + sphere_index.rec_on n 0 (λ n k, nat.succ k) + + 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 succ_sub_one (n : ℕ) : (nat.succ n)..-1 = n :> ℕ₋₁ := idp @@ -145,6 +156,29 @@ namespace sphere_index protected definition le_succ {n m : ℕ₋₁} (H1 : n ≤[ℕ₋₁] m): n ≤[ℕ₋₁] m.+1 := le.step H1 + 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 sphere_index_of_nat_add_one (n : ℕ₋₁) : sphere_index.of_nat (add_one n) = n.+1 := + begin induction n with n IH, reflexivity, exact ap succ IH end + + definition add_one_succ (n : ℕ₋₁) : add_one (n.+1) = succ (add_one n) := + by reflexivity + + definition add_one_sub_one (n : ℕ) : add_one (n..-1) = n := + begin induction n with n IH, reflexivity, exact ap nat.succ IH end + + definition add_one_of_nat (n : ℕ) : add_one n = nat.succ n := + ap nat.succ (add_one_sub_one n) + + definition sphere_index.of_nat_succ (n : ℕ) + : sphere_index.of_nat (nat.succ n) = (sphere_index.of_nat n).+1 := + begin induction n with n IH, reflexivity, exact ap succ IH end + /- warning: if this coercion is available, the coercion ℕ → ℕ₋₂ is the composition of the coercions ℕ → ℕ₋₁ → ℕ₋₂. We don't want this composition as coercion, because it has worse computational @@ -152,7 +186,6 @@ namespace sphere_index -/ attribute trunc_index.of_sphere_index [coercion] - end sphere_index open sphere_index definition weak_order_sphere_index [trans_instance] [reducible] : weak_order sphere_index := @@ -197,13 +230,18 @@ namespace trunc_index : trunc_index._trans_to_of_sphere_index n = of_nat n :> ℕ₋₂ := of_sphere_index_of_nat n + definition trunc_index_of_nat_add_one (n : ℕ₋₁) + : trunc_index.of_nat (add_one n) = (of_sphere_index 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 + end trunc_index open sphere_index equiv -definition sphere : ℕ₋₁ → Type₀ -| -1 := empty -| n.+1 := susp (sphere n) +definition sphere (n : ℕ₋₁) : Type₀ := iterate_susp (add_one n) empty namespace sphere @@ -214,6 +252,7 @@ namespace sphere pointed.mk base definition psphere [constructor] (n : ℕ) : Type* := pointed.mk' (sphere n) + namespace ops abbreviation S := sphere notation `S.` := psphere @@ -221,13 +260,22 @@ namespace sphere open sphere.ops definition sphere_minus_one : S -1 = empty := idp - definition sphere_succ (n : ℕ₋₁) : S n.+1 = susp (S n) := idp + definition sphere_succ [unfold_full] (n : ℕ₋₁) : S n.+1 = susp (S n) := idp + definition psphere_succ [unfold_full] (n : ℕ) : S. (n + 1) = psusp (S. n) := idp + definition psphere_eq_iterate_susp (n : ℕ) + : S. n = pointed.MK (iterate_susp (succ n) empty) !north := + begin + esimp, + apply ap (λx, pointed.MK (susp x) (@north x)); apply ap (λx, iterate_susp x empty), + apply add_one_sub_one + end + definition equator (n : ℕ) : map₊ (S. n) (Ω (S. (succ n))) := pmap.mk (λa, merid a ⬝ (merid base)⁻¹) !con.right_inv definition surf {n : ℕ} : Ω[n] S. n := - nat.rec_on n (proof base qed) + nat.rec_on n (proof @base 0 qed) (begin intro m s, refine cast _ (apn m (equator m) s), exact ap carrier !loop_space_succ_eq_in⁻¹ end) diff --git a/hott/homotopy/sphere2.hlean b/hott/homotopy/sphere2.hlean new file mode 100644 index 000000000..e7ef85897 --- /dev/null +++ b/hott/homotopy/sphere2.hlean @@ -0,0 +1,126 @@ +/- +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 + +Calculating homotopy groups of spheres. + +In this file we calculate +π₂(S²) = Z +πₙ(S²) = πₙ(S³) for n > 2 +πₙ(Sⁿ) = Z for n > 0 +π₂(S³) = Z +-/ + +import .homotopy_group .freudenthal +open eq group algebra is_equiv equiv fin prod chain_complex pointed fiber nat is_trunc trunc_index + sphere.ops trunc is_conn susp + +namespace sphere + /- Corollaries of the complex hopf fibration combined with the LES of homotopy groups -/ + open sphere sphere.ops int circle hopf + + definition π2S2 : πg[1+1] (S. 2) ≃g gℤ := + begin + refine _ ⬝g fundamental_group_of_circle, + refine _ ⬝g homotopy_group_isomorphism_of_pequiv _ pfiber_complex_phopf, + fapply isomorphism_of_equiv, + { 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 πg[n+2 +1] (S. 2) := + begin + fapply isomorphism_of_equiv, + { 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 + + definition sphere_stability_pequiv (k n : ℕ) (H : k + 2 ≤ 2 * n) : + π*[k + 1] (S. (n+1)) ≃* π*[k] (S. n) := + begin rewrite [+ psphere_eq_iterate_susp], exact iterate_susp_stability_pequiv empty H end + + definition stability_isomorphism (k n : ℕ) (H : k + 3 ≤ 2 * n) + : πg[k+1 +1] (S. (n+1)) ≃g πg[k+1] (S. n) := + begin rewrite [+ psphere_eq_iterate_susp], exact iterate_susp_stability_isomorphism empty H end + + open int circle hopf + definition πnSn (n : ℕ) : πg[n+1] (S. (succ n)) ≃g gℤ := + begin + cases n with n IH, + { exact fundamental_group_of_circle}, + { induction n with n IH, + { exact π2S2}, + { refine _ ⬝g IH, apply stability_isomorphism, + rexact add_mul_le_mul_add n 1 2}} + end + + 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, + have H3 : is_contr ℤ, from is_trunc_equiv_closed _ (equiv_of_isomorphism (πnSn n)), + have H4 : (0 : ℤ) ≠ (1 : ℤ), from dec_star, + apply H4, + apply is_prop.elim, + end + + section + open sphere_index + + 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 (add_one n), + rewrite [▸*, trunc_index_of_nat_add_one, -add_one_succ, + sphere_index_of_nat_add_one], + exact H} + end + + end + + definition π3S2 : πg[2+1] (S. 2) ≃g gℤ := + (πnS3_eq_πnS2 0)⁻¹ᵍ ⬝g πnSn 2 + +end sphere diff --git a/hott/homotopy/susp.hlean b/hott/homotopy/susp.hlean index 228d705a6..7097106df 100644 --- a/hott/homotopy/susp.hlean +++ b/hott/homotopy/susp.hlean @@ -354,4 +354,29 @@ namespace susp apply psusp_functor_compose end + definition iterate_susp (n : ℕ) (A : Type) : Type := iterate susp n A + definition iterate_psusp (n : ℕ) (A : Type*) : Type* := iterate (λX, psusp X) n A + + open is_conn trunc_index nat + definition iterate_susp_succ (n : ℕ) (A : Type) : + iterate_susp (succ n) A = susp (iterate_susp n A) := + idp + + definition is_conn_iterate_susp [instance] (n : ℕ₋₂) (m : ℕ) (A : Type) + [H : is_conn n A] : is_conn (n + m) (iterate_susp m A) := + begin induction m with m IH, exact H, exact @is_conn_susp _ _ IH end + + definition is_conn_iterate_psusp [instance] (n : ℕ₋₂) (m : ℕ) (A : Type*) + [H : is_conn n A] : is_conn (n + m) (iterate_psusp m A) := + begin induction m with m IH, exact H, exact @is_conn_susp _ _ IH end + + -- Separate cases for n = 0, which comes up often + definition is_conn_iterate_susp_zero [instance] (m : ℕ) (A : Type) + [H : is_conn 0 A] : is_conn m (iterate_susp m A) := + begin induction m with m IH, exact H, exact @is_conn_susp _ _ IH end + + definition is_conn_iterate_psusp_zero [instance] (m : ℕ) (A : Type*) + [H : is_conn 0 A] : is_conn m (iterate_psusp m A) := + begin induction m with m IH, exact H, exact @is_conn_susp _ _ IH end + end susp diff --git a/hott/homotopy/wedge.hlean b/hott/homotopy/wedge.hlean index 3268a7997..a70f8799b 100644 --- a/hott/homotopy/wedge.hlean +++ b/hott/homotopy/wedge.hlean @@ -5,7 +5,7 @@ Authors: Jakob von Raumer, Ulrik Buchholtz The Wedge Sum of Two pType Types -/ -import hit.pointed_pushout .connectedness +import hit.pointed_pushout .connectedness types.unit open eq pushout pointed unit trunc_index diff --git a/hott/init/equiv.hlean b/hott/init/equiv.hlean index 7f283a1f1..2dda02d68 100644 --- a/hott/init/equiv.hlean +++ b/hott/init/equiv.hlean @@ -131,6 +131,7 @@ namespace is_equiv definition is_equiv_inv [instance] [constructor] : is_equiv f⁻¹ := adjointify f⁻¹ f (left_inv f) (right_inv f) + -- The 2-out-of-3 properties definition cancel_right (g : B → C) [Hgf : is_equiv (g ∘ f)] : (is_equiv g) := have Hfinv : is_equiv f⁻¹, from is_equiv_inv f, @homotopy_closed _ _ _ _ (is_equiv_compose f⁻¹ (g ∘ f)) (λb, ap g (@right_inv _ _ f _ b)) @@ -142,28 +143,24 @@ namespace is_equiv definition eq_of_fn_eq_fn' {x y : A} (q : f x = f y) : x = y := (left_inv f x)⁻¹ ⬝ ap f⁻¹ q ⬝ left_inv f y - theorem ap_eq_of_fn_eq_fn' {x y : A} (q : f x = f y) : ap f (eq_of_fn_eq_fn' f q) = q := - begin - rewrite [↑eq_of_fn_eq_fn',+ap_con,ap_inv,-+adj,-ap_compose,con.assoc, - ap_con_eq_con_ap (right_inv f) q,inv_con_cancel_left,ap_id], - end + definition ap_eq_of_fn_eq_fn' {x y : A} (q : f x = f y) : ap f (eq_of_fn_eq_fn' f q) = q := + !ap_con ⬝ whisker_right !ap_con _ + ⬝ ((!ap_inv ⬝ inverse2 (adj f _)⁻¹) + ◾ (inverse (ap_compose f f⁻¹ _)) + ◾ (adj f _)⁻¹) + ⬝ con_ap_con_eq_con_con (right_inv f) _ _ + ⬝ whisker_right !con.left_inv _ + ⬝ !idp_con + + definition eq_of_fn_eq_fn'_ap {x y : A} (q : x = y) : eq_of_fn_eq_fn' f (ap f q) = q := + by induction q; apply con.left_inv definition is_equiv_ap [instance] [constructor] (x y : A) : is_equiv (ap f : x = y → f x = f y) := adjointify (ap f) (eq_of_fn_eq_fn' f) - abstract (λq, !ap_con - ⬝ whisker_right !ap_con _ - ⬝ ((!ap_inv ⬝ inverse2 (adj f _)⁻¹) - ◾ (inverse (ap_compose f f⁻¹ _)) - ◾ (adj f _)⁻¹) - ⬝ con_ap_con_eq_con_con (right_inv f) _ _ - ⬝ whisker_right !con.left_inv _ - ⬝ !idp_con) end - abstract (λp, whisker_right (whisker_left _ (ap_compose f⁻¹ f _)⁻¹) _ - ⬝ con_ap_con_eq_con_con (left_inv f) _ _ - ⬝ whisker_right !con.left_inv _ - ⬝ !idp_con) end + (ap_eq_of_fn_eq_fn' f) + (eq_of_fn_eq_fn'_ap f) -- The function equiv_rect says that given an equivalence f : A → B, -- and a hypothesis from B, one may always assume that the hypothesis diff --git a/hott/init/path.hlean b/hott/init/path.hlean index f47bec2f2..8a8f40608 100644 --- a/hott/init/path.hlean +++ b/hott/init/path.hlean @@ -62,6 +62,11 @@ namespace eq (p ⬝ q) ⬝ r = p ⬝ (q ⬝ r) := by induction r; reflexivity + definition con.assoc5 {a₁ a₂ a₃ a₄ a₅ a₆ : A} + (p₁ : a₁ = a₂) (p₂ : a₂ = a₃) (p₃ : a₃ = a₄) (p₄ : a₄ = a₅) (p₅ : a₅ = a₆) : + p₁ ⬝ (p₂ ⬝ p₃ ⬝ p₄) ⬝ p₅ = (p₁ ⬝ p₂) ⬝ p₃ ⬝ (p₄ ⬝ p₅) := + by induction p₅; induction p₄; induction p₃; reflexivity + -- The left inverse law. definition con.right_inv [unfold 4] (p : x = y) : p ⬝ p⁻¹ = idp := by induction p; reflexivity @@ -486,6 +491,11 @@ namespace eq -- using the following notation notation p ` ▸D `:65 x:64 := transportD _ p _ x + -- transporting over 2 one-dimensional paths + 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) + -- Transporting along higher-dimensional paths definition transport2 [unfold 7] (P : A → Type) {x y : A} {p q : x = y} (r : p = q) (z : P x) : p ▸ z = q ▸ z := @@ -734,3 +744,14 @@ namespace eq by induction r2; induction r1; induction p1; reflexivity end eq + +/- + an auxillary namespace for concatenation and inversion for homotopies. We put this is a separate + namespace because ⁻¹ʰ is also used as the inverse of a homomorphism +-/ + +open eq +namespace homotopy + infix ` ⬝h `:75 := homotopy.trans + postfix `⁻¹ʰ`:(max+1) := homotopy.symm +end homotopy diff --git a/hott/init/pointed.hlean b/hott/init/pointed.hlean index f7c7ea810..4b0cc5eb7 100644 --- a/hott/init/pointed.hlean +++ b/hott/init/pointed.hlean @@ -75,6 +75,11 @@ namespace pointed attribute ptrunctype._trans_of_to_pType ptrunctype.to_pType ptrunctype.to_trunctype [unfold 2] + -- Any contractible type is pointed + definition pointed_of_is_contr [instance] [priority 800] [constructor] + (A : Type) [H : is_contr A] : pointed A := + pointed.mk !center + end pointed /- pointed maps -/ @@ -111,5 +116,4 @@ namespace pointed infix ` ≃* `:25 := pequiv attribute pequiv.to_pmap [coercion] attribute pequiv.to_is_equiv [instance] - end pointed diff --git a/hott/init/trunc.hlean b/hott/init/trunc.hlean index 3c53f2794..4b5ebb4e4 100644 --- a/hott/init/trunc.hlean +++ b/hott/init/trunc.hlean @@ -302,6 +302,10 @@ namespace is_trunc (f : A → B) (g : B → A) : is_equiv f := is_equiv.mk f g (λb, !is_prop.elim) (λa, !is_prop.elim) (λa, !is_set.elim) + definition is_equiv_of_is_contr [constructor] [HA : is_contr A] [HB : is_contr B] + (f : A → B) : is_equiv f := + is_equiv.mk f (λx, !center) (λb, !is_prop.elim) (λa, !is_prop.elim) (λa, !is_set.elim) + definition equiv_of_is_prop [constructor] [HA : is_prop A] [HB : is_prop B] (f : A → B) (g : B → A) : A ≃ B := equiv.mk f (is_equiv_of_is_prop f g) diff --git a/hott/init/ua.hlean b/hott/init/ua.hlean index 6ba8c5756..6e79f4f5c 100644 --- a/hott/init/ua.hlean +++ b/hott/init/ua.hlean @@ -15,11 +15,11 @@ section universe variable l variables {A B : Type.{l}} - definition is_equiv_cast_of_eq [constructor] (H : A = B) : is_equiv (cast H) := + definition is_equiv_cast [constructor] (H : A = B) : is_equiv (cast H) := is_equiv_tr (λX, X) H definition equiv_of_eq [constructor] (H : A = B) : A ≃ B := - equiv.mk _ (is_equiv_cast_of_eq H) + equiv.mk _ (is_equiv_cast H) definition equiv_of_eq_refl [reducible] [unfold_full] (A : Type) : equiv_of_eq (refl A) = equiv.refl A := diff --git a/hott/types/bool.hlean b/hott/types/bool.hlean index f11b82261..7b3453d23 100644 --- a/hott/types/bool.hlean +++ b/hott/types/bool.hlean @@ -168,6 +168,17 @@ namespace bool { intro b, cases b, reflexivity, reflexivity}, end + /- pointed and truncated bool -/ + open pointed + definition pointed_bool [instance] [constructor] : pointed bool := + pointed.mk ff + + definition pbool [constructor] : Set* := + pSet.mk' bool + definition tbool [constructor] : Set := trunctype.mk bool _ + notation `bool*` := pbool + + end bool diff --git a/hott/types/fiber.hlean b/hott/types/fiber.hlean index e595d7b5e..f0eee0ee2 100644 --- a/hott/types/fiber.hlean +++ b/hott/types/fiber.hlean @@ -79,15 +79,16 @@ namespace fiber definition pointed_fiber [constructor] (f : A → B) (a : A) : Type* := pointed.Mk (fiber.mk a (idpath (f a))) - definition is_trunc_fun [reducible] (n : trunc_index) (f : A → B) := + definition is_trunc_fun [reducible] (n : ℕ₋₂) (f : A → B) := Π(b : B), is_trunc n (fiber f b) definition is_contr_fun [reducible] (f : A → B) := is_trunc_fun -2 f -- pre and post composition with equivalences open function - protected definition equiv_postcompose [constructor] {B' : Type} (g : B → B') [H : is_equiv g] - : fiber (g ∘ f) (g b) ≃ fiber f b := + variable (f) + protected definition equiv_postcompose [constructor] {B' : Type} (g : B ≃ B') --[H : is_equiv g] + (b : B) : fiber (g ∘ f) (g b) ≃ fiber f b := calc fiber (g ∘ f) (g b) ≃ Σa : A, g (f a) = g b : fiber.sigma_char ... ≃ Σa : A, f a = b : begin @@ -96,12 +97,12 @@ namespace fiber end ... ≃ fiber f b : fiber.sigma_char - protected definition equiv_precompose [constructor] {A' : Type} (g : A' → A) [H : is_equiv g] - : fiber (f ∘ g) b ≃ fiber f b := + protected definition equiv_precompose [constructor] {A' : Type} (g : A' ≃ A) --[H : is_equiv g] + (b : B) : fiber (f ∘ g) b ≃ fiber f b := calc fiber (f ∘ g) b ≃ Σa' : A', f (g a') = b : fiber.sigma_char ... ≃ Σa : A, f a = b : begin - apply sigma_equiv_sigma (equiv.mk g H), + apply sigma_equiv_sigma g, intro a', apply erfl end ... ≃ fiber f b : fiber.sigma_char diff --git a/hott/types/fin.hlean b/hott/types/fin.hlean index 595cf985c..6f2a9905c 100644 --- a/hott/types/fin.hlean +++ b/hott/types/fin.hlean @@ -1,7 +1,7 @@ /- Copyright (c) 2015 Haitao Zhang. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Haitao Zhang, Leonardo de Moura, Jakob von Raumer +Authors: Haitao Zhang, Leonardo de Moura, Jakob von Raumer, Floris van Doorn Finite ordinal types. -/ @@ -577,4 +577,54 @@ begin have fin m ≃ fin n, from unit_sum_equiv_cancel this, apply ap nat.succ, apply IH _ this }, end + + definition cyclic_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 + + /- + We want to say that fin (succ n) always has a 0 and 1. However, we want a bit more, because + sometimes we want a zero of (fin a) where a is either + - equal to a successor, but not definitionally a successor (e.g. (0 : fin (3 + n))) + - definitionally equal to a successor, but not in a way that type class inference can infer. + (e.g. (0 : fin 4). Note that 4 is bit0 (bit0 one), but (bit0 x) (defined as x + x), + is not always a successor) + To solve this we use an auxillary class `is_succ` which can solve whether a number is a + successor. + -/ + + inductive is_succ [class] : ℕ → Type := + | mk : Π(n : ℕ), is_succ (nat.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 [instance] (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 + + /- this is a version of `madd` which might compute better -/ + protected definition add {n : ℕ} (x y : fin n) : fin n := + iterate cyclic_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 (cyclic_succ (fin.zero n)) + + definition has_add_fin [instance] (n : ℕ) : has_add (fin n) := + has_add.mk fin.add + end fin diff --git a/hott/types/lift.hlean b/hott/types/lift.hlean index fc16a6a29..6ecf37fe0 100644 --- a/hott/types/lift.hlean +++ b/hott/types/lift.hlean @@ -146,5 +146,33 @@ namespace lift -- is_trunc_lift is defined in init.trunc + 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 pequiv_plift [constructor] (A : Type*) : A ≃* plift A := + pequiv_of_equiv (equiv_lift A) idp + + 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 + end lift diff --git a/hott/types/nat/hott.hlean b/hott/types/nat/hott.hlean index 9b4cbddb6..a3b7c51b9 100644 --- a/hott/types/nat/hott.hlean +++ b/hott/types/nat/hott.hlean @@ -119,4 +119,29 @@ namespace nat definition pointed_nat [instance] [constructor] : pointed ℕ := pointed.mk 0 + 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 + + /- this inequality comes up a couple of times when using the freudenthal suspension theorem -/ + definition add_mul_le_mul_add (n m k : ℕ) : n + (succ m) * k ≤ (succ m) * (n + k) := + calc + n + (succ m) * k ≤ (m * n + n) + (succ m) * k : add_le_add_right !le_add_left _ + ... = (succ m) * n + (succ m) * k : by rewrite -succ_mul + ... = (succ m) * (n + k) : !left_distrib⁻¹ + end nat diff --git a/hott/types/nat/order.hlean b/hott/types/nat/order.hlean index 71fac0d3b..0d33b8934 100644 --- a/hott/types/nat/order.hlean +++ b/hott/types/nat/order.hlean @@ -228,6 +228,12 @@ lt.base n lemma lt_succ_of_lt {i j : nat} : i < j → i < succ j := assume Plt, lt.trans Plt (self_lt_succ j) +lemma one_le_succ (n : ℕ) : 1 ≤ succ n := +nat.succ_le_succ !zero_le + +lemma two_le_succ_succ (n : ℕ) : 2 ≤ succ (succ n) := +nat.succ_le_succ !one_le_succ + /- other forms of induction -/ protected definition strong_rec_on {P : nat → Type} (n : ℕ) (H : Πn, (Πm, m < n → P m) → P n) : P n := diff --git a/hott/types/pi.hlean b/hott/types/pi.hlean index 1e35829c9..557c25e43 100644 --- a/hott/types/pi.hlean +++ b/hott/types/pi.hlean @@ -341,3 +341,22 @@ namespace pi end pi attribute pi.is_trunc_pi [instance] [priority 1520] + +namespace pi + + /- pointed pi types -/ + open pointed + + definition pointed_pi [instance] [constructor] {A : Type} (P : A → Type) [H : Πx, pointed (P x)] + : pointed (Πx, P x) := + pointed.mk (λx, pt) + + definition ppi [constructor] {A : Type} (P : A → Type*) : Type* := + pointed.mk' (Πa, P a) + + notation `Π*` binders `, ` r:(scoped P, ppi P) := r + + definition ptpi [constructor] {n : ℕ₋₂} {A : Type} (P : A → n-Type*) : n-Type* := + ptrunctype.mk' n (Πa, P a) + +end pi diff --git a/hott/types/pointed.hlean b/hott/types/pointed.hlean index f2c218b0d..28a98cec1 100644 --- a/hott/types/pointed.hlean +++ b/hott/types/pointed.hlean @@ -13,48 +13,9 @@ open is_trunc eq prod sigma nat equiv option is_equiv bool unit algebra sigma.op namespace pointed variables {A B : Type} - -- Any contractible type is pointed - definition pointed_of_is_contr [instance] [priority 800] [constructor] - (A : Type) [H : is_contr A] : pointed A := - pointed.mk !center - - -- A pi type with a pointed target is pointed - definition pointed_pi [instance] [constructor] (P : A → Type) [H : Πx, pointed (P x)] - : pointed (Πx, P x) := - pointed.mk (λx, pt) - - -- A sigma type of pointed components is pointed - definition pointed_sigma [instance] [constructor] (P : A → Type) [G : pointed A] - [H : pointed (P pt)] : pointed (Σx, P x) := - pointed.mk ⟨pt,pt⟩ - - definition pointed_prod [instance] [constructor] (A B : Type) [H1 : pointed A] [H2 : pointed B] - : pointed (A × B) := - pointed.mk (pt,pt) - definition pointed_loop [instance] [constructor] (a : A) : pointed (a = a) := pointed.mk idp - definition pointed_bool [instance] [constructor] : pointed bool := - pointed.mk ff - - definition pprod [constructor] (A B : Type*) : Type* := - pointed.mk' (A × B) - - definition psum [constructor] (A B : Type*) : Type* := - pointed.MK (A ⊎ B) (inl pt) - - definition ppi [constructor] {A : Type} (P : A → Type*) : Type* := - pointed.mk' (Πa, P a) - - definition psigma [constructor] {A : Type*} (P : A → Type*) : Type* := - pointed.mk' (Σa, P a) - - infixr ` ×* `:35 := pprod - infixr ` +* `:30 := psum - notation `Σ*` binders `, ` r:(scoped P, psigma P) := r - notation `Π*` binders `, ` r:(scoped P, ppi P) := r - definition pointed_fun_closed [constructor] (f : A → B) [H : pointed A] : pointed B := pointed.mk (f pt) @@ -65,9 +26,13 @@ namespace pointed | iterated_ploop_space 0 X := X | iterated_ploop_space (n+1) X := ploop_space (iterated_ploop_space n X) - prefix `Ω`:(max+5) := ploop_space + notation `Ω` := ploop_space notation `Ω[`:95 n:0 `] `:0 A:95 := iterated_ploop_space n A + definition is_trunc_loop [instance] [priority 1100] (A : Type*) + (n : ℕ₋₂) [H : is_trunc (n.+1) A] : is_trunc n (Ω A) := + !is_trunc_eq + definition iterated_ploop_space_zero [unfold_full] (A : Type*) : Ω[0] A = A := rfl @@ -129,27 +94,9 @@ namespace pointed exact ptrunctype_eq q r end - definition pbool [constructor] : Set* := - pSet.mk' bool - - definition punit [constructor] : Set* := - pSet.mk' unit - - notation `bool*` := pbool - notation `unit*` := punit - definition is_trunc_ptrunctype [instance] {n : ℕ₋₂} (A : n-Type*) : is_trunc n A := trunctype.struct A - definition ptprod [constructor] {n : ℕ₋₂} (A B : n-Type*) : n-Type* := - ptrunctype.mk' n (A × B) - - definition ptpi [constructor] {n : ℕ₋₂} {A : Type} (P : A → n-Type*) : n-Type* := - ptrunctype.mk' n (Πa, P a) - - definition ptsigma [constructor] {n : ℕ₋₂} {A : n-Type*} (P : A → n-Type*) : n-Type* := - ptrunctype.mk' n (Σa, P a) - /- properties of iterated loop space -/ variable (A : Type*) definition loop_space_succ_eq_in (n : ℕ) : Ω[succ n] A = Ω[n] (Ω A) := @@ -206,6 +153,10 @@ namespace pointed /- categorical properties of pointed maps -/ + definition pmap_of_map [constructor] {A B : Type} (f : A → B) (a : A) : + pointed.MK A a →* pointed.MK B (f a) := + pmap.mk f idp + definition pid [constructor] [refl] (A : Type*) : A →* A := pmap.mk id idp @@ -297,6 +248,12 @@ namespace pointed /- instances of pointed maps -/ + definition pcast [constructor] {A B : Type*} (p : A = B) : A →* B := + pmap.mk (cast (ap pType.carrier p)) (by induction p; reflexivity) + + definition pinverse [constructor] {X : Type*} : Ω X →* Ω X := + pmap.mk eq.inverse idp + definition ap1 [constructor] (f : A →* B) : Ω A →* Ω B := begin fconstructor, @@ -304,7 +261,7 @@ namespace pointed { esimp, apply con.left_inv} end - definition apn (n : ℕ) (f : map₊ A B) : Ω[n] A →* Ω[n] B := + definition apn (n : ℕ) (f : A →* B) : Ω[n] A →* Ω[n] B := begin induction n with n IH, { exact f}, @@ -314,15 +271,6 @@ namespace pointed prefix `Ω→`:(max+5) := ap1 notation `Ω→[`:95 n:0 `] `:0 f:95 := apn n f - definition apn_zero [unfold_full] (f : map₊ A B) : Ω→[0] f = f := idp - definition apn_succ [unfold_full] (n : ℕ) (f : map₊ A B) : Ω→[n + 1] f = ap1 (Ω→[n] f) := idp - - definition pcast [constructor] {A B : Type*} (p : A = B) : A →* B := - pmap.mk (cast (ap pType.carrier p)) (by induction p; reflexivity) - - definition pinverse [constructor] {X : Type*} : Ω X →* Ω X := - pmap.mk eq.inverse idp - /- categorical properties of pointed homotopies -/ protected definition phomotopy.refl [constructor] [refl] (f : A →* B) : f ~* f := @@ -332,7 +280,7 @@ namespace pointed { apply idp_con} end - protected definition phomotopy.rfl [constructor] {A B : Type*} {f : A →* B} : f ~* f := + protected definition phomotopy.rfl [constructor] {f : A →* B} : f ~* f := phomotopy.refl f protected definition phomotopy.trans [constructor] [trans] (p : f ~* g) (q : g ~* h) @@ -355,14 +303,14 @@ namespace pointed /- properties about the given pointed maps -/ - definition is_equiv_ap1 {A B : Type*} (f : A →* B) [is_equiv f] : is_equiv (ap1 f) := + definition is_equiv_ap1 (f : A →* B) [is_equiv f] : is_equiv (ap1 f) := begin induction B with B b, induction f with f pf, esimp at *, cases pf, esimp, apply is_equiv.homotopy_closed (ap f), intro p, exact !idp_con⁻¹ end - definition is_equiv_apn {A B : Type*} (n : ℕ) (f : A →* B) [H : is_equiv f] + definition is_equiv_apn (n : ℕ) (f : A →* B) [H : is_equiv f] : is_equiv (apn n f) := begin induction n with n IH, @@ -370,6 +318,9 @@ namespace pointed { exact is_equiv_ap1 (apn n f)} end + definition is_equiv_pcast [instance] {A B : Type*} (p : A = B) : is_equiv (pcast p) := + !is_equiv_cast + definition ap1_id [constructor] {A : Type*} : ap1 (pid A) ~* pid (Ω A) := begin fapply phomotopy.mk, @@ -426,6 +377,12 @@ namespace pointed : pinverse p⁻¹ = (pinverse p)⁻¹ := idp + definition pcast_idp [constructor] {A : Type*} : pcast (idpath A) ~* pid A := + by reflexivity + + definition apn_zero [unfold_full] (f : A →* B) : Ω→[0] f = f := idp + definition apn_succ [unfold_full] (n : ℕ) (f : A →* B) : Ω→[n + 1] f = Ω→ (Ω→[n] f) := idp + /- more on pointed homotopies -/ definition phomotopy_of_eq [constructor] {A B : Type*} {f g : A →* B} (p : f = g) : f ~* g := @@ -474,11 +431,10 @@ namespace pointed In general we need function extensionality for pap, but for particular F we can do it without function extensionality. -/ - definition pap {A B C D : Type*} (F : (A →* B) → (C →* D)) - {f g : A →* B} (p : f ~* g) : F f ~* F g := + definition pap (F : (A →* B) → (C →* D)) {f g : A →* B} (p : f ~* g) : F f ~* F g := phomotopy.mk (ap010 F (eq_of_phomotopy p)) begin cases eq_of_phomotopy p, apply idp_con end - definition ap1_phomotopy {A B : Type*} {f g : A →* B} (p : f ~* g) + definition ap1_phomotopy {f g : A →* B} (p : f ~* g) : ap1 f ~* ap1 g := begin induction p with p q, induction f with f pf, induction g with g pg, induction B with B b, @@ -490,6 +446,13 @@ namespace pointed induction q, reflexivity} end + definition apn_phomotopy {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 + 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, @@ -518,6 +481,38 @@ namespace pointed { reflexivity} end + definition pcast_loop_space [constructor] {A B : Type*} (p : A = B) : + pcast (ap Ω p) ~* ap1 (pcast p) := + begin + fapply phomotopy.mk, + { intro a, induction p, esimp, exact (!idp_con ⬝ !ap_id)⁻¹}, + { induction p, reflexivity} + end + + definition apn_succ_phomotopy_in (n : ℕ) (f : A →* B) : + pcast (loop_space_succ_eq_in B n) ∘* Ω→[n + 1] f ~* + Ω→[n] (Ω→ f) ∘* pcast (loop_space_succ_eq_in A n) := + begin + induction n with n IH, + { reflexivity}, + { refine pwhisker_right _ (pcast_loop_space (loop_space_succ_eq_in B n)) ⬝* _, + refine _ ⬝* pwhisker_left _ (pcast_loop_space (loop_space_succ_eq_in A n))⁻¹*, + refine (ap1_compose _ (Ω→[n + 1] f))⁻¹* ⬝* _ ⬝* ap1_compose (Ω→[n] (Ω→ f)) _, + exact ap1_phomotopy IH} + end + + definition ap1_pmap_of_map [constructor] {A B : Type} (f : A → B) (a : A) : + ap1 (pmap_of_map f a) ~* pmap_of_map (ap f) (idpath a) := + begin + fapply phomotopy.mk, + { intro a, esimp, apply idp_con}, + { reflexivity} + end + + definition pmap_of_eq_pt [constructor] {A : Type} {a a' : A} (p : a = a') : + pointed.MK A a →* pointed.MK A a' := + pmap.mk id p + /- pointed equivalences -/ definition pequiv_of_pmap [constructor] (f : A →* B) (H : is_equiv f) : A ≃* B := @@ -750,6 +745,10 @@ namespace pointed loopn_pequiv_loopn (n+1) f p ⬝ loopn_pequiv_loopn (n+1) f q := ap1_con (loopn_pequiv_loopn n f) p q + 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 loopn_pequiv_loopn_rfl (n : ℕ) (A : Type*) : loopn_pequiv_loopn n (pequiv.refl A) = pequiv.refl (Ω[n] A) := begin @@ -773,6 +772,10 @@ namespace pointed definition pequiv_pinverse (A : Type*) : Ω A ≃* Ω A := pequiv_of_pmap pinverse !is_equiv_eq_inverse + definition pequiv_of_eq_pt [constructor] {A : Type} {a a' : A} (p : a = a') : + pointed.MK A a ≃* pointed.MK A a' := + pequiv_of_pmap (pmap_of_eq_pt p) !is_equiv_id + /- -- TODO definition pmap_pequiv_pmap {A A' B B' : Type*} (f : A ≃* A') (g : B ≃* B') : ppmap A B ≃* ppmap A' B' := diff --git a/hott/types/prod.hlean b/hott/types/prod.hlean index 8f3288a5e..38e4a08c7 100644 --- a/hott/types/prod.hlean +++ b/hott/types/prod.hlean @@ -249,7 +249,33 @@ namespace prod end prod attribute prod.is_trunc_prod [instance] [priority 1510] -definition tprod [constructor] {n : trunc_index} (A B : n-Type) : n-Type := -trunctype.mk (A × B) _ -infixr `×t`:30 := tprod +namespace prod + /- pointed products -/ + open pointed + definition pointed_prod [instance] [constructor] (A B : Type) [H1 : pointed A] [H2 : pointed B] + : pointed (A × B) := + pointed.mk (pt,pt) + + definition pprod [constructor] (A B : Type*) : Type* := + pointed.mk' (A × B) + + infixr ` ×* `:35 := pprod + + definition ppr1 [constructor] {A B : Type*} : A ×* B →* A := + pmap.mk pr1 idp + + definition ppr2 [constructor] {A B : Type*} : A ×* B →* B := + pmap.mk pr2 idp + + definition tprod [constructor] {n : trunc_index} (A B : n-Type) : n-Type := + trunctype.mk (A × B) _ + + infixr `×t`:30 := tprod + + definition ptprod [constructor] {n : ℕ₋₂} (A B : n-Type*) : n-Type* := + ptrunctype.mk' n (A × B) + + + +end prod diff --git a/hott/types/sigma.hlean b/hott/types/sigma.hlean index 8b449d179..a4a85feda 100644 --- a/hott/types/sigma.hlean +++ b/hott/types/sigma.hlean @@ -491,3 +491,28 @@ end sigma attribute sigma.is_trunc_sigma [instance] [priority 1490] attribute sigma.is_trunc_subtype [instance] [priority 1200] + +namespace sigma + + /- pointed sigma type -/ + open pointed + + definition pointed_sigma [instance] [constructor] {A : Type} (P : A → Type) [G : pointed A] + [H : pointed (P pt)] : pointed (Σx, P x) := + pointed.mk ⟨pt,pt⟩ + + definition psigma [constructor] {A : Type*} (P : A → Type*) : Type* := + pointed.mk' (Σa, P a) + + notation `Σ*` binders `, ` r:(scoped P, psigma P) := r + + 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 + + definition ptsigma [constructor] {n : ℕ₋₂} {A : n-Type*} (P : A → n-Type*) : n-Type* := + ptrunctype.mk' n (Σa, P a) + +end sigma diff --git a/hott/types/sum.hlean b/hott/types/sum.hlean index 91365b1f5..98aaa85eb 100644 --- a/hott/types/sum.hlean +++ b/hott/types/sum.hlean @@ -353,6 +353,15 @@ namespace sum begin intro v, induction v with b x, induction b, all_goals reflexivity end begin intro z, induction z with a b, all_goals reflexivity end + /- pointed sums. We arbitrarily choose (inl pt) as basepoint for the sum -/ + + open pointed + definition psum [constructor] (A B : Type*) : Type* := + pointed.MK (A ⊎ B) (inl pt) + + infixr ` +* `:30 := psum + + end sum open sum pi diff --git a/hott/types/trunc.hlean b/hott/types/trunc.hlean index 0ebf33c30..a67bd7d11 100644 --- a/hott/types/trunc.hlean +++ b/hott/types/trunc.hlean @@ -332,6 +332,9 @@ namespace is_trunc definition tcast [unfold 4] {n : ℕ₋₂} {A B : n-Type} (p : A = B) (a : A) : B := cast (ap trunctype.carrier p) a + definition ptcast [constructor] {n : ℕ₋₂} {A B : n-Type*} (p : A = B) : A →* B := + pcast (ap ptrunctype.to_pType p) + theorem tcast_tua_fn {n : ℕ₋₂} {A B : n-Type} (f : A ≃ B) : tcast (tua f) = to_fun f := begin cases A with A HA, cases B with B HB, esimp at *, @@ -579,6 +582,12 @@ namespace trunc { apply trunc_trunc_equiv_left, exact H}, end + 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 + definition trunc_functor_homotopy_of_le {n k : ℕ₋₂} {A B : Type} (f : A → B) (H : n ≤ k) : to_fun (trunc_trunc_equiv_left B H) ∘ trunc_functor n (trunc_functor k f) ∘ @@ -601,17 +610,10 @@ namespace trunc cases n with n: intro b, { exact tr (fiber.mk !center !is_prop.elim)}, { refine @trunc.rec _ _ _ _ _ b, {intro x, exact is_trunc_of_le _ !minus_one_le_succ}, - clear b, intro b, induction H b with v, induction v with a p, + clear b, intro b, induction H b with a p, exact tr (fiber.mk (tr a) (ap tr p))} end - /- the image of a map is the (-1)-truncated fiber -/ - definition image [constructor] {A B : Type} (f : A → B) (b : B) : Prop := ∥ fiber f b ∥ - - definition image.mk [constructor] {A B : Type} {f : A → B} {b : B} (a : A) (p : f a = b) - : image f b := - tr (fiber.mk a p) - /- truncation of pointed types and its functorial action -/ definition ptrunc [constructor] (n : ℕ₋₂) (X : Type*) : n-Type* := ptrunctype.mk (trunc n X) _ (tr pt) @@ -666,6 +668,24 @@ namespace trunc rewrite succ_add_nat} end + 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 + + 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 := + equiv.inv_preserve_binary (iterated_loop_ptrunc_pequiv n (succ k) A) concat trunc_concat + (@iterated_loop_ptrunc_pequiv_con n k A) p q + definition ptrunc_functor_pcompose [constructor] {X Y Z : Type*} (n : ℕ₋₂) (g : Y →* Z) (f : X →* Y) : ptrunc_functor n (g ∘* f) ~* ptrunc_functor n g ∘* ptrunc_functor n f := begin @@ -692,16 +712,73 @@ namespace trunc { induction p, reflexivity}, end + 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 + + definition pcast_ptrunc [constructor] (n : ℕ₋₂) {A B : Type*} (p : A = B) : + pcast (ap (ptrunc n) p) ~* ptrunc_functor n (pcast p) := + begin + fapply phomotopy.mk, + { intro a, induction p, esimp, exact !trunc_functor_id⁻¹}, + { induction p, reflexivity} + end + end trunc open trunc +/- some consequences for properties about functions (surjectivity etc.) -/ namespace function variables {A B : Type} definition is_surjective_of_is_equiv [instance] (f : A → B) [H : is_equiv f] : is_surjective f := - λb, begin esimp, apply center end + λb, begin esimp, apply center, apply is_trunc_trunc_of_is_trunc end definition is_equiv_equiv_is_embedding_times_is_surjective [constructor] (f : A → B) : is_equiv f ≃ (is_embedding f × is_surjective f) := equiv_of_is_prop (λH, (_, _)) (λP, prod.rec_on P (λH₁ H₂, !is_equiv_of_is_surjective_of_is_embedding)) + /- + Theorem 8.8.1: + A function is an equivalence if it's an embedding and it's action on sets is an surjection + -/ + definition is_equiv_of_is_surjective_trunc_of_is_embedding {A B : Type} (f : A → B) + [H : is_embedding f] [H' : is_surjective (trunc_functor 0 f)] : is_equiv f := + have is_surjective f, + begin + intro b, + induction H' (tr b) with a p, + induction a with a, esimp at p, + induction (tr_eq_tr_equiv _ _ _ p) with q, + exact image.mk a q + end, + is_equiv_of_is_surjective_of_is_embedding f + + /- + Corollary 8.8.2: + A function f is an equivalence if Ωf and trunc_functor 0 f are equivalences + -/ + definition is_equiv_of_is_equiv_ap1_of_is_equiv_trunc {A B : Type} (f : A → B) + [H : Πa, is_equiv (ap1 (pmap_of_map f a))] [H' : is_equiv (trunc_functor 0 f)] : + is_equiv f := + have is_embedding f, + begin + intro a a', + apply is_equiv_of_imp_is_equiv, + intro p, + note q := ap (@tr 0 _) p, + note r := @(eq_of_fn_eq_fn' (trunc_functor 0 f)) _ (tr a) (tr a') q, + induction (tr_eq_tr_equiv _ _ _ r) with s, + induction s, + apply is_equiv.homotopy_closed (ap1 (pmap_of_map f a)), + intro p, apply idp_con + end, + is_equiv_of_is_surjective_trunc_of_is_embedding f + + -- Whitehead's principle itself is in homotopy.homotopy_group, since it needs the definition of + -- a homotopy group. + end function diff --git a/hott/types/unit.hlean b/hott/types/unit.hlean index 7ce4d19ff..2892c978e 100644 --- a/hott/types/unit.hlean +++ b/hott/types/unit.hlean @@ -6,7 +6,7 @@ Authors: Floris van Doorn Theorems about the unit type -/ -open equiv option eq +open equiv option eq pointed is_trunc namespace unit @@ -25,6 +25,13 @@ namespace unit -- equivalences involving unit and other type constructors are in the file -- of the other constructor + /- pointed and truncated unit -/ + + definition punit [constructor] : Set* := + pSet.mk' unit + + notation `unit*` := punit + end unit open unit is_trunc diff --git a/library/data/nat/order.lean b/library/data/nat/order.lean index 5b6842cba..1461486af 100644 --- a/library/data/nat/order.lean +++ b/library/data/nat/order.lean @@ -228,6 +228,12 @@ lt.base n lemma lt_succ_of_lt {i j : nat} : i < j → i < succ j := assume Plt, lt.trans Plt (self_lt_succ j) +lemma one_le_succ (n : ℕ) : 1 ≤ succ n := +nat.succ_le_succ !zero_le + +lemma two_le_succ_succ (n : ℕ) : 2 ≤ succ (succ n) := +nat.succ_le_succ !one_le_succ + /- increasing and decreasing functions -/ section